WORST_CASE(NON_POLY,?) proof of input_MQ6LTxk7Sc.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(EXP, 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), 9 ms] (8) typed CpxTrs (9) OrderProof [LOWER BOUND(ID), 0 ms] (10) typed CpxTrs (11) RewriteLemmaProof [LOWER BOUND(ID), 327 ms] (12) BEST (13) proven lower bound (14) LowerBoundPropagationProof [FINISHED, 0 ms] (15) BOUNDS(n^1, INF) (16) typed CpxTrs (17) RewriteLemmaProof [LOWER BOUND(ID), 36 ms] (18) typed CpxTrs (19) RewriteLemmaProof [LOWER BOUND(ID), 2135 ms] (20) typed CpxTrs (21) RewriteLemmaProof [LOWER BOUND(ID), 55 ms] (22) typed CpxTrs (23) RewriteLemmaProof [FINISHED, 444 ms] (24) BOUNDS(EXP, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(EXP, INF). The TRS R consists of the following rules: min(0, y) -> 0 min(x, 0) -> 0 min(s(x), s(y)) -> s(min(x, y)) max(0, y) -> y max(x, 0) -> x max(s(x), s(y)) -> s(max(x, y)) +(0, y) -> y +(s(x), y) -> s(+(x, y)) -(x, 0) -> x -(s(x), s(y)) -> -(x, y) *(x, 0) -> 0 *(x, s(y)) -> +(x, *(x, y)) p(s(x)) -> x f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))) 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: min(0, z0) -> 0 min(z0, 0) -> 0 min(s(z0), s(z1)) -> s(min(z0, z1)) max(0, z0) -> z0 max(z0, 0) -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +(0, z0) -> z0 +(s(z0), z1) -> s(+(z0, z1)) -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) *(z0, 0) -> 0 *(z0, s(z1)) -> +(z0, *(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))) Tuples: MIN(0, z0) -> c MIN(z0, 0) -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0, z0) -> c3 MAX(z0, 0) -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0, z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0) -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0) -> c10 *'(z0, s(z1)) -> c11(+'(z0, *(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), *'(s(z0), s(z1))) S tuples: MIN(0, z0) -> c MIN(z0, 0) -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0, z0) -> c3 MAX(z0, 0) -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0, z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0) -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0) -> c10 *'(z0, s(z1)) -> c11(+'(z0, *(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), *'(s(z0), s(z1))) K tuples:none Defined Rule Symbols: min_2, max_2, +_2, -_2, *_2, p_1, f_2 Defined Pair Symbols: MIN_2, MAX_2, +'_2, -'_2, *'_2, P_1, F_2 Compound Symbols: c, c1, c2_1, c3, c4, c5_1, c6, c7_1, c8, c9_1, c10, c11_2, c12, c13_3, c14_3, c15_2 ---------------------------------------- (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(EXP, INF). The TRS R consists of the following rules: MIN(0, z0) -> c MIN(z0, 0) -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0, z0) -> c3 MAX(z0, 0) -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0, z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0) -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0) -> c10 *'(z0, s(z1)) -> c11(+'(z0, *(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(z1))), *'(s(z0), s(z1))) The (relative) TRS S consists of the following rules: min(0, z0) -> 0 min(z0, 0) -> 0 min(s(z0), s(z1)) -> s(min(z0, z1)) max(0, z0) -> z0 max(z0, 0) -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +(0, z0) -> z0 +(s(z0), z1) -> s(+(z0, z1)) -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) *(z0, 0) -> 0 *(z0, s(z1)) -> +(z0, *(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *(s(z0), s(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(EXP, INF). The TRS R consists of the following rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) The (relative) TRS S consists of the following rules: min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (8) Obligation: Innermost TRS: Rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 ---------------------------------------- (9) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: MIN, MAX, +', -', *', F, -, min, max, f They will be analysed ascendingly in the following order: MIN < F MAX < F +' < *' -' < F *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (10) Obligation: Innermost TRS: Rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 Generator Equations: gen_c:c1:c28_16(0) <=> c gen_c:c1:c28_16(+(x, 1)) <=> c2(gen_c:c1:c28_16(x)) gen_0':s:c6:c7:c10:c119_16(0) <=> 0' gen_0':s:c6:c7:c10:c119_16(+(x, 1)) <=> s(gen_0':s:c6:c7:c10:c119_16(x)) gen_c3:c4:c510_16(0) <=> c3 gen_c3:c4:c510_16(+(x, 1)) <=> c5(gen_c3:c4:c510_16(x)) gen_c8:c911_16(0) <=> c8 gen_c8:c911_16(+(x, 1)) <=> c9(gen_c8:c911_16(x)) gen_c13:c14:c1512_16(0) <=> hole_c13:c14:c156_16 gen_c13:c14:c1512_16(+(x, 1)) <=> c13(gen_c13:c14:c1512_16(x), c8, c) The following defined symbols remain to be analysed: MIN, MAX, +', -', *', F, -, min, max, f They will be analysed ascendingly in the following order: MIN < F MAX < F +' < *' -' < F *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MIN(gen_0':s:c6:c7:c10:c119_16(n14_16), gen_0':s:c6:c7:c10:c119_16(n14_16)) -> gen_c:c1:c28_16(n14_16), rt in Omega(1 + n14_16) Induction Base: MIN(gen_0':s:c6:c7:c10:c119_16(0), gen_0':s:c6:c7:c10:c119_16(0)) ->_R^Omega(1) c Induction Step: MIN(gen_0':s:c6:c7:c10:c119_16(+(n14_16, 1)), gen_0':s:c6:c7:c10:c119_16(+(n14_16, 1))) ->_R^Omega(1) c2(MIN(gen_0':s:c6:c7:c10:c119_16(n14_16), gen_0':s:c6:c7:c10:c119_16(n14_16))) ->_IH c2(gen_c:c1:c28_16(c15_16)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (12) Complex Obligation (BEST) ---------------------------------------- (13) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 Generator Equations: gen_c:c1:c28_16(0) <=> c gen_c:c1:c28_16(+(x, 1)) <=> c2(gen_c:c1:c28_16(x)) gen_0':s:c6:c7:c10:c119_16(0) <=> 0' gen_0':s:c6:c7:c10:c119_16(+(x, 1)) <=> s(gen_0':s:c6:c7:c10:c119_16(x)) gen_c3:c4:c510_16(0) <=> c3 gen_c3:c4:c510_16(+(x, 1)) <=> c5(gen_c3:c4:c510_16(x)) gen_c8:c911_16(0) <=> c8 gen_c8:c911_16(+(x, 1)) <=> c9(gen_c8:c911_16(x)) gen_c13:c14:c1512_16(0) <=> hole_c13:c14:c156_16 gen_c13:c14:c1512_16(+(x, 1)) <=> c13(gen_c13:c14:c1512_16(x), c8, c) The following defined symbols remain to be analysed: MIN, MAX, +', -', *', F, -, min, max, f They will be analysed ascendingly in the following order: MIN < F MAX < F +' < *' -' < F *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (14) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (15) BOUNDS(n^1, INF) ---------------------------------------- (16) Obligation: Innermost TRS: Rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 Lemmas: MIN(gen_0':s:c6:c7:c10:c119_16(n14_16), gen_0':s:c6:c7:c10:c119_16(n14_16)) -> gen_c:c1:c28_16(n14_16), rt in Omega(1 + n14_16) Generator Equations: gen_c:c1:c28_16(0) <=> c gen_c:c1:c28_16(+(x, 1)) <=> c2(gen_c:c1:c28_16(x)) gen_0':s:c6:c7:c10:c119_16(0) <=> 0' gen_0':s:c6:c7:c10:c119_16(+(x, 1)) <=> s(gen_0':s:c6:c7:c10:c119_16(x)) gen_c3:c4:c510_16(0) <=> c3 gen_c3:c4:c510_16(+(x, 1)) <=> c5(gen_c3:c4:c510_16(x)) gen_c8:c911_16(0) <=> c8 gen_c8:c911_16(+(x, 1)) <=> c9(gen_c8:c911_16(x)) gen_c13:c14:c1512_16(0) <=> hole_c13:c14:c156_16 gen_c13:c14:c1512_16(+(x, 1)) <=> c13(gen_c13:c14:c1512_16(x), c8, c) The following defined symbols remain to be analysed: MAX, +', -', *', F, -, min, max, f They will be analysed ascendingly in the following order: MAX < F +' < *' -' < F *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (17) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MAX(gen_0':s:c6:c7:c10:c119_16(n588_16), gen_0':s:c6:c7:c10:c119_16(n588_16)) -> gen_c3:c4:c510_16(n588_16), rt in Omega(1 + n588_16) Induction Base: MAX(gen_0':s:c6:c7:c10:c119_16(0), gen_0':s:c6:c7:c10:c119_16(0)) ->_R^Omega(1) c3 Induction Step: MAX(gen_0':s:c6:c7:c10:c119_16(+(n588_16, 1)), gen_0':s:c6:c7:c10:c119_16(+(n588_16, 1))) ->_R^Omega(1) c5(MAX(gen_0':s:c6:c7:c10:c119_16(n588_16), gen_0':s:c6:c7:c10:c119_16(n588_16))) ->_IH c5(gen_c3:c4:c510_16(c589_16)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (18) Obligation: Innermost TRS: Rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 Lemmas: MIN(gen_0':s:c6:c7:c10:c119_16(n14_16), gen_0':s:c6:c7:c10:c119_16(n14_16)) -> gen_c:c1:c28_16(n14_16), rt in Omega(1 + n14_16) MAX(gen_0':s:c6:c7:c10:c119_16(n588_16), gen_0':s:c6:c7:c10:c119_16(n588_16)) -> gen_c3:c4:c510_16(n588_16), rt in Omega(1 + n588_16) Generator Equations: gen_c:c1:c28_16(0) <=> c gen_c:c1:c28_16(+(x, 1)) <=> c2(gen_c:c1:c28_16(x)) gen_0':s:c6:c7:c10:c119_16(0) <=> 0' gen_0':s:c6:c7:c10:c119_16(+(x, 1)) <=> s(gen_0':s:c6:c7:c10:c119_16(x)) gen_c3:c4:c510_16(0) <=> c3 gen_c3:c4:c510_16(+(x, 1)) <=> c5(gen_c3:c4:c510_16(x)) gen_c8:c911_16(0) <=> c8 gen_c8:c911_16(+(x, 1)) <=> c9(gen_c8:c911_16(x)) gen_c13:c14:c1512_16(0) <=> hole_c13:c14:c156_16 gen_c13:c14:c1512_16(+(x, 1)) <=> c13(gen_c13:c14:c1512_16(x), c8, c) The following defined symbols remain to be analysed: +', -', *', F, -, min, max, f They will be analysed ascendingly in the following order: +' < *' -' < F *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (19) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: +'(gen_0':s:c6:c7:c10:c119_16(+(1, n1237_16)), gen_0':s:c6:c7:c10:c119_16(b)) -> *13_16, rt in Omega(n1237_16) Induction Base: +'(gen_0':s:c6:c7:c10:c119_16(+(1, 0)), gen_0':s:c6:c7:c10:c119_16(b)) Induction Step: +'(gen_0':s:c6:c7:c10:c119_16(+(1, +(n1237_16, 1))), gen_0':s:c6:c7:c10:c119_16(b)) ->_R^Omega(1) c7(+'(gen_0':s:c6:c7:c10:c119_16(+(1, n1237_16)), gen_0':s:c6:c7:c10:c119_16(b))) ->_IH c7(*13_16) 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: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 Lemmas: MIN(gen_0':s:c6:c7:c10:c119_16(n14_16), gen_0':s:c6:c7:c10:c119_16(n14_16)) -> gen_c:c1:c28_16(n14_16), rt in Omega(1 + n14_16) MAX(gen_0':s:c6:c7:c10:c119_16(n588_16), gen_0':s:c6:c7:c10:c119_16(n588_16)) -> gen_c3:c4:c510_16(n588_16), rt in Omega(1 + n588_16) +'(gen_0':s:c6:c7:c10:c119_16(+(1, n1237_16)), gen_0':s:c6:c7:c10:c119_16(b)) -> *13_16, rt in Omega(n1237_16) Generator Equations: gen_c:c1:c28_16(0) <=> c gen_c:c1:c28_16(+(x, 1)) <=> c2(gen_c:c1:c28_16(x)) gen_0':s:c6:c7:c10:c119_16(0) <=> 0' gen_0':s:c6:c7:c10:c119_16(+(x, 1)) <=> s(gen_0':s:c6:c7:c10:c119_16(x)) gen_c3:c4:c510_16(0) <=> c3 gen_c3:c4:c510_16(+(x, 1)) <=> c5(gen_c3:c4:c510_16(x)) gen_c8:c911_16(0) <=> c8 gen_c8:c911_16(+(x, 1)) <=> c9(gen_c8:c911_16(x)) gen_c13:c14:c1512_16(0) <=> hole_c13:c14:c156_16 gen_c13:c14:c1512_16(+(x, 1)) <=> c13(gen_c13:c14:c1512_16(x), c8, c) The following defined symbols remain to be analysed: -', *', F, -, min, max, f They will be analysed ascendingly in the following order: -' < F *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (21) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: -'(gen_0':s:c6:c7:c10:c119_16(n3887_16), gen_0':s:c6:c7:c10:c119_16(n3887_16)) -> gen_c8:c911_16(n3887_16), rt in Omega(1 + n3887_16) Induction Base: -'(gen_0':s:c6:c7:c10:c119_16(0), gen_0':s:c6:c7:c10:c119_16(0)) ->_R^Omega(1) c8 Induction Step: -'(gen_0':s:c6:c7:c10:c119_16(+(n3887_16, 1)), gen_0':s:c6:c7:c10:c119_16(+(n3887_16, 1))) ->_R^Omega(1) c9(-'(gen_0':s:c6:c7:c10:c119_16(n3887_16), gen_0':s:c6:c7:c10:c119_16(n3887_16))) ->_IH c9(gen_c8:c911_16(c3888_16)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (22) Obligation: Innermost TRS: Rules: MIN(0', z0) -> c MIN(z0, 0') -> c1 MIN(s(z0), s(z1)) -> c2(MIN(z0, z1)) MAX(0', z0) -> c3 MAX(z0, 0') -> c4 MAX(s(z0), s(z1)) -> c5(MAX(z0, z1)) +'(0', z0) -> c6 +'(s(z0), z1) -> c7(+'(z0, z1)) -'(z0, 0') -> c8 -'(s(z0), s(z1)) -> c9(-'(z0, z1)) *'(z0, 0') -> c10 *'(z0, s(z1)) -> c11(+'(z0, *'(z0, z1)), *'(z0, z1)) P(s(z0)) -> c12 F(s(z0), s(z1)) -> c13(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MIN(s(z0), s(z1))) F(s(z0), s(z1)) -> c14(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), -'(min(s(z0), s(z1)), max(s(z0), s(z1))), MAX(s(z0), s(z1))) F(s(z0), s(z1)) -> c15(F(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))), *'(s(z0), s(z1))) min(0', z0) -> 0' min(z0, 0') -> 0' min(s(z0), s(z1)) -> s(min(z0, z1)) max(0', z0) -> z0 max(z0, 0') -> z0 max(s(z0), s(z1)) -> s(max(z0, z1)) +'(0', z0) -> z0 +'(s(z0), z1) -> s(+'(z0, z1)) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(z0, *'(z0, z1)) p(s(z0)) -> z0 f(s(z0), s(z1)) -> f(-(min(s(z0), s(z1)), max(s(z0), s(z1))), *'(s(z0), s(z1))) Types: MIN :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c:c1:c2 0' :: 0':s:c6:c7:c10:c11 c :: c:c1:c2 c1 :: c:c1:c2 s :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c2 :: c:c1:c2 -> c:c1:c2 MAX :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c3:c4:c5 c3 :: c3:c4:c5 c4 :: c3:c4:c5 c5 :: c3:c4:c5 -> c3:c4:c5 +' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c6 :: 0':s:c6:c7:c10:c11 c7 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c8:c9 c8 :: c8:c9 c9 :: c8:c9 -> c8:c9 *' :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c10 :: 0':s:c6:c7:c10:c11 c11 :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 P :: 0':s:c6:c7:c10:c11 -> c12 c12 :: c12 F :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 c13 :: c13:c14:c15 -> c8:c9 -> c:c1:c2 -> c13:c14:c15 - :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 min :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 max :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 c14 :: c13:c14:c15 -> c8:c9 -> c3:c4:c5 -> c13:c14:c15 c15 :: c13:c14:c15 -> 0':s:c6:c7:c10:c11 -> c13:c14:c15 p :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 f :: 0':s:c6:c7:c10:c11 -> 0':s:c6:c7:c10:c11 -> f hole_c:c1:c21_16 :: c:c1:c2 hole_0':s:c6:c7:c10:c112_16 :: 0':s:c6:c7:c10:c11 hole_c3:c4:c53_16 :: c3:c4:c5 hole_c8:c94_16 :: c8:c9 hole_c125_16 :: c12 hole_c13:c14:c156_16 :: c13:c14:c15 hole_f7_16 :: f gen_c:c1:c28_16 :: Nat -> c:c1:c2 gen_0':s:c6:c7:c10:c119_16 :: Nat -> 0':s:c6:c7:c10:c11 gen_c3:c4:c510_16 :: Nat -> c3:c4:c5 gen_c8:c911_16 :: Nat -> c8:c9 gen_c13:c14:c1512_16 :: Nat -> c13:c14:c15 Lemmas: MIN(gen_0':s:c6:c7:c10:c119_16(n14_16), gen_0':s:c6:c7:c10:c119_16(n14_16)) -> gen_c:c1:c28_16(n14_16), rt in Omega(1 + n14_16) MAX(gen_0':s:c6:c7:c10:c119_16(n588_16), gen_0':s:c6:c7:c10:c119_16(n588_16)) -> gen_c3:c4:c510_16(n588_16), rt in Omega(1 + n588_16) +'(gen_0':s:c6:c7:c10:c119_16(+(1, n1237_16)), gen_0':s:c6:c7:c10:c119_16(b)) -> *13_16, rt in Omega(n1237_16) -'(gen_0':s:c6:c7:c10:c119_16(n3887_16), gen_0':s:c6:c7:c10:c119_16(n3887_16)) -> gen_c8:c911_16(n3887_16), rt in Omega(1 + n3887_16) Generator Equations: gen_c:c1:c28_16(0) <=> c gen_c:c1:c28_16(+(x, 1)) <=> c2(gen_c:c1:c28_16(x)) gen_0':s:c6:c7:c10:c119_16(0) <=> 0' gen_0':s:c6:c7:c10:c119_16(+(x, 1)) <=> s(gen_0':s:c6:c7:c10:c119_16(x)) gen_c3:c4:c510_16(0) <=> c3 gen_c3:c4:c510_16(+(x, 1)) <=> c5(gen_c3:c4:c510_16(x)) gen_c8:c911_16(0) <=> c8 gen_c8:c911_16(+(x, 1)) <=> c9(gen_c8:c911_16(x)) gen_c13:c14:c1512_16(0) <=> hole_c13:c14:c156_16 gen_c13:c14:c1512_16(+(x, 1)) <=> c13(gen_c13:c14:c1512_16(x), c8, c) The following defined symbols remain to be analysed: *', F, -, min, max, f They will be analysed ascendingly in the following order: *' < F *' < f - < F min < F max < F - < f min < f max < f ---------------------------------------- (23) RewriteLemmaProof (FINISHED) Proved the following rewrite lemma: *'(gen_0':s:c6:c7:c10:c119_16(a), gen_0':s:c6:c7:c10:c119_16(+(1, n4679_16))) -> *13_16, rt in Omega(EXP) Induction Base: *'(gen_0':s:c6:c7:c10:c119_16(a), gen_0':s:c6:c7:c10:c119_16(+(1, 0))) Induction Step: *'(gen_0':s:c6:c7:c10:c119_16(a), gen_0':s:c6:c7:c10:c119_16(+(1, +(n4679_16, 1)))) ->_R^Omega(1) c11(+'(gen_0':s:c6:c7:c10:c119_16(a), *'(gen_0':s:c6:c7:c10:c119_16(a), gen_0':s:c6:c7:c10:c119_16(+(1, n4679_16)))), *'(gen_0':s:c6:c7:c10:c119_16(a), gen_0':s:c6:c7:c10:c119_16(+(1, n4679_16)))) ->_IH c11(+'(gen_0':s:c6:c7:c10:c119_16(a), *13_16), *'(gen_0':s:c6:c7:c10:c119_16(a), gen_0':s:c6:c7:c10:c119_16(+(1, n4679_16)))) ->_IH c11(+'(gen_0':s:c6:c7:c10:c119_16(a), *13_16), *13_16) We have rt in EXP and sz in O(n). Thus, we have irc_R in EXP ---------------------------------------- (24) BOUNDS(EXP, INF)