WORST_CASE(Omega(n^2),?) proof of input_ngRmE9FSTB.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF). (0) CpxTRS (1) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 45 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), 364 ms] (12) typed CpxTrs (13) RewriteLemmaProof [LOWER BOUND(ID), 219 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), 783 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 61 ms] (22) typed CpxTrs (23) RewriteLemmaProof [LOWER BOUND(ID), 72 ms] (24) typed CpxTrs (25) RewriteLemmaProof [LOWER BOUND(ID), 26 ms] (26) typed CpxTrs (27) RewriteLemmaProof [LOWER BOUND(ID), 33 ms] (28) typed CpxTrs (29) RewriteLemmaProof [LOWER BOUND(ID), 38 ms] (30) typed CpxTrs (31) RewriteLemmaProof [LOWER BOUND(ID), 1452 ms] (32) BEST (33) proven lower bound (34) LowerBoundPropagationProof [FINISHED, 0 ms] (35) BOUNDS(n^2, INF) (36) typed CpxTrs (37) RewriteLemmaProof [LOWER BOUND(ID), 112 ms] (38) BOUNDS(1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, INF). The TRS R consists of the following rules: max(nil) -> 0 max(cons(x, nil)) -> x max(cons(x, cons(y, xs))) -> if1(ge(x, y), x, y, xs) if1(true, x, y, xs) -> max(cons(x, xs)) if1(false, x, y, xs) -> max(cons(y, xs)) del(x, nil) -> nil del(x, cons(y, xs)) -> if2(eq(x, y), x, y, xs) if2(true, x, y, xs) -> xs if2(false, x, y, xs) -> cons(y, del(x, xs)) eq(0, 0) -> true eq(0, s(y)) -> false eq(s(x), 0) -> false eq(s(x), s(y)) -> eq(x, y) sort(nil) -> nil sort(cons(x, xs)) -> cons(max(cons(x, xs)), sort(h(del(max(cons(x, xs)), cons(x, xs))))) ge(0, 0) -> true ge(s(x), 0) -> true ge(0, s(x)) -> false ge(s(x), s(y)) -> ge(x, y) h(nil) -> nil h(cons(x, xs)) -> cons(x, h(xs)) 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: max(nil) -> 0 max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0, 0) -> true ge(s(z0), 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Tuples: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0, 0) -> c9 EQ(0, s(z0)) -> c10 EQ(s(z0), 0) -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0, 0) -> c16 GE(s(z0), 0) -> c17 GE(0, s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) S tuples: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0, 0) -> c9 EQ(0, s(z0)) -> c10 EQ(s(z0), 0) -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0, 0) -> c16 GE(s(z0), 0) -> c17 GE(0, s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) K tuples:none Defined Rule Symbols: max_1, if1_4, del_2, if2_4, eq_2, sort_1, ge_2, h_1 Defined Pair Symbols: MAX_1, IF1_4, DEL_2, IF2_4, EQ_2, SORT_1, GE_2, H_1 Compound Symbols: c, c1, c2_2, c3_1, c4_1, c5, c6_2, c7, c8_1, c9, c10, c11, c12_1, c13, c14_1, c15_4, c16, c17, c18, c19_1, c20, c21_1 ---------------------------------------- (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^2, INF). The TRS R consists of the following rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0, 0) -> c9 EQ(0, s(z0)) -> c10 EQ(s(z0), 0) -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0, 0) -> c16 GE(s(z0), 0) -> c17 GE(0, s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) The (relative) TRS S consists of the following rules: max(nil) -> 0 max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0, 0) -> true ge(s(z0), 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) 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^2, INF). The TRS R consists of the following rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) The (relative) TRS S consists of the following rules: max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (8) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 ---------------------------------------- (9) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: MAX, ge, GE, DEL, eq, EQ, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: ge < MAX GE < MAX MAX < SORT ge < max eq < DEL EQ < DEL DEL < SORT eq < del h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (10) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: ge, MAX, GE, DEL, eq, EQ, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: ge < MAX GE < MAX MAX < SORT ge < max eq < DEL EQ < DEL DEL < SORT eq < del h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) Induction Base: ge(gen_0':s13_22(0), gen_0':s13_22(0)) ->_R^Omega(0) true Induction Step: ge(gen_0':s13_22(+(n19_22, 1)), gen_0':s13_22(+(n19_22, 1))) ->_R^Omega(0) ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) ->_IH true 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: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: GE, MAX, DEL, eq, EQ, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: GE < MAX MAX < SORT eq < DEL EQ < DEL DEL < SORT eq < del h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (13) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) Induction Base: GE(gen_0':s13_22(0), gen_0':s13_22(0)) ->_R^Omega(1) c16 Induction Step: GE(gen_0':s13_22(+(n726_22, 1)), gen_0':s13_22(+(n726_22, 1))) ->_R^Omega(1) c19(GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22))) ->_IH c19(gen_c16:c17:c18:c1914_22(c727_22)) 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: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: GE, MAX, DEL, eq, EQ, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: GE < MAX MAX < SORT eq < DEL EQ < DEL DEL < SORT eq < del h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (16) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (17) BOUNDS(n^1, INF) ---------------------------------------- (18) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: MAX, DEL, eq, EQ, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: MAX < SORT eq < DEL EQ < DEL DEL < SORT eq < del h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (19) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) Induction Base: MAX(gen_nil:cons12_22(+(1, 0))) Induction Step: MAX(gen_nil:cons12_22(+(1, +(n1859_22, 1)))) ->_R^Omega(1) c2(IF1(ge(0', 0'), 0', 0', gen_nil:cons12_22(n1859_22)), GE(0', 0')) ->_L^Omega(0) c2(IF1(true, 0', 0', gen_nil:cons12_22(n1859_22)), GE(0', 0')) ->_R^Omega(1) c2(c3(MAX(cons(0', gen_nil:cons12_22(n1859_22)))), GE(0', 0')) ->_IH c2(c3(*18_22), GE(0', 0')) ->_L^Omega(1) c2(c3(*18_22), gen_c16:c17:c18:c1914_22(0)) 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: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: eq, DEL, EQ, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: eq < DEL EQ < DEL DEL < SORT eq < del h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) Induction Base: eq(gen_0':s13_22(0), gen_0':s13_22(0)) ->_R^Omega(0) true Induction Step: eq(gen_0':s13_22(+(n8351_22, 1)), gen_0':s13_22(+(n8351_22, 1))) ->_R^Omega(0) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) ->_IH true 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: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: EQ, DEL, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: EQ < DEL DEL < SORT h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (23) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) Induction Base: EQ(gen_0':s13_22(0), gen_0':s13_22(0)) ->_R^Omega(1) c9 Induction Step: EQ(gen_0':s13_22(+(n9136_22, 1)), gen_0':s13_22(+(n9136_22, 1))) ->_R^Omega(1) c12(EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22))) ->_IH c12(gen_c9:c10:c11:c1215_22(c9137_22)) 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: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: DEL, SORT, h, del, max, H, sort They will be analysed ascendingly in the following order: DEL < SORT h < SORT del < SORT max < SORT H < SORT h < sort del < sort max < sort ---------------------------------------- (25) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: h(gen_nil:cons12_22(n11177_22)) -> gen_nil:cons12_22(n11177_22), rt in Omega(0) Induction Base: h(gen_nil:cons12_22(0)) ->_R^Omega(0) nil Induction Step: h(gen_nil:cons12_22(+(n11177_22, 1))) ->_R^Omega(0) cons(0', h(gen_nil:cons12_22(n11177_22))) ->_IH cons(0', gen_nil:cons12_22(c11178_22)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (26) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) h(gen_nil:cons12_22(n11177_22)) -> gen_nil:cons12_22(n11177_22), rt in Omega(0) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: del, SORT, max, H, sort They will be analysed ascendingly in the following order: del < SORT max < SORT H < SORT del < sort max < sort ---------------------------------------- (27) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: max(gen_nil:cons12_22(+(1, n12182_22))) -> gen_0':s13_22(0), rt in Omega(0) Induction Base: max(gen_nil:cons12_22(+(1, 0))) ->_R^Omega(0) 0' Induction Step: max(gen_nil:cons12_22(+(1, +(n12182_22, 1)))) ->_R^Omega(0) if1(ge(0', 0'), 0', 0', gen_nil:cons12_22(n12182_22)) ->_L^Omega(0) if1(true, 0', 0', gen_nil:cons12_22(n12182_22)) ->_R^Omega(0) max(cons(0', gen_nil:cons12_22(n12182_22))) ->_IH gen_0':s13_22(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (28) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) h(gen_nil:cons12_22(n11177_22)) -> gen_nil:cons12_22(n11177_22), rt in Omega(0) max(gen_nil:cons12_22(+(1, n12182_22))) -> gen_0':s13_22(0), rt in Omega(0) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: H, SORT, sort They will be analysed ascendingly in the following order: H < SORT ---------------------------------------- (29) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: H(gen_nil:cons12_22(n13136_22)) -> gen_c20:c2117_22(n13136_22), rt in Omega(1 + n13136_22) Induction Base: H(gen_nil:cons12_22(0)) ->_R^Omega(1) c20 Induction Step: H(gen_nil:cons12_22(+(n13136_22, 1))) ->_R^Omega(1) c21(H(gen_nil:cons12_22(n13136_22))) ->_IH c21(gen_c20:c2117_22(c13137_22)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (30) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) h(gen_nil:cons12_22(n11177_22)) -> gen_nil:cons12_22(n11177_22), rt in Omega(0) max(gen_nil:cons12_22(+(1, n12182_22))) -> gen_0':s13_22(0), rt in Omega(0) H(gen_nil:cons12_22(n13136_22)) -> gen_c20:c2117_22(n13136_22), rt in Omega(1 + n13136_22) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: SORT, sort ---------------------------------------- (31) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: SORT(gen_nil:cons12_22(n13790_22)) -> *18_22, rt in Omega(n13790_22 + n13790_22^2) Induction Base: SORT(gen_nil:cons12_22(0)) Induction Step: SORT(gen_nil:cons12_22(+(n13790_22, 1))) ->_R^Omega(1) c15(SORT(h(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))))), H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(SORT(h(del(gen_0':s13_22(0), cons(0', gen_nil:cons12_22(n13790_22))))), H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_R^Omega(0) c15(SORT(h(if2(eq(gen_0':s13_22(0), 0'), gen_0':s13_22(0), 0', gen_nil:cons12_22(n13790_22)))), H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(SORT(h(if2(true, gen_0':s13_22(0), 0', gen_nil:cons12_22(n13790_22)))), H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_R^Omega(0) c15(SORT(h(gen_nil:cons12_22(n13790_22))), H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(SORT(gen_nil:cons12_22(n13790_22)), H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_IH c15(*18_22, H(del(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(*18_22, H(del(gen_0':s13_22(0), cons(0', gen_nil:cons12_22(n13790_22)))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_R^Omega(0) c15(*18_22, H(if2(eq(gen_0':s13_22(0), 0'), gen_0':s13_22(0), 0', gen_nil:cons12_22(n13790_22))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(*18_22, H(if2(true, gen_0':s13_22(0), 0', gen_nil:cons12_22(n13790_22))), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_R^Omega(0) c15(*18_22, H(gen_nil:cons12_22(n13790_22)), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(1 + n13790_22) c15(*18_22, gen_c20:c2117_22(n13790_22), DEL(max(cons(0', gen_nil:cons12_22(n13790_22))), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(*18_22, gen_c20:c2117_22(n13790_22), DEL(gen_0':s13_22(0), cons(0', gen_nil:cons12_22(n13790_22))), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_R^Omega(1) c15(*18_22, gen_c20:c2117_22(n13790_22), c6(IF2(eq(gen_0':s13_22(0), 0'), gen_0':s13_22(0), 0', gen_nil:cons12_22(n13790_22)), EQ(gen_0':s13_22(0), 0')), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(0) c15(*18_22, gen_c20:c2117_22(n13790_22), c6(IF2(true, gen_0':s13_22(0), 0', gen_nil:cons12_22(n13790_22)), EQ(gen_0':s13_22(0), 0')), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_R^Omega(1) c15(*18_22, gen_c20:c2117_22(n13790_22), c6(c7, EQ(gen_0':s13_22(0), 0')), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(1) c15(*18_22, gen_c20:c2117_22(n13790_22), c6(c7, gen_c9:c10:c11:c1215_22(0)), MAX(cons(0', gen_nil:cons12_22(n13790_22)))) ->_L^Omega(n13790_22) c15(*18_22, gen_c20:c2117_22(n13790_22), c6(c7, gen_c9:c10:c11:c1215_22(0)), *18_22) We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2). ---------------------------------------- (32) Complex Obligation (BEST) ---------------------------------------- (33) Obligation: Proved the lower bound n^2 for the following obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) h(gen_nil:cons12_22(n11177_22)) -> gen_nil:cons12_22(n11177_22), rt in Omega(0) max(gen_nil:cons12_22(+(1, n12182_22))) -> gen_0':s13_22(0), rt in Omega(0) H(gen_nil:cons12_22(n13136_22)) -> gen_c20:c2117_22(n13136_22), rt in Omega(1 + n13136_22) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: SORT, sort ---------------------------------------- (34) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (35) BOUNDS(n^2, INF) ---------------------------------------- (36) Obligation: Innermost TRS: Rules: MAX(nil) -> c MAX(cons(z0, nil)) -> c1 MAX(cons(z0, cons(z1, z2))) -> c2(IF1(ge(z0, z1), z0, z1, z2), GE(z0, z1)) IF1(true, z0, z1, z2) -> c3(MAX(cons(z0, z2))) IF1(false, z0, z1, z2) -> c4(MAX(cons(z1, z2))) DEL(z0, nil) -> c5 DEL(z0, cons(z1, z2)) -> c6(IF2(eq(z0, z1), z0, z1, z2), EQ(z0, z1)) IF2(true, z0, z1, z2) -> c7 IF2(false, z0, z1, z2) -> c8(DEL(z0, z2)) EQ(0', 0') -> c9 EQ(0', s(z0)) -> c10 EQ(s(z0), 0') -> c11 EQ(s(z0), s(z1)) -> c12(EQ(z0, z1)) SORT(nil) -> c13 SORT(cons(z0, z1)) -> c14(MAX(cons(z0, z1))) SORT(cons(z0, z1)) -> c15(SORT(h(del(max(cons(z0, z1)), cons(z0, z1)))), H(del(max(cons(z0, z1)), cons(z0, z1))), DEL(max(cons(z0, z1)), cons(z0, z1)), MAX(cons(z0, z1))) GE(0', 0') -> c16 GE(s(z0), 0') -> c17 GE(0', s(z0)) -> c18 GE(s(z0), s(z1)) -> c19(GE(z0, z1)) H(nil) -> c20 H(cons(z0, z1)) -> c21(H(z1)) max(nil) -> 0' max(cons(z0, nil)) -> z0 max(cons(z0, cons(z1, z2))) -> if1(ge(z0, z1), z0, z1, z2) if1(true, z0, z1, z2) -> max(cons(z0, z2)) if1(false, z0, z1, z2) -> max(cons(z1, z2)) del(z0, nil) -> nil del(z0, cons(z1, z2)) -> if2(eq(z0, z1), z0, z1, z2) if2(true, z0, z1, z2) -> z2 if2(false, z0, z1, z2) -> cons(z1, del(z0, z2)) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) sort(nil) -> nil sort(cons(z0, z1)) -> cons(max(cons(z0, z1)), sort(h(del(max(cons(z0, z1)), cons(z0, z1))))) ge(0', 0') -> true ge(s(z0), 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) h(nil) -> nil h(cons(z0, z1)) -> cons(z0, h(z1)) Types: MAX :: nil:cons -> c:c1:c2 nil :: nil:cons c :: c:c1:c2 cons :: 0':s -> nil:cons -> nil:cons c1 :: c:c1:c2 c2 :: c3:c4 -> c16:c17:c18:c19 -> c:c1:c2 IF1 :: true:false -> 0':s -> 0':s -> nil:cons -> c3:c4 ge :: 0':s -> 0':s -> true:false GE :: 0':s -> 0':s -> c16:c17:c18:c19 true :: true:false c3 :: c:c1:c2 -> c3:c4 false :: true:false c4 :: c:c1:c2 -> c3:c4 DEL :: 0':s -> nil:cons -> c5:c6 c5 :: c5:c6 c6 :: c7:c8 -> c9:c10:c11:c12 -> c5:c6 IF2 :: true:false -> 0':s -> 0':s -> nil:cons -> c7:c8 eq :: 0':s -> 0':s -> true:false EQ :: 0':s -> 0':s -> c9:c10:c11:c12 c7 :: c7:c8 c8 :: c5:c6 -> c7:c8 0' :: 0':s c9 :: c9:c10:c11:c12 s :: 0':s -> 0':s c10 :: c9:c10:c11:c12 c11 :: c9:c10:c11:c12 c12 :: c9:c10:c11:c12 -> c9:c10:c11:c12 SORT :: nil:cons -> c13:c14:c15 c13 :: c13:c14:c15 c14 :: c:c1:c2 -> c13:c14:c15 c15 :: c13:c14:c15 -> c20:c21 -> c5:c6 -> c:c1:c2 -> c13:c14:c15 h :: nil:cons -> nil:cons del :: 0':s -> nil:cons -> nil:cons max :: nil:cons -> 0':s H :: nil:cons -> c20:c21 c16 :: c16:c17:c18:c19 c17 :: c16:c17:c18:c19 c18 :: c16:c17:c18:c19 c19 :: c16:c17:c18:c19 -> c16:c17:c18:c19 c20 :: c20:c21 c21 :: c20:c21 -> c20:c21 if1 :: true:false -> 0':s -> 0':s -> nil:cons -> 0':s if2 :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c21_22 :: c:c1:c2 hole_nil:cons2_22 :: nil:cons hole_0':s3_22 :: 0':s hole_c3:c44_22 :: c3:c4 hole_c16:c17:c18:c195_22 :: c16:c17:c18:c19 hole_true:false6_22 :: true:false hole_c5:c67_22 :: c5:c6 hole_c7:c88_22 :: c7:c8 hole_c9:c10:c11:c129_22 :: c9:c10:c11:c12 hole_c13:c14:c1510_22 :: c13:c14:c15 hole_c20:c2111_22 :: c20:c21 gen_nil:cons12_22 :: Nat -> nil:cons gen_0':s13_22 :: Nat -> 0':s gen_c16:c17:c18:c1914_22 :: Nat -> c16:c17:c18:c19 gen_c9:c10:c11:c1215_22 :: Nat -> c9:c10:c11:c12 gen_c13:c14:c1516_22 :: Nat -> c13:c14:c15 gen_c20:c2117_22 :: Nat -> c20:c21 Lemmas: ge(gen_0':s13_22(n19_22), gen_0':s13_22(n19_22)) -> true, rt in Omega(0) GE(gen_0':s13_22(n726_22), gen_0':s13_22(n726_22)) -> gen_c16:c17:c18:c1914_22(n726_22), rt in Omega(1 + n726_22) MAX(gen_nil:cons12_22(+(1, n1859_22))) -> *18_22, rt in Omega(n1859_22) eq(gen_0':s13_22(n8351_22), gen_0':s13_22(n8351_22)) -> true, rt in Omega(0) EQ(gen_0':s13_22(n9136_22), gen_0':s13_22(n9136_22)) -> gen_c9:c10:c11:c1215_22(n9136_22), rt in Omega(1 + n9136_22) h(gen_nil:cons12_22(n11177_22)) -> gen_nil:cons12_22(n11177_22), rt in Omega(0) max(gen_nil:cons12_22(+(1, n12182_22))) -> gen_0':s13_22(0), rt in Omega(0) H(gen_nil:cons12_22(n13136_22)) -> gen_c20:c2117_22(n13136_22), rt in Omega(1 + n13136_22) SORT(gen_nil:cons12_22(n13790_22)) -> *18_22, rt in Omega(n13790_22 + n13790_22^2) Generator Equations: gen_nil:cons12_22(0) <=> nil gen_nil:cons12_22(+(x, 1)) <=> cons(0', gen_nil:cons12_22(x)) gen_0':s13_22(0) <=> 0' gen_0':s13_22(+(x, 1)) <=> s(gen_0':s13_22(x)) gen_c16:c17:c18:c1914_22(0) <=> c16 gen_c16:c17:c18:c1914_22(+(x, 1)) <=> c19(gen_c16:c17:c18:c1914_22(x)) gen_c9:c10:c11:c1215_22(0) <=> c9 gen_c9:c10:c11:c1215_22(+(x, 1)) <=> c12(gen_c9:c10:c11:c1215_22(x)) gen_c13:c14:c1516_22(0) <=> c13 gen_c13:c14:c1516_22(+(x, 1)) <=> c15(gen_c13:c14:c1516_22(x), c20, c5, c) gen_c20:c2117_22(0) <=> c20 gen_c20:c2117_22(+(x, 1)) <=> c21(gen_c20:c2117_22(x)) The following defined symbols remain to be analysed: sort ---------------------------------------- (37) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: sort(gen_nil:cons12_22(n32520_22)) -> gen_nil:cons12_22(n32520_22), rt in Omega(0) Induction Base: sort(gen_nil:cons12_22(0)) ->_R^Omega(0) nil Induction Step: sort(gen_nil:cons12_22(+(n32520_22, 1))) ->_R^Omega(0) cons(max(cons(0', gen_nil:cons12_22(n32520_22))), sort(h(del(max(cons(0', gen_nil:cons12_22(n32520_22))), cons(0', gen_nil:cons12_22(n32520_22)))))) ->_L^Omega(0) cons(gen_0':s13_22(0), sort(h(del(max(cons(0', gen_nil:cons12_22(n32520_22))), cons(0', gen_nil:cons12_22(n32520_22)))))) ->_L^Omega(0) cons(gen_0':s13_22(0), sort(h(del(gen_0':s13_22(0), cons(0', gen_nil:cons12_22(n32520_22)))))) ->_R^Omega(0) cons(gen_0':s13_22(0), sort(h(if2(eq(gen_0':s13_22(0), 0'), gen_0':s13_22(0), 0', gen_nil:cons12_22(n32520_22))))) ->_L^Omega(0) cons(gen_0':s13_22(0), sort(h(if2(true, gen_0':s13_22(0), 0', gen_nil:cons12_22(n32520_22))))) ->_R^Omega(0) cons(gen_0':s13_22(0), sort(h(gen_nil:cons12_22(n32520_22)))) ->_L^Omega(0) cons(gen_0':s13_22(0), sort(gen_nil:cons12_22(n32520_22))) ->_IH cons(gen_0':s13_22(0), gen_nil:cons12_22(c32521_22)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (38) BOUNDS(1, INF)