WORST_CASE(Omega(n^1),O(n^1)) proof of input_hRFEgjwDYF.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). (0) CpxTRS (1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (2) CpxTRS (3) CpxTrsMatchBoundsTAProof [FINISHED, 71 ms] (4) BOUNDS(1, n^1) (5) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxRelTRS (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) typed CpxTrs (13) OrderProof [LOWER BOUND(ID), 11 ms] (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 291 ms] (16) BEST (17) proven lower bound (18) LowerBoundPropagationProof [FINISHED, 0 ms] (19) BOUNDS(n^1, INF) (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 87 ms] (22) typed CpxTrs (23) RewriteLemmaProof [LOWER BOUND(ID), 263 ms] (24) typed CpxTrs (25) RewriteLemmaProof [LOWER BOUND(ID), 0 ms] (26) BOUNDS(1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1). The TRS R consists of the following rules: concat(leaf, Y) -> Y concat(cons(U, V), Y) -> cons(U, concat(V, Y)) lessleaves(X, leaf) -> false lessleaves(leaf, cons(W, Z)) -> true lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: concat(leaf, Y) -> Y concat(cons(U, V), Y) -> cons(U, concat(V, Y)) lessleaves(X, leaf) -> false lessleaves(leaf, cons(W, Z)) -> true lessleaves(cons(U, V), cons(W, Z)) -> lessleaves(concat(U, V), concat(W, Z)) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsMatchBoundsTAProof (FINISHED) A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2. The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: final states : [1, 2] transitions: leaf0() -> 0 cons0(0, 0) -> 0 false0() -> 0 true0() -> 0 concat0(0, 0) -> 1 lessleaves0(0, 0) -> 2 concat1(0, 0) -> 3 cons1(0, 3) -> 1 false1() -> 2 true1() -> 2 concat1(0, 0) -> 4 concat1(0, 0) -> 5 lessleaves1(4, 5) -> 2 cons1(0, 3) -> 3 cons1(0, 3) -> 4 cons1(0, 3) -> 5 concat1(0, 3) -> 5 concat1(0, 3) -> 4 concat2(0, 3) -> 6 concat2(0, 3) -> 7 lessleaves2(6, 7) -> 2 concat1(0, 3) -> 3 0 -> 1 0 -> 3 0 -> 4 0 -> 5 3 -> 4 3 -> 5 3 -> 6 3 -> 7 ---------------------------------------- (4) BOUNDS(1, n^1) ---------------------------------------- (5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Tuples: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) S tuples: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) K tuples:none Defined Rule Symbols: concat_2, lessleaves_2 Defined Pair Symbols: CONCAT_2, LESSLEAVES_2 Compound Symbols: c, c1_1, c2, c3, c4_2, c5_2 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) 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: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) The (relative) TRS S consists of the following rules: concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Rewrite Strategy: INNERMOST ---------------------------------------- (9) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (10) 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: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) The (relative) TRS S consists of the following rules: concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (12) Obligation: Innermost TRS: Rules: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Types: CONCAT :: leaf:cons -> leaf:cons -> c:c1 leaf :: leaf:cons c :: c:c1 cons :: leaf:cons -> leaf:cons -> leaf:cons c1 :: c:c1 -> c:c1 LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 concat :: leaf:cons -> leaf:cons -> leaf:cons c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 lessleaves :: leaf:cons -> leaf:cons -> false:true false :: false:true true :: false:true hole_c:c11_6 :: c:c1 hole_leaf:cons2_6 :: leaf:cons hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5 hole_false:true4_6 :: false:true gen_c:c15_6 :: Nat -> c:c1 gen_leaf:cons6_6 :: Nat -> leaf:cons gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5 ---------------------------------------- (13) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: CONCAT, LESSLEAVES, concat, lessleaves They will be analysed ascendingly in the following order: CONCAT < LESSLEAVES concat < LESSLEAVES concat < lessleaves ---------------------------------------- (14) Obligation: Innermost TRS: Rules: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Types: CONCAT :: leaf:cons -> leaf:cons -> c:c1 leaf :: leaf:cons c :: c:c1 cons :: leaf:cons -> leaf:cons -> leaf:cons c1 :: c:c1 -> c:c1 LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 concat :: leaf:cons -> leaf:cons -> leaf:cons c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 lessleaves :: leaf:cons -> leaf:cons -> false:true false :: false:true true :: false:true hole_c:c11_6 :: c:c1 hole_leaf:cons2_6 :: leaf:cons hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5 hole_false:true4_6 :: false:true gen_c:c15_6 :: Nat -> c:c1 gen_leaf:cons6_6 :: Nat -> leaf:cons gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5 Generator Equations: gen_c:c15_6(0) <=> c gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x)) gen_leaf:cons6_6(0) <=> leaf gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x)) gen_c2:c3:c4:c57_6(0) <=> c2 gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c) The following defined symbols remain to be analysed: CONCAT, LESSLEAVES, concat, lessleaves They will be analysed ascendingly in the following order: CONCAT < LESSLEAVES concat < LESSLEAVES concat < lessleaves ---------------------------------------- (15) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: CONCAT(gen_leaf:cons6_6(n9_6), gen_leaf:cons6_6(b)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6) Induction Base: CONCAT(gen_leaf:cons6_6(0), gen_leaf:cons6_6(b)) ->_R^Omega(1) c Induction Step: CONCAT(gen_leaf:cons6_6(+(n9_6, 1)), gen_leaf:cons6_6(b)) ->_R^Omega(1) c1(CONCAT(gen_leaf:cons6_6(n9_6), gen_leaf:cons6_6(b))) ->_IH c1(gen_c:c15_6(c10_6)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (16) Complex Obligation (BEST) ---------------------------------------- (17) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Types: CONCAT :: leaf:cons -> leaf:cons -> c:c1 leaf :: leaf:cons c :: c:c1 cons :: leaf:cons -> leaf:cons -> leaf:cons c1 :: c:c1 -> c:c1 LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 concat :: leaf:cons -> leaf:cons -> leaf:cons c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 lessleaves :: leaf:cons -> leaf:cons -> false:true false :: false:true true :: false:true hole_c:c11_6 :: c:c1 hole_leaf:cons2_6 :: leaf:cons hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5 hole_false:true4_6 :: false:true gen_c:c15_6 :: Nat -> c:c1 gen_leaf:cons6_6 :: Nat -> leaf:cons gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5 Generator Equations: gen_c:c15_6(0) <=> c gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x)) gen_leaf:cons6_6(0) <=> leaf gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x)) gen_c2:c3:c4:c57_6(0) <=> c2 gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c) The following defined symbols remain to be analysed: CONCAT, LESSLEAVES, concat, lessleaves They will be analysed ascendingly in the following order: CONCAT < LESSLEAVES concat < LESSLEAVES concat < lessleaves ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (20) Obligation: Innermost TRS: Rules: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Types: CONCAT :: leaf:cons -> leaf:cons -> c:c1 leaf :: leaf:cons c :: c:c1 cons :: leaf:cons -> leaf:cons -> leaf:cons c1 :: c:c1 -> c:c1 LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 concat :: leaf:cons -> leaf:cons -> leaf:cons c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 lessleaves :: leaf:cons -> leaf:cons -> false:true false :: false:true true :: false:true hole_c:c11_6 :: c:c1 hole_leaf:cons2_6 :: leaf:cons hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5 hole_false:true4_6 :: false:true gen_c:c15_6 :: Nat -> c:c1 gen_leaf:cons6_6 :: Nat -> leaf:cons gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5 Lemmas: CONCAT(gen_leaf:cons6_6(n9_6), gen_leaf:cons6_6(b)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6) Generator Equations: gen_c:c15_6(0) <=> c gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x)) gen_leaf:cons6_6(0) <=> leaf gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x)) gen_c2:c3:c4:c57_6(0) <=> c2 gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c) The following defined symbols remain to be analysed: concat, LESSLEAVES, lessleaves They will be analysed ascendingly in the following order: concat < LESSLEAVES concat < lessleaves ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: concat(gen_leaf:cons6_6(n403_6), gen_leaf:cons6_6(b)) -> gen_leaf:cons6_6(+(n403_6, b)), rt in Omega(0) Induction Base: concat(gen_leaf:cons6_6(0), gen_leaf:cons6_6(b)) ->_R^Omega(0) gen_leaf:cons6_6(b) Induction Step: concat(gen_leaf:cons6_6(+(n403_6, 1)), gen_leaf:cons6_6(b)) ->_R^Omega(0) cons(leaf, concat(gen_leaf:cons6_6(n403_6), gen_leaf:cons6_6(b))) ->_IH cons(leaf, gen_leaf:cons6_6(+(b, c404_6))) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (22) Obligation: Innermost TRS: Rules: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Types: CONCAT :: leaf:cons -> leaf:cons -> c:c1 leaf :: leaf:cons c :: c:c1 cons :: leaf:cons -> leaf:cons -> leaf:cons c1 :: c:c1 -> c:c1 LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 concat :: leaf:cons -> leaf:cons -> leaf:cons c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 lessleaves :: leaf:cons -> leaf:cons -> false:true false :: false:true true :: false:true hole_c:c11_6 :: c:c1 hole_leaf:cons2_6 :: leaf:cons hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5 hole_false:true4_6 :: false:true gen_c:c15_6 :: Nat -> c:c1 gen_leaf:cons6_6 :: Nat -> leaf:cons gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5 Lemmas: CONCAT(gen_leaf:cons6_6(n9_6), gen_leaf:cons6_6(b)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6) concat(gen_leaf:cons6_6(n403_6), gen_leaf:cons6_6(b)) -> gen_leaf:cons6_6(+(n403_6, b)), rt in Omega(0) Generator Equations: gen_c:c15_6(0) <=> c gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x)) gen_leaf:cons6_6(0) <=> leaf gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x)) gen_c2:c3:c4:c57_6(0) <=> c2 gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c) The following defined symbols remain to be analysed: LESSLEAVES, lessleaves ---------------------------------------- (23) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LESSLEAVES(gen_leaf:cons6_6(n1284_6), gen_leaf:cons6_6(n1284_6)) -> gen_c2:c3:c4:c57_6(n1284_6), rt in Omega(1 + n1284_6) Induction Base: LESSLEAVES(gen_leaf:cons6_6(0), gen_leaf:cons6_6(0)) ->_R^Omega(1) c2 Induction Step: LESSLEAVES(gen_leaf:cons6_6(+(n1284_6, 1)), gen_leaf:cons6_6(+(n1284_6, 1))) ->_R^Omega(1) c4(LESSLEAVES(concat(leaf, gen_leaf:cons6_6(n1284_6)), concat(leaf, gen_leaf:cons6_6(n1284_6))), CONCAT(leaf, gen_leaf:cons6_6(n1284_6))) ->_L^Omega(0) c4(LESSLEAVES(gen_leaf:cons6_6(+(0, n1284_6)), concat(leaf, gen_leaf:cons6_6(n1284_6))), CONCAT(leaf, gen_leaf:cons6_6(n1284_6))) ->_L^Omega(0) c4(LESSLEAVES(gen_leaf:cons6_6(n1284_6), gen_leaf:cons6_6(+(0, n1284_6))), CONCAT(leaf, gen_leaf:cons6_6(n1284_6))) ->_IH c4(gen_c2:c3:c4:c57_6(c1285_6), CONCAT(leaf, gen_leaf:cons6_6(n1284_6))) ->_L^Omega(1) c4(gen_c2:c3:c4:c57_6(n1284_6), gen_c:c15_6(0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (24) Obligation: Innermost TRS: Rules: CONCAT(leaf, z0) -> c CONCAT(cons(z0, z1), z2) -> c1(CONCAT(z1, z2)) LESSLEAVES(z0, leaf) -> c2 LESSLEAVES(leaf, cons(z0, z1)) -> c3 LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c4(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z0, z1)) LESSLEAVES(cons(z0, z1), cons(z2, z3)) -> c5(LESSLEAVES(concat(z0, z1), concat(z2, z3)), CONCAT(z2, z3)) concat(leaf, z0) -> z0 concat(cons(z0, z1), z2) -> cons(z0, concat(z1, z2)) lessleaves(z0, leaf) -> false lessleaves(leaf, cons(z0, z1)) -> true lessleaves(cons(z0, z1), cons(z2, z3)) -> lessleaves(concat(z0, z1), concat(z2, z3)) Types: CONCAT :: leaf:cons -> leaf:cons -> c:c1 leaf :: leaf:cons c :: c:c1 cons :: leaf:cons -> leaf:cons -> leaf:cons c1 :: c:c1 -> c:c1 LESSLEAVES :: leaf:cons -> leaf:cons -> c2:c3:c4:c5 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 concat :: leaf:cons -> leaf:cons -> leaf:cons c5 :: c2:c3:c4:c5 -> c:c1 -> c2:c3:c4:c5 lessleaves :: leaf:cons -> leaf:cons -> false:true false :: false:true true :: false:true hole_c:c11_6 :: c:c1 hole_leaf:cons2_6 :: leaf:cons hole_c2:c3:c4:c53_6 :: c2:c3:c4:c5 hole_false:true4_6 :: false:true gen_c:c15_6 :: Nat -> c:c1 gen_leaf:cons6_6 :: Nat -> leaf:cons gen_c2:c3:c4:c57_6 :: Nat -> c2:c3:c4:c5 Lemmas: CONCAT(gen_leaf:cons6_6(n9_6), gen_leaf:cons6_6(b)) -> gen_c:c15_6(n9_6), rt in Omega(1 + n9_6) concat(gen_leaf:cons6_6(n403_6), gen_leaf:cons6_6(b)) -> gen_leaf:cons6_6(+(n403_6, b)), rt in Omega(0) LESSLEAVES(gen_leaf:cons6_6(n1284_6), gen_leaf:cons6_6(n1284_6)) -> gen_c2:c3:c4:c57_6(n1284_6), rt in Omega(1 + n1284_6) Generator Equations: gen_c:c15_6(0) <=> c gen_c:c15_6(+(x, 1)) <=> c1(gen_c:c15_6(x)) gen_leaf:cons6_6(0) <=> leaf gen_leaf:cons6_6(+(x, 1)) <=> cons(leaf, gen_leaf:cons6_6(x)) gen_c2:c3:c4:c57_6(0) <=> c2 gen_c2:c3:c4:c57_6(+(x, 1)) <=> c4(gen_c2:c3:c4:c57_6(x), c) The following defined symbols remain to be analysed: lessleaves ---------------------------------------- (25) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: lessleaves(gen_leaf:cons6_6(n3724_6), gen_leaf:cons6_6(n3724_6)) -> false, rt in Omega(0) Induction Base: lessleaves(gen_leaf:cons6_6(0), gen_leaf:cons6_6(0)) ->_R^Omega(0) false Induction Step: lessleaves(gen_leaf:cons6_6(+(n3724_6, 1)), gen_leaf:cons6_6(+(n3724_6, 1))) ->_R^Omega(0) lessleaves(concat(leaf, gen_leaf:cons6_6(n3724_6)), concat(leaf, gen_leaf:cons6_6(n3724_6))) ->_L^Omega(0) lessleaves(gen_leaf:cons6_6(+(0, n3724_6)), concat(leaf, gen_leaf:cons6_6(n3724_6))) ->_L^Omega(0) lessleaves(gen_leaf:cons6_6(n3724_6), gen_leaf:cons6_6(+(0, n3724_6))) ->_IH false We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (26) BOUNDS(1, INF)