WORST_CASE(NON_POLY,?) proof of /export/starexec/sandbox/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(EXP, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 635 ms] (2) CpxRelTRS (3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxRelTRS (5) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (6) typed CpxTrs (7) OrderProof [LOWER BOUND(ID), 16 ms] (8) typed CpxTrs (9) RewriteLemmaProof [LOWER BOUND(ID), 319 ms] (10) BEST (11) proven lower bound (12) LowerBoundPropagationProof [FINISHED, 0 ms] (13) BOUNDS(n^1, INF) (14) typed CpxTrs (15) RewriteLemmaProof [LOWER BOUND(ID), 92 ms] (16) typed CpxTrs (17) RewriteLemmaProof [LOWER BOUND(ID), 2146 ms] (18) typed CpxTrs (19) RewriteLemmaProof [LOWER BOUND(ID), 65 ms] (20) typed CpxTrs (21) RewriteLemmaProof [FINISHED, 285 ms] (22) BOUNDS(EXP, INF) ---------------------------------------- (0) 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 ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) 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 ---------------------------------------- (3) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (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) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (6) 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 ---------------------------------------- (7) 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 ---------------------------------------- (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 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 ---------------------------------------- (9) 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). ---------------------------------------- (10) Complex Obligation (BEST) ---------------------------------------- (11) 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 ---------------------------------------- (12) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (13) BOUNDS(n^1, INF) ---------------------------------------- (14) 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 ---------------------------------------- (15) 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). ---------------------------------------- (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) 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 ---------------------------------------- (17) 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). ---------------------------------------- (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) +'(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 ---------------------------------------- (19) 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). ---------------------------------------- (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) -'(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 ---------------------------------------- (21) 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 ---------------------------------------- (22) BOUNDS(EXP, INF)