WORST_CASE(Omega(n^1),?) proof of input_9hUosurCNk.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, INF). (0) CpxTRS (1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CdtProblem (3) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxRelTRS (5) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxRelTRS (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) typed CpxTrs (9) OrderProof [LOWER BOUND(ID), 0 ms] (10) typed CpxTrs (11) RewriteLemmaProof [LOWER BOUND(ID), 338 ms] (12) typed CpxTrs (13) RewriteLemmaProof [LOWER BOUND(ID), 161 ms] (14) BEST (15) proven lower bound (16) LowerBoundPropagationProof [FINISHED, 0 ms] (17) BOUNDS(n^1, INF) (18) typed CpxTrs (19) RewriteLemmaProof [LOWER BOUND(ID), 11.8 s] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 654 ms] (22) BOUNDS(1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: plus(x, y) -> plusIter(x, y, 0) plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) ifPlus(true, x, y, z) -> y ifPlus(false, x, y, z) -> plusIter(x, s(y), s(z)) le(s(x), 0) -> false le(0, y) -> true le(s(x), s(y)) -> le(x, y) sum(xs) -> sumIter(xs, 0) sumIter(xs, x) -> ifSum(isempty(xs), xs, x, plus(x, head(xs))) ifSum(true, xs, x, y) -> x ifSum(false, xs, x, y) -> sumIter(tail(xs), y) isempty(nil) -> true isempty(cons(x, xs)) -> false head(nil) -> error head(cons(x, xs)) -> x tail(nil) -> nil tail(cons(x, xs)) -> xs a -> b a -> c S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: plus(z0, z1) -> plusIter(z0, z1, 0) plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0) -> false le(0, z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0) sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Tuples: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0)) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0) -> c5 LE(0, z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0)) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 S tuples: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0)) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0) -> c5 LE(0, z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0)) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 K tuples:none Defined Rule Symbols: plus_2, plusIter_3, ifPlus_4, le_2, sum_1, sumIter_2, ifSum_4, isempty_1, head_1, tail_1, a Defined Pair Symbols: PLUS_2, PLUSITER_3, IFPLUS_4, LE_2, SUM_1, SUMITER_2, IFSUM_4, ISEMPTY_1, HEAD_1, TAIL_1, A Compound Symbols: c1_1, c2_2, c3, c4_1, c5, c6, c7_1, c8_1, c9_2, c10_3, c11, c12_2, c13, c14, c15, c16, c17, c18, c19, c20 ---------------------------------------- (3) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (4) 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(z0, z1) -> c1(PLUSITER(z0, z1, 0)) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0) -> c5 LE(0, z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0)) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 The (relative) TRS S consists of the following rules: plus(z0, z1) -> plusIter(z0, z1, 0) plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0) -> false le(0, z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0) sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Rewrite Strategy: INNERMOST ---------------------------------------- (5) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (6) 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(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 The (relative) TRS S consists of the following rules: plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (8) Obligation: Innermost TRS: Rules: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Types: PLUS :: 0':s:error -> 0':s:error -> c1 c1 :: c2 -> c1 PLUSITER :: 0':s:error -> 0':s:error -> 0':s:error -> c2 0' :: 0':s:error c2 :: c3:c4 -> c5:c6:c7 -> c2 IFPLUS :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c3:c4 le :: 0':s:error -> 0':s:error -> true:false LE :: 0':s:error -> 0':s:error -> c5:c6:c7 true :: true:false c3 :: c3:c4 false :: true:false c4 :: c2 -> c3:c4 s :: 0':s:error -> 0':s:error c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 SUM :: nil:cons -> c8 c8 :: c9:c10 -> c8 SUMITER :: nil:cons -> 0':s:error -> c9:c10 c9 :: c11:c12 -> c13:c14 -> c9:c10 IFSUM :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> c11:c12 isempty :: nil:cons -> true:false plus :: 0':s:error -> 0':s:error -> 0':s:error head :: nil:cons -> 0':s:error ISEMPTY :: nil:cons -> c13:c14 c10 :: c11:c12 -> c1 -> c15:c16 -> c9:c10 HEAD :: nil:cons -> c15:c16 c11 :: c11:c12 c12 :: c9:c10 -> c17:c18 -> c11:c12 tail :: nil:cons -> nil:cons TAIL :: nil:cons -> c17:c18 nil :: nil:cons c13 :: c13:c14 cons :: 0':s:error -> nil:cons -> nil:cons c14 :: c13:c14 c15 :: c15:c16 c16 :: c15:c16 c17 :: c17:c18 c18 :: c17:c18 A :: c19:c20 c19 :: c19:c20 c20 :: c19:c20 plusIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error ifPlus :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error sum :: nil:cons -> 0':s:error sumIter :: nil:cons -> 0':s:error -> 0':s:error ifSum :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> 0':s:error error :: 0':s:error a :: b:c b :: b:c c :: b:c hole_c11_21 :: c1 hole_0':s:error2_21 :: 0':s:error hole_c23_21 :: c2 hole_c3:c44_21 :: c3:c4 hole_c5:c6:c75_21 :: c5:c6:c7 hole_true:false6_21 :: true:false hole_c87_21 :: c8 hole_nil:cons8_21 :: nil:cons hole_c9:c109_21 :: c9:c10 hole_c11:c1210_21 :: c11:c12 hole_c13:c1411_21 :: c13:c14 hole_c15:c1612_21 :: c15:c16 hole_c17:c1813_21 :: c17:c18 hole_c19:c2014_21 :: c19:c20 hole_b:c15_21 :: b:c gen_0':s:error16_21 :: Nat -> 0':s:error gen_c5:c6:c717_21 :: Nat -> c5:c6:c7 gen_nil:cons18_21 :: Nat -> nil:cons ---------------------------------------- (9) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: PLUSITER, le, LE, SUMITER, plusIter, sumIter They will be analysed ascendingly in the following order: le < PLUSITER LE < PLUSITER le < plusIter ---------------------------------------- (10) Obligation: Innermost TRS: Rules: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Types: PLUS :: 0':s:error -> 0':s:error -> c1 c1 :: c2 -> c1 PLUSITER :: 0':s:error -> 0':s:error -> 0':s:error -> c2 0' :: 0':s:error c2 :: c3:c4 -> c5:c6:c7 -> c2 IFPLUS :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c3:c4 le :: 0':s:error -> 0':s:error -> true:false LE :: 0':s:error -> 0':s:error -> c5:c6:c7 true :: true:false c3 :: c3:c4 false :: true:false c4 :: c2 -> c3:c4 s :: 0':s:error -> 0':s:error c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 SUM :: nil:cons -> c8 c8 :: c9:c10 -> c8 SUMITER :: nil:cons -> 0':s:error -> c9:c10 c9 :: c11:c12 -> c13:c14 -> c9:c10 IFSUM :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> c11:c12 isempty :: nil:cons -> true:false plus :: 0':s:error -> 0':s:error -> 0':s:error head :: nil:cons -> 0':s:error ISEMPTY :: nil:cons -> c13:c14 c10 :: c11:c12 -> c1 -> c15:c16 -> c9:c10 HEAD :: nil:cons -> c15:c16 c11 :: c11:c12 c12 :: c9:c10 -> c17:c18 -> c11:c12 tail :: nil:cons -> nil:cons TAIL :: nil:cons -> c17:c18 nil :: nil:cons c13 :: c13:c14 cons :: 0':s:error -> nil:cons -> nil:cons c14 :: c13:c14 c15 :: c15:c16 c16 :: c15:c16 c17 :: c17:c18 c18 :: c17:c18 A :: c19:c20 c19 :: c19:c20 c20 :: c19:c20 plusIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error ifPlus :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error sum :: nil:cons -> 0':s:error sumIter :: nil:cons -> 0':s:error -> 0':s:error ifSum :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> 0':s:error error :: 0':s:error a :: b:c b :: b:c c :: b:c hole_c11_21 :: c1 hole_0':s:error2_21 :: 0':s:error hole_c23_21 :: c2 hole_c3:c44_21 :: c3:c4 hole_c5:c6:c75_21 :: c5:c6:c7 hole_true:false6_21 :: true:false hole_c87_21 :: c8 hole_nil:cons8_21 :: nil:cons hole_c9:c109_21 :: c9:c10 hole_c11:c1210_21 :: c11:c12 hole_c13:c1411_21 :: c13:c14 hole_c15:c1612_21 :: c15:c16 hole_c17:c1813_21 :: c17:c18 hole_c19:c2014_21 :: c19:c20 hole_b:c15_21 :: b:c gen_0':s:error16_21 :: Nat -> 0':s:error gen_c5:c6:c717_21 :: Nat -> c5:c6:c7 gen_nil:cons18_21 :: Nat -> nil:cons Generator Equations: gen_0':s:error16_21(0) <=> 0' gen_0':s:error16_21(+(x, 1)) <=> s(gen_0':s:error16_21(x)) gen_c5:c6:c717_21(0) <=> c5 gen_c5:c6:c717_21(+(x, 1)) <=> c7(gen_c5:c6:c717_21(x)) gen_nil:cons18_21(0) <=> nil gen_nil:cons18_21(+(x, 1)) <=> cons(0', gen_nil:cons18_21(x)) The following defined symbols remain to be analysed: le, PLUSITER, LE, SUMITER, plusIter, sumIter They will be analysed ascendingly in the following order: le < PLUSITER LE < PLUSITER le < plusIter ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: le(gen_0':s:error16_21(+(1, n20_21)), gen_0':s:error16_21(n20_21)) -> false, rt in Omega(0) Induction Base: le(gen_0':s:error16_21(+(1, 0)), gen_0':s:error16_21(0)) ->_R^Omega(0) false Induction Step: le(gen_0':s:error16_21(+(1, +(n20_21, 1))), gen_0':s:error16_21(+(n20_21, 1))) ->_R^Omega(0) le(gen_0':s:error16_21(+(1, n20_21)), gen_0':s:error16_21(n20_21)) ->_IH false We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (12) Obligation: Innermost TRS: Rules: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Types: PLUS :: 0':s:error -> 0':s:error -> c1 c1 :: c2 -> c1 PLUSITER :: 0':s:error -> 0':s:error -> 0':s:error -> c2 0' :: 0':s:error c2 :: c3:c4 -> c5:c6:c7 -> c2 IFPLUS :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c3:c4 le :: 0':s:error -> 0':s:error -> true:false LE :: 0':s:error -> 0':s:error -> c5:c6:c7 true :: true:false c3 :: c3:c4 false :: true:false c4 :: c2 -> c3:c4 s :: 0':s:error -> 0':s:error c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 SUM :: nil:cons -> c8 c8 :: c9:c10 -> c8 SUMITER :: nil:cons -> 0':s:error -> c9:c10 c9 :: c11:c12 -> c13:c14 -> c9:c10 IFSUM :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> c11:c12 isempty :: nil:cons -> true:false plus :: 0':s:error -> 0':s:error -> 0':s:error head :: nil:cons -> 0':s:error ISEMPTY :: nil:cons -> c13:c14 c10 :: c11:c12 -> c1 -> c15:c16 -> c9:c10 HEAD :: nil:cons -> c15:c16 c11 :: c11:c12 c12 :: c9:c10 -> c17:c18 -> c11:c12 tail :: nil:cons -> nil:cons TAIL :: nil:cons -> c17:c18 nil :: nil:cons c13 :: c13:c14 cons :: 0':s:error -> nil:cons -> nil:cons c14 :: c13:c14 c15 :: c15:c16 c16 :: c15:c16 c17 :: c17:c18 c18 :: c17:c18 A :: c19:c20 c19 :: c19:c20 c20 :: c19:c20 plusIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error ifPlus :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error sum :: nil:cons -> 0':s:error sumIter :: nil:cons -> 0':s:error -> 0':s:error ifSum :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> 0':s:error error :: 0':s:error a :: b:c b :: b:c c :: b:c hole_c11_21 :: c1 hole_0':s:error2_21 :: 0':s:error hole_c23_21 :: c2 hole_c3:c44_21 :: c3:c4 hole_c5:c6:c75_21 :: c5:c6:c7 hole_true:false6_21 :: true:false hole_c87_21 :: c8 hole_nil:cons8_21 :: nil:cons hole_c9:c109_21 :: c9:c10 hole_c11:c1210_21 :: c11:c12 hole_c13:c1411_21 :: c13:c14 hole_c15:c1612_21 :: c15:c16 hole_c17:c1813_21 :: c17:c18 hole_c19:c2014_21 :: c19:c20 hole_b:c15_21 :: b:c gen_0':s:error16_21 :: Nat -> 0':s:error gen_c5:c6:c717_21 :: Nat -> c5:c6:c7 gen_nil:cons18_21 :: Nat -> nil:cons Lemmas: le(gen_0':s:error16_21(+(1, n20_21)), gen_0':s:error16_21(n20_21)) -> false, rt in Omega(0) Generator Equations: gen_0':s:error16_21(0) <=> 0' gen_0':s:error16_21(+(x, 1)) <=> s(gen_0':s:error16_21(x)) gen_c5:c6:c717_21(0) <=> c5 gen_c5:c6:c717_21(+(x, 1)) <=> c7(gen_c5:c6:c717_21(x)) gen_nil:cons18_21(0) <=> nil gen_nil:cons18_21(+(x, 1)) <=> cons(0', gen_nil:cons18_21(x)) The following defined symbols remain to be analysed: LE, PLUSITER, SUMITER, plusIter, sumIter They will be analysed ascendingly in the following order: LE < PLUSITER ---------------------------------------- (13) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LE(gen_0':s:error16_21(+(1, n505_21)), gen_0':s:error16_21(n505_21)) -> gen_c5:c6:c717_21(n505_21), rt in Omega(1 + n505_21) Induction Base: LE(gen_0':s:error16_21(+(1, 0)), gen_0':s:error16_21(0)) ->_R^Omega(1) c5 Induction Step: LE(gen_0':s:error16_21(+(1, +(n505_21, 1))), gen_0':s:error16_21(+(n505_21, 1))) ->_R^Omega(1) c7(LE(gen_0':s:error16_21(+(1, n505_21)), gen_0':s:error16_21(n505_21))) ->_IH c7(gen_c5:c6:c717_21(c506_21)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (14) Complex Obligation (BEST) ---------------------------------------- (15) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Types: PLUS :: 0':s:error -> 0':s:error -> c1 c1 :: c2 -> c1 PLUSITER :: 0':s:error -> 0':s:error -> 0':s:error -> c2 0' :: 0':s:error c2 :: c3:c4 -> c5:c6:c7 -> c2 IFPLUS :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c3:c4 le :: 0':s:error -> 0':s:error -> true:false LE :: 0':s:error -> 0':s:error -> c5:c6:c7 true :: true:false c3 :: c3:c4 false :: true:false c4 :: c2 -> c3:c4 s :: 0':s:error -> 0':s:error c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 SUM :: nil:cons -> c8 c8 :: c9:c10 -> c8 SUMITER :: nil:cons -> 0':s:error -> c9:c10 c9 :: c11:c12 -> c13:c14 -> c9:c10 IFSUM :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> c11:c12 isempty :: nil:cons -> true:false plus :: 0':s:error -> 0':s:error -> 0':s:error head :: nil:cons -> 0':s:error ISEMPTY :: nil:cons -> c13:c14 c10 :: c11:c12 -> c1 -> c15:c16 -> c9:c10 HEAD :: nil:cons -> c15:c16 c11 :: c11:c12 c12 :: c9:c10 -> c17:c18 -> c11:c12 tail :: nil:cons -> nil:cons TAIL :: nil:cons -> c17:c18 nil :: nil:cons c13 :: c13:c14 cons :: 0':s:error -> nil:cons -> nil:cons c14 :: c13:c14 c15 :: c15:c16 c16 :: c15:c16 c17 :: c17:c18 c18 :: c17:c18 A :: c19:c20 c19 :: c19:c20 c20 :: c19:c20 plusIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error ifPlus :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error sum :: nil:cons -> 0':s:error sumIter :: nil:cons -> 0':s:error -> 0':s:error ifSum :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> 0':s:error error :: 0':s:error a :: b:c b :: b:c c :: b:c hole_c11_21 :: c1 hole_0':s:error2_21 :: 0':s:error hole_c23_21 :: c2 hole_c3:c44_21 :: c3:c4 hole_c5:c6:c75_21 :: c5:c6:c7 hole_true:false6_21 :: true:false hole_c87_21 :: c8 hole_nil:cons8_21 :: nil:cons hole_c9:c109_21 :: c9:c10 hole_c11:c1210_21 :: c11:c12 hole_c13:c1411_21 :: c13:c14 hole_c15:c1612_21 :: c15:c16 hole_c17:c1813_21 :: c17:c18 hole_c19:c2014_21 :: c19:c20 hole_b:c15_21 :: b:c gen_0':s:error16_21 :: Nat -> 0':s:error gen_c5:c6:c717_21 :: Nat -> c5:c6:c7 gen_nil:cons18_21 :: Nat -> nil:cons Lemmas: le(gen_0':s:error16_21(+(1, n20_21)), gen_0':s:error16_21(n20_21)) -> false, rt in Omega(0) Generator Equations: gen_0':s:error16_21(0) <=> 0' gen_0':s:error16_21(+(x, 1)) <=> s(gen_0':s:error16_21(x)) gen_c5:c6:c717_21(0) <=> c5 gen_c5:c6:c717_21(+(x, 1)) <=> c7(gen_c5:c6:c717_21(x)) gen_nil:cons18_21(0) <=> nil gen_nil:cons18_21(+(x, 1)) <=> cons(0', gen_nil:cons18_21(x)) The following defined symbols remain to be analysed: LE, PLUSITER, SUMITER, plusIter, sumIter They will be analysed ascendingly in the following order: LE < PLUSITER ---------------------------------------- (16) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (17) BOUNDS(n^1, INF) ---------------------------------------- (18) Obligation: Innermost TRS: Rules: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Types: PLUS :: 0':s:error -> 0':s:error -> c1 c1 :: c2 -> c1 PLUSITER :: 0':s:error -> 0':s:error -> 0':s:error -> c2 0' :: 0':s:error c2 :: c3:c4 -> c5:c6:c7 -> c2 IFPLUS :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c3:c4 le :: 0':s:error -> 0':s:error -> true:false LE :: 0':s:error -> 0':s:error -> c5:c6:c7 true :: true:false c3 :: c3:c4 false :: true:false c4 :: c2 -> c3:c4 s :: 0':s:error -> 0':s:error c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 SUM :: nil:cons -> c8 c8 :: c9:c10 -> c8 SUMITER :: nil:cons -> 0':s:error -> c9:c10 c9 :: c11:c12 -> c13:c14 -> c9:c10 IFSUM :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> c11:c12 isempty :: nil:cons -> true:false plus :: 0':s:error -> 0':s:error -> 0':s:error head :: nil:cons -> 0':s:error ISEMPTY :: nil:cons -> c13:c14 c10 :: c11:c12 -> c1 -> c15:c16 -> c9:c10 HEAD :: nil:cons -> c15:c16 c11 :: c11:c12 c12 :: c9:c10 -> c17:c18 -> c11:c12 tail :: nil:cons -> nil:cons TAIL :: nil:cons -> c17:c18 nil :: nil:cons c13 :: c13:c14 cons :: 0':s:error -> nil:cons -> nil:cons c14 :: c13:c14 c15 :: c15:c16 c16 :: c15:c16 c17 :: c17:c18 c18 :: c17:c18 A :: c19:c20 c19 :: c19:c20 c20 :: c19:c20 plusIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error ifPlus :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error sum :: nil:cons -> 0':s:error sumIter :: nil:cons -> 0':s:error -> 0':s:error ifSum :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> 0':s:error error :: 0':s:error a :: b:c b :: b:c c :: b:c hole_c11_21 :: c1 hole_0':s:error2_21 :: 0':s:error hole_c23_21 :: c2 hole_c3:c44_21 :: c3:c4 hole_c5:c6:c75_21 :: c5:c6:c7 hole_true:false6_21 :: true:false hole_c87_21 :: c8 hole_nil:cons8_21 :: nil:cons hole_c9:c109_21 :: c9:c10 hole_c11:c1210_21 :: c11:c12 hole_c13:c1411_21 :: c13:c14 hole_c15:c1612_21 :: c15:c16 hole_c17:c1813_21 :: c17:c18 hole_c19:c2014_21 :: c19:c20 hole_b:c15_21 :: b:c gen_0':s:error16_21 :: Nat -> 0':s:error gen_c5:c6:c717_21 :: Nat -> c5:c6:c7 gen_nil:cons18_21 :: Nat -> nil:cons Lemmas: le(gen_0':s:error16_21(+(1, n20_21)), gen_0':s:error16_21(n20_21)) -> false, rt in Omega(0) LE(gen_0':s:error16_21(+(1, n505_21)), gen_0':s:error16_21(n505_21)) -> gen_c5:c6:c717_21(n505_21), rt in Omega(1 + n505_21) Generator Equations: gen_0':s:error16_21(0) <=> 0' gen_0':s:error16_21(+(x, 1)) <=> s(gen_0':s:error16_21(x)) gen_c5:c6:c717_21(0) <=> c5 gen_c5:c6:c717_21(+(x, 1)) <=> c7(gen_c5:c6:c717_21(x)) gen_nil:cons18_21(0) <=> nil gen_nil:cons18_21(+(x, 1)) <=> cons(0', gen_nil:cons18_21(x)) The following defined symbols remain to be analysed: PLUSITER, SUMITER, plusIter, sumIter ---------------------------------------- (19) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: SUMITER(gen_nil:cons18_21(n6468_21), gen_0':s:error16_21(1)) -> *19_21, rt in Omega(n6468_21) Induction Base: SUMITER(gen_nil:cons18_21(0), gen_0':s:error16_21(1)) Induction Step: SUMITER(gen_nil:cons18_21(+(n6468_21, 1)), gen_0':s:error16_21(1)) ->_R^Omega(1) c9(IFSUM(isempty(gen_nil:cons18_21(+(n6468_21, 1))), gen_nil:cons18_21(+(n6468_21, 1)), gen_0':s:error16_21(1), plus(gen_0':s:error16_21(1), head(gen_nil:cons18_21(+(n6468_21, 1))))), ISEMPTY(gen_nil:cons18_21(+(n6468_21, 1)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), plus(gen_0':s:error16_21(1), head(gen_nil:cons18_21(+(1, n6468_21))))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), plus(gen_0':s:error16_21(1), 0')), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), plusIter(gen_0':s:error16_21(1), 0', 0')), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), ifPlus(le(gen_0':s:error16_21(1), 0'), gen_0':s:error16_21(1), 0', 0')), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_L^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), ifPlus(false, gen_0':s:error16_21(1), 0', 0')), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), plusIter(gen_0':s:error16_21(1), s(0'), s(0'))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), ifPlus(le(gen_0':s:error16_21(1), s(0')), gen_0':s:error16_21(1), s(0'), s(0'))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), ifPlus(le(gen_0':s:error16_21(0), 0'), gen_0':s:error16_21(1), s(0'), s(0'))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), ifPlus(true, gen_0':s:error16_21(1), s(0'), s(0'))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(IFSUM(false, gen_nil:cons18_21(+(1, n6468_21)), gen_0':s:error16_21(1), s(0')), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(1) c9(c12(SUMITER(tail(gen_nil:cons18_21(+(1, n6468_21))), s(0')), TAIL(gen_nil:cons18_21(+(1, n6468_21)))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(0) c9(c12(SUMITER(gen_nil:cons18_21(n6468_21), s(0')), TAIL(gen_nil:cons18_21(+(1, n6468_21)))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_IH c9(c12(*19_21, TAIL(gen_nil:cons18_21(+(1, n6468_21)))), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(1) c9(c12(*19_21, c18), ISEMPTY(gen_nil:cons18_21(+(1, n6468_21)))) ->_R^Omega(1) c9(c12(*19_21, c18), c14) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (20) Obligation: Innermost TRS: Rules: PLUS(z0, z1) -> c1(PLUSITER(z0, z1, 0')) PLUSITER(z0, z1, z2) -> c2(IFPLUS(le(z0, z2), z0, z1, z2), LE(z0, z2)) IFPLUS(true, z0, z1, z2) -> c3 IFPLUS(false, z0, z1, z2) -> c4(PLUSITER(z0, s(z1), s(z2))) LE(s(z0), 0') -> c5 LE(0', z0) -> c6 LE(s(z0), s(z1)) -> c7(LE(z0, z1)) SUM(z0) -> c8(SUMITER(z0, 0')) SUMITER(z0, z1) -> c9(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), ISEMPTY(z0)) SUMITER(z0, z1) -> c10(IFSUM(isempty(z0), z0, z1, plus(z1, head(z0))), PLUS(z1, head(z0)), HEAD(z0)) IFSUM(true, z0, z1, z2) -> c11 IFSUM(false, z0, z1, z2) -> c12(SUMITER(tail(z0), z2), TAIL(z0)) ISEMPTY(nil) -> c13 ISEMPTY(cons(z0, z1)) -> c14 HEAD(nil) -> c15 HEAD(cons(z0, z1)) -> c16 TAIL(nil) -> c17 TAIL(cons(z0, z1)) -> c18 A -> c19 A -> c20 plus(z0, z1) -> plusIter(z0, z1, 0') plusIter(z0, z1, z2) -> ifPlus(le(z0, z2), z0, z1, z2) ifPlus(true, z0, z1, z2) -> z1 ifPlus(false, z0, z1, z2) -> plusIter(z0, s(z1), s(z2)) le(s(z0), 0') -> false le(0', z0) -> true le(s(z0), s(z1)) -> le(z0, z1) sum(z0) -> sumIter(z0, 0') sumIter(z0, z1) -> ifSum(isempty(z0), z0, z1, plus(z1, head(z0))) ifSum(true, z0, z1, z2) -> z1 ifSum(false, z0, z1, z2) -> sumIter(tail(z0), z2) isempty(nil) -> true isempty(cons(z0, z1)) -> false head(nil) -> error head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 a -> b a -> c Types: PLUS :: 0':s:error -> 0':s:error -> c1 c1 :: c2 -> c1 PLUSITER :: 0':s:error -> 0':s:error -> 0':s:error -> c2 0' :: 0':s:error c2 :: c3:c4 -> c5:c6:c7 -> c2 IFPLUS :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> c3:c4 le :: 0':s:error -> 0':s:error -> true:false LE :: 0':s:error -> 0':s:error -> c5:c6:c7 true :: true:false c3 :: c3:c4 false :: true:false c4 :: c2 -> c3:c4 s :: 0':s:error -> 0':s:error c5 :: c5:c6:c7 c6 :: c5:c6:c7 c7 :: c5:c6:c7 -> c5:c6:c7 SUM :: nil:cons -> c8 c8 :: c9:c10 -> c8 SUMITER :: nil:cons -> 0':s:error -> c9:c10 c9 :: c11:c12 -> c13:c14 -> c9:c10 IFSUM :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> c11:c12 isempty :: nil:cons -> true:false plus :: 0':s:error -> 0':s:error -> 0':s:error head :: nil:cons -> 0':s:error ISEMPTY :: nil:cons -> c13:c14 c10 :: c11:c12 -> c1 -> c15:c16 -> c9:c10 HEAD :: nil:cons -> c15:c16 c11 :: c11:c12 c12 :: c9:c10 -> c17:c18 -> c11:c12 tail :: nil:cons -> nil:cons TAIL :: nil:cons -> c17:c18 nil :: nil:cons c13 :: c13:c14 cons :: 0':s:error -> nil:cons -> nil:cons c14 :: c13:c14 c15 :: c15:c16 c16 :: c15:c16 c17 :: c17:c18 c18 :: c17:c18 A :: c19:c20 c19 :: c19:c20 c20 :: c19:c20 plusIter :: 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error ifPlus :: true:false -> 0':s:error -> 0':s:error -> 0':s:error -> 0':s:error sum :: nil:cons -> 0':s:error sumIter :: nil:cons -> 0':s:error -> 0':s:error ifSum :: true:false -> nil:cons -> 0':s:error -> 0':s:error -> 0':s:error error :: 0':s:error a :: b:c b :: b:c c :: b:c hole_c11_21 :: c1 hole_0':s:error2_21 :: 0':s:error hole_c23_21 :: c2 hole_c3:c44_21 :: c3:c4 hole_c5:c6:c75_21 :: c5:c6:c7 hole_true:false6_21 :: true:false hole_c87_21 :: c8 hole_nil:cons8_21 :: nil:cons hole_c9:c109_21 :: c9:c10 hole_c11:c1210_21 :: c11:c12 hole_c13:c1411_21 :: c13:c14 hole_c15:c1612_21 :: c15:c16 hole_c17:c1813_21 :: c17:c18 hole_c19:c2014_21 :: c19:c20 hole_b:c15_21 :: b:c gen_0':s:error16_21 :: Nat -> 0':s:error gen_c5:c6:c717_21 :: Nat -> c5:c6:c7 gen_nil:cons18_21 :: Nat -> nil:cons Lemmas: le(gen_0':s:error16_21(+(1, n20_21)), gen_0':s:error16_21(n20_21)) -> false, rt in Omega(0) LE(gen_0':s:error16_21(+(1, n505_21)), gen_0':s:error16_21(n505_21)) -> gen_c5:c6:c717_21(n505_21), rt in Omega(1 + n505_21) SUMITER(gen_nil:cons18_21(n6468_21), gen_0':s:error16_21(1)) -> *19_21, rt in Omega(n6468_21) Generator Equations: gen_0':s:error16_21(0) <=> 0' gen_0':s:error16_21(+(x, 1)) <=> s(gen_0':s:error16_21(x)) gen_c5:c6:c717_21(0) <=> c5 gen_c5:c6:c717_21(+(x, 1)) <=> c7(gen_c5:c6:c717_21(x)) gen_nil:cons18_21(0) <=> nil gen_nil:cons18_21(+(x, 1)) <=> cons(0', gen_nil:cons18_21(x)) The following defined symbols remain to be analysed: plusIter, sumIter ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: sumIter(gen_nil:cons18_21(n221484_21), gen_0':s:error16_21(1)) -> *19_21, rt in Omega(0) Induction Base: sumIter(gen_nil:cons18_21(0), gen_0':s:error16_21(1)) Induction Step: sumIter(gen_nil:cons18_21(+(n221484_21, 1)), gen_0':s:error16_21(1)) ->_R^Omega(0) ifSum(isempty(gen_nil:cons18_21(+(n221484_21, 1))), gen_nil:cons18_21(+(n221484_21, 1)), gen_0':s:error16_21(1), plus(gen_0':s:error16_21(1), head(gen_nil:cons18_21(+(n221484_21, 1))))) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), plus(gen_0':s:error16_21(1), head(gen_nil:cons18_21(+(1, n221484_21))))) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), plus(gen_0':s:error16_21(1), 0')) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), plusIter(gen_0':s:error16_21(1), 0', 0')) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), ifPlus(le(gen_0':s:error16_21(1), 0'), gen_0':s:error16_21(1), 0', 0')) ->_L^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), ifPlus(false, gen_0':s:error16_21(1), 0', 0')) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), plusIter(gen_0':s:error16_21(1), s(0'), s(0'))) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), ifPlus(le(gen_0':s:error16_21(1), s(0')), gen_0':s:error16_21(1), s(0'), s(0'))) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), ifPlus(le(gen_0':s:error16_21(0), 0'), gen_0':s:error16_21(1), s(0'), s(0'))) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), ifPlus(true, gen_0':s:error16_21(1), s(0'), s(0'))) ->_R^Omega(0) ifSum(false, gen_nil:cons18_21(+(1, n221484_21)), gen_0':s:error16_21(1), s(0')) ->_R^Omega(0) sumIter(tail(gen_nil:cons18_21(+(1, n221484_21))), s(0')) ->_R^Omega(0) sumIter(gen_nil:cons18_21(n221484_21), s(0')) ->_IH *19_21 We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (22) BOUNDS(1, INF)