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), 5539 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 6 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 3 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__U11(tt) -> c2 A__U11(z0) -> c3 A__U21(tt) -> c4 A__U21(z0) -> c5 A__U31(tt) -> c6 A__U31(z0) -> c7 A__U41(tt, z0) -> c8(A__U42(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U41(z0, z1) -> c9 A__U42(tt) -> c10 A__U42(z0) -> c11 A__U51(tt, z0) -> c12(A__U52(a__isNatList(z0)), A__ISNATLIST(z0)) A__U51(z0, z1) -> c13 A__U52(tt) -> c14 A__U52(z0) -> c15 A__U61(tt, z0) -> c16(A__U62(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U61(z0, z1) -> c17 A__U62(tt) -> c18 A__U62(z0) -> c19 A__U71(tt, z0, z1) -> c20(A__U72(a__isNat(z1), z0), A__ISNAT(z1)) A__U71(z0, z1, z2) -> c21 A__U72(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U72(z0, z1) -> c23 A__U81(tt) -> c24 A__U81(z0) -> c25 A__U91(tt, z0, z1, z2) -> c26(A__U92(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U91(z0, z1, z2, z3) -> c27 A__U92(tt, z0, z1, z2) -> c28(A__U93(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U92(z0, z1, z2, z3) -> c29 A__U93(tt, z0, z1, z2) -> c30(MARK(z2)) A__U93(z0, z1, z2, z3) -> c31 A__ISNAT(0) -> c32 A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)), A__ISNAT(z0)) A__ISNAT(z0) -> c35 A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNATILIST(zeros) -> c37 A__ISNATILIST(cons(z0, z1)) -> c38(A__U41(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATILIST(z0) -> c39 A__ISNATLIST(nil) -> c40 A__ISNATLIST(cons(z0, z1)) -> c41(A__U51(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(take(z0, z1)) -> c42(A__U61(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(z0) -> c43 A__LENGTH(nil) -> c44 A__LENGTH(cons(z0, z1)) -> c45(A__U71(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c46 A__TAKE(0, z0) -> c47(A__U81(a__isNatIList(z0)), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c48(A__U91(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c49 MARK(zeros) -> c50(A__ZEROS) MARK(U11(z0)) -> c51(A__U11(mark(z0)), MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)), MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)), MARK(z0)) MARK(U41(z0, z1)) -> c54(A__U41(mark(z0), z1), MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(U51(z0, z1)) -> c57(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(U61(z0, z1)) -> c60(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0, z1, z2)) -> c62(A__U71(mark(z0), z1, z2), MARK(z0)) MARK(U72(z0, z1)) -> c63(A__U72(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2, z3)) -> c67(A__U91(mark(z0), z1, z2, z3), MARK(z0)) MARK(U92(z0, z1, z2, z3)) -> c68(A__U92(mark(z0), z1, z2, z3), MARK(z0)) MARK(U93(z0, z1, z2, z3)) -> c69(A__U93(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c70(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c71(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c72(MARK(z0)) MARK(0) -> c73 MARK(tt) -> c74 MARK(s(z0)) -> c75(MARK(z0)) MARK(nil) -> c76 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U11(tt) -> tt a__U11(z0) -> U11(z0) a__U21(tt) -> tt a__U21(z0) -> U21(z0) a__U31(tt) -> tt a__U31(z0) -> U31(z0) a__U41(tt, z0) -> a__U42(a__isNatIList(z0)) a__U41(z0, z1) -> U41(z0, z1) a__U42(tt) -> tt a__U42(z0) -> U42(z0) a__U51(tt, z0) -> a__U52(a__isNatList(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIList(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt, z0, z1) -> a__U72(a__isNat(z1), z0) a__U71(z0, z1, z2) -> U71(z0, z1, z2) a__U72(tt, z0) -> s(a__length(mark(z0))) a__U72(z0, z1) -> U72(z0, z1) a__U81(tt) -> nil a__U81(z0) -> U81(z0) a__U91(tt, z0, z1, z2) -> a__U92(a__isNat(z1), z0, z1, z2) a__U91(z0, z1, z2, z3) -> U91(z0, z1, z2, z3) a__U92(tt, z0, z1, z2) -> a__U93(a__isNat(z2), z0, z1, z2) a__U92(z0, z1, z2, z3) -> U92(z0, z1, z2, z3) a__U93(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U93(z0, z1, z2, z3) -> U93(z0, z1, z2, z3) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNat(z0), z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U51(a__isNat(z0), z1) a__isNatList(take(z0, z1)) -> a__U61(a__isNat(z0), z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U71(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0), cons(z1, z2)) -> a__U91(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0, z1)) -> a__U41(mark(z0), z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0, z1, z2)) -> a__U71(mark(z0), z1, z2) mark(U72(z0, z1)) -> a__U72(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(length(z0)) -> a__length(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2, z3)) -> a__U91(mark(z0), z1, z2, z3) mark(U92(z0, z1, z2, z3)) -> a__U92(mark(z0), z1, z2, z3) mark(U93(z0, z1, z2, z3)) -> a__U93(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) 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__U11(tt) -> c2 A__U11(z0) -> c3 A__U21(tt) -> c4 A__U21(z0) -> c5 A__U31(tt) -> c6 A__U31(z0) -> c7 A__U41(tt, z0) -> c8(A__U42(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U41(z0, z1) -> c9 A__U42(tt) -> c10 A__U42(z0) -> c11 A__U51(tt, z0) -> c12(A__U52(a__isNatList(z0)), A__ISNATLIST(z0)) A__U51(z0, z1) -> c13 A__U52(tt) -> c14 A__U52(z0) -> c15 A__U61(tt, z0) -> c16(A__U62(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U61(z0, z1) -> c17 A__U62(tt) -> c18 A__U62(z0) -> c19 A__U71(tt, z0, z1) -> c20(A__U72(a__isNat(z1), z0), A__ISNAT(z1)) A__U71(z0, z1, z2) -> c21 A__U72(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U72(z0, z1) -> c23 A__U81(tt) -> c24 A__U81(z0) -> c25 A__U91(tt, z0, z1, z2) -> c26(A__U92(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U91(z0, z1, z2, z3) -> c27 A__U92(tt, z0, z1, z2) -> c28(A__U93(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U92(z0, z1, z2, z3) -> c29 A__U93(tt, z0, z1, z2) -> c30(MARK(z2)) A__U93(z0, z1, z2, z3) -> c31 A__ISNAT(0) -> c32 A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)), A__ISNAT(z0)) A__ISNAT(z0) -> c35 A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNATILIST(zeros) -> c37 A__ISNATILIST(cons(z0, z1)) -> c38(A__U41(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATILIST(z0) -> c39 A__ISNATLIST(nil) -> c40 A__ISNATLIST(cons(z0, z1)) -> c41(A__U51(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(take(z0, z1)) -> c42(A__U61(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(z0) -> c43 A__LENGTH(nil) -> c44 A__LENGTH(cons(z0, z1)) -> c45(A__U71(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c46 A__TAKE(0, z0) -> c47(A__U81(a__isNatIList(z0)), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c48(A__U91(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c49 MARK(zeros) -> c50(A__ZEROS) MARK(U11(z0)) -> c51(A__U11(mark(z0)), MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)), MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)), MARK(z0)) MARK(U41(z0, z1)) -> c54(A__U41(mark(z0), z1), MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(U51(z0, z1)) -> c57(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(U61(z0, z1)) -> c60(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0, z1, z2)) -> c62(A__U71(mark(z0), z1, z2), MARK(z0)) MARK(U72(z0, z1)) -> c63(A__U72(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2, z3)) -> c67(A__U91(mark(z0), z1, z2, z3), MARK(z0)) MARK(U92(z0, z1, z2, z3)) -> c68(A__U92(mark(z0), z1, z2, z3), MARK(z0)) MARK(U93(z0, z1, z2, z3)) -> c69(A__U93(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c70(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c71(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c72(MARK(z0)) MARK(0) -> c73 MARK(tt) -> c74 MARK(s(z0)) -> c75(MARK(z0)) MARK(nil) -> c76 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U11(tt) -> tt a__U11(z0) -> U11(z0) a__U21(tt) -> tt a__U21(z0) -> U21(z0) a__U31(tt) -> tt a__U31(z0) -> U31(z0) a__U41(tt, z0) -> a__U42(a__isNatIList(z0)) a__U41(z0, z1) -> U41(z0, z1) a__U42(tt) -> tt a__U42(z0) -> U42(z0) a__U51(tt, z0) -> a__U52(a__isNatList(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIList(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt, z0, z1) -> a__U72(a__isNat(z1), z0) a__U71(z0, z1, z2) -> U71(z0, z1, z2) a__U72(tt, z0) -> s(a__length(mark(z0))) a__U72(z0, z1) -> U72(z0, z1) a__U81(tt) -> nil a__U81(z0) -> U81(z0) a__U91(tt, z0, z1, z2) -> a__U92(a__isNat(z1), z0, z1, z2) a__U91(z0, z1, z2, z3) -> U91(z0, z1, z2, z3) a__U92(tt, z0, z1, z2) -> a__U93(a__isNat(z2), z0, z1, z2) a__U92(z0, z1, z2, z3) -> U92(z0, z1, z2, z3) a__U93(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U93(z0, z1, z2, z3) -> U93(z0, z1, z2, z3) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNat(z0), z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U51(a__isNat(z0), z1) a__isNatList(take(z0, z1)) -> a__U61(a__isNat(z0), z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U71(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0), cons(z1, z2)) -> a__U91(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0, z1)) -> a__U41(mark(z0), z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0, z1, z2)) -> a__U71(mark(z0), z1, z2) mark(U72(z0, z1)) -> a__U72(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(length(z0)) -> a__length(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2, z3)) -> a__U91(mark(z0), z1, z2, z3) mark(U92(z0, z1, z2, z3)) -> a__U92(mark(z0), z1, z2, z3) mark(U93(z0, z1, z2, z3)) -> a__U93(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) 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__U11(tt) -> c2 A__U11(z0) -> c3 A__U21(tt) -> c4 A__U21(z0) -> c5 A__U31(tt) -> c6 A__U31(z0) -> c7 A__U41(tt, z0) -> c8(A__U42(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U41(z0, z1) -> c9 A__U42(tt) -> c10 A__U42(z0) -> c11 A__U51(tt, z0) -> c12(A__U52(a__isNatList(z0)), A__ISNATLIST(z0)) A__U51(z0, z1) -> c13 A__U52(tt) -> c14 A__U52(z0) -> c15 A__U61(tt, z0) -> c16(A__U62(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U61(z0, z1) -> c17 A__U62(tt) -> c18 A__U62(z0) -> c19 A__U71(tt, z0, z1) -> c20(A__U72(a__isNat(z1), z0), A__ISNAT(z1)) A__U71(z0, z1, z2) -> c21 A__U72(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U72(z0, z1) -> c23 A__U81(tt) -> c24 A__U81(z0) -> c25 A__U91(tt, z0, z1, z2) -> c26(A__U92(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U91(z0, z1, z2, z3) -> c27 A__U92(tt, z0, z1, z2) -> c28(A__U93(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U92(z0, z1, z2, z3) -> c29 A__U93(tt, z0, z1, z2) -> c30(MARK(z2)) A__U93(z0, z1, z2, z3) -> c31 A__ISNAT(0) -> c32 A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)), A__ISNAT(z0)) A__ISNAT(z0) -> c35 A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNATILIST(zeros) -> c37 A__ISNATILIST(cons(z0, z1)) -> c38(A__U41(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATILIST(z0) -> c39 A__ISNATLIST(nil) -> c40 A__ISNATLIST(cons(z0, z1)) -> c41(A__U51(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(take(z0, z1)) -> c42(A__U61(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(z0) -> c43 A__LENGTH(nil) -> c44 A__LENGTH(cons(z0, z1)) -> c45(A__U71(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c46 A__TAKE(0, z0) -> c47(A__U81(a__isNatIList(z0)), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c48(A__U91(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c49 MARK(zeros) -> c50(A__ZEROS) MARK(U11(z0)) -> c51(A__U11(mark(z0)), MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)), MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)), MARK(z0)) MARK(U41(z0, z1)) -> c54(A__U41(mark(z0), z1), MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(U51(z0, z1)) -> c57(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(U61(z0, z1)) -> c60(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0, z1, z2)) -> c62(A__U71(mark(z0), z1, z2), MARK(z0)) MARK(U72(z0, z1)) -> c63(A__U72(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2, z3)) -> c67(A__U91(mark(z0), z1, z2, z3), MARK(z0)) MARK(U92(z0, z1, z2, z3)) -> c68(A__U92(mark(z0), z1, z2, z3), MARK(z0)) MARK(U93(z0, z1, z2, z3)) -> c69(A__U93(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c70(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c71(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c72(MARK(z0)) MARK(0) -> c73 MARK(tt) -> c74 MARK(s(z0)) -> c75(MARK(z0)) MARK(nil) -> c76 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U11(tt) -> tt a__U11(z0) -> U11(z0) a__U21(tt) -> tt a__U21(z0) -> U21(z0) a__U31(tt) -> tt a__U31(z0) -> U31(z0) a__U41(tt, z0) -> a__U42(a__isNatIList(z0)) a__U41(z0, z1) -> U41(z0, z1) a__U42(tt) -> tt a__U42(z0) -> U42(z0) a__U51(tt, z0) -> a__U52(a__isNatList(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIList(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt, z0, z1) -> a__U72(a__isNat(z1), z0) a__U71(z0, z1, z2) -> U71(z0, z1, z2) a__U72(tt, z0) -> s(a__length(mark(z0))) a__U72(z0, z1) -> U72(z0, z1) a__U81(tt) -> nil a__U81(z0) -> U81(z0) a__U91(tt, z0, z1, z2) -> a__U92(a__isNat(z1), z0, z1, z2) a__U91(z0, z1, z2, z3) -> U91(z0, z1, z2, z3) a__U92(tt, z0, z1, z2) -> a__U93(a__isNat(z2), z0, z1, z2) a__U92(z0, z1, z2, z3) -> U92(z0, z1, z2, z3) a__U93(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U93(z0, z1, z2, z3) -> U93(z0, z1, z2, z3) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNat(z0), z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U51(a__isNat(z0), z1) a__isNatList(take(z0, z1)) -> a__U61(a__isNat(z0), z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U71(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0), cons(z1, z2)) -> a__U91(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0, z1)) -> a__U41(mark(z0), z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0, z1, z2)) -> a__U71(mark(z0), z1, z2) mark(U72(z0, z1)) -> a__U72(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(length(z0)) -> a__length(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2, z3)) -> a__U91(mark(z0), z1, z2, z3) mark(U92(z0, z1, z2, z3)) -> a__U92(mark(z0), z1, z2, z3) mark(U93(z0, z1, z2, z3)) -> a__U93(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) 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(U81(z0)) ->^+ c66(A__U81(mark(z0)), MARK(z0)) gives rise to a decreasing loop by considering the right hand sides subterm at position [1]. The pumping substitution is [z0 / U81(z0)]. 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__U11(tt) -> c2 A__U11(z0) -> c3 A__U21(tt) -> c4 A__U21(z0) -> c5 A__U31(tt) -> c6 A__U31(z0) -> c7 A__U41(tt, z0) -> c8(A__U42(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U41(z0, z1) -> c9 A__U42(tt) -> c10 A__U42(z0) -> c11 A__U51(tt, z0) -> c12(A__U52(a__isNatList(z0)), A__ISNATLIST(z0)) A__U51(z0, z1) -> c13 A__U52(tt) -> c14 A__U52(z0) -> c15 A__U61(tt, z0) -> c16(A__U62(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U61(z0, z1) -> c17 A__U62(tt) -> c18 A__U62(z0) -> c19 A__U71(tt, z0, z1) -> c20(A__U72(a__isNat(z1), z0), A__ISNAT(z1)) A__U71(z0, z1, z2) -> c21 A__U72(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U72(z0, z1) -> c23 A__U81(tt) -> c24 A__U81(z0) -> c25 A__U91(tt, z0, z1, z2) -> c26(A__U92(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U91(z0, z1, z2, z3) -> c27 A__U92(tt, z0, z1, z2) -> c28(A__U93(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U92(z0, z1, z2, z3) -> c29 A__U93(tt, z0, z1, z2) -> c30(MARK(z2)) A__U93(z0, z1, z2, z3) -> c31 A__ISNAT(0) -> c32 A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)), A__ISNAT(z0)) A__ISNAT(z0) -> c35 A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNATILIST(zeros) -> c37 A__ISNATILIST(cons(z0, z1)) -> c38(A__U41(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATILIST(z0) -> c39 A__ISNATLIST(nil) -> c40 A__ISNATLIST(cons(z0, z1)) -> c41(A__U51(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(take(z0, z1)) -> c42(A__U61(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(z0) -> c43 A__LENGTH(nil) -> c44 A__LENGTH(cons(z0, z1)) -> c45(A__U71(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c46 A__TAKE(0, z0) -> c47(A__U81(a__isNatIList(z0)), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c48(A__U91(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c49 MARK(zeros) -> c50(A__ZEROS) MARK(U11(z0)) -> c51(A__U11(mark(z0)), MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)), MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)), MARK(z0)) MARK(U41(z0, z1)) -> c54(A__U41(mark(z0), z1), MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(U51(z0, z1)) -> c57(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(U61(z0, z1)) -> c60(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0, z1, z2)) -> c62(A__U71(mark(z0), z1, z2), MARK(z0)) MARK(U72(z0, z1)) -> c63(A__U72(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2, z3)) -> c67(A__U91(mark(z0), z1, z2, z3), MARK(z0)) MARK(U92(z0, z1, z2, z3)) -> c68(A__U92(mark(z0), z1, z2, z3), MARK(z0)) MARK(U93(z0, z1, z2, z3)) -> c69(A__U93(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c70(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c71(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c72(MARK(z0)) MARK(0) -> c73 MARK(tt) -> c74 MARK(s(z0)) -> c75(MARK(z0)) MARK(nil) -> c76 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U11(tt) -> tt a__U11(z0) -> U11(z0) a__U21(tt) -> tt a__U21(z0) -> U21(z0) a__U31(tt) -> tt a__U31(z0) -> U31(z0) a__U41(tt, z0) -> a__U42(a__isNatIList(z0)) a__U41(z0, z1) -> U41(z0, z1) a__U42(tt) -> tt a__U42(z0) -> U42(z0) a__U51(tt, z0) -> a__U52(a__isNatList(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIList(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt, z0, z1) -> a__U72(a__isNat(z1), z0) a__U71(z0, z1, z2) -> U71(z0, z1, z2) a__U72(tt, z0) -> s(a__length(mark(z0))) a__U72(z0, z1) -> U72(z0, z1) a__U81(tt) -> nil a__U81(z0) -> U81(z0) a__U91(tt, z0, z1, z2) -> a__U92(a__isNat(z1), z0, z1, z2) a__U91(z0, z1, z2, z3) -> U91(z0, z1, z2, z3) a__U92(tt, z0, z1, z2) -> a__U93(a__isNat(z2), z0, z1, z2) a__U92(z0, z1, z2, z3) -> U92(z0, z1, z2, z3) a__U93(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U93(z0, z1, z2, z3) -> U93(z0, z1, z2, z3) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNat(z0), z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U51(a__isNat(z0), z1) a__isNatList(take(z0, z1)) -> a__U61(a__isNat(z0), z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U71(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0), cons(z1, z2)) -> a__U91(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0, z1)) -> a__U41(mark(z0), z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0, z1, z2)) -> a__U71(mark(z0), z1, z2) mark(U72(z0, z1)) -> a__U72(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(length(z0)) -> a__length(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2, z3)) -> a__U91(mark(z0), z1, z2, z3) mark(U92(z0, z1, z2, z3)) -> a__U92(mark(z0), z1, z2, z3) mark(U93(z0, z1, z2, z3)) -> a__U93(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) 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__U11(tt) -> c2 A__U11(z0) -> c3 A__U21(tt) -> c4 A__U21(z0) -> c5 A__U31(tt) -> c6 A__U31(z0) -> c7 A__U41(tt, z0) -> c8(A__U42(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U41(z0, z1) -> c9 A__U42(tt) -> c10 A__U42(z0) -> c11 A__U51(tt, z0) -> c12(A__U52(a__isNatList(z0)), A__ISNATLIST(z0)) A__U51(z0, z1) -> c13 A__U52(tt) -> c14 A__U52(z0) -> c15 A__U61(tt, z0) -> c16(A__U62(a__isNatIList(z0)), A__ISNATILIST(z0)) A__U61(z0, z1) -> c17 A__U62(tt) -> c18 A__U62(z0) -> c19 A__U71(tt, z0, z1) -> c20(A__U72(a__isNat(z1), z0), A__ISNAT(z1)) A__U71(z0, z1, z2) -> c21 A__U72(tt, z0) -> c22(A__LENGTH(mark(z0)), MARK(z0)) A__U72(z0, z1) -> c23 A__U81(tt) -> c24 A__U81(z0) -> c25 A__U91(tt, z0, z1, z2) -> c26(A__U92(a__isNat(z1), z0, z1, z2), A__ISNAT(z1)) A__U91(z0, z1, z2, z3) -> c27 A__U92(tt, z0, z1, z2) -> c28(A__U93(a__isNat(z2), z0, z1, z2), A__ISNAT(z2)) A__U92(z0, z1, z2, z3) -> c29 A__U93(tt, z0, z1, z2) -> c30(MARK(z2)) A__U93(z0, z1, z2, z3) -> c31 A__ISNAT(0) -> c32 A__ISNAT(length(z0)) -> c33(A__U11(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c34(A__U21(a__isNat(z0)), A__ISNAT(z0)) A__ISNAT(z0) -> c35 A__ISNATILIST(z0) -> c36(A__U31(a__isNatList(z0)), A__ISNATLIST(z0)) A__ISNATILIST(zeros) -> c37 A__ISNATILIST(cons(z0, z1)) -> c38(A__U41(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATILIST(z0) -> c39 A__ISNATLIST(nil) -> c40 A__ISNATLIST(cons(z0, z1)) -> c41(A__U51(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(take(z0, z1)) -> c42(A__U61(a__isNat(z0), z1), A__ISNAT(z0)) A__ISNATLIST(z0) -> c43 A__LENGTH(nil) -> c44 A__LENGTH(cons(z0, z1)) -> c45(A__U71(a__isNatList(z1), z1, z0), A__ISNATLIST(z1)) A__LENGTH(z0) -> c46 A__TAKE(0, z0) -> c47(A__U81(a__isNatIList(z0)), A__ISNATILIST(z0)) A__TAKE(s(z0), cons(z1, z2)) -> c48(A__U91(a__isNatIList(z2), z2, z0, z1), A__ISNATILIST(z2)) A__TAKE(z0, z1) -> c49 MARK(zeros) -> c50(A__ZEROS) MARK(U11(z0)) -> c51(A__U11(mark(z0)), MARK(z0)) MARK(U21(z0)) -> c52(A__U21(mark(z0)), MARK(z0)) MARK(U31(z0)) -> c53(A__U31(mark(z0)), MARK(z0)) MARK(U41(z0, z1)) -> c54(A__U41(mark(z0), z1), MARK(z0)) MARK(U42(z0)) -> c55(A__U42(mark(z0)), MARK(z0)) MARK(isNatIList(z0)) -> c56(A__ISNATILIST(z0)) MARK(U51(z0, z1)) -> c57(A__U51(mark(z0), z1), MARK(z0)) MARK(U52(z0)) -> c58(A__U52(mark(z0)), MARK(z0)) MARK(isNatList(z0)) -> c59(A__ISNATLIST(z0)) MARK(U61(z0, z1)) -> c60(A__U61(mark(z0), z1), MARK(z0)) MARK(U62(z0)) -> c61(A__U62(mark(z0)), MARK(z0)) MARK(U71(z0, z1, z2)) -> c62(A__U71(mark(z0), z1, z2), MARK(z0)) MARK(U72(z0, z1)) -> c63(A__U72(mark(z0), z1), MARK(z0)) MARK(isNat(z0)) -> c64(A__ISNAT(z0)) MARK(length(z0)) -> c65(A__LENGTH(mark(z0)), MARK(z0)) MARK(U81(z0)) -> c66(A__U81(mark(z0)), MARK(z0)) MARK(U91(z0, z1, z2, z3)) -> c67(A__U91(mark(z0), z1, z2, z3), MARK(z0)) MARK(U92(z0, z1, z2, z3)) -> c68(A__U92(mark(z0), z1, z2, z3), MARK(z0)) MARK(U93(z0, z1, z2, z3)) -> c69(A__U93(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c70(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c71(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c72(MARK(z0)) MARK(0) -> c73 MARK(tt) -> c74 MARK(s(z0)) -> c75(MARK(z0)) MARK(nil) -> c76 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U11(tt) -> tt a__U11(z0) -> U11(z0) a__U21(tt) -> tt a__U21(z0) -> U21(z0) a__U31(tt) -> tt a__U31(z0) -> U31(z0) a__U41(tt, z0) -> a__U42(a__isNatIList(z0)) a__U41(z0, z1) -> U41(z0, z1) a__U42(tt) -> tt a__U42(z0) -> U42(z0) a__U51(tt, z0) -> a__U52(a__isNatList(z0)) a__U51(z0, z1) -> U51(z0, z1) a__U52(tt) -> tt a__U52(z0) -> U52(z0) a__U61(tt, z0) -> a__U62(a__isNatIList(z0)) a__U61(z0, z1) -> U61(z0, z1) a__U62(tt) -> tt a__U62(z0) -> U62(z0) a__U71(tt, z0, z1) -> a__U72(a__isNat(z1), z0) a__U71(z0, z1, z2) -> U71(z0, z1, z2) a__U72(tt, z0) -> s(a__length(mark(z0))) a__U72(z0, z1) -> U72(z0, z1) a__U81(tt) -> nil a__U81(z0) -> U81(z0) a__U91(tt, z0, z1, z2) -> a__U92(a__isNat(z1), z0, z1, z2) a__U91(z0, z1, z2, z3) -> U91(z0, z1, z2, z3) a__U92(tt, z0, z1, z2) -> a__U93(a__isNat(z2), z0, z1, z2) a__U92(z0, z1, z2, z3) -> U92(z0, z1, z2, z3) a__U93(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U93(z0, z1, z2, z3) -> U93(z0, z1, z2, z3) a__isNat(0) -> tt a__isNat(length(z0)) -> a__U11(a__isNatList(z0)) a__isNat(s(z0)) -> a__U21(a__isNat(z0)) a__isNat(z0) -> isNat(z0) a__isNatIList(z0) -> a__U31(a__isNatList(z0)) a__isNatIList(zeros) -> tt a__isNatIList(cons(z0, z1)) -> a__U41(a__isNat(z0), z1) a__isNatIList(z0) -> isNatIList(z0) a__isNatList(nil) -> tt a__isNatList(cons(z0, z1)) -> a__U51(a__isNat(z0), z1) a__isNatList(take(z0, z1)) -> a__U61(a__isNat(z0), z1) a__isNatList(z0) -> isNatList(z0) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U71(a__isNatList(z1), z1, z0) a__length(z0) -> length(z0) a__take(0, z0) -> a__U81(a__isNatIList(z0)) a__take(s(z0), cons(z1, z2)) -> a__U91(a__isNatIList(z2), z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0)) -> a__U11(mark(z0)) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0)) -> a__U31(mark(z0)) mark(U41(z0, z1)) -> a__U41(mark(z0), z1) mark(U42(z0)) -> a__U42(mark(z0)) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(U51(z0, z1)) -> a__U51(mark(z0), z1) mark(U52(z0)) -> a__U52(mark(z0)) mark(isNatList(z0)) -> a__isNatList(z0) mark(U61(z0, z1)) -> a__U61(mark(z0), z1) mark(U62(z0)) -> a__U62(mark(z0)) mark(U71(z0, z1, z2)) -> a__U71(mark(z0), z1, z2) mark(U72(z0, z1)) -> a__U72(mark(z0), z1) mark(isNat(z0)) -> a__isNat(z0) mark(length(z0)) -> a__length(mark(z0)) mark(U81(z0)) -> a__U81(mark(z0)) mark(U91(z0, z1, z2, z3)) -> a__U91(mark(z0), z1, z2, z3) mark(U92(z0, z1, z2, z3)) -> a__U92(mark(z0), z1, z2, z3) mark(U93(z0, z1, z2, z3)) -> a__U93(mark(z0), z1, z2, z3) mark(take(z0, z1)) -> a__take(mark(z0), mark(z1)) 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