WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox/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) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxRelTRS (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) typed CpxTrs (5) OrderProof [LOWER BOUND(ID), 19 ms] (6) typed CpxTrs (7) RewriteLemmaProof [LOWER BOUND(ID), 31.7 s] (8) typed CpxTrs (9) RewriteLemmaProof [LOWER BOUND(ID), 44.4 s] (10) BEST (11) proven lower bound (12) LowerBoundPropagationProof [FINISHED, 0 ms] (13) BOUNDS(n^1, INF) (14) typed CpxTrs ---------------------------------------- (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, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0, z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0) -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 The (relative) TRS S consists of the following rules: a__zeros -> cons(0, zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0 a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0, z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (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, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0', z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0') -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 The (relative) TRS S consists of the following rules: a__zeros -> cons(0', zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0' a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0', z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Innermost TRS: Rules: A__ZEROS -> c A__ZEROS -> c1 A__U11(tt, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0', z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0') -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 a__zeros -> cons(0', zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0' a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0', z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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 Types: A__ZEROS :: c:c1 c :: c:c1 c1 :: c:c1 A__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c2:c3 tt :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c2 :: c4:c5 -> c2:c3 A__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c4:c5 c3 :: c2:c3 c4 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c4:c5 A__LENGTH :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c12:c13:c14 mark :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take MARK :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c5 :: c4:c5 A__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c6:c7 c6 :: c8:c9 -> c6:c7 A__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c8:c9 c7 :: c6:c7 c8 :: c10:c11 -> c8:c9 A__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c10:c11 c9 :: c8:c9 c10 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c10:c11 c11 :: c10:c11 nil :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c12 :: c12:c13:c14 cons :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c13 :: c2:c3 -> c12:c13:c14 c14 :: c12:c13:c14 A__TAKE :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c15:c16:c17 0' :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c15 :: c15:c16:c17 s :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c16 :: c6:c7 -> c15:c16:c17 c17 :: c15:c16:c17 zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c18 :: c:c1 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c19 :: c2:c3 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c20 :: c4:c5 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c21 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c22 :: c6:c7 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c23 :: c8:c9 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c24 :: c10:c11 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c25 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c26 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 a__zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c:c11_32 :: c:c1 hole_c2:c32_32 :: c2:c3 hole_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take3_32 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c4:c54_32 :: c4:c5 hole_c12:c13:c145_32 :: c12:c13:c14 hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c316_32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 hole_c6:c77_32 :: c6:c7 hole_c8:c98_32 :: c8:c9 hole_c10:c119_32 :: c10:c11 hole_c15:c16:c1710_32 :: c15:c16:c17 gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32 :: Nat -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32 :: Nat -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 ---------------------------------------- (5) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: A__U11, A__U12, A__LENGTH, mark, MARK, A__U21, A__U22, A__U23, a__U11, a__U12, a__length, a__U21, a__U22, a__U23 They will be analysed ascendingly in the following order: A__U11 = A__U12 A__U11 = A__LENGTH A__U11 = MARK A__U11 = A__U21 A__U11 = A__U22 A__U11 = A__U23 A__U12 = A__LENGTH mark < A__U12 A__U12 = MARK A__U12 = A__U21 A__U12 = A__U22 A__U12 = A__U23 A__LENGTH = MARK A__LENGTH = A__U21 A__LENGTH = A__U22 A__LENGTH = A__U23 mark < MARK mark = a__U11 mark = a__U12 mark = a__length mark = a__U21 mark = a__U22 mark = a__U23 MARK = A__U21 MARK = A__U22 MARK = A__U23 A__U21 = A__U22 A__U21 = A__U23 A__U22 = A__U23 a__U11 = a__U12 a__U11 = a__length a__U11 = a__U21 a__U11 = a__U22 a__U11 = a__U23 a__U12 = a__length a__U12 = a__U21 a__U12 = a__U22 a__U12 = a__U23 a__length = a__U21 a__length = a__U22 a__length = a__U23 a__U21 = a__U22 a__U21 = a__U23 a__U22 = a__U23 ---------------------------------------- (6) Obligation: Innermost TRS: Rules: A__ZEROS -> c A__ZEROS -> c1 A__U11(tt, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0', z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0') -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 a__zeros -> cons(0', zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0' a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0', z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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 Types: A__ZEROS :: c:c1 c :: c:c1 c1 :: c:c1 A__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c2:c3 tt :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c2 :: c4:c5 -> c2:c3 A__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c4:c5 c3 :: c2:c3 c4 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c4:c5 A__LENGTH :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c12:c13:c14 mark :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take MARK :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c5 :: c4:c5 A__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c6:c7 c6 :: c8:c9 -> c6:c7 A__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c8:c9 c7 :: c6:c7 c8 :: c10:c11 -> c8:c9 A__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c10:c11 c9 :: c8:c9 c10 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c10:c11 c11 :: c10:c11 nil :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c12 :: c12:c13:c14 cons :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c13 :: c2:c3 -> c12:c13:c14 c14 :: c12:c13:c14 A__TAKE :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c15:c16:c17 0' :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c15 :: c15:c16:c17 s :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c16 :: c6:c7 -> c15:c16:c17 c17 :: c15:c16:c17 zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c18 :: c:c1 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c19 :: c2:c3 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c20 :: c4:c5 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c21 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c22 :: c6:c7 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c23 :: c8:c9 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c24 :: c10:c11 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c25 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c26 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 a__zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c:c11_32 :: c:c1 hole_c2:c32_32 :: c2:c3 hole_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take3_32 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c4:c54_32 :: c4:c5 hole_c12:c13:c145_32 :: c12:c13:c14 hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c316_32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 hole_c6:c77_32 :: c6:c7 hole_c8:c98_32 :: c8:c9 hole_c10:c119_32 :: c10:c11 hole_c15:c16:c1710_32 :: c15:c16:c17 gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32 :: Nat -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32 :: Nat -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 Generator Equations: gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(0) <=> tt gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(x, 1)) <=> cons(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(x), tt) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(0) <=> c18(c) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(+(x, 1)) <=> c19(c2(c4(c12, c18(c))), gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(x)) The following defined symbols remain to be analysed: a__U11, A__U11, A__U12, A__LENGTH, mark, MARK, A__U21, A__U22, A__U23, a__U12, a__length, a__U21, a__U22, a__U23 They will be analysed ascendingly in the following order: A__U11 = A__U12 A__U11 = A__LENGTH A__U11 = MARK A__U11 = A__U21 A__U11 = A__U22 A__U11 = A__U23 A__U12 = A__LENGTH mark < A__U12 A__U12 = MARK A__U12 = A__U21 A__U12 = A__U22 A__U12 = A__U23 A__LENGTH = MARK A__LENGTH = A__U21 A__LENGTH = A__U22 A__LENGTH = A__U23 mark < MARK mark = a__U11 mark = a__U12 mark = a__length mark = a__U21 mark = a__U22 mark = a__U23 MARK = A__U21 MARK = A__U22 MARK = A__U23 A__U21 = A__U22 A__U21 = A__U23 A__U22 = A__U23 a__U11 = a__U12 a__U11 = a__length a__U11 = a__U21 a__U11 = a__U22 a__U11 = a__U23 a__U12 = a__length a__U12 = a__U21 a__U12 = a__U22 a__U12 = a__U23 a__length = a__U21 a__length = a__U22 a__length = a__U23 a__U21 = a__U22 a__U21 = a__U23 a__U22 = a__U23 ---------------------------------------- (7) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32)) -> gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32), rt in Omega(0) Induction Base: mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(0)) ->_R^Omega(0) tt Induction Step: mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(n2246130_32, 1))) ->_R^Omega(0) cons(mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32)), tt) ->_IH cons(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(c2246131_32), tt) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (8) Obligation: Innermost TRS: Rules: A__ZEROS -> c A__ZEROS -> c1 A__U11(tt, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0', z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0') -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 a__zeros -> cons(0', zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0' a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0', z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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 Types: A__ZEROS :: c:c1 c :: c:c1 c1 :: c:c1 A__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c2:c3 tt :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c2 :: c4:c5 -> c2:c3 A__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c4:c5 c3 :: c2:c3 c4 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c4:c5 A__LENGTH :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c12:c13:c14 mark :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take MARK :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c5 :: c4:c5 A__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c6:c7 c6 :: c8:c9 -> c6:c7 A__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c8:c9 c7 :: c6:c7 c8 :: c10:c11 -> c8:c9 A__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c10:c11 c9 :: c8:c9 c10 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c10:c11 c11 :: c10:c11 nil :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c12 :: c12:c13:c14 cons :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c13 :: c2:c3 -> c12:c13:c14 c14 :: c12:c13:c14 A__TAKE :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c15:c16:c17 0' :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c15 :: c15:c16:c17 s :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c16 :: c6:c7 -> c15:c16:c17 c17 :: c15:c16:c17 zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c18 :: c:c1 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c19 :: c2:c3 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c20 :: c4:c5 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c21 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c22 :: c6:c7 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c23 :: c8:c9 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c24 :: c10:c11 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c25 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c26 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 a__zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c:c11_32 :: c:c1 hole_c2:c32_32 :: c2:c3 hole_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take3_32 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c4:c54_32 :: c4:c5 hole_c12:c13:c145_32 :: c12:c13:c14 hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c316_32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 hole_c6:c77_32 :: c6:c7 hole_c8:c98_32 :: c8:c9 hole_c10:c119_32 :: c10:c11 hole_c15:c16:c1710_32 :: c15:c16:c17 gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32 :: Nat -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32 :: Nat -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 Lemmas: mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32)) -> gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32), rt in Omega(0) Generator Equations: gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(0) <=> tt gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(x, 1)) <=> cons(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(x), tt) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(0) <=> c18(c) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(+(x, 1)) <=> c19(c2(c4(c12, c18(c))), gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(x)) The following defined symbols remain to be analysed: a__U21, A__U11, A__U12, A__LENGTH, MARK, A__U21, A__U22, A__U23, a__U11, a__U12, a__length, a__U22, a__U23 They will be analysed ascendingly in the following order: A__U11 = A__U12 A__U11 = A__LENGTH A__U11 = MARK A__U11 = A__U21 A__U11 = A__U22 A__U11 = A__U23 A__U12 = A__LENGTH mark < A__U12 A__U12 = MARK A__U12 = A__U21 A__U12 = A__U22 A__U12 = A__U23 A__LENGTH = MARK A__LENGTH = A__U21 A__LENGTH = A__U22 A__LENGTH = A__U23 mark < MARK mark = a__U11 mark = a__U12 mark = a__length mark = a__U21 mark = a__U22 mark = a__U23 MARK = A__U21 MARK = A__U22 MARK = A__U23 A__U21 = A__U22 A__U21 = A__U23 A__U22 = A__U23 a__U11 = a__U12 a__U11 = a__length a__U11 = a__U21 a__U11 = a__U22 a__U11 = a__U23 a__U12 = a__length a__U12 = a__U21 a__U12 = a__U22 a__U12 = a__U23 a__length = a__U21 a__length = a__U22 a__length = a__U23 a__U21 = a__U22 a__U21 = a__U23 a__U22 = a__U23 ---------------------------------------- (9) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MARK(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(1, n4472469_32))) -> *13_32, rt in Omega(n4472469_32) Induction Base: MARK(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(1, 0))) Induction Step: MARK(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(1, +(n4472469_32, 1)))) ->_R^Omega(1) c27(MARK(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(1, n4472469_32)))) ->_IH c27(*13_32) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (10) Complex Obligation (BEST) ---------------------------------------- (11) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: A__ZEROS -> c A__ZEROS -> c1 A__U11(tt, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0', z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0') -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 a__zeros -> cons(0', zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0' a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0', z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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 Types: A__ZEROS :: c:c1 c :: c:c1 c1 :: c:c1 A__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c2:c3 tt :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c2 :: c4:c5 -> c2:c3 A__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c4:c5 c3 :: c2:c3 c4 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c4:c5 A__LENGTH :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c12:c13:c14 mark :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take MARK :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c5 :: c4:c5 A__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c6:c7 c6 :: c8:c9 -> c6:c7 A__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c8:c9 c7 :: c6:c7 c8 :: c10:c11 -> c8:c9 A__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c10:c11 c9 :: c8:c9 c10 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c10:c11 c11 :: c10:c11 nil :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c12 :: c12:c13:c14 cons :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c13 :: c2:c3 -> c12:c13:c14 c14 :: c12:c13:c14 A__TAKE :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c15:c16:c17 0' :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c15 :: c15:c16:c17 s :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c16 :: c6:c7 -> c15:c16:c17 c17 :: c15:c16:c17 zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c18 :: c:c1 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c19 :: c2:c3 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c20 :: c4:c5 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c21 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c22 :: c6:c7 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c23 :: c8:c9 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c24 :: c10:c11 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c25 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c26 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 a__zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c:c11_32 :: c:c1 hole_c2:c32_32 :: c2:c3 hole_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take3_32 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c4:c54_32 :: c4:c5 hole_c12:c13:c145_32 :: c12:c13:c14 hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c316_32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 hole_c6:c77_32 :: c6:c7 hole_c8:c98_32 :: c8:c9 hole_c10:c119_32 :: c10:c11 hole_c15:c16:c1710_32 :: c15:c16:c17 gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32 :: Nat -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32 :: Nat -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 Lemmas: mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32)) -> gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32), rt in Omega(0) Generator Equations: gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(0) <=> tt gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(x, 1)) <=> cons(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(x), tt) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(0) <=> c18(c) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(+(x, 1)) <=> c19(c2(c4(c12, c18(c))), gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(x)) The following defined symbols remain to be analysed: MARK, A__U21, A__U22, A__U23 They will be analysed ascendingly in the following order: A__U11 = A__U12 A__U11 = A__LENGTH A__U11 = MARK A__U11 = A__U21 A__U11 = A__U22 A__U11 = A__U23 A__U12 = A__LENGTH A__U12 = MARK A__U12 = A__U21 A__U12 = A__U22 A__U12 = A__U23 A__LENGTH = MARK A__LENGTH = A__U21 A__LENGTH = A__U22 A__LENGTH = A__U23 MARK = A__U21 MARK = A__U22 MARK = A__U23 A__U21 = A__U22 A__U21 = A__U23 A__U22 = A__U23 ---------------------------------------- (12) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (13) BOUNDS(n^1, INF) ---------------------------------------- (14) Obligation: Innermost TRS: Rules: A__ZEROS -> c A__ZEROS -> c1 A__U11(tt, z0) -> c2(A__U12(tt, z0)) A__U11(z0, z1) -> c3 A__U12(tt, z0) -> c4(A__LENGTH(mark(z0)), MARK(z0)) A__U12(z0, z1) -> c5 A__U21(tt, z0, z1, z2) -> c6(A__U22(tt, z0, z1, z2)) A__U21(z0, z1, z2, z3) -> c7 A__U22(tt, z0, z1, z2) -> c8(A__U23(tt, z0, z1, z2)) A__U22(z0, z1, z2, z3) -> c9 A__U23(tt, z0, z1, z2) -> c10(MARK(z2)) A__U23(z0, z1, z2, z3) -> c11 A__LENGTH(nil) -> c12 A__LENGTH(cons(z0, z1)) -> c13(A__U11(tt, z1)) A__LENGTH(z0) -> c14 A__TAKE(0', z0) -> c15 A__TAKE(s(z0), cons(z1, z2)) -> c16(A__U21(tt, z2, z0, z1)) A__TAKE(z0, z1) -> c17 MARK(zeros) -> c18(A__ZEROS) MARK(U11(z0, z1)) -> c19(A__U11(mark(z0), z1), MARK(z0)) MARK(U12(z0, z1)) -> c20(A__U12(mark(z0), z1), MARK(z0)) MARK(length(z0)) -> c21(A__LENGTH(mark(z0)), MARK(z0)) MARK(U21(z0, z1, z2, z3)) -> c22(A__U21(mark(z0), z1, z2, z3), MARK(z0)) MARK(U22(z0, z1, z2, z3)) -> c23(A__U22(mark(z0), z1, z2, z3), MARK(z0)) MARK(U23(z0, z1, z2, z3)) -> c24(A__U23(mark(z0), z1, z2, z3), MARK(z0)) MARK(take(z0, z1)) -> c25(A__TAKE(mark(z0), mark(z1)), MARK(z0)) MARK(take(z0, z1)) -> c26(A__TAKE(mark(z0), mark(z1)), MARK(z1)) MARK(cons(z0, z1)) -> c27(MARK(z0)) MARK(0') -> c28 MARK(tt) -> c29 MARK(s(z0)) -> c30(MARK(z0)) MARK(nil) -> c31 a__zeros -> cons(0', zeros) a__zeros -> zeros a__U11(tt, z0) -> a__U12(tt, z0) a__U11(z0, z1) -> U11(z0, z1) a__U12(tt, z0) -> s(a__length(mark(z0))) a__U12(z0, z1) -> U12(z0, z1) a__U21(tt, z0, z1, z2) -> a__U22(tt, z0, z1, z2) a__U21(z0, z1, z2, z3) -> U21(z0, z1, z2, z3) a__U22(tt, z0, z1, z2) -> a__U23(tt, z0, z1, z2) a__U22(z0, z1, z2, z3) -> U22(z0, z1, z2, z3) a__U23(tt, z0, z1, z2) -> cons(mark(z2), take(z1, z0)) a__U23(z0, z1, z2, z3) -> U23(z0, z1, z2, z3) a__length(nil) -> 0' a__length(cons(z0, z1)) -> a__U11(tt, z1) a__length(z0) -> length(z0) a__take(0', z0) -> nil a__take(s(z0), cons(z1, z2)) -> a__U21(tt, z2, z0, z1) a__take(z0, z1) -> take(z0, z1) mark(zeros) -> a__zeros mark(U11(z0, z1)) -> a__U11(mark(z0), z1) mark(U12(z0, z1)) -> a__U12(mark(z0), z1) mark(length(z0)) -> a__length(mark(z0)) mark(U21(z0, z1, z2, z3)) -> a__U21(mark(z0), z1, z2, z3) mark(U22(z0, z1, z2, z3)) -> a__U22(mark(z0), z1, z2, z3) mark(U23(z0, z1, z2, z3)) -> a__U23(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 Types: A__ZEROS :: c:c1 c :: c:c1 c1 :: c:c1 A__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c2:c3 tt :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c2 :: c4:c5 -> c2:c3 A__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c4:c5 c3 :: c2:c3 c4 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c4:c5 A__LENGTH :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c12:c13:c14 mark :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take MARK :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c5 :: c4:c5 A__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c6:c7 c6 :: c8:c9 -> c6:c7 A__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c8:c9 c7 :: c6:c7 c8 :: c10:c11 -> c8:c9 A__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c10:c11 c9 :: c8:c9 c10 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c10:c11 c11 :: c10:c11 nil :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c12 :: c12:c13:c14 cons :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c13 :: c2:c3 -> c12:c13:c14 c14 :: c12:c13:c14 A__TAKE :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> c15:c16:c17 0' :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c15 :: c15:c16:c17 s :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c16 :: c6:c7 -> c15:c16:c17 c17 :: c15:c16:c17 zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c18 :: c:c1 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c19 :: c2:c3 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c20 :: c4:c5 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c21 :: c12:c13:c14 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c22 :: c6:c7 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c23 :: c8:c9 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c24 :: c10:c11 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take c25 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c26 :: c15:c16:c17 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c27 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c28 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c29 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c30 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 c31 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 a__zeros :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U11 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U12 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__length :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U21 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U22 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__U23 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take a__take :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c:c11_32 :: c:c1 hole_c2:c32_32 :: c2:c3 hole_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take3_32 :: tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take hole_c4:c54_32 :: c4:c5 hole_c12:c13:c145_32 :: c12:c13:c14 hole_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c316_32 :: c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 hole_c6:c77_32 :: c6:c7 hole_c8:c98_32 :: c8:c9 hole_c10:c119_32 :: c10:c11 hole_c15:c16:c1710_32 :: c15:c16:c17 gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32 :: Nat -> tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32 :: Nat -> c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31 Lemmas: mark(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32)) -> gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(n2246130_32), rt in Omega(0) MARK(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(1, n4472469_32))) -> *13_32, rt in Omega(n4472469_32) Generator Equations: gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(0) <=> tt gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(+(x, 1)) <=> cons(gen_tt:nil:cons:0':s:zeros:U11:U12:length:U21:U22:U23:take11_32(x), tt) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(0) <=> c18(c) gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(+(x, 1)) <=> c19(c2(c4(c12, c18(c))), gen_c18:c19:c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c3112_32(x)) The following defined symbols remain to be analysed: A__U21, A__U11, A__U12, A__LENGTH, A__U22, A__U23 They will be analysed ascendingly in the following order: A__U11 = A__U12 A__U11 = A__LENGTH A__U11 = MARK A__U11 = A__U21 A__U11 = A__U22 A__U11 = A__U23 A__U12 = A__LENGTH A__U12 = MARK A__U12 = A__U21 A__U12 = A__U22 A__U12 = A__U23 A__LENGTH = MARK A__LENGTH = A__U21 A__LENGTH = A__U22 A__LENGTH = A__U23 MARK = A__U21 MARK = A__U22 MARK = A__U23 A__U21 = A__U22 A__U21 = A__U23 A__U22 = A__U23