WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 22.3 s] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (6) BEST (7) proven lower bound (8) LowerBoundPropagationProof [FINISHED, 0 ms] (9) BOUNDS(n^1, INF) (10) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: A__ZEROS -> c A__ZEROS -> c1 A__U101(tt, z0, z1) -> c2(A__U102(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U101(z0, z1, z2) -> c3 A__U102(tt, z0, z1) -> c4(A__U103(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U102(z0, z1, z2) -> c5 A__U103(tt, z0, z1) -> c6(A__U104(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U103(z0, z1, z2) -> c7 A__U104(tt, z0, z1) -> c8(A__U105(a__isNat(z0), z1), A__ISNAT(z0)) A__U104(z0, z1, z2) -> c9 A__U105(tt, z0) -> c10(A__U106(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U105(z0, z1) -> c11 A__U106(tt) -> c12 A__U106(z0) -> c13 A__U11(tt, z0) -> c14(A__U12(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U11(z0, z1) -> c15 A__U111(tt, z0, z1) -> c16(A__U112(a__isNatIListKind(z0), z0, z1), A__ISNATILISTKIND(z0)) A__U111(z0, z1, z2) -> c17 A__U112(tt, z0, z1) -> c18(A__U113(a__isNat(z1), z0, z1), A__ISNAT(z1)) A__U112(z0, z1, z2) -> c19 A__U113(tt, z0, z1) -> c20(A__U114(a__isNatKind(z1), z0), A__ISNATKIND(z1)) A__U113(z0, z1, z2) -> c21 A__U114(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U114(z0, z1) -> c23 A__U12(tt, z0) -> c24(A__U13(a__isNatList(z0)), A__ISNATLIST(z0)) A__U12(z0, z1) -> c25 A__U121(tt, z0) -> c26(A__U122(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U121(z0, z1) -> c27 A__U122(tt) -> c28 A__U122(z0) -> c29 A__U13(tt) -> c30 A__U13(z0) -> c31 A__U131(tt, z0, z1, z2) -> c32(A__U132(a__isNatIListKind(z0), z0, z1, z2), A__ISNATILISTKIND(z0)) A__U131(z0, z1, z2, z3) -> c33 A__U132(tt, z0, z1, z2) -> c34(A__U133(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U132(z0, z1, z2, z3) -> c35 A__U133(tt, z0, z1, z2) -> c36(A__U134(a__isNatKind(z1), z0, z1, z2), A__ISNATKIND(z1)) A__U133(z0, z1, z2, z3) -> c37 A__U134(tt, z0, z1, z2) -> c38(A__U135(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U134(z0, z1, z2, z3) -> c39 A__U135(tt, z0, z1, z2) -> c40(A__U136(a__isNatKind(z2), z0, z1, z2), A__ISNATKIND(z2)) A__U135(z0, z1, z2, z3) -> c41 A__U136(tt, z0, z1, z2) -> c42(MARK(z2)) A__U136(z0, z1, z2, z3) -> c43 A__U21(tt, z0) -> c44(A__U22(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__U21(z0, z1) -> c45 A__U22(tt, z0) -> c46(A__U23(a__isNat(z0)), A__ISNAT(z0)) A__U22(z0, z1) -> c47 A__U23(tt) -> c48 A__U23(z0) -> c49 A__U31(tt, z0) -> c50(A__U32(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U31(z0, z1) -> c51 A__U32(tt, z0) -> c52(A__U33(a__isNatList(z0)), A__ISNATLIST(z0)) A__U32(z0, z1) -> c53 A__U33(tt) -> c54 A__U33(z0) -> c55 A__U41(tt, z0, z1) -> c56(A__U42(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U41(z0, z1, z2) -> c57 A__U42(tt, z0, z1) -> c58(A__U43(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U42(z0, z1, z2) -> c59 A__U43(tt, z0, z1) -> c60(A__U44(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U43(z0, z1, z2) -> c61 A__U44(tt, z0, z1) -> c62(A__U45(a__isNat(z0), z1), A__ISNAT(z0)) A__U44(z0, z1, z2) -> c63 A__U45(tt, z0) -> c64(A__U46(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U45(z0, z1) -> c65 A__U46(tt) -> c66 A__U46(z0) -> c67 A__U51(tt, z0) -> c68(A__U52(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U51(z0, z1) -> c69 A__U52(tt) -> c70 A__U52(z0) -> c71 A__U61(tt, z0) -> c72(A__U62(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U61(z0, z1) -> c73 A__U62(tt) -> c74 A__U62(z0) -> c75 A__U71(tt) -> c76 A__U71(z0) -> c77 A__U81(tt) -> c78 A__U81(z0) -> c79 A__U91(tt, z0, z1) -> c80(A__U92(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U91(z0, z1, z2) -> c81 A__U92(tt, z0, z1) -> c82(A__U93(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U92(z0, z1, z2) -> c83 A__U93(tt, z0, z1) -> c84(A__U94(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U93(z0, z1, z2) -> c85 A__U94(tt, z0, z1) -> c86(A__U95(a__isNat(z0), z1), A__ISNAT(z0)) A__U94(z0, z1, z2) -> c87 A__U95(tt, z0) -> c88(A__U96(a__isNatList(z0)), A__ISNATLIST(z0)) A__U95(z0, z1) -> c89 A__U96(tt) -> c90 A__U96(z0) -> c91 A__ISNAT(0) -> c92 A__ISNAT(length(z0)) -> c93(A__U11(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c94(A__U21(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__ISNAT(z0) -> c95 A__ISNATILIST(z0) -> c96(A__U31(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNATILIST(zeros) -> c97 A__ISNATILIST(cons(z0, z1)) -> c98(A__U41(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c99 A__ISNATILISTKIND(nil) -> c100 A__ISNATILISTKIND(zeros) -> c101 A__ISNATILISTKIND(cons(z0, z1)) -> c102(A__U51(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(take(z0, z1)) -> c103(A__U61(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(z0) -> c104 A__ISNATKIND(0) -> c105 A__ISNATKIND(length(z0)) -> c106(A__U71(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c107(A__U81(a__isNatKind(z0)), A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c108 A__ISNATLIST(nil) -> c109 A__ISNATLIST(cons(z0, z1)) -> c110(A__U91(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(take(z0, z1)) -> c111(A__U101(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c112 A__LENGTH(nil) -> c113 A__LENGTH(cons(z0, z1)) -> c114(A__U111(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c115 A__TAKE(0, z0) -> c116(A__U121(a__isNatIList(z0), z0), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c117(A__U131(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c118 MARK(zeros) -> c119(A__ZEROS) MARK(U101(z0, z1, z2)) -> c120(A__U101(mark(z0), z1, z2), MARK(z0)) MARK(U102(z0, z1, z2)) -> c121(A__U102(mark(z0), z1, z2), MARK(z0)) MARK(isNatKind(z0)) -> c122(A__ISNATKIND(z0)) MARK(U103(z0, z1, z2)) -> c123(A__U103(mark(z0), z1, z2), MARK(z0)) MARK(isNatIListKind(z0)) -> c124(A__ISNATILISTKIND(z0)) MARK(U104(z0, z1, z2)) -> c125(A__U104(mark(z0), z1, z2), MARK(z0)) MARK(U105(z0, z1)) -> c126(A__U105(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c127(A__ISNAT(z0)) MARK(U106(z0)) -> c128(A__U106(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c129(A__ISNATILIST(z0)) MARK(U11(z0, z1)) -> c130(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c131(A__U12(mark(z0), z1), MARK(z0)) MARK(U111(z0, z1, z2)) -> c132(A__U111(mark(z0), z1, z2), MARK(z0)) MARK(U112(z0, z1, z2)) -> c133(A__U112(mark(z0), z1, z2), MARK(z0)) MARK(U113(z0, z1, z2)) -> c134(A__U113(mark(z0), z1, z2), MARK(z0)) MARK(U114(z0, z1)) -> c135(A__U114(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c136(A__LENGTH(mark(z0)), MARK(z0)) MARK(U13(z0)) -> c137(A__U13(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c138(A__ISNATLIST(z0)) MARK(U121(z0, z1)) -> c139(A__U121(mark(z0), z1), MARK(z0)) MARK(U122(z0)) -> c140(A__U122(mark(z0)), MARK(z0)) MARK(U131(z0, z1, z2, z3)) -> c141(A__U131(mark(z0), z1, z2, z3), MARK(z0)) MARK(U132(z0, z1, z2, z3)) -> c142(A__U132(mark(z0), z1, z2, z3), MARK(z0)) MARK(U133(z0, z1, z2, z3)) -> c143(A__U133(mark(z0), z1, z2, z3), MARK(z0)) MARK(U134(z0, z1, z2, z3)) -> c144(A__U134(mark(z0), z1, z2, z3), MARK(z0)) MARK(U135(z0, z1, z2, z3)) -> c145(A__U135(mark(z0), z1, z2, z3), MARK(z0)) MARK(U136(z0, z1, z2, z3)) -> c146(A__U136(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c147(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c148(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(U21(z0, z1)) -> c149(A__U21(mark(z0), z1), MARK(z0)) MARK(U22(z0, z1)) -> c150(A__U22(mark(z0), z1), MARK(z0)) MARK(U23(z0)) -> c151(A__U23(mark(z0)), MARK(z0)) MARK(U31(z0, z1)) -> c152(A__U31(mark(z0), z1), MARK(z0)) MARK(U32(z0, z1)) -> c153(A__U32(mark(z0), z1), MARK(z0)) MARK(U33(z0)) -> c154(A__U33(mark(z0)), MARK(z0)) MARK(U41(z0, z1, z2)) -> c155(A__U41(mark(z0), z1, z2), MARK(z0)) MARK(U42(z0, z1, z2)) -> c156(A__U42(mark(z0), z1, z2), MARK(z0)) MARK(U43(z0, z1, z2)) -> c157(A__U43(mark(z0), z1, z2), MARK(z0)) MARK(U44(z0, z1, z2)) -> c158(A__U44(mark(z0), z1, z2), MARK(z0)) MARK(U45(z0, z1)) -> c159(A__U45(mark(z0), z1), MARK(z0)) MARK(U46(z0)) -> c160(A__U46(mark(z0)), MARK(z0)) MARK(U51(z0, z1)) -> c161(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c162(A__U52(mark(z0)), MARK(z0)) MARK(U61(z0, z1)) -> c163(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c164(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0)) -> c165(A__U71(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c166(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2)) -> c167(A__U91(mark(z0), z1, z2), MARK(z0)) MARK(U92(z0, z1, z2)) -> c168(A__U92(mark(z0), z1, z2), MARK(z0)) MARK(U93(z0, z1, z2)) -> c169(A__U93(mark(z0), z1, z2), MARK(z0)) MARK(U94(z0, z1, z2)) -> c170(A__U94(mark(z0), z1, z2), MARK(z0)) MARK(U95(z0, z1)) -> c171(A__U95(mark(z0), z1), MARK(z0)) MARK(U96(z0)) -> c172(A__U96(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c173(MARK(z0)) MARK(0) -> c174 MARK(tt) -> c175 MARK(s(z0)) -> c176(MARK(z0)) MARK(nil) -> c177 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U101(tt, z0, z1) -> a__U102(a__isNatKind(z0), z0, z1) a__U101(z0, z1, z2) -> U101(z0, z1, z2) a__U102(tt, z0, z1) -> a__U103(a__isNatIListKind(z1), z0, z1) a__U102(z0, z1, z2) -> U102(z0, z1, z2) a__U103(tt, z0, z1) -> a__U104(a__isNatIListKind(z1), z0, z1) a__U103(z0, z1, z2) -> U103(z0, z1, z2) a__U104(tt, z0, z1) -> a__U105(a__isNat(z0), z1) a__U104(z0, z1, z2) -> U104(z0, z1, z2) a__U105(tt, z0) -> a__U106(a__isNatIList(z0)) a__U105(z0, z1) -> U105(z0, z1) a__U106(tt) -> tt a__U106(z0) -> U106(z0) a__U11(tt, z0) -> a__U12(a__isNatIListKind(z0), z0) a__U11(z0, z1) -> U11(z0, z1) a__U111(tt, z0, z1) -> a__U112(a__isNatIListKind(z0), z0, z1) a__U111(z0, z1, z2) -> U111(z0, z1, z2) a__U112(tt, z0, z1) -> a__U113(a__isNat(z1), z0, z1) a__U112(z0, z1, z2) -> U112(z0, z1, z2) a__U113(tt, z0, z1) -> a__U114(a__isNatKind(z1), z0) a__U113(z0, z1, z2) -> U113(z0, z1, z2) a__U114(tt, z0) -> s(a__length(mark(z0))) a__U114(z0, z1) -> U114(z0, z1) a__U12(tt, z0) -> a__U13(a__isNatList(z0)) a__U12(z0, z1) -> U12(z0, z1) a__U121(tt, z0) -> a__U122(a__isNatIListKind(z0)) a__U121(z0, z1) -> U121(z0, z1) a__U122(tt) -> nil a__U122(z0) -> U122(z0) a__U13(tt) -> tt a__U13(z0) -> U13(z0) a__U131(tt, z0, z1, z2) -> a__U132(a__isNatIListKind(z0), z0, z1, z2) a__U131(z0, z1, z2, z3) -> U131(z0, z1, z2, z3) a__U132(tt, z0, z1, z2) -> a__U133(a__isNat(z1), z0, z1, z2) a__U132(z0, z1, z2, z3) -> U132(z0, z1, z2, z3) a__U133(tt, z0, z1, z2) -> a__U134(a__isNatKind(z1), z0, z1, z2) a__U133(z0, z1, z2, z3) -> U133(z0, z1, z2, z3) a__U134(tt, z0, z1, z2) -> a__U135(a__isNat(z2), z0, z1, z2) a__U134(z0, z1, z2, z3) -> U134(z0, z1, z2, z3) a__U135(tt, z0, z1, z2) -> a__U136(a__isNatKind(z2), z0, z1, z2) a__U135(z0, z1, z2, z3) -> U135(z0, z1, z2, z3) a__U136(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U136(z0, z1, z2, z3) -> U136(z0, z1, z2, z3) a__U21(tt, z0) -> a__U22(a__isNatKind(z0), z0) a__U21(z0, z1) -> U21(z0, z1) a__U22(tt, z0) -> a__U23(a__isNat(z0)) a__U22(z0, z1) -> U22(z0, z1) a__U23(tt) -> tt a__U23(z0) -> U23(z0) a__U31(tt, z0) -> a__U32(a__isNatIListKind(z0), z0) a__U31(z0, z1) -> U31(z0, z1) a__U32(tt, z0) -> a__U33(a__isNatList(z0)) a__U32(z0, z1) -> U32(z0, z1) a__U33(tt) -> tt a__U33(z0) -> U33(z0) a__U41(tt, z0, z1) -> a__U42(a__isNatKind(z0), z0, z1) a__U41(z0, z1, z2) -> U41(z0, z1, z2) a__U42(tt, z0, z1) -> a__U43(a__isNatIListKind(z1), z0, z1) a__U42(z0, z1, z2) -> U42(z0, z1, z2) a__U43(tt, z0, z1) -> a__U44(a__isNatIListKind(z1), z0, z1) a__U43(z0, z1, z2) -> U43(z0, z1, z2) a__U44(tt, z0, z1) -> a__U45(a__isNat(z0), z1) a__U44(z0, z1, z2) -> U44(z0, z1, z2) a__U45(tt, z0) -> a__U46(a__isNatIList(z0)) a__U45(z0, z1) -> U45(z0, z1) a__U46(tt) -> tt a__U46(z0) -> U46(z0) a__U51(tt, z0) -> a__U52(a__isNatIListKind(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIListKind(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt) -> tt a__U71(z0) -> U71(z0) a__U81(tt) -> tt a__U81(z0) -> U81(z0) a__U91(tt, z0, z1) -> a__U92(a__isNatKind(z0), z0, z1) a__U91(z0, z1, z2) -> U91(z0, z1, z2) a__U92(tt, z0, z1) -> a__U93(a__isNatIListKind(z1), z0, z1) a__U92(z0, z1, z2) -> U92(z0, z1, z2) a__U93(tt, z0, z1) -> a__U94(a__isNatIListKind(z1), z0, z1) a__U93(z0, z1, z2) -> U93(z0, z1, z2) a__U94(tt, z0, z1) -> a__U95(a__isNat(z0), z1) a__U94(z0, z1, z2) -> U94(z0, z1, z2) a__U95(tt, z0) -> a__U96(a__isNatList(z0)) a__U95(z0, z1) -> U95(z0, z1) a__U96(tt) -> tt a__U96(z0) -> U96(z0) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatIListKind(z0), z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0), z0) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0), z0) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNatKind(z0), z0, z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatIListKind(nil) -> tt a__isNatIListKind(zeros) -> tt a__isNatIListKind(cons(z0, z1)) -> a__U51(a__isNatKind(z0), z1) a__isNatIListKind(take(z0, z1)) -> a__U61(a__isNatKind(z0), z1) a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatKind(0) -> tt a__isNatKind(length(z0)) -> a__U71(a__isNatIListKind(z0)) a__isNatKind(s(z0)) -> a__U81(a__isNatKind(z0)) a__isNatKind(z0) -> isNatKind(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U91(a__isNatKind(z0), z0, z1) a__isNatList(take(z0, z1)) -> a__U101(a__isNatKind(z0), z0, z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U111(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U121(a__isNatIList(z0), z0) a__take(s(z0), cons(z1, z2)) -> a__U131(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U101(z0, z1, z2)) -> a__U101(mark(z0), z1, z2) mark(U102(z0, z1, z2)) -> a__U102(mark(z0), z1, z2) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(U103(z0, z1, z2)) -> a__U103(mark(z0), z1, z2) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(U104(z0, z1, z2)) -> a__U104(mark(z0), z1, z2) mark(U105(z0, z1)) -> a__U105(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(U106(z0)) -> a__U106(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(U111(z0, z1, z2)) -> a__U111(mark(z0), z1, z2) mark(U112(z0, z1, z2)) -> a__U112(mark(z0), z1, z2) mark(U113(z0, z1, z2)) -> a__U113(mark(z0), z1, z2) mark(U114(z0, z1)) -> a__U114(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U13(z0)) -> a__U13(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U121(z0, z1)) -> a__U121(mark(z0), z1) mark(U122(z0)) -> a__U122(mark(z0)) mark(U131(z0, z1, z2, z3)) -> a__U131(mark(z0), z1, z2, z3) mark(U132(z0, z1, z2, z3)) -> a__U132(mark(z0), z1, z2, z3) mark(U133(z0, z1, z2, z3)) -> a__U133(mark(z0), z1, z2, z3) mark(U134(z0, z1, z2, z3)) -> a__U134(mark(z0), z1, z2, z3) mark(U135(z0, z1, z2, z3)) -> a__U135(mark(z0), z1, z2, z3) mark(U136(z0, z1, z2, z3)) -> a__U136(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(U21(z0, z1)) -> a__U21(mark(z0), z1) mark(U22(z0, z1)) -> a__U22(mark(z0), z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0, z1)) -> a__U31(mark(z0), z1) mark(U32(z0, z1)) -> a__U32(mark(z0), z1) mark(U33(z0)) -> a__U33(mark(z0)) mark(U41(z0, z1, z2)) -> a__U41(mark(z0), z1, z2) mark(U42(z0, z1, z2)) -> a__U42(mark(z0), z1, z2) mark(U43(z0, z1, z2)) -> a__U43(mark(z0), z1, z2) mark(U44(z0, z1, z2)) -> a__U44(mark(z0), z1, z2) mark(U45(z0, z1)) -> a__U45(mark(z0), z1) mark(U46(z0)) -> a__U46(mark(z0)) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0)) -> a__U71(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2)) -> a__U91(mark(z0), z1, z2) mark(U92(z0, z1, z2)) -> a__U92(mark(z0), z1, z2) mark(U93(z0, z1, z2)) -> a__U93(mark(z0), z1, z2) mark(U94(z0, z1, z2)) -> a__U94(mark(z0), z1, z2) mark(U95(z0, z1)) -> a__U95(mark(z0), z1) mark(U96(z0)) -> a__U96(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(tt) -> tt mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: A__ZEROS -> c A__ZEROS -> c1 A__U101(tt, z0, z1) -> c2(A__U102(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U101(z0, z1, z2) -> c3 A__U102(tt, z0, z1) -> c4(A__U103(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U102(z0, z1, z2) -> c5 A__U103(tt, z0, z1) -> c6(A__U104(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U103(z0, z1, z2) -> c7 A__U104(tt, z0, z1) -> c8(A__U105(a__isNat(z0), z1), A__ISNAT(z0)) A__U104(z0, z1, z2) -> c9 A__U105(tt, z0) -> c10(A__U106(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U105(z0, z1) -> c11 A__U106(tt) -> c12 A__U106(z0) -> c13 A__U11(tt, z0) -> c14(A__U12(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U11(z0, z1) -> c15 A__U111(tt, z0, z1) -> c16(A__U112(a__isNatIListKind(z0), z0, z1), A__ISNATILISTKIND(z0)) A__U111(z0, z1, z2) -> c17 A__U112(tt, z0, z1) -> c18(A__U113(a__isNat(z1), z0, z1), A__ISNAT(z1)) A__U112(z0, z1, z2) -> c19 A__U113(tt, z0, z1) -> c20(A__U114(a__isNatKind(z1), z0), A__ISNATKIND(z1)) A__U113(z0, z1, z2) -> c21 A__U114(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U114(z0, z1) -> c23 A__U12(tt, z0) -> c24(A__U13(a__isNatList(z0)), A__ISNATLIST(z0)) A__U12(z0, z1) -> c25 A__U121(tt, z0) -> c26(A__U122(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U121(z0, z1) -> c27 A__U122(tt) -> c28 A__U122(z0) -> c29 A__U13(tt) -> c30 A__U13(z0) -> c31 A__U131(tt, z0, z1, z2) -> c32(A__U132(a__isNatIListKind(z0), z0, z1, z2), A__ISNATILISTKIND(z0)) A__U131(z0, z1, z2, z3) -> c33 A__U132(tt, z0, z1, z2) -> c34(A__U133(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U132(z0, z1, z2, z3) -> c35 A__U133(tt, z0, z1, z2) -> c36(A__U134(a__isNatKind(z1), z0, z1, z2), A__ISNATKIND(z1)) A__U133(z0, z1, z2, z3) -> c37 A__U134(tt, z0, z1, z2) -> c38(A__U135(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U134(z0, z1, z2, z3) -> c39 A__U135(tt, z0, z1, z2) -> c40(A__U136(a__isNatKind(z2), z0, z1, z2), A__ISNATKIND(z2)) A__U135(z0, z1, z2, z3) -> c41 A__U136(tt, z0, z1, z2) -> c42(MARK(z2)) A__U136(z0, z1, z2, z3) -> c43 A__U21(tt, z0) -> c44(A__U22(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__U21(z0, z1) -> c45 A__U22(tt, z0) -> c46(A__U23(a__isNat(z0)), A__ISNAT(z0)) A__U22(z0, z1) -> c47 A__U23(tt) -> c48 A__U23(z0) -> c49 A__U31(tt, z0) -> c50(A__U32(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U31(z0, z1) -> c51 A__U32(tt, z0) -> c52(A__U33(a__isNatList(z0)), A__ISNATLIST(z0)) A__U32(z0, z1) -> c53 A__U33(tt) -> c54 A__U33(z0) -> c55 A__U41(tt, z0, z1) -> c56(A__U42(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U41(z0, z1, z2) -> c57 A__U42(tt, z0, z1) -> c58(A__U43(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U42(z0, z1, z2) -> c59 A__U43(tt, z0, z1) -> c60(A__U44(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U43(z0, z1, z2) -> c61 A__U44(tt, z0, z1) -> c62(A__U45(a__isNat(z0), z1), A__ISNAT(z0)) A__U44(z0, z1, z2) -> c63 A__U45(tt, z0) -> c64(A__U46(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U45(z0, z1) -> c65 A__U46(tt) -> c66 A__U46(z0) -> c67 A__U51(tt, z0) -> c68(A__U52(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U51(z0, z1) -> c69 A__U52(tt) -> c70 A__U52(z0) -> c71 A__U61(tt, z0) -> c72(A__U62(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U61(z0, z1) -> c73 A__U62(tt) -> c74 A__U62(z0) -> c75 A__U71(tt) -> c76 A__U71(z0) -> c77 A__U81(tt) -> c78 A__U81(z0) -> c79 A__U91(tt, z0, z1) -> c80(A__U92(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U91(z0, z1, z2) -> c81 A__U92(tt, z0, z1) -> c82(A__U93(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U92(z0, z1, z2) -> c83 A__U93(tt, z0, z1) -> c84(A__U94(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U93(z0, z1, z2) -> c85 A__U94(tt, z0, z1) -> c86(A__U95(a__isNat(z0), z1), A__ISNAT(z0)) A__U94(z0, z1, z2) -> c87 A__U95(tt, z0) -> c88(A__U96(a__isNatList(z0)), A__ISNATLIST(z0)) A__U95(z0, z1) -> c89 A__U96(tt) -> c90 A__U96(z0) -> c91 A__ISNAT(0) -> c92 A__ISNAT(length(z0)) -> c93(A__U11(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c94(A__U21(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__ISNAT(z0) -> c95 A__ISNATILIST(z0) -> c96(A__U31(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNATILIST(zeros) -> c97 A__ISNATILIST(cons(z0, z1)) -> c98(A__U41(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c99 A__ISNATILISTKIND(nil) -> c100 A__ISNATILISTKIND(zeros) -> c101 A__ISNATILISTKIND(cons(z0, z1)) -> c102(A__U51(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(take(z0, z1)) -> c103(A__U61(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(z0) -> c104 A__ISNATKIND(0) -> c105 A__ISNATKIND(length(z0)) -> c106(A__U71(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c107(A__U81(a__isNatKind(z0)), A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c108 A__ISNATLIST(nil) -> c109 A__ISNATLIST(cons(z0, z1)) -> c110(A__U91(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(take(z0, z1)) -> c111(A__U101(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c112 A__LENGTH(nil) -> c113 A__LENGTH(cons(z0, z1)) -> c114(A__U111(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c115 A__TAKE(0, z0) -> c116(A__U121(a__isNatIList(z0), z0), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c117(A__U131(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c118 MARK(zeros) -> c119(A__ZEROS) MARK(U101(z0, z1, z2)) -> c120(A__U101(mark(z0), z1, z2), MARK(z0)) MARK(U102(z0, z1, z2)) -> c121(A__U102(mark(z0), z1, z2), MARK(z0)) MARK(isNatKind(z0)) -> c122(A__ISNATKIND(z0)) MARK(U103(z0, z1, z2)) -> c123(A__U103(mark(z0), z1, z2), MARK(z0)) MARK(isNatIListKind(z0)) -> c124(A__ISNATILISTKIND(z0)) MARK(U104(z0, z1, z2)) -> c125(A__U104(mark(z0), z1, z2), MARK(z0)) MARK(U105(z0, z1)) -> c126(A__U105(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c127(A__ISNAT(z0)) MARK(U106(z0)) -> c128(A__U106(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c129(A__ISNATILIST(z0)) MARK(U11(z0, z1)) -> c130(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c131(A__U12(mark(z0), z1), MARK(z0)) MARK(U111(z0, z1, z2)) -> c132(A__U111(mark(z0), z1, z2), MARK(z0)) MARK(U112(z0, z1, z2)) -> c133(A__U112(mark(z0), z1, z2), MARK(z0)) MARK(U113(z0, z1, z2)) -> c134(A__U113(mark(z0), z1, z2), MARK(z0)) MARK(U114(z0, z1)) -> c135(A__U114(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c136(A__LENGTH(mark(z0)), MARK(z0)) MARK(U13(z0)) -> c137(A__U13(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c138(A__ISNATLIST(z0)) MARK(U121(z0, z1)) -> c139(A__U121(mark(z0), z1), MARK(z0)) MARK(U122(z0)) -> c140(A__U122(mark(z0)), MARK(z0)) MARK(U131(z0, z1, z2, z3)) -> c141(A__U131(mark(z0), z1, z2, z3), MARK(z0)) MARK(U132(z0, z1, z2, z3)) -> c142(A__U132(mark(z0), z1, z2, z3), MARK(z0)) MARK(U133(z0, z1, z2, z3)) -> c143(A__U133(mark(z0), z1, z2, z3), MARK(z0)) MARK(U134(z0, z1, z2, z3)) -> c144(A__U134(mark(z0), z1, z2, z3), MARK(z0)) MARK(U135(z0, z1, z2, z3)) -> c145(A__U135(mark(z0), z1, z2, z3), MARK(z0)) MARK(U136(z0, z1, z2, z3)) -> c146(A__U136(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c147(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c148(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(U21(z0, z1)) -> c149(A__U21(mark(z0), z1), MARK(z0)) MARK(U22(z0, z1)) -> c150(A__U22(mark(z0), z1), MARK(z0)) MARK(U23(z0)) -> c151(A__U23(mark(z0)), MARK(z0)) MARK(U31(z0, z1)) -> c152(A__U31(mark(z0), z1), MARK(z0)) MARK(U32(z0, z1)) -> c153(A__U32(mark(z0), z1), MARK(z0)) MARK(U33(z0)) -> c154(A__U33(mark(z0)), MARK(z0)) MARK(U41(z0, z1, z2)) -> c155(A__U41(mark(z0), z1, z2), MARK(z0)) MARK(U42(z0, z1, z2)) -> c156(A__U42(mark(z0), z1, z2), MARK(z0)) MARK(U43(z0, z1, z2)) -> c157(A__U43(mark(z0), z1, z2), MARK(z0)) MARK(U44(z0, z1, z2)) -> c158(A__U44(mark(z0), z1, z2), MARK(z0)) MARK(U45(z0, z1)) -> c159(A__U45(mark(z0), z1), MARK(z0)) MARK(U46(z0)) -> c160(A__U46(mark(z0)), MARK(z0)) MARK(U51(z0, z1)) -> c161(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c162(A__U52(mark(z0)), MARK(z0)) MARK(U61(z0, z1)) -> c163(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c164(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0)) -> c165(A__U71(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c166(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2)) -> c167(A__U91(mark(z0), z1, z2), MARK(z0)) MARK(U92(z0, z1, z2)) -> c168(A__U92(mark(z0), z1, z2), MARK(z0)) MARK(U93(z0, z1, z2)) -> c169(A__U93(mark(z0), z1, z2), MARK(z0)) MARK(U94(z0, z1, z2)) -> c170(A__U94(mark(z0), z1, z2), MARK(z0)) MARK(U95(z0, z1)) -> c171(A__U95(mark(z0), z1), MARK(z0)) MARK(U96(z0)) -> c172(A__U96(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c173(MARK(z0)) MARK(0) -> c174 MARK(tt) -> c175 MARK(s(z0)) -> c176(MARK(z0)) MARK(nil) -> c177 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U101(tt, z0, z1) -> a__U102(a__isNatKind(z0), z0, z1) a__U101(z0, z1, z2) -> U101(z0, z1, z2) a__U102(tt, z0, z1) -> a__U103(a__isNatIListKind(z1), z0, z1) a__U102(z0, z1, z2) -> U102(z0, z1, z2) a__U103(tt, z0, z1) -> a__U104(a__isNatIListKind(z1), z0, z1) a__U103(z0, z1, z2) -> U103(z0, z1, z2) a__U104(tt, z0, z1) -> a__U105(a__isNat(z0), z1) a__U104(z0, z1, z2) -> U104(z0, z1, z2) a__U105(tt, z0) -> a__U106(a__isNatIList(z0)) a__U105(z0, z1) -> U105(z0, z1) a__U106(tt) -> tt a__U106(z0) -> U106(z0) a__U11(tt, z0) -> a__U12(a__isNatIListKind(z0), z0) a__U11(z0, z1) -> U11(z0, z1) a__U111(tt, z0, z1) -> a__U112(a__isNatIListKind(z0), z0, z1) a__U111(z0, z1, z2) -> U111(z0, z1, z2) a__U112(tt, z0, z1) -> a__U113(a__isNat(z1), z0, z1) a__U112(z0, z1, z2) -> U112(z0, z1, z2) a__U113(tt, z0, z1) -> a__U114(a__isNatKind(z1), z0) a__U113(z0, z1, z2) -> U113(z0, z1, z2) a__U114(tt, z0) -> s(a__length(mark(z0))) a__U114(z0, z1) -> U114(z0, z1) a__U12(tt, z0) -> a__U13(a__isNatList(z0)) a__U12(z0, z1) -> U12(z0, z1) a__U121(tt, z0) -> a__U122(a__isNatIListKind(z0)) a__U121(z0, z1) -> U121(z0, z1) a__U122(tt) -> nil a__U122(z0) -> U122(z0) a__U13(tt) -> tt a__U13(z0) -> U13(z0) a__U131(tt, z0, z1, z2) -> a__U132(a__isNatIListKind(z0), z0, z1, z2) a__U131(z0, z1, z2, z3) -> U131(z0, z1, z2, z3) a__U132(tt, z0, z1, z2) -> a__U133(a__isNat(z1), z0, z1, z2) a__U132(z0, z1, z2, z3) -> U132(z0, z1, z2, z3) a__U133(tt, z0, z1, z2) -> a__U134(a__isNatKind(z1), z0, z1, z2) a__U133(z0, z1, z2, z3) -> U133(z0, z1, z2, z3) a__U134(tt, z0, z1, z2) -> a__U135(a__isNat(z2), z0, z1, z2) a__U134(z0, z1, z2, z3) -> U134(z0, z1, z2, z3) a__U135(tt, z0, z1, z2) -> a__U136(a__isNatKind(z2), z0, z1, z2) a__U135(z0, z1, z2, z3) -> U135(z0, z1, z2, z3) a__U136(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U136(z0, z1, z2, z3) -> U136(z0, z1, z2, z3) a__U21(tt, z0) -> a__U22(a__isNatKind(z0), z0) a__U21(z0, z1) -> U21(z0, z1) a__U22(tt, z0) -> a__U23(a__isNat(z0)) a__U22(z0, z1) -> U22(z0, z1) a__U23(tt) -> tt a__U23(z0) -> U23(z0) a__U31(tt, z0) -> a__U32(a__isNatIListKind(z0), z0) a__U31(z0, z1) -> U31(z0, z1) a__U32(tt, z0) -> a__U33(a__isNatList(z0)) a__U32(z0, z1) -> U32(z0, z1) a__U33(tt) -> tt a__U33(z0) -> U33(z0) a__U41(tt, z0, z1) -> a__U42(a__isNatKind(z0), z0, z1) a__U41(z0, z1, z2) -> U41(z0, z1, z2) a__U42(tt, z0, z1) -> a__U43(a__isNatIListKind(z1), z0, z1) a__U42(z0, z1, z2) -> U42(z0, z1, z2) a__U43(tt, z0, z1) -> a__U44(a__isNatIListKind(z1), z0, z1) a__U43(z0, z1, z2) -> U43(z0, z1, z2) a__U44(tt, z0, z1) -> a__U45(a__isNat(z0), z1) a__U44(z0, z1, z2) -> U44(z0, z1, z2) a__U45(tt, z0) -> a__U46(a__isNatIList(z0)) a__U45(z0, z1) -> U45(z0, z1) a__U46(tt) -> tt a__U46(z0) -> U46(z0) a__U51(tt, z0) -> a__U52(a__isNatIListKind(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIListKind(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt) -> tt a__U71(z0) -> U71(z0) a__U81(tt) -> tt a__U81(z0) -> U81(z0) a__U91(tt, z0, z1) -> a__U92(a__isNatKind(z0), z0, z1) a__U91(z0, z1, z2) -> U91(z0, z1, z2) a__U92(tt, z0, z1) -> a__U93(a__isNatIListKind(z1), z0, z1) a__U92(z0, z1, z2) -> U92(z0, z1, z2) a__U93(tt, z0, z1) -> a__U94(a__isNatIListKind(z1), z0, z1) a__U93(z0, z1, z2) -> U93(z0, z1, z2) a__U94(tt, z0, z1) -> a__U95(a__isNat(z0), z1) a__U94(z0, z1, z2) -> U94(z0, z1, z2) a__U95(tt, z0) -> a__U96(a__isNatList(z0)) a__U95(z0, z1) -> U95(z0, z1) a__U96(tt) -> tt a__U96(z0) -> U96(z0) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatIListKind(z0), z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0), z0) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0), z0) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNatKind(z0), z0, z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatIListKind(nil) -> tt a__isNatIListKind(zeros) -> tt a__isNatIListKind(cons(z0, z1)) -> a__U51(a__isNatKind(z0), z1) a__isNatIListKind(take(z0, z1)) -> a__U61(a__isNatKind(z0), z1) a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatKind(0) -> tt a__isNatKind(length(z0)) -> a__U71(a__isNatIListKind(z0)) a__isNatKind(s(z0)) -> a__U81(a__isNatKind(z0)) a__isNatKind(z0) -> isNatKind(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U91(a__isNatKind(z0), z0, z1) a__isNatList(take(z0, z1)) -> a__U101(a__isNatKind(z0), z0, z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U111(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U121(a__isNatIList(z0), z0) a__take(s(z0), cons(z1, z2)) -> a__U131(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U101(z0, z1, z2)) -> a__U101(mark(z0), z1, z2) mark(U102(z0, z1, z2)) -> a__U102(mark(z0), z1, z2) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(U103(z0, z1, z2)) -> a__U103(mark(z0), z1, z2) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(U104(z0, z1, z2)) -> a__U104(mark(z0), z1, z2) mark(U105(z0, z1)) -> a__U105(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(U106(z0)) -> a__U106(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(U111(z0, z1, z2)) -> a__U111(mark(z0), z1, z2) mark(U112(z0, z1, z2)) -> a__U112(mark(z0), z1, z2) mark(U113(z0, z1, z2)) -> a__U113(mark(z0), z1, z2) mark(U114(z0, z1)) -> a__U114(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U13(z0)) -> a__U13(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U121(z0, z1)) -> a__U121(mark(z0), z1) mark(U122(z0)) -> a__U122(mark(z0)) mark(U131(z0, z1, z2, z3)) -> a__U131(mark(z0), z1, z2, z3) mark(U132(z0, z1, z2, z3)) -> a__U132(mark(z0), z1, z2, z3) mark(U133(z0, z1, z2, z3)) -> a__U133(mark(z0), z1, z2, z3) mark(U134(z0, z1, z2, z3)) -> a__U134(mark(z0), z1, z2, z3) mark(U135(z0, z1, z2, z3)) -> a__U135(mark(z0), z1, z2, z3) mark(U136(z0, z1, z2, z3)) -> a__U136(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(U21(z0, z1)) -> a__U21(mark(z0), z1) mark(U22(z0, z1)) -> a__U22(mark(z0), z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0, z1)) -> a__U31(mark(z0), z1) mark(U32(z0, z1)) -> a__U32(mark(z0), z1) mark(U33(z0)) -> a__U33(mark(z0)) mark(U41(z0, z1, z2)) -> a__U41(mark(z0), z1, z2) mark(U42(z0, z1, z2)) -> a__U42(mark(z0), z1, z2) mark(U43(z0, z1, z2)) -> a__U43(mark(z0), z1, z2) mark(U44(z0, z1, z2)) -> a__U44(mark(z0), z1, z2) mark(U45(z0, z1)) -> a__U45(mark(z0), z1) mark(U46(z0)) -> a__U46(mark(z0)) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0)) -> a__U71(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2)) -> a__U91(mark(z0), z1, z2) mark(U92(z0, z1, z2)) -> a__U92(mark(z0), z1, z2) mark(U93(z0, z1, z2)) -> a__U93(mark(z0), z1, z2) mark(U94(z0, z1, z2)) -> a__U94(mark(z0), z1, z2) mark(U95(z0, z1)) -> a__U95(mark(z0), z1) mark(U96(z0)) -> a__U96(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(tt) -> tt mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (4) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: A__ZEROS -> c A__ZEROS -> c1 A__U101(tt, z0, z1) -> c2(A__U102(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U101(z0, z1, z2) -> c3 A__U102(tt, z0, z1) -> c4(A__U103(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U102(z0, z1, z2) -> c5 A__U103(tt, z0, z1) -> c6(A__U104(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U103(z0, z1, z2) -> c7 A__U104(tt, z0, z1) -> c8(A__U105(a__isNat(z0), z1), A__ISNAT(z0)) A__U104(z0, z1, z2) -> c9 A__U105(tt, z0) -> c10(A__U106(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U105(z0, z1) -> c11 A__U106(tt) -> c12 A__U106(z0) -> c13 A__U11(tt, z0) -> c14(A__U12(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U11(z0, z1) -> c15 A__U111(tt, z0, z1) -> c16(A__U112(a__isNatIListKind(z0), z0, z1), A__ISNATILISTKIND(z0)) A__U111(z0, z1, z2) -> c17 A__U112(tt, z0, z1) -> c18(A__U113(a__isNat(z1), z0, z1), A__ISNAT(z1)) A__U112(z0, z1, z2) -> c19 A__U113(tt, z0, z1) -> c20(A__U114(a__isNatKind(z1), z0), A__ISNATKIND(z1)) A__U113(z0, z1, z2) -> c21 A__U114(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U114(z0, z1) -> c23 A__U12(tt, z0) -> c24(A__U13(a__isNatList(z0)), A__ISNATLIST(z0)) A__U12(z0, z1) -> c25 A__U121(tt, z0) -> c26(A__U122(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U121(z0, z1) -> c27 A__U122(tt) -> c28 A__U122(z0) -> c29 A__U13(tt) -> c30 A__U13(z0) -> c31 A__U131(tt, z0, z1, z2) -> c32(A__U132(a__isNatIListKind(z0), z0, z1, z2), A__ISNATILISTKIND(z0)) A__U131(z0, z1, z2, z3) -> c33 A__U132(tt, z0, z1, z2) -> c34(A__U133(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U132(z0, z1, z2, z3) -> c35 A__U133(tt, z0, z1, z2) -> c36(A__U134(a__isNatKind(z1), z0, z1, z2), A__ISNATKIND(z1)) A__U133(z0, z1, z2, z3) -> c37 A__U134(tt, z0, z1, z2) -> c38(A__U135(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U134(z0, z1, z2, z3) -> c39 A__U135(tt, z0, z1, z2) -> c40(A__U136(a__isNatKind(z2), z0, z1, z2), A__ISNATKIND(z2)) A__U135(z0, z1, z2, z3) -> c41 A__U136(tt, z0, z1, z2) -> c42(MARK(z2)) A__U136(z0, z1, z2, z3) -> c43 A__U21(tt, z0) -> c44(A__U22(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__U21(z0, z1) -> c45 A__U22(tt, z0) -> c46(A__U23(a__isNat(z0)), A__ISNAT(z0)) A__U22(z0, z1) -> c47 A__U23(tt) -> c48 A__U23(z0) -> c49 A__U31(tt, z0) -> c50(A__U32(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U31(z0, z1) -> c51 A__U32(tt, z0) -> c52(A__U33(a__isNatList(z0)), A__ISNATLIST(z0)) A__U32(z0, z1) -> c53 A__U33(tt) -> c54 A__U33(z0) -> c55 A__U41(tt, z0, z1) -> c56(A__U42(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U41(z0, z1, z2) -> c57 A__U42(tt, z0, z1) -> c58(A__U43(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U42(z0, z1, z2) -> c59 A__U43(tt, z0, z1) -> c60(A__U44(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U43(z0, z1, z2) -> c61 A__U44(tt, z0, z1) -> c62(A__U45(a__isNat(z0), z1), A__ISNAT(z0)) A__U44(z0, z1, z2) -> c63 A__U45(tt, z0) -> c64(A__U46(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U45(z0, z1) -> c65 A__U46(tt) -> c66 A__U46(z0) -> c67 A__U51(tt, z0) -> c68(A__U52(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U51(z0, z1) -> c69 A__U52(tt) -> c70 A__U52(z0) -> c71 A__U61(tt, z0) -> c72(A__U62(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U61(z0, z1) -> c73 A__U62(tt) -> c74 A__U62(z0) -> c75 A__U71(tt) -> c76 A__U71(z0) -> c77 A__U81(tt) -> c78 A__U81(z0) -> c79 A__U91(tt, z0, z1) -> c80(A__U92(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U91(z0, z1, z2) -> c81 A__U92(tt, z0, z1) -> c82(A__U93(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U92(z0, z1, z2) -> c83 A__U93(tt, z0, z1) -> c84(A__U94(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U93(z0, z1, z2) -> c85 A__U94(tt, z0, z1) -> c86(A__U95(a__isNat(z0), z1), A__ISNAT(z0)) A__U94(z0, z1, z2) -> c87 A__U95(tt, z0) -> c88(A__U96(a__isNatList(z0)), A__ISNATLIST(z0)) A__U95(z0, z1) -> c89 A__U96(tt) -> c90 A__U96(z0) -> c91 A__ISNAT(0) -> c92 A__ISNAT(length(z0)) -> c93(A__U11(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c94(A__U21(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__ISNAT(z0) -> c95 A__ISNATILIST(z0) -> c96(A__U31(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNATILIST(zeros) -> c97 A__ISNATILIST(cons(z0, z1)) -> c98(A__U41(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c99 A__ISNATILISTKIND(nil) -> c100 A__ISNATILISTKIND(zeros) -> c101 A__ISNATILISTKIND(cons(z0, z1)) -> c102(A__U51(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(take(z0, z1)) -> c103(A__U61(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(z0) -> c104 A__ISNATKIND(0) -> c105 A__ISNATKIND(length(z0)) -> c106(A__U71(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c107(A__U81(a__isNatKind(z0)), A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c108 A__ISNATLIST(nil) -> c109 A__ISNATLIST(cons(z0, z1)) -> c110(A__U91(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(take(z0, z1)) -> c111(A__U101(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c112 A__LENGTH(nil) -> c113 A__LENGTH(cons(z0, z1)) -> c114(A__U111(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c115 A__TAKE(0, z0) -> c116(A__U121(a__isNatIList(z0), z0), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c117(A__U131(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c118 MARK(zeros) -> c119(A__ZEROS) MARK(U101(z0, z1, z2)) -> c120(A__U101(mark(z0), z1, z2), MARK(z0)) MARK(U102(z0, z1, z2)) -> c121(A__U102(mark(z0), z1, z2), MARK(z0)) MARK(isNatKind(z0)) -> c122(A__ISNATKIND(z0)) MARK(U103(z0, z1, z2)) -> c123(A__U103(mark(z0), z1, z2), MARK(z0)) MARK(isNatIListKind(z0)) -> c124(A__ISNATILISTKIND(z0)) MARK(U104(z0, z1, z2)) -> c125(A__U104(mark(z0), z1, z2), MARK(z0)) MARK(U105(z0, z1)) -> c126(A__U105(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c127(A__ISNAT(z0)) MARK(U106(z0)) -> c128(A__U106(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c129(A__ISNATILIST(z0)) MARK(U11(z0, z1)) -> c130(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c131(A__U12(mark(z0), z1), MARK(z0)) MARK(U111(z0, z1, z2)) -> c132(A__U111(mark(z0), z1, z2), MARK(z0)) MARK(U112(z0, z1, z2)) -> c133(A__U112(mark(z0), z1, z2), MARK(z0)) MARK(U113(z0, z1, z2)) -> c134(A__U113(mark(z0), z1, z2), MARK(z0)) MARK(U114(z0, z1)) -> c135(A__U114(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c136(A__LENGTH(mark(z0)), MARK(z0)) MARK(U13(z0)) -> c137(A__U13(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c138(A__ISNATLIST(z0)) MARK(U121(z0, z1)) -> c139(A__U121(mark(z0), z1), MARK(z0)) MARK(U122(z0)) -> c140(A__U122(mark(z0)), MARK(z0)) MARK(U131(z0, z1, z2, z3)) -> c141(A__U131(mark(z0), z1, z2, z3), MARK(z0)) MARK(U132(z0, z1, z2, z3)) -> c142(A__U132(mark(z0), z1, z2, z3), MARK(z0)) MARK(U133(z0, z1, z2, z3)) -> c143(A__U133(mark(z0), z1, z2, z3), MARK(z0)) MARK(U134(z0, z1, z2, z3)) -> c144(A__U134(mark(z0), z1, z2, z3), MARK(z0)) MARK(U135(z0, z1, z2, z3)) -> c145(A__U135(mark(z0), z1, z2, z3), MARK(z0)) MARK(U136(z0, z1, z2, z3)) -> c146(A__U136(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c147(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c148(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(U21(z0, z1)) -> c149(A__U21(mark(z0), z1), MARK(z0)) MARK(U22(z0, z1)) -> c150(A__U22(mark(z0), z1), MARK(z0)) MARK(U23(z0)) -> c151(A__U23(mark(z0)), MARK(z0)) MARK(U31(z0, z1)) -> c152(A__U31(mark(z0), z1), MARK(z0)) MARK(U32(z0, z1)) -> c153(A__U32(mark(z0), z1), MARK(z0)) MARK(U33(z0)) -> c154(A__U33(mark(z0)), MARK(z0)) MARK(U41(z0, z1, z2)) -> c155(A__U41(mark(z0), z1, z2), MARK(z0)) MARK(U42(z0, z1, z2)) -> c156(A__U42(mark(z0), z1, z2), MARK(z0)) MARK(U43(z0, z1, z2)) -> c157(A__U43(mark(z0), z1, z2), MARK(z0)) MARK(U44(z0, z1, z2)) -> c158(A__U44(mark(z0), z1, z2), MARK(z0)) MARK(U45(z0, z1)) -> c159(A__U45(mark(z0), z1), MARK(z0)) MARK(U46(z0)) -> c160(A__U46(mark(z0)), MARK(z0)) MARK(U51(z0, z1)) -> c161(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c162(A__U52(mark(z0)), MARK(z0)) MARK(U61(z0, z1)) -> c163(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c164(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0)) -> c165(A__U71(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c166(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2)) -> c167(A__U91(mark(z0), z1, z2), MARK(z0)) MARK(U92(z0, z1, z2)) -> c168(A__U92(mark(z0), z1, z2), MARK(z0)) MARK(U93(z0, z1, z2)) -> c169(A__U93(mark(z0), z1, z2), MARK(z0)) MARK(U94(z0, z1, z2)) -> c170(A__U94(mark(z0), z1, z2), MARK(z0)) MARK(U95(z0, z1)) -> c171(A__U95(mark(z0), z1), MARK(z0)) MARK(U96(z0)) -> c172(A__U96(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c173(MARK(z0)) MARK(0) -> c174 MARK(tt) -> c175 MARK(s(z0)) -> c176(MARK(z0)) MARK(nil) -> c177 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U101(tt, z0, z1) -> a__U102(a__isNatKind(z0), z0, z1) a__U101(z0, z1, z2) -> U101(z0, z1, z2) a__U102(tt, z0, z1) -> a__U103(a__isNatIListKind(z1), z0, z1) a__U102(z0, z1, z2) -> U102(z0, z1, z2) a__U103(tt, z0, z1) -> a__U104(a__isNatIListKind(z1), z0, z1) a__U103(z0, z1, z2) -> U103(z0, z1, z2) a__U104(tt, z0, z1) -> a__U105(a__isNat(z0), z1) a__U104(z0, z1, z2) -> U104(z0, z1, z2) a__U105(tt, z0) -> a__U106(a__isNatIList(z0)) a__U105(z0, z1) -> U105(z0, z1) a__U106(tt) -> tt a__U106(z0) -> U106(z0) a__U11(tt, z0) -> a__U12(a__isNatIListKind(z0), z0) a__U11(z0, z1) -> U11(z0, z1) a__U111(tt, z0, z1) -> a__U112(a__isNatIListKind(z0), z0, z1) a__U111(z0, z1, z2) -> U111(z0, z1, z2) a__U112(tt, z0, z1) -> a__U113(a__isNat(z1), z0, z1) a__U112(z0, z1, z2) -> U112(z0, z1, z2) a__U113(tt, z0, z1) -> a__U114(a__isNatKind(z1), z0) a__U113(z0, z1, z2) -> U113(z0, z1, z2) a__U114(tt, z0) -> s(a__length(mark(z0))) a__U114(z0, z1) -> U114(z0, z1) a__U12(tt, z0) -> a__U13(a__isNatList(z0)) a__U12(z0, z1) -> U12(z0, z1) a__U121(tt, z0) -> a__U122(a__isNatIListKind(z0)) a__U121(z0, z1) -> U121(z0, z1) a__U122(tt) -> nil a__U122(z0) -> U122(z0) a__U13(tt) -> tt a__U13(z0) -> U13(z0) a__U131(tt, z0, z1, z2) -> a__U132(a__isNatIListKind(z0), z0, z1, z2) a__U131(z0, z1, z2, z3) -> U131(z0, z1, z2, z3) a__U132(tt, z0, z1, z2) -> a__U133(a__isNat(z1), z0, z1, z2) a__U132(z0, z1, z2, z3) -> U132(z0, z1, z2, z3) a__U133(tt, z0, z1, z2) -> a__U134(a__isNatKind(z1), z0, z1, z2) a__U133(z0, z1, z2, z3) -> U133(z0, z1, z2, z3) a__U134(tt, z0, z1, z2) -> a__U135(a__isNat(z2), z0, z1, z2) a__U134(z0, z1, z2, z3) -> U134(z0, z1, z2, z3) a__U135(tt, z0, z1, z2) -> a__U136(a__isNatKind(z2), z0, z1, z2) a__U135(z0, z1, z2, z3) -> U135(z0, z1, z2, z3) a__U136(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U136(z0, z1, z2, z3) -> U136(z0, z1, z2, z3) a__U21(tt, z0) -> a__U22(a__isNatKind(z0), z0) a__U21(z0, z1) -> U21(z0, z1) a__U22(tt, z0) -> a__U23(a__isNat(z0)) a__U22(z0, z1) -> U22(z0, z1) a__U23(tt) -> tt a__U23(z0) -> U23(z0) a__U31(tt, z0) -> a__U32(a__isNatIListKind(z0), z0) a__U31(z0, z1) -> U31(z0, z1) a__U32(tt, z0) -> a__U33(a__isNatList(z0)) a__U32(z0, z1) -> U32(z0, z1) a__U33(tt) -> tt a__U33(z0) -> U33(z0) a__U41(tt, z0, z1) -> a__U42(a__isNatKind(z0), z0, z1) a__U41(z0, z1, z2) -> U41(z0, z1, z2) a__U42(tt, z0, z1) -> a__U43(a__isNatIListKind(z1), z0, z1) a__U42(z0, z1, z2) -> U42(z0, z1, z2) a__U43(tt, z0, z1) -> a__U44(a__isNatIListKind(z1), z0, z1) a__U43(z0, z1, z2) -> U43(z0, z1, z2) a__U44(tt, z0, z1) -> a__U45(a__isNat(z0), z1) a__U44(z0, z1, z2) -> U44(z0, z1, z2) a__U45(tt, z0) -> a__U46(a__isNatIList(z0)) a__U45(z0, z1) -> U45(z0, z1) a__U46(tt) -> tt a__U46(z0) -> U46(z0) a__U51(tt, z0) -> a__U52(a__isNatIListKind(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIListKind(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt) -> tt a__U71(z0) -> U71(z0) a__U81(tt) -> tt a__U81(z0) -> U81(z0) a__U91(tt, z0, z1) -> a__U92(a__isNatKind(z0), z0, z1) a__U91(z0, z1, z2) -> U91(z0, z1, z2) a__U92(tt, z0, z1) -> a__U93(a__isNatIListKind(z1), z0, z1) a__U92(z0, z1, z2) -> U92(z0, z1, z2) a__U93(tt, z0, z1) -> a__U94(a__isNatIListKind(z1), z0, z1) a__U93(z0, z1, z2) -> U93(z0, z1, z2) a__U94(tt, z0, z1) -> a__U95(a__isNat(z0), z1) a__U94(z0, z1, z2) -> U94(z0, z1, z2) a__U95(tt, z0) -> a__U96(a__isNatList(z0)) a__U95(z0, z1) -> U95(z0, z1) a__U96(tt) -> tt a__U96(z0) -> U96(z0) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatIListKind(z0), z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0), z0) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0), z0) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNatKind(z0), z0, z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatIListKind(nil) -> tt a__isNatIListKind(zeros) -> tt a__isNatIListKind(cons(z0, z1)) -> a__U51(a__isNatKind(z0), z1) a__isNatIListKind(take(z0, z1)) -> a__U61(a__isNatKind(z0), z1) a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatKind(0) -> tt a__isNatKind(length(z0)) -> a__U71(a__isNatIListKind(z0)) a__isNatKind(s(z0)) -> a__U81(a__isNatKind(z0)) a__isNatKind(z0) -> isNatKind(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U91(a__isNatKind(z0), z0, z1) a__isNatList(take(z0, z1)) -> a__U101(a__isNatKind(z0), z0, z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U111(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U121(a__isNatIList(z0), z0) a__take(s(z0), cons(z1, z2)) -> a__U131(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U101(z0, z1, z2)) -> a__U101(mark(z0), z1, z2) mark(U102(z0, z1, z2)) -> a__U102(mark(z0), z1, z2) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(U103(z0, z1, z2)) -> a__U103(mark(z0), z1, z2) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(U104(z0, z1, z2)) -> a__U104(mark(z0), z1, z2) mark(U105(z0, z1)) -> a__U105(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(U106(z0)) -> a__U106(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(U111(z0, z1, z2)) -> a__U111(mark(z0), z1, z2) mark(U112(z0, z1, z2)) -> a__U112(mark(z0), z1, z2) mark(U113(z0, z1, z2)) -> a__U113(mark(z0), z1, z2) mark(U114(z0, z1)) -> a__U114(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U13(z0)) -> a__U13(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U121(z0, z1)) -> a__U121(mark(z0), z1) mark(U122(z0)) -> a__U122(mark(z0)) mark(U131(z0, z1, z2, z3)) -> a__U131(mark(z0), z1, z2, z3) mark(U132(z0, z1, z2, z3)) -> a__U132(mark(z0), z1, z2, z3) mark(U133(z0, z1, z2, z3)) -> a__U133(mark(z0), z1, z2, z3) mark(U134(z0, z1, z2, z3)) -> a__U134(mark(z0), z1, z2, z3) mark(U135(z0, z1, z2, z3)) -> a__U135(mark(z0), z1, z2, z3) mark(U136(z0, z1, z2, z3)) -> a__U136(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(U21(z0, z1)) -> a__U21(mark(z0), z1) mark(U22(z0, z1)) -> a__U22(mark(z0), z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0, z1)) -> a__U31(mark(z0), z1) mark(U32(z0, z1)) -> a__U32(mark(z0), z1) mark(U33(z0)) -> a__U33(mark(z0)) mark(U41(z0, z1, z2)) -> a__U41(mark(z0), z1, z2) mark(U42(z0, z1, z2)) -> a__U42(mark(z0), z1, z2) mark(U43(z0, z1, z2)) -> a__U43(mark(z0), z1, z2) mark(U44(z0, z1, z2)) -> a__U44(mark(z0), z1, z2) mark(U45(z0, z1)) -> a__U45(mark(z0), z1) mark(U46(z0)) -> a__U46(mark(z0)) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0)) -> a__U71(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2)) -> a__U91(mark(z0), z1, z2) mark(U92(z0, z1, z2)) -> a__U92(mark(z0), z1, z2) mark(U93(z0, z1, z2)) -> a__U93(mark(z0), z1, z2) mark(U94(z0, z1, z2)) -> a__U94(mark(z0), z1, z2) mark(U95(z0, z1)) -> a__U95(mark(z0), z1) mark(U96(z0)) -> a__U96(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(tt) -> tt mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (5) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence MARK(U11(z0, z1)) ->^+ c130(A__U11(mark(z0), z1), MARK(z0)) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [z0 / U11(z0, z1)]. The result substitution is [ ]. ---------------------------------------- (6) Complex Obligation (BEST) ---------------------------------------- (7) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: A__ZEROS -> c A__ZEROS -> c1 A__U101(tt, z0, z1) -> c2(A__U102(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U101(z0, z1, z2) -> c3 A__U102(tt, z0, z1) -> c4(A__U103(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U102(z0, z1, z2) -> c5 A__U103(tt, z0, z1) -> c6(A__U104(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U103(z0, z1, z2) -> c7 A__U104(tt, z0, z1) -> c8(A__U105(a__isNat(z0), z1), A__ISNAT(z0)) A__U104(z0, z1, z2) -> c9 A__U105(tt, z0) -> c10(A__U106(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U105(z0, z1) -> c11 A__U106(tt) -> c12 A__U106(z0) -> c13 A__U11(tt, z0) -> c14(A__U12(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U11(z0, z1) -> c15 A__U111(tt, z0, z1) -> c16(A__U112(a__isNatIListKind(z0), z0, z1), A__ISNATILISTKIND(z0)) A__U111(z0, z1, z2) -> c17 A__U112(tt, z0, z1) -> c18(A__U113(a__isNat(z1), z0, z1), A__ISNAT(z1)) A__U112(z0, z1, z2) -> c19 A__U113(tt, z0, z1) -> c20(A__U114(a__isNatKind(z1), z0), A__ISNATKIND(z1)) A__U113(z0, z1, z2) -> c21 A__U114(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U114(z0, z1) -> c23 A__U12(tt, z0) -> c24(A__U13(a__isNatList(z0)), A__ISNATLIST(z0)) A__U12(z0, z1) -> c25 A__U121(tt, z0) -> c26(A__U122(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U121(z0, z1) -> c27 A__U122(tt) -> c28 A__U122(z0) -> c29 A__U13(tt) -> c30 A__U13(z0) -> c31 A__U131(tt, z0, z1, z2) -> c32(A__U132(a__isNatIListKind(z0), z0, z1, z2), A__ISNATILISTKIND(z0)) A__U131(z0, z1, z2, z3) -> c33 A__U132(tt, z0, z1, z2) -> c34(A__U133(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U132(z0, z1, z2, z3) -> c35 A__U133(tt, z0, z1, z2) -> c36(A__U134(a__isNatKind(z1), z0, z1, z2), A__ISNATKIND(z1)) A__U133(z0, z1, z2, z3) -> c37 A__U134(tt, z0, z1, z2) -> c38(A__U135(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U134(z0, z1, z2, z3) -> c39 A__U135(tt, z0, z1, z2) -> c40(A__U136(a__isNatKind(z2), z0, z1, z2), A__ISNATKIND(z2)) A__U135(z0, z1, z2, z3) -> c41 A__U136(tt, z0, z1, z2) -> c42(MARK(z2)) A__U136(z0, z1, z2, z3) -> c43 A__U21(tt, z0) -> c44(A__U22(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__U21(z0, z1) -> c45 A__U22(tt, z0) -> c46(A__U23(a__isNat(z0)), A__ISNAT(z0)) A__U22(z0, z1) -> c47 A__U23(tt) -> c48 A__U23(z0) -> c49 A__U31(tt, z0) -> c50(A__U32(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U31(z0, z1) -> c51 A__U32(tt, z0) -> c52(A__U33(a__isNatList(z0)), A__ISNATLIST(z0)) A__U32(z0, z1) -> c53 A__U33(tt) -> c54 A__U33(z0) -> c55 A__U41(tt, z0, z1) -> c56(A__U42(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U41(z0, z1, z2) -> c57 A__U42(tt, z0, z1) -> c58(A__U43(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U42(z0, z1, z2) -> c59 A__U43(tt, z0, z1) -> c60(A__U44(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U43(z0, z1, z2) -> c61 A__U44(tt, z0, z1) -> c62(A__U45(a__isNat(z0), z1), A__ISNAT(z0)) A__U44(z0, z1, z2) -> c63 A__U45(tt, z0) -> c64(A__U46(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U45(z0, z1) -> c65 A__U46(tt) -> c66 A__U46(z0) -> c67 A__U51(tt, z0) -> c68(A__U52(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U51(z0, z1) -> c69 A__U52(tt) -> c70 A__U52(z0) -> c71 A__U61(tt, z0) -> c72(A__U62(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U61(z0, z1) -> c73 A__U62(tt) -> c74 A__U62(z0) -> c75 A__U71(tt) -> c76 A__U71(z0) -> c77 A__U81(tt) -> c78 A__U81(z0) -> c79 A__U91(tt, z0, z1) -> c80(A__U92(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U91(z0, z1, z2) -> c81 A__U92(tt, z0, z1) -> c82(A__U93(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U92(z0, z1, z2) -> c83 A__U93(tt, z0, z1) -> c84(A__U94(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U93(z0, z1, z2) -> c85 A__U94(tt, z0, z1) -> c86(A__U95(a__isNat(z0), z1), A__ISNAT(z0)) A__U94(z0, z1, z2) -> c87 A__U95(tt, z0) -> c88(A__U96(a__isNatList(z0)), A__ISNATLIST(z0)) A__U95(z0, z1) -> c89 A__U96(tt) -> c90 A__U96(z0) -> c91 A__ISNAT(0) -> c92 A__ISNAT(length(z0)) -> c93(A__U11(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c94(A__U21(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__ISNAT(z0) -> c95 A__ISNATILIST(z0) -> c96(A__U31(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNATILIST(zeros) -> c97 A__ISNATILIST(cons(z0, z1)) -> c98(A__U41(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c99 A__ISNATILISTKIND(nil) -> c100 A__ISNATILISTKIND(zeros) -> c101 A__ISNATILISTKIND(cons(z0, z1)) -> c102(A__U51(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(take(z0, z1)) -> c103(A__U61(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(z0) -> c104 A__ISNATKIND(0) -> c105 A__ISNATKIND(length(z0)) -> c106(A__U71(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c107(A__U81(a__isNatKind(z0)), A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c108 A__ISNATLIST(nil) -> c109 A__ISNATLIST(cons(z0, z1)) -> c110(A__U91(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(take(z0, z1)) -> c111(A__U101(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c112 A__LENGTH(nil) -> c113 A__LENGTH(cons(z0, z1)) -> c114(A__U111(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c115 A__TAKE(0, z0) -> c116(A__U121(a__isNatIList(z0), z0), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c117(A__U131(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c118 MARK(zeros) -> c119(A__ZEROS) MARK(U101(z0, z1, z2)) -> c120(A__U101(mark(z0), z1, z2), MARK(z0)) MARK(U102(z0, z1, z2)) -> c121(A__U102(mark(z0), z1, z2), MARK(z0)) MARK(isNatKind(z0)) -> c122(A__ISNATKIND(z0)) MARK(U103(z0, z1, z2)) -> c123(A__U103(mark(z0), z1, z2), MARK(z0)) MARK(isNatIListKind(z0)) -> c124(A__ISNATILISTKIND(z0)) MARK(U104(z0, z1, z2)) -> c125(A__U104(mark(z0), z1, z2), MARK(z0)) MARK(U105(z0, z1)) -> c126(A__U105(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c127(A__ISNAT(z0)) MARK(U106(z0)) -> c128(A__U106(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c129(A__ISNATILIST(z0)) MARK(U11(z0, z1)) -> c130(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c131(A__U12(mark(z0), z1), MARK(z0)) MARK(U111(z0, z1, z2)) -> c132(A__U111(mark(z0), z1, z2), MARK(z0)) MARK(U112(z0, z1, z2)) -> c133(A__U112(mark(z0), z1, z2), MARK(z0)) MARK(U113(z0, z1, z2)) -> c134(A__U113(mark(z0), z1, z2), MARK(z0)) MARK(U114(z0, z1)) -> c135(A__U114(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c136(A__LENGTH(mark(z0)), MARK(z0)) MARK(U13(z0)) -> c137(A__U13(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c138(A__ISNATLIST(z0)) MARK(U121(z0, z1)) -> c139(A__U121(mark(z0), z1), MARK(z0)) MARK(U122(z0)) -> c140(A__U122(mark(z0)), MARK(z0)) MARK(U131(z0, z1, z2, z3)) -> c141(A__U131(mark(z0), z1, z2, z3), MARK(z0)) MARK(U132(z0, z1, z2, z3)) -> c142(A__U132(mark(z0), z1, z2, z3), MARK(z0)) MARK(U133(z0, z1, z2, z3)) -> c143(A__U133(mark(z0), z1, z2, z3), MARK(z0)) MARK(U134(z0, z1, z2, z3)) -> c144(A__U134(mark(z0), z1, z2, z3), MARK(z0)) MARK(U135(z0, z1, z2, z3)) -> c145(A__U135(mark(z0), z1, z2, z3), MARK(z0)) MARK(U136(z0, z1, z2, z3)) -> c146(A__U136(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c147(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c148(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(U21(z0, z1)) -> c149(A__U21(mark(z0), z1), MARK(z0)) MARK(U22(z0, z1)) -> c150(A__U22(mark(z0), z1), MARK(z0)) MARK(U23(z0)) -> c151(A__U23(mark(z0)), MARK(z0)) MARK(U31(z0, z1)) -> c152(A__U31(mark(z0), z1), MARK(z0)) MARK(U32(z0, z1)) -> c153(A__U32(mark(z0), z1), MARK(z0)) MARK(U33(z0)) -> c154(A__U33(mark(z0)), MARK(z0)) MARK(U41(z0, z1, z2)) -> c155(A__U41(mark(z0), z1, z2), MARK(z0)) MARK(U42(z0, z1, z2)) -> c156(A__U42(mark(z0), z1, z2), MARK(z0)) MARK(U43(z0, z1, z2)) -> c157(A__U43(mark(z0), z1, z2), MARK(z0)) MARK(U44(z0, z1, z2)) -> c158(A__U44(mark(z0), z1, z2), MARK(z0)) MARK(U45(z0, z1)) -> c159(A__U45(mark(z0), z1), MARK(z0)) MARK(U46(z0)) -> c160(A__U46(mark(z0)), MARK(z0)) MARK(U51(z0, z1)) -> c161(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c162(A__U52(mark(z0)), MARK(z0)) MARK(U61(z0, z1)) -> c163(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c164(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0)) -> c165(A__U71(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c166(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2)) -> c167(A__U91(mark(z0), z1, z2), MARK(z0)) MARK(U92(z0, z1, z2)) -> c168(A__U92(mark(z0), z1, z2), MARK(z0)) MARK(U93(z0, z1, z2)) -> c169(A__U93(mark(z0), z1, z2), MARK(z0)) MARK(U94(z0, z1, z2)) -> c170(A__U94(mark(z0), z1, z2), MARK(z0)) MARK(U95(z0, z1)) -> c171(A__U95(mark(z0), z1), MARK(z0)) MARK(U96(z0)) -> c172(A__U96(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c173(MARK(z0)) MARK(0) -> c174 MARK(tt) -> c175 MARK(s(z0)) -> c176(MARK(z0)) MARK(nil) -> c177 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U101(tt, z0, z1) -> a__U102(a__isNatKind(z0), z0, z1) a__U101(z0, z1, z2) -> U101(z0, z1, z2) a__U102(tt, z0, z1) -> a__U103(a__isNatIListKind(z1), z0, z1) a__U102(z0, z1, z2) -> U102(z0, z1, z2) a__U103(tt, z0, z1) -> a__U104(a__isNatIListKind(z1), z0, z1) a__U103(z0, z1, z2) -> U103(z0, z1, z2) a__U104(tt, z0, z1) -> a__U105(a__isNat(z0), z1) a__U104(z0, z1, z2) -> U104(z0, z1, z2) a__U105(tt, z0) -> a__U106(a__isNatIList(z0)) a__U105(z0, z1) -> U105(z0, z1) a__U106(tt) -> tt a__U106(z0) -> U106(z0) a__U11(tt, z0) -> a__U12(a__isNatIListKind(z0), z0) a__U11(z0, z1) -> U11(z0, z1) a__U111(tt, z0, z1) -> a__U112(a__isNatIListKind(z0), z0, z1) a__U111(z0, z1, z2) -> U111(z0, z1, z2) a__U112(tt, z0, z1) -> a__U113(a__isNat(z1), z0, z1) a__U112(z0, z1, z2) -> U112(z0, z1, z2) a__U113(tt, z0, z1) -> a__U114(a__isNatKind(z1), z0) a__U113(z0, z1, z2) -> U113(z0, z1, z2) a__U114(tt, z0) -> s(a__length(mark(z0))) a__U114(z0, z1) -> U114(z0, z1) a__U12(tt, z0) -> a__U13(a__isNatList(z0)) a__U12(z0, z1) -> U12(z0, z1) a__U121(tt, z0) -> a__U122(a__isNatIListKind(z0)) a__U121(z0, z1) -> U121(z0, z1) a__U122(tt) -> nil a__U122(z0) -> U122(z0) a__U13(tt) -> tt a__U13(z0) -> U13(z0) a__U131(tt, z0, z1, z2) -> a__U132(a__isNatIListKind(z0), z0, z1, z2) a__U131(z0, z1, z2, z3) -> U131(z0, z1, z2, z3) a__U132(tt, z0, z1, z2) -> a__U133(a__isNat(z1), z0, z1, z2) a__U132(z0, z1, z2, z3) -> U132(z0, z1, z2, z3) a__U133(tt, z0, z1, z2) -> a__U134(a__isNatKind(z1), z0, z1, z2) a__U133(z0, z1, z2, z3) -> U133(z0, z1, z2, z3) a__U134(tt, z0, z1, z2) -> a__U135(a__isNat(z2), z0, z1, z2) a__U134(z0, z1, z2, z3) -> U134(z0, z1, z2, z3) a__U135(tt, z0, z1, z2) -> a__U136(a__isNatKind(z2), z0, z1, z2) a__U135(z0, z1, z2, z3) -> U135(z0, z1, z2, z3) a__U136(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U136(z0, z1, z2, z3) -> U136(z0, z1, z2, z3) a__U21(tt, z0) -> a__U22(a__isNatKind(z0), z0) a__U21(z0, z1) -> U21(z0, z1) a__U22(tt, z0) -> a__U23(a__isNat(z0)) a__U22(z0, z1) -> U22(z0, z1) a__U23(tt) -> tt a__U23(z0) -> U23(z0) a__U31(tt, z0) -> a__U32(a__isNatIListKind(z0), z0) a__U31(z0, z1) -> U31(z0, z1) a__U32(tt, z0) -> a__U33(a__isNatList(z0)) a__U32(z0, z1) -> U32(z0, z1) a__U33(tt) -> tt a__U33(z0) -> U33(z0) a__U41(tt, z0, z1) -> a__U42(a__isNatKind(z0), z0, z1) a__U41(z0, z1, z2) -> U41(z0, z1, z2) a__U42(tt, z0, z1) -> a__U43(a__isNatIListKind(z1), z0, z1) a__U42(z0, z1, z2) -> U42(z0, z1, z2) a__U43(tt, z0, z1) -> a__U44(a__isNatIListKind(z1), z0, z1) a__U43(z0, z1, z2) -> U43(z0, z1, z2) a__U44(tt, z0, z1) -> a__U45(a__isNat(z0), z1) a__U44(z0, z1, z2) -> U44(z0, z1, z2) a__U45(tt, z0) -> a__U46(a__isNatIList(z0)) a__U45(z0, z1) -> U45(z0, z1) a__U46(tt) -> tt a__U46(z0) -> U46(z0) a__U51(tt, z0) -> a__U52(a__isNatIListKind(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIListKind(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt) -> tt a__U71(z0) -> U71(z0) a__U81(tt) -> tt a__U81(z0) -> U81(z0) a__U91(tt, z0, z1) -> a__U92(a__isNatKind(z0), z0, z1) a__U91(z0, z1, z2) -> U91(z0, z1, z2) a__U92(tt, z0, z1) -> a__U93(a__isNatIListKind(z1), z0, z1) a__U92(z0, z1, z2) -> U92(z0, z1, z2) a__U93(tt, z0, z1) -> a__U94(a__isNatIListKind(z1), z0, z1) a__U93(z0, z1, z2) -> U93(z0, z1, z2) a__U94(tt, z0, z1) -> a__U95(a__isNat(z0), z1) a__U94(z0, z1, z2) -> U94(z0, z1, z2) a__U95(tt, z0) -> a__U96(a__isNatList(z0)) a__U95(z0, z1) -> U95(z0, z1) a__U96(tt) -> tt a__U96(z0) -> U96(z0) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatIListKind(z0), z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0), z0) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0), z0) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNatKind(z0), z0, z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatIListKind(nil) -> tt a__isNatIListKind(zeros) -> tt a__isNatIListKind(cons(z0, z1)) -> a__U51(a__isNatKind(z0), z1) a__isNatIListKind(take(z0, z1)) -> a__U61(a__isNatKind(z0), z1) a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatKind(0) -> tt a__isNatKind(length(z0)) -> a__U71(a__isNatIListKind(z0)) a__isNatKind(s(z0)) -> a__U81(a__isNatKind(z0)) a__isNatKind(z0) -> isNatKind(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U91(a__isNatKind(z0), z0, z1) a__isNatList(take(z0, z1)) -> a__U101(a__isNatKind(z0), z0, z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U111(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U121(a__isNatIList(z0), z0) a__take(s(z0), cons(z1, z2)) -> a__U131(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U101(z0, z1, z2)) -> a__U101(mark(z0), z1, z2) mark(U102(z0, z1, z2)) -> a__U102(mark(z0), z1, z2) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(U103(z0, z1, z2)) -> a__U103(mark(z0), z1, z2) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(U104(z0, z1, z2)) -> a__U104(mark(z0), z1, z2) mark(U105(z0, z1)) -> a__U105(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(U106(z0)) -> a__U106(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(U111(z0, z1, z2)) -> a__U111(mark(z0), z1, z2) mark(U112(z0, z1, z2)) -> a__U112(mark(z0), z1, z2) mark(U113(z0, z1, z2)) -> a__U113(mark(z0), z1, z2) mark(U114(z0, z1)) -> a__U114(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U13(z0)) -> a__U13(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U121(z0, z1)) -> a__U121(mark(z0), z1) mark(U122(z0)) -> a__U122(mark(z0)) mark(U131(z0, z1, z2, z3)) -> a__U131(mark(z0), z1, z2, z3) mark(U132(z0, z1, z2, z3)) -> a__U132(mark(z0), z1, z2, z3) mark(U133(z0, z1, z2, z3)) -> a__U133(mark(z0), z1, z2, z3) mark(U134(z0, z1, z2, z3)) -> a__U134(mark(z0), z1, z2, z3) mark(U135(z0, z1, z2, z3)) -> a__U135(mark(z0), z1, z2, z3) mark(U136(z0, z1, z2, z3)) -> a__U136(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(U21(z0, z1)) -> a__U21(mark(z0), z1) mark(U22(z0, z1)) -> a__U22(mark(z0), z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0, z1)) -> a__U31(mark(z0), z1) mark(U32(z0, z1)) -> a__U32(mark(z0), z1) mark(U33(z0)) -> a__U33(mark(z0)) mark(U41(z0, z1, z2)) -> a__U41(mark(z0), z1, z2) mark(U42(z0, z1, z2)) -> a__U42(mark(z0), z1, z2) mark(U43(z0, z1, z2)) -> a__U43(mark(z0), z1, z2) mark(U44(z0, z1, z2)) -> a__U44(mark(z0), z1, z2) mark(U45(z0, z1)) -> a__U45(mark(z0), z1) mark(U46(z0)) -> a__U46(mark(z0)) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0)) -> a__U71(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2)) -> a__U91(mark(z0), z1, z2) mark(U92(z0, z1, z2)) -> a__U92(mark(z0), z1, z2) mark(U93(z0, z1, z2)) -> a__U93(mark(z0), z1, z2) mark(U94(z0, z1, z2)) -> a__U94(mark(z0), z1, z2) mark(U95(z0, z1)) -> a__U95(mark(z0), z1) mark(U96(z0)) -> a__U96(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(tt) -> tt mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil Rewrite Strategy: INNERMOST ---------------------------------------- (8) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (9) BOUNDS(n^1, INF) ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: A__ZEROS -> c A__ZEROS -> c1 A__U101(tt, z0, z1) -> c2(A__U102(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U101(z0, z1, z2) -> c3 A__U102(tt, z0, z1) -> c4(A__U103(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U102(z0, z1, z2) -> c5 A__U103(tt, z0, z1) -> c6(A__U104(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U103(z0, z1, z2) -> c7 A__U104(tt, z0, z1) -> c8(A__U105(a__isNat(z0), z1), A__ISNAT(z0)) A__U104(z0, z1, z2) -> c9 A__U105(tt, z0) -> c10(A__U106(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U105(z0, z1) -> c11 A__U106(tt) -> c12 A__U106(z0) -> c13 A__U11(tt, z0) -> c14(A__U12(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U11(z0, z1) -> c15 A__U111(tt, z0, z1) -> c16(A__U112(a__isNatIListKind(z0), z0, z1), A__ISNATILISTKIND(z0)) A__U111(z0, z1, z2) -> c17 A__U112(tt, z0, z1) -> c18(A__U113(a__isNat(z1), z0, z1), A__ISNAT(z1)) A__U112(z0, z1, z2) -> c19 A__U113(tt, z0, z1) -> c20(A__U114(a__isNatKind(z1), z0), A__ISNATKIND(z1)) A__U113(z0, z1, z2) -> c21 A__U114(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U114(z0, z1) -> c23 A__U12(tt, z0) -> c24(A__U13(a__isNatList(z0)), A__ISNATLIST(z0)) A__U12(z0, z1) -> c25 A__U121(tt, z0) -> c26(A__U122(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U121(z0, z1) -> c27 A__U122(tt) -> c28 A__U122(z0) -> c29 A__U13(tt) -> c30 A__U13(z0) -> c31 A__U131(tt, z0, z1, z2) -> c32(A__U132(a__isNatIListKind(z0), z0, z1, z2), A__ISNATILISTKIND(z0)) A__U131(z0, z1, z2, z3) -> c33 A__U132(tt, z0, z1, z2) -> c34(A__U133(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U132(z0, z1, z2, z3) -> c35 A__U133(tt, z0, z1, z2) -> c36(A__U134(a__isNatKind(z1), z0, z1, z2), A__ISNATKIND(z1)) A__U133(z0, z1, z2, z3) -> c37 A__U134(tt, z0, z1, z2) -> c38(A__U135(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U134(z0, z1, z2, z3) -> c39 A__U135(tt, z0, z1, z2) -> c40(A__U136(a__isNatKind(z2), z0, z1, z2), A__ISNATKIND(z2)) A__U135(z0, z1, z2, z3) -> c41 A__U136(tt, z0, z1, z2) -> c42(MARK(z2)) A__U136(z0, z1, z2, z3) -> c43 A__U21(tt, z0) -> c44(A__U22(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__U21(z0, z1) -> c45 A__U22(tt, z0) -> c46(A__U23(a__isNat(z0)), A__ISNAT(z0)) A__U22(z0, z1) -> c47 A__U23(tt) -> c48 A__U23(z0) -> c49 A__U31(tt, z0) -> c50(A__U32(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__U31(z0, z1) -> c51 A__U32(tt, z0) -> c52(A__U33(a__isNatList(z0)), A__ISNATLIST(z0)) A__U32(z0, z1) -> c53 A__U33(tt) -> c54 A__U33(z0) -> c55 A__U41(tt, z0, z1) -> c56(A__U42(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U41(z0, z1, z2) -> c57 A__U42(tt, z0, z1) -> c58(A__U43(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U42(z0, z1, z2) -> c59 A__U43(tt, z0, z1) -> c60(A__U44(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U43(z0, z1, z2) -> c61 A__U44(tt, z0, z1) -> c62(A__U45(a__isNat(z0), z1), A__ISNAT(z0)) A__U44(z0, z1, z2) -> c63 A__U45(tt, z0) -> c64(A__U46(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U45(z0, z1) -> c65 A__U46(tt) -> c66 A__U46(z0) -> c67 A__U51(tt, z0) -> c68(A__U52(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U51(z0, z1) -> c69 A__U52(tt) -> c70 A__U52(z0) -> c71 A__U61(tt, z0) -> c72(A__U62(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__U61(z0, z1) -> c73 A__U62(tt) -> c74 A__U62(z0) -> c75 A__U71(tt) -> c76 A__U71(z0) -> c77 A__U81(tt) -> c78 A__U81(z0) -> c79 A__U91(tt, z0, z1) -> c80(A__U92(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__U91(z0, z1, z2) -> c81 A__U92(tt, z0, z1) -> c82(A__U93(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U92(z0, z1, z2) -> c83 A__U93(tt, z0, z1) -> c84(A__U94(a__isNatIListKind(z1), z0, z1), A__ISNATILISTKIND(z1)) A__U93(z0, z1, z2) -> c85 A__U94(tt, z0, z1) -> c86(A__U95(a__isNat(z0), z1), A__ISNAT(z0)) A__U94(z0, z1, z2) -> c87 A__U95(tt, z0) -> c88(A__U96(a__isNatList(z0)), A__ISNATLIST(z0)) A__U95(z0, z1) -> c89 A__U96(tt) -> c90 A__U96(z0) -> c91 A__ISNAT(0) -> c92 A__ISNAT(length(z0)) -> c93(A__U11(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNAT(s(z0)) -> c94(A__U21(a__isNatKind(z0), z0), A__ISNATKIND(z0)) A__ISNAT(z0) -> c95 A__ISNATILIST(z0) -> c96(A__U31(a__isNatIListKind(z0), z0), A__ISNATILISTKIND(z0)) A__ISNATILIST(zeros) -> c97 A__ISNATILIST(cons(z0, z1)) -> c98(A__U41(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATILIST(z0) -> c99 A__ISNATILISTKIND(nil) -> c100 A__ISNATILISTKIND(zeros) -> c101 A__ISNATILISTKIND(cons(z0, z1)) -> c102(A__U51(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(take(z0, z1)) -> c103(A__U61(a__isNatKind(z0), z1), A__ISNATKIND(z0)) A__ISNATILISTKIND(z0) -> c104 A__ISNATKIND(0) -> c105 A__ISNATKIND(length(z0)) -> c106(A__U71(a__isNatIListKind(z0)), A__ISNATILISTKIND(z0)) A__ISNATKIND(s(z0)) -> c107(A__U81(a__isNatKind(z0)), A__ISNATKIND(z0)) A__ISNATKIND(z0) -> c108 A__ISNATLIST(nil) -> c109 A__ISNATLIST(cons(z0, z1)) -> c110(A__U91(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(take(z0, z1)) -> c111(A__U101(a__isNatKind(z0), z0, z1), A__ISNATKIND(z0)) A__ISNATLIST(z0) -> c112 A__LENGTH(nil) -> c113 A__LENGTH(cons(z0, z1)) -> c114(A__U111(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c115 A__TAKE(0, z0) -> c116(A__U121(a__isNatIList(z0), z0), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c117(A__U131(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c118 MARK(zeros) -> c119(A__ZEROS) MARK(U101(z0, z1, z2)) -> c120(A__U101(mark(z0), z1, z2), MARK(z0)) MARK(U102(z0, z1, z2)) -> c121(A__U102(mark(z0), z1, z2), MARK(z0)) MARK(isNatKind(z0)) -> c122(A__ISNATKIND(z0)) MARK(U103(z0, z1, z2)) -> c123(A__U103(mark(z0), z1, z2), MARK(z0)) MARK(isNatIListKind(z0)) -> c124(A__ISNATILISTKIND(z0)) MARK(U104(z0, z1, z2)) -> c125(A__U104(mark(z0), z1, z2), MARK(z0)) MARK(U105(z0, z1)) -> c126(A__U105(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c127(A__ISNAT(z0)) MARK(U106(z0)) -> c128(A__U106(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c129(A__ISNATILIST(z0)) MARK(U11(z0, z1)) -> c130(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c131(A__U12(mark(z0), z1), MARK(z0)) MARK(U111(z0, z1, z2)) -> c132(A__U111(mark(z0), z1, z2), MARK(z0)) MARK(U112(z0, z1, z2)) -> c133(A__U112(mark(z0), z1, z2), MARK(z0)) MARK(U113(z0, z1, z2)) -> c134(A__U113(mark(z0), z1, z2), MARK(z0)) MARK(U114(z0, z1)) -> c135(A__U114(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c136(A__LENGTH(mark(z0)), MARK(z0)) MARK(U13(z0)) -> c137(A__U13(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c138(A__ISNATLIST(z0)) MARK(U121(z0, z1)) -> c139(A__U121(mark(z0), z1), MARK(z0)) MARK(U122(z0)) -> c140(A__U122(mark(z0)), MARK(z0)) MARK(U131(z0, z1, z2, z3)) -> c141(A__U131(mark(z0), z1, z2, z3), MARK(z0)) MARK(U132(z0, z1, z2, z3)) -> c142(A__U132(mark(z0), z1, z2, z3), MARK(z0)) MARK(U133(z0, z1, z2, z3)) -> c143(A__U133(mark(z0), z1, z2, z3), MARK(z0)) MARK(U134(z0, z1, z2, z3)) -> c144(A__U134(mark(z0), z1, z2, z3), MARK(z0)) MARK(U135(z0, z1, z2, z3)) -> c145(A__U135(mark(z0), z1, z2, z3), MARK(z0)) MARK(U136(z0, z1, z2, z3)) -> c146(A__U136(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c147(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c148(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(U21(z0, z1)) -> c149(A__U21(mark(z0), z1), MARK(z0)) MARK(U22(z0, z1)) -> c150(A__U22(mark(z0), z1), MARK(z0)) MARK(U23(z0)) -> c151(A__U23(mark(z0)), MARK(z0)) MARK(U31(z0, z1)) -> c152(A__U31(mark(z0), z1), MARK(z0)) MARK(U32(z0, z1)) -> c153(A__U32(mark(z0), z1), MARK(z0)) MARK(U33(z0)) -> c154(A__U33(mark(z0)), MARK(z0)) MARK(U41(z0, z1, z2)) -> c155(A__U41(mark(z0), z1, z2), MARK(z0)) MARK(U42(z0, z1, z2)) -> c156(A__U42(mark(z0), z1, z2), MARK(z0)) MARK(U43(z0, z1, z2)) -> c157(A__U43(mark(z0), z1, z2), MARK(z0)) MARK(U44(z0, z1, z2)) -> c158(A__U44(mark(z0), z1, z2), MARK(z0)) MARK(U45(z0, z1)) -> c159(A__U45(mark(z0), z1), MARK(z0)) MARK(U46(z0)) -> c160(A__U46(mark(z0)), MARK(z0)) MARK(U51(z0, z1)) -> c161(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c162(A__U52(mark(z0)), MARK(z0)) MARK(U61(z0, z1)) -> c163(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c164(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0)) -> c165(A__U71(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c166(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2)) -> c167(A__U91(mark(z0), z1, z2), MARK(z0)) MARK(U92(z0, z1, z2)) -> c168(A__U92(mark(z0), z1, z2), MARK(z0)) MARK(U93(z0, z1, z2)) -> c169(A__U93(mark(z0), z1, z2), MARK(z0)) MARK(U94(z0, z1, z2)) -> c170(A__U94(mark(z0), z1, z2), MARK(z0)) MARK(U95(z0, z1)) -> c171(A__U95(mark(z0), z1), MARK(z0)) MARK(U96(z0)) -> c172(A__U96(mark(z0)), MARK(z0)) MARK(cons(z0, z1)) -> c173(MARK(z0)) MARK(0) -> c174 MARK(tt) -> c175 MARK(s(z0)) -> c176(MARK(z0)) MARK(nil) -> c177 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U101(tt, z0, z1) -> a__U102(a__isNatKind(z0), z0, z1) a__U101(z0, z1, z2) -> U101(z0, z1, z2) a__U102(tt, z0, z1) -> a__U103(a__isNatIListKind(z1), z0, z1) a__U102(z0, z1, z2) -> U102(z0, z1, z2) a__U103(tt, z0, z1) -> a__U104(a__isNatIListKind(z1), z0, z1) a__U103(z0, z1, z2) -> U103(z0, z1, z2) a__U104(tt, z0, z1) -> a__U105(a__isNat(z0), z1) a__U104(z0, z1, z2) -> U104(z0, z1, z2) a__U105(tt, z0) -> a__U106(a__isNatIList(z0)) a__U105(z0, z1) -> U105(z0, z1) a__U106(tt) -> tt a__U106(z0) -> U106(z0) a__U11(tt, z0) -> a__U12(a__isNatIListKind(z0), z0) a__U11(z0, z1) -> U11(z0, z1) a__U111(tt, z0, z1) -> a__U112(a__isNatIListKind(z0), z0, z1) a__U111(z0, z1, z2) -> U111(z0, z1, z2) a__U112(tt, z0, z1) -> a__U113(a__isNat(z1), z0, z1) a__U112(z0, z1, z2) -> U112(z0, z1, z2) a__U113(tt, z0, z1) -> a__U114(a__isNatKind(z1), z0) a__U113(z0, z1, z2) -> U113(z0, z1, z2) a__U114(tt, z0) -> s(a__length(mark(z0))) a__U114(z0, z1) -> U114(z0, z1) a__U12(tt, z0) -> a__U13(a__isNatList(z0)) a__U12(z0, z1) -> U12(z0, z1) a__U121(tt, z0) -> a__U122(a__isNatIListKind(z0)) a__U121(z0, z1) -> U121(z0, z1) a__U122(tt) -> nil a__U122(z0) -> U122(z0) a__U13(tt) -> tt a__U13(z0) -> U13(z0) a__U131(tt, z0, z1, z2) -> a__U132(a__isNatIListKind(z0), z0, z1, z2) a__U131(z0, z1, z2, z3) -> U131(z0, z1, z2, z3) a__U132(tt, z0, z1, z2) -> a__U133(a__isNat(z1), z0, z1, z2) a__U132(z0, z1, z2, z3) -> U132(z0, z1, z2, z3) a__U133(tt, z0, z1, z2) -> a__U134(a__isNatKind(z1), z0, z1, z2) a__U133(z0, z1, z2, z3) -> U133(z0, z1, z2, z3) a__U134(tt, z0, z1, z2) -> a__U135(a__isNat(z2), z0, z1, z2) a__U134(z0, z1, z2, z3) -> U134(z0, z1, z2, z3) a__U135(tt, z0, z1, z2) -> a__U136(a__isNatKind(z2), z0, z1, z2) a__U135(z0, z1, z2, z3) -> U135(z0, z1, z2, z3) a__U136(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U136(z0, z1, z2, z3) -> U136(z0, z1, z2, z3) a__U21(tt, z0) -> a__U22(a__isNatKind(z0), z0) a__U21(z0, z1) -> U21(z0, z1) a__U22(tt, z0) -> a__U23(a__isNat(z0)) a__U22(z0, z1) -> U22(z0, z1) a__U23(tt) -> tt a__U23(z0) -> U23(z0) a__U31(tt, z0) -> a__U32(a__isNatIListKind(z0), z0) a__U31(z0, z1) -> U31(z0, z1) a__U32(tt, z0) -> a__U33(a__isNatList(z0)) a__U32(z0, z1) -> U32(z0, z1) a__U33(tt) -> tt a__U33(z0) -> U33(z0) a__U41(tt, z0, z1) -> a__U42(a__isNatKind(z0), z0, z1) a__U41(z0, z1, z2) -> U41(z0, z1, z2) a__U42(tt, z0, z1) -> a__U43(a__isNatIListKind(z1), z0, z1) a__U42(z0, z1, z2) -> U42(z0, z1, z2) a__U43(tt, z0, z1) -> a__U44(a__isNatIListKind(z1), z0, z1) a__U43(z0, z1, z2) -> U43(z0, z1, z2) a__U44(tt, z0, z1) -> a__U45(a__isNat(z0), z1) a__U44(z0, z1, z2) -> U44(z0, z1, z2) a__U45(tt, z0) -> a__U46(a__isNatIList(z0)) a__U45(z0, z1) -> U45(z0, z1) a__U46(tt) -> tt a__U46(z0) -> U46(z0) a__U51(tt, z0) -> a__U52(a__isNatIListKind(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIListKind(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt) -> tt a__U71(z0) -> U71(z0) a__U81(tt) -> tt a__U81(z0) -> U81(z0) a__U91(tt, z0, z1) -> a__U92(a__isNatKind(z0), z0, z1) a__U91(z0, z1, z2) -> U91(z0, z1, z2) a__U92(tt, z0, z1) -> a__U93(a__isNatIListKind(z1), z0, z1) a__U92(z0, z1, z2) -> U92(z0, z1, z2) a__U93(tt, z0, z1) -> a__U94(a__isNatIListKind(z1), z0, z1) a__U93(z0, z1, z2) -> U93(z0, z1, z2) a__U94(tt, z0, z1) -> a__U95(a__isNat(z0), z1) a__U94(z0, z1, z2) -> U94(z0, z1, z2) a__U95(tt, z0) -> a__U96(a__isNatList(z0)) a__U95(z0, z1) -> U95(z0, z1) a__U96(tt) -> tt a__U96(z0) -> U96(z0) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatIListKind(z0), z0) a__isNat(s(z0)) -> a__U21(a__isNatKind(z0), z0) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatIListKind(z0), z0) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNatKind(z0), z0, z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatIListKind(nil) -> tt a__isNatIListKind(zeros) -> tt a__isNatIListKind(cons(z0, z1)) -> a__U51(a__isNatKind(z0), z1) a__isNatIListKind(take(z0, z1)) -> a__U61(a__isNatKind(z0), z1) a__isNatIListKind(z0) -> isNatIListKind(z0) a__isNatKind(0) -> tt a__isNatKind(length(z0)) -> a__U71(a__isNatIListKind(z0)) a__isNatKind(s(z0)) -> a__U81(a__isNatKind(z0)) a__isNatKind(z0) -> isNatKind(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U91(a__isNatKind(z0), z0, z1) a__isNatList(take(z0, z1)) -> a__U101(a__isNatKind(z0), z0, z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U111(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U121(a__isNatIList(z0), z0) a__take(s(z0), cons(z1, z2)) -> a__U131(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U101(z0, z1, z2)) -> a__U101(mark(z0), z1, z2) mark(U102(z0, z1, z2)) -> a__U102(mark(z0), z1, z2) mark(isNatKind(z0)) -> a__isNatKind(z0) mark(U103(z0, z1, z2)) -> a__U103(mark(z0), z1, z2) mark(isNatIListKind(z0)) -> a__isNatIListKind(z0) mark(U104(z0, z1, z2)) -> a__U104(mark(z0), z1, z2) mark(U105(z0, z1)) -> a__U105(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(U106(z0)) -> a__U106(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(U111(z0, z1, z2)) -> a__U111(mark(z0), z1, z2) mark(U112(z0, z1, z2)) -> a__U112(mark(z0), z1, z2) mark(U113(z0, z1, z2)) -> a__U113(mark(z0), z1, z2) mark(U114(z0, z1)) -> a__U114(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U13(z0)) -> a__U13(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U121(z0, z1)) -> a__U121(mark(z0), z1) mark(U122(z0)) -> a__U122(mark(z0)) mark(U131(z0, z1, z2, z3)) -> a__U131(mark(z0), z1, z2, z3) mark(U132(z0, z1, z2, z3)) -> a__U132(mark(z0), z1, z2, z3) mark(U133(z0, z1, z2, z3)) -> a__U133(mark(z0), z1, z2, z3) mark(U134(z0, z1, z2, z3)) -> a__U134(mark(z0), z1, z2, z3) mark(U135(z0, z1, z2, z3)) -> a__U135(mark(z0), z1, z2, z3) mark(U136(z0, z1, z2, z3)) -> a__U136(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) mark(U21(z0, z1)) -> a__U21(mark(z0), z1) mark(U22(z0, z1)) -> a__U22(mark(z0), z1) mark(U23(z0)) -> a__U23(mark(z0)) mark(U31(z0, z1)) -> a__U31(mark(z0), z1) mark(U32(z0, z1)) -> a__U32(mark(z0), z1) mark(U33(z0)) -> a__U33(mark(z0)) mark(U41(z0, z1, z2)) -> a__U41(mark(z0), z1, z2) mark(U42(z0, z1, z2)) -> a__U42(mark(z0), z1, z2) mark(U43(z0, z1, z2)) -> a__U43(mark(z0), z1, z2) mark(U44(z0, z1, z2)) -> a__U44(mark(z0), z1, z2) mark(U45(z0, z1)) -> a__U45(mark(z0), z1) mark(U46(z0)) -> a__U46(mark(z0)) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0)) -> a__U71(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2)) -> a__U91(mark(z0), z1, z2) mark(U92(z0, z1, z2)) -> a__U92(mark(z0), z1, z2) mark(U93(z0, z1, z2)) -> a__U93(mark(z0), z1, z2) mark(U94(z0, z1, z2)) -> a__U94(mark(z0), z1, z2) mark(U95(z0, z1)) -> a__U95(mark(z0), z1) mark(U96(z0)) -> a__U96(mark(z0)) mark(cons(z0, z1)) -> cons(mark(z0), z1) mark(0) -> 0 mark(tt) -> tt mark(s(z0)) -> s(mark(z0)) mark(nil) -> nil Rewrite Strategy: INNERMOST