WORST_CASE(Omega(n^1),O(n^1)) proof of input_QW8V9WOOsn.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, 30 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), 9 ms] (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 295 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), 92 ms] (22) typed CpxTrs (23) RewriteLemmaProof [LOWER BOUND(ID), 0 ms] (24) typed CpxTrs (25) RewriteLemmaProof [LOWER BOUND(ID), 26 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: plus#2(0, x12) -> x12 plus#2(S(x4), x2) -> S(plus#2(x4, x2)) fold#3(Nil) -> 0 fold#3(Cons(x4, x2)) -> plus#2(x4, fold#3(x2)) main(x1) -> fold#3(x1) 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: plus#2(0, x12) -> x12 plus#2(S(x4), x2) -> S(plus#2(x4, x2)) fold#3(Nil) -> 0 fold#3(Cons(x4, x2)) -> plus#2(x4, fold#3(x2)) main(x1) -> fold#3(x1) 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 1. The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: final states : [1, 2, 3] transitions: 00() -> 0 S0(0) -> 0 Nil0() -> 0 Cons0(0, 0) -> 0 plus#20(0, 0) -> 1 fold#30(0) -> 2 main0(0) -> 3 plus#21(0, 0) -> 4 S1(4) -> 1 01() -> 2 fold#31(0) -> 5 plus#21(0, 5) -> 2 fold#31(0) -> 3 plus#21(0, 5) -> 4 S1(4) -> 2 S1(4) -> 4 01() -> 3 01() -> 5 plus#21(0, 5) -> 3 plus#21(0, 5) -> 5 S1(4) -> 3 S1(4) -> 5 0 -> 1 0 -> 4 5 -> 2 5 -> 3 5 -> 4 ---------------------------------------- (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: plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0 fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Tuples: PLUS#2(0, z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) S tuples: PLUS#2(0, z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) K tuples:none Defined Rule Symbols: plus#2_2, fold#3_1, main_1 Defined Pair Symbols: PLUS#2_2, FOLD#3_1, MAIN_1 Compound Symbols: c, c1_1, c2, c3_2, c4_1 ---------------------------------------- (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: PLUS#2(0, z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) The (relative) TRS S consists of the following rules: plus#2(0, z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0 fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) 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: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) The (relative) TRS S consists of the following rules: plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (12) Obligation: Innermost TRS: Rules: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Types: PLUS#2 :: 0':S -> 0':S -> c:c1 0' :: 0':S c :: c:c1 S :: 0':S -> 0':S c1 :: c:c1 -> c:c1 FOLD#3 :: Nil:Cons -> c2:c3 Nil :: Nil:Cons c2 :: c2:c3 Cons :: 0':S -> Nil:Cons -> Nil:Cons c3 :: c:c1 -> c2:c3 -> c2:c3 fold#3 :: Nil:Cons -> 0':S MAIN :: Nil:Cons -> c4 c4 :: c2:c3 -> c4 plus#2 :: 0':S -> 0':S -> 0':S main :: Nil:Cons -> 0':S hole_c:c11_5 :: c:c1 hole_0':S2_5 :: 0':S hole_c2:c33_5 :: c2:c3 hole_Nil:Cons4_5 :: Nil:Cons hole_c45_5 :: c4 gen_c:c16_5 :: Nat -> c:c1 gen_0':S7_5 :: Nat -> 0':S gen_c2:c38_5 :: Nat -> c2:c3 gen_Nil:Cons9_5 :: Nat -> Nil:Cons ---------------------------------------- (13) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: PLUS#2, FOLD#3, fold#3, plus#2 They will be analysed ascendingly in the following order: PLUS#2 < FOLD#3 fold#3 < FOLD#3 plus#2 < fold#3 ---------------------------------------- (14) Obligation: Innermost TRS: Rules: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Types: PLUS#2 :: 0':S -> 0':S -> c:c1 0' :: 0':S c :: c:c1 S :: 0':S -> 0':S c1 :: c:c1 -> c:c1 FOLD#3 :: Nil:Cons -> c2:c3 Nil :: Nil:Cons c2 :: c2:c3 Cons :: 0':S -> Nil:Cons -> Nil:Cons c3 :: c:c1 -> c2:c3 -> c2:c3 fold#3 :: Nil:Cons -> 0':S MAIN :: Nil:Cons -> c4 c4 :: c2:c3 -> c4 plus#2 :: 0':S -> 0':S -> 0':S main :: Nil:Cons -> 0':S hole_c:c11_5 :: c:c1 hole_0':S2_5 :: 0':S hole_c2:c33_5 :: c2:c3 hole_Nil:Cons4_5 :: Nil:Cons hole_c45_5 :: c4 gen_c:c16_5 :: Nat -> c:c1 gen_0':S7_5 :: Nat -> 0':S gen_c2:c38_5 :: Nat -> c2:c3 gen_Nil:Cons9_5 :: Nat -> Nil:Cons Generator Equations: gen_c:c16_5(0) <=> c gen_c:c16_5(+(x, 1)) <=> c1(gen_c:c16_5(x)) gen_0':S7_5(0) <=> 0' gen_0':S7_5(+(x, 1)) <=> S(gen_0':S7_5(x)) gen_c2:c38_5(0) <=> c2 gen_c2:c38_5(+(x, 1)) <=> c3(c, gen_c2:c38_5(x)) gen_Nil:Cons9_5(0) <=> Nil gen_Nil:Cons9_5(+(x, 1)) <=> Cons(0', gen_Nil:Cons9_5(x)) The following defined symbols remain to be analysed: PLUS#2, FOLD#3, fold#3, plus#2 They will be analysed ascendingly in the following order: PLUS#2 < FOLD#3 fold#3 < FOLD#3 plus#2 < fold#3 ---------------------------------------- (15) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: PLUS#2(gen_0':S7_5(n11_5), gen_0':S7_5(b)) -> gen_c:c16_5(n11_5), rt in Omega(1 + n11_5) Induction Base: PLUS#2(gen_0':S7_5(0), gen_0':S7_5(b)) ->_R^Omega(1) c Induction Step: PLUS#2(gen_0':S7_5(+(n11_5, 1)), gen_0':S7_5(b)) ->_R^Omega(1) c1(PLUS#2(gen_0':S7_5(n11_5), gen_0':S7_5(b))) ->_IH c1(gen_c:c16_5(c12_5)) 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: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Types: PLUS#2 :: 0':S -> 0':S -> c:c1 0' :: 0':S c :: c:c1 S :: 0':S -> 0':S c1 :: c:c1 -> c:c1 FOLD#3 :: Nil:Cons -> c2:c3 Nil :: Nil:Cons c2 :: c2:c3 Cons :: 0':S -> Nil:Cons -> Nil:Cons c3 :: c:c1 -> c2:c3 -> c2:c3 fold#3 :: Nil:Cons -> 0':S MAIN :: Nil:Cons -> c4 c4 :: c2:c3 -> c4 plus#2 :: 0':S -> 0':S -> 0':S main :: Nil:Cons -> 0':S hole_c:c11_5 :: c:c1 hole_0':S2_5 :: 0':S hole_c2:c33_5 :: c2:c3 hole_Nil:Cons4_5 :: Nil:Cons hole_c45_5 :: c4 gen_c:c16_5 :: Nat -> c:c1 gen_0':S7_5 :: Nat -> 0':S gen_c2:c38_5 :: Nat -> c2:c3 gen_Nil:Cons9_5 :: Nat -> Nil:Cons Generator Equations: gen_c:c16_5(0) <=> c gen_c:c16_5(+(x, 1)) <=> c1(gen_c:c16_5(x)) gen_0':S7_5(0) <=> 0' gen_0':S7_5(+(x, 1)) <=> S(gen_0':S7_5(x)) gen_c2:c38_5(0) <=> c2 gen_c2:c38_5(+(x, 1)) <=> c3(c, gen_c2:c38_5(x)) gen_Nil:Cons9_5(0) <=> Nil gen_Nil:Cons9_5(+(x, 1)) <=> Cons(0', gen_Nil:Cons9_5(x)) The following defined symbols remain to be analysed: PLUS#2, FOLD#3, fold#3, plus#2 They will be analysed ascendingly in the following order: PLUS#2 < FOLD#3 fold#3 < FOLD#3 plus#2 < fold#3 ---------------------------------------- (18) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (19) BOUNDS(n^1, INF) ---------------------------------------- (20) Obligation: Innermost TRS: Rules: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Types: PLUS#2 :: 0':S -> 0':S -> c:c1 0' :: 0':S c :: c:c1 S :: 0':S -> 0':S c1 :: c:c1 -> c:c1 FOLD#3 :: Nil:Cons -> c2:c3 Nil :: Nil:Cons c2 :: c2:c3 Cons :: 0':S -> Nil:Cons -> Nil:Cons c3 :: c:c1 -> c2:c3 -> c2:c3 fold#3 :: Nil:Cons -> 0':S MAIN :: Nil:Cons -> c4 c4 :: c2:c3 -> c4 plus#2 :: 0':S -> 0':S -> 0':S main :: Nil:Cons -> 0':S hole_c:c11_5 :: c:c1 hole_0':S2_5 :: 0':S hole_c2:c33_5 :: c2:c3 hole_Nil:Cons4_5 :: Nil:Cons hole_c45_5 :: c4 gen_c:c16_5 :: Nat -> c:c1 gen_0':S7_5 :: Nat -> 0':S gen_c2:c38_5 :: Nat -> c2:c3 gen_Nil:Cons9_5 :: Nat -> Nil:Cons Lemmas: PLUS#2(gen_0':S7_5(n11_5), gen_0':S7_5(b)) -> gen_c:c16_5(n11_5), rt in Omega(1 + n11_5) Generator Equations: gen_c:c16_5(0) <=> c gen_c:c16_5(+(x, 1)) <=> c1(gen_c:c16_5(x)) gen_0':S7_5(0) <=> 0' gen_0':S7_5(+(x, 1)) <=> S(gen_0':S7_5(x)) gen_c2:c38_5(0) <=> c2 gen_c2:c38_5(+(x, 1)) <=> c3(c, gen_c2:c38_5(x)) gen_Nil:Cons9_5(0) <=> Nil gen_Nil:Cons9_5(+(x, 1)) <=> Cons(0', gen_Nil:Cons9_5(x)) The following defined symbols remain to be analysed: plus#2, FOLD#3, fold#3 They will be analysed ascendingly in the following order: fold#3 < FOLD#3 plus#2 < fold#3 ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: plus#2(gen_0':S7_5(n408_5), gen_0':S7_5(b)) -> gen_0':S7_5(+(n408_5, b)), rt in Omega(0) Induction Base: plus#2(gen_0':S7_5(0), gen_0':S7_5(b)) ->_R^Omega(0) gen_0':S7_5(b) Induction Step: plus#2(gen_0':S7_5(+(n408_5, 1)), gen_0':S7_5(b)) ->_R^Omega(0) S(plus#2(gen_0':S7_5(n408_5), gen_0':S7_5(b))) ->_IH S(gen_0':S7_5(+(b, c409_5))) 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: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Types: PLUS#2 :: 0':S -> 0':S -> c:c1 0' :: 0':S c :: c:c1 S :: 0':S -> 0':S c1 :: c:c1 -> c:c1 FOLD#3 :: Nil:Cons -> c2:c3 Nil :: Nil:Cons c2 :: c2:c3 Cons :: 0':S -> Nil:Cons -> Nil:Cons c3 :: c:c1 -> c2:c3 -> c2:c3 fold#3 :: Nil:Cons -> 0':S MAIN :: Nil:Cons -> c4 c4 :: c2:c3 -> c4 plus#2 :: 0':S -> 0':S -> 0':S main :: Nil:Cons -> 0':S hole_c:c11_5 :: c:c1 hole_0':S2_5 :: 0':S hole_c2:c33_5 :: c2:c3 hole_Nil:Cons4_5 :: Nil:Cons hole_c45_5 :: c4 gen_c:c16_5 :: Nat -> c:c1 gen_0':S7_5 :: Nat -> 0':S gen_c2:c38_5 :: Nat -> c2:c3 gen_Nil:Cons9_5 :: Nat -> Nil:Cons Lemmas: PLUS#2(gen_0':S7_5(n11_5), gen_0':S7_5(b)) -> gen_c:c16_5(n11_5), rt in Omega(1 + n11_5) plus#2(gen_0':S7_5(n408_5), gen_0':S7_5(b)) -> gen_0':S7_5(+(n408_5, b)), rt in Omega(0) Generator Equations: gen_c:c16_5(0) <=> c gen_c:c16_5(+(x, 1)) <=> c1(gen_c:c16_5(x)) gen_0':S7_5(0) <=> 0' gen_0':S7_5(+(x, 1)) <=> S(gen_0':S7_5(x)) gen_c2:c38_5(0) <=> c2 gen_c2:c38_5(+(x, 1)) <=> c3(c, gen_c2:c38_5(x)) gen_Nil:Cons9_5(0) <=> Nil gen_Nil:Cons9_5(+(x, 1)) <=> Cons(0', gen_Nil:Cons9_5(x)) The following defined symbols remain to be analysed: fold#3, FOLD#3 They will be analysed ascendingly in the following order: fold#3 < FOLD#3 ---------------------------------------- (23) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: fold#3(gen_Nil:Cons9_5(n1379_5)) -> gen_0':S7_5(0), rt in Omega(0) Induction Base: fold#3(gen_Nil:Cons9_5(0)) ->_R^Omega(0) 0' Induction Step: fold#3(gen_Nil:Cons9_5(+(n1379_5, 1))) ->_R^Omega(0) plus#2(0', fold#3(gen_Nil:Cons9_5(n1379_5))) ->_IH plus#2(0', gen_0':S7_5(0)) ->_L^Omega(0) gen_0':S7_5(+(0, 0)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (24) Obligation: Innermost TRS: Rules: PLUS#2(0', z0) -> c PLUS#2(S(z0), z1) -> c1(PLUS#2(z0, z1)) FOLD#3(Nil) -> c2 FOLD#3(Cons(z0, z1)) -> c3(PLUS#2(z0, fold#3(z1)), FOLD#3(z1)) MAIN(z0) -> c4(FOLD#3(z0)) plus#2(0', z0) -> z0 plus#2(S(z0), z1) -> S(plus#2(z0, z1)) fold#3(Nil) -> 0' fold#3(Cons(z0, z1)) -> plus#2(z0, fold#3(z1)) main(z0) -> fold#3(z0) Types: PLUS#2 :: 0':S -> 0':S -> c:c1 0' :: 0':S c :: c:c1 S :: 0':S -> 0':S c1 :: c:c1 -> c:c1 FOLD#3 :: Nil:Cons -> c2:c3 Nil :: Nil:Cons c2 :: c2:c3 Cons :: 0':S -> Nil:Cons -> Nil:Cons c3 :: c:c1 -> c2:c3 -> c2:c3 fold#3 :: Nil:Cons -> 0':S MAIN :: Nil:Cons -> c4 c4 :: c2:c3 -> c4 plus#2 :: 0':S -> 0':S -> 0':S main :: Nil:Cons -> 0':S hole_c:c11_5 :: c:c1 hole_0':S2_5 :: 0':S hole_c2:c33_5 :: c2:c3 hole_Nil:Cons4_5 :: Nil:Cons hole_c45_5 :: c4 gen_c:c16_5 :: Nat -> c:c1 gen_0':S7_5 :: Nat -> 0':S gen_c2:c38_5 :: Nat -> c2:c3 gen_Nil:Cons9_5 :: Nat -> Nil:Cons Lemmas: PLUS#2(gen_0':S7_5(n11_5), gen_0':S7_5(b)) -> gen_c:c16_5(n11_5), rt in Omega(1 + n11_5) plus#2(gen_0':S7_5(n408_5), gen_0':S7_5(b)) -> gen_0':S7_5(+(n408_5, b)), rt in Omega(0) fold#3(gen_Nil:Cons9_5(n1379_5)) -> gen_0':S7_5(0), rt in Omega(0) Generator Equations: gen_c:c16_5(0) <=> c gen_c:c16_5(+(x, 1)) <=> c1(gen_c:c16_5(x)) gen_0':S7_5(0) <=> 0' gen_0':S7_5(+(x, 1)) <=> S(gen_0':S7_5(x)) gen_c2:c38_5(0) <=> c2 gen_c2:c38_5(+(x, 1)) <=> c3(c, gen_c2:c38_5(x)) gen_Nil:Cons9_5(0) <=> Nil gen_Nil:Cons9_5(+(x, 1)) <=> Cons(0', gen_Nil:Cons9_5(x)) The following defined symbols remain to be analysed: FOLD#3 ---------------------------------------- (25) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: FOLD#3(gen_Nil:Cons9_5(n1739_5)) -> gen_c2:c38_5(n1739_5), rt in Omega(1 + n1739_5) Induction Base: FOLD#3(gen_Nil:Cons9_5(0)) ->_R^Omega(1) c2 Induction Step: FOLD#3(gen_Nil:Cons9_5(+(n1739_5, 1))) ->_R^Omega(1) c3(PLUS#2(0', fold#3(gen_Nil:Cons9_5(n1739_5))), FOLD#3(gen_Nil:Cons9_5(n1739_5))) ->_L^Omega(0) c3(PLUS#2(0', gen_0':S7_5(0)), FOLD#3(gen_Nil:Cons9_5(n1739_5))) ->_L^Omega(1) c3(gen_c:c16_5(0), FOLD#3(gen_Nil:Cons9_5(n1739_5))) ->_IH c3(gen_c:c16_5(0), gen_c2:c38_5(c1740_5)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (26) BOUNDS(1, INF)