WORST_CASE(NON_POLY,?) proof of input_yUS2VtJBKw.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 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), 0 ms] (8) typed CpxTrs (9) OrderProof [LOWER BOUND(ID), 7 ms] (10) typed CpxTrs (11) RewriteLemmaProof [LOWER BOUND(ID), 1972 ms] (12) BEST (13) proven lower bound (14) LowerBoundPropagationProof [FINISHED, 0 ms] (15) BOUNDS(n^1, INF) (16) typed CpxTrs (17) RewriteLemmaProof [FINISHED, 355 ms] (18) 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: +(x, 0) -> x +(x, s(y)) -> s(+(x, y)) *(x, 0) -> 0 *(x, s(y)) -> +(*(x, y), x) ge(x, 0) -> true ge(0, s(y)) -> false ge(s(x), s(y)) -> ge(x, y) -(x, 0) -> x -(s(x), s(y)) -> -(x, y) fact(x) -> iffact(x, ge(x, s(s(0)))) iffact(x, true) -> *(x, fact(-(x, s(0)))) iffact(x, false) -> s(0) 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: +(z0, 0) -> z0 +(z0, s(z1)) -> s(+(z0, z1)) *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0)))) iffact(z0, true) -> *(z0, fact(-(z0, s(0)))) iffact(z0, false) -> s(0) Tuples: +'(z0, 0) -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0) -> c2 *'(z0, s(z1)) -> c3(+'(*(z0, z1), z0), *'(z0, z1)) GE(z0, 0) -> c4 GE(0, s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0) -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0)))), GE(z0, s(s(0)))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0)))), FACT(-(z0, s(0))), -'(z0, s(0))) IFFACT(z0, false) -> c11 S tuples: +'(z0, 0) -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0) -> c2 *'(z0, s(z1)) -> c3(+'(*(z0, z1), z0), *'(z0, z1)) GE(z0, 0) -> c4 GE(0, s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0) -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0)))), GE(z0, s(s(0)))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0)))), FACT(-(z0, s(0))), -'(z0, s(0))) IFFACT(z0, false) -> c11 K tuples:none Defined Rule Symbols: +_2, *_2, ge_2, -_2, fact_1, iffact_2 Defined Pair Symbols: +'_2, *'_2, GE_2, -'_2, FACT_1, IFFACT_2 Compound Symbols: c, c1_1, c2, c3_2, c4, c5, c6_1, c7, c8_1, c9_2, c10_3, c11 ---------------------------------------- (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: +'(z0, 0) -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0) -> c2 *'(z0, s(z1)) -> c3(+'(*(z0, z1), z0), *'(z0, z1)) GE(z0, 0) -> c4 GE(0, s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0) -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0)))), GE(z0, s(s(0)))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0)))), FACT(-(z0, s(0))), -'(z0, s(0))) IFFACT(z0, false) -> c11 The (relative) TRS S consists of the following rules: +(z0, 0) -> z0 +(z0, s(z1)) -> s(+(z0, z1)) *(z0, 0) -> 0 *(z0, s(z1)) -> +(*(z0, z1), z0) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0) -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0)))) iffact(z0, true) -> *(z0, fact(-(z0, s(0)))) iffact(z0, false) -> s(0) 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: +'(z0, 0') -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0') -> c2 *'(z0, s(z1)) -> c3(+'(*'(z0, z1), z0), *'(z0, z1)) GE(z0, 0') -> c4 GE(0', s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0') -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0')))), GE(z0, s(s(0')))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0')))), FACT(-(z0, s(0'))), -'(z0, s(0'))) IFFACT(z0, false) -> c11 The (relative) TRS S consists of the following rules: +'(z0, 0') -> z0 +'(z0, s(z1)) -> s(+'(z0, z1)) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(*'(z0, z1), z0) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0')))) iffact(z0, true) -> *'(z0, fact(-(z0, s(0')))) iffact(z0, false) -> s(0') Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (8) Obligation: Innermost TRS: Rules: +'(z0, 0') -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0') -> c2 *'(z0, s(z1)) -> c3(+'(*'(z0, z1), z0), *'(z0, z1)) GE(z0, 0') -> c4 GE(0', s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0') -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0')))), GE(z0, s(s(0')))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0')))), FACT(-(z0, s(0'))), -'(z0, s(0'))) IFFACT(z0, false) -> c11 +'(z0, 0') -> z0 +'(z0, s(z1)) -> s(+'(z0, z1)) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(*'(z0, z1), z0) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0')))) iffact(z0, true) -> *'(z0, fact(-(z0, s(0')))) iffact(z0, false) -> s(0') Types: +' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 0' :: 0':c:s:c1:c2:c3 c :: 0':c:s:c1:c2:c3 s :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c1 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 *' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c2 :: 0':c:s:c1:c2:c3 c3 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 GE :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 -' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c7:c8 c7 :: c7:c8 c8 :: c7:c8 -> c7:c8 FACT :: 0':c:s:c1:c2:c3 -> c9 c9 :: c10:c11 -> c4:c5:c6 -> c9 IFFACT :: 0':c:s:c1:c2:c3 -> true:false -> c10:c11 ge :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> true:false true :: true:false c10 :: 0':c:s:c1:c2:c3 -> c9 -> c7:c8 -> c10:c11 fact :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 - :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 false :: true:false c11 :: c10:c11 iffact :: 0':c:s:c1:c2:c3 -> true:false -> 0':c:s:c1:c2:c3 hole_0':c:s:c1:c2:c31_12 :: 0':c:s:c1:c2:c3 hole_c4:c5:c62_12 :: c4:c5:c6 hole_c7:c83_12 :: c7:c8 hole_c94_12 :: c9 hole_c10:c115_12 :: c10:c11 hole_true:false6_12 :: true:false gen_0':c:s:c1:c2:c37_12 :: Nat -> 0':c:s:c1:c2:c3 gen_c4:c5:c68_12 :: Nat -> c4:c5:c6 gen_c7:c89_12 :: Nat -> c7:c8 ---------------------------------------- (9) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: +', *', GE, -', FACT, ge, fact, - They will be analysed ascendingly in the following order: +' < *' *' < FACT *' < fact GE < FACT -' < FACT ge < FACT fact < FACT - < FACT ge < fact - < fact ---------------------------------------- (10) Obligation: Innermost TRS: Rules: +'(z0, 0') -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0') -> c2 *'(z0, s(z1)) -> c3(+'(*'(z0, z1), z0), *'(z0, z1)) GE(z0, 0') -> c4 GE(0', s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0') -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0')))), GE(z0, s(s(0')))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0')))), FACT(-(z0, s(0'))), -'(z0, s(0'))) IFFACT(z0, false) -> c11 +'(z0, 0') -> z0 +'(z0, s(z1)) -> s(+'(z0, z1)) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(*'(z0, z1), z0) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0')))) iffact(z0, true) -> *'(z0, fact(-(z0, s(0')))) iffact(z0, false) -> s(0') Types: +' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 0' :: 0':c:s:c1:c2:c3 c :: 0':c:s:c1:c2:c3 s :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c1 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 *' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c2 :: 0':c:s:c1:c2:c3 c3 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 GE :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 -' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c7:c8 c7 :: c7:c8 c8 :: c7:c8 -> c7:c8 FACT :: 0':c:s:c1:c2:c3 -> c9 c9 :: c10:c11 -> c4:c5:c6 -> c9 IFFACT :: 0':c:s:c1:c2:c3 -> true:false -> c10:c11 ge :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> true:false true :: true:false c10 :: 0':c:s:c1:c2:c3 -> c9 -> c7:c8 -> c10:c11 fact :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 - :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 false :: true:false c11 :: c10:c11 iffact :: 0':c:s:c1:c2:c3 -> true:false -> 0':c:s:c1:c2:c3 hole_0':c:s:c1:c2:c31_12 :: 0':c:s:c1:c2:c3 hole_c4:c5:c62_12 :: c4:c5:c6 hole_c7:c83_12 :: c7:c8 hole_c94_12 :: c9 hole_c10:c115_12 :: c10:c11 hole_true:false6_12 :: true:false gen_0':c:s:c1:c2:c37_12 :: Nat -> 0':c:s:c1:c2:c3 gen_c4:c5:c68_12 :: Nat -> c4:c5:c6 gen_c7:c89_12 :: Nat -> c7:c8 Generator Equations: gen_0':c:s:c1:c2:c37_12(0) <=> 0' gen_0':c:s:c1:c2:c37_12(+(x, 1)) <=> s(gen_0':c:s:c1:c2:c37_12(x)) gen_c4:c5:c68_12(0) <=> c4 gen_c4:c5:c68_12(+(x, 1)) <=> c6(gen_c4:c5:c68_12(x)) gen_c7:c89_12(0) <=> c7 gen_c7:c89_12(+(x, 1)) <=> c8(gen_c7:c89_12(x)) The following defined symbols remain to be analysed: +', *', GE, -', FACT, ge, fact, - They will be analysed ascendingly in the following order: +' < *' *' < FACT *' < fact GE < FACT -' < FACT ge < FACT fact < FACT - < FACT ge < fact - < fact ---------------------------------------- (11) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: +'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n11_12))) -> *10_12, rt in Omega(n11_12) Induction Base: +'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, 0))) Induction Step: +'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, +(n11_12, 1)))) ->_R^Omega(1) c1(+'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n11_12)))) ->_IH c1(*10_12) 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: +'(z0, 0') -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0') -> c2 *'(z0, s(z1)) -> c3(+'(*'(z0, z1), z0), *'(z0, z1)) GE(z0, 0') -> c4 GE(0', s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0') -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0')))), GE(z0, s(s(0')))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0')))), FACT(-(z0, s(0'))), -'(z0, s(0'))) IFFACT(z0, false) -> c11 +'(z0, 0') -> z0 +'(z0, s(z1)) -> s(+'(z0, z1)) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(*'(z0, z1), z0) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0')))) iffact(z0, true) -> *'(z0, fact(-(z0, s(0')))) iffact(z0, false) -> s(0') Types: +' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 0' :: 0':c:s:c1:c2:c3 c :: 0':c:s:c1:c2:c3 s :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c1 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 *' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c2 :: 0':c:s:c1:c2:c3 c3 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 GE :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 -' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c7:c8 c7 :: c7:c8 c8 :: c7:c8 -> c7:c8 FACT :: 0':c:s:c1:c2:c3 -> c9 c9 :: c10:c11 -> c4:c5:c6 -> c9 IFFACT :: 0':c:s:c1:c2:c3 -> true:false -> c10:c11 ge :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> true:false true :: true:false c10 :: 0':c:s:c1:c2:c3 -> c9 -> c7:c8 -> c10:c11 fact :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 - :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 false :: true:false c11 :: c10:c11 iffact :: 0':c:s:c1:c2:c3 -> true:false -> 0':c:s:c1:c2:c3 hole_0':c:s:c1:c2:c31_12 :: 0':c:s:c1:c2:c3 hole_c4:c5:c62_12 :: c4:c5:c6 hole_c7:c83_12 :: c7:c8 hole_c94_12 :: c9 hole_c10:c115_12 :: c10:c11 hole_true:false6_12 :: true:false gen_0':c:s:c1:c2:c37_12 :: Nat -> 0':c:s:c1:c2:c3 gen_c4:c5:c68_12 :: Nat -> c4:c5:c6 gen_c7:c89_12 :: Nat -> c7:c8 Generator Equations: gen_0':c:s:c1:c2:c37_12(0) <=> 0' gen_0':c:s:c1:c2:c37_12(+(x, 1)) <=> s(gen_0':c:s:c1:c2:c37_12(x)) gen_c4:c5:c68_12(0) <=> c4 gen_c4:c5:c68_12(+(x, 1)) <=> c6(gen_c4:c5:c68_12(x)) gen_c7:c89_12(0) <=> c7 gen_c7:c89_12(+(x, 1)) <=> c8(gen_c7:c89_12(x)) The following defined symbols remain to be analysed: +', *', GE, -', FACT, ge, fact, - They will be analysed ascendingly in the following order: +' < *' *' < FACT *' < fact GE < FACT -' < FACT ge < FACT fact < FACT - < FACT ge < fact - < fact ---------------------------------------- (14) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (15) BOUNDS(n^1, INF) ---------------------------------------- (16) Obligation: Innermost TRS: Rules: +'(z0, 0') -> c +'(z0, s(z1)) -> c1(+'(z0, z1)) *'(z0, 0') -> c2 *'(z0, s(z1)) -> c3(+'(*'(z0, z1), z0), *'(z0, z1)) GE(z0, 0') -> c4 GE(0', s(z0)) -> c5 GE(s(z0), s(z1)) -> c6(GE(z0, z1)) -'(z0, 0') -> c7 -'(s(z0), s(z1)) -> c8(-'(z0, z1)) FACT(z0) -> c9(IFFACT(z0, ge(z0, s(s(0')))), GE(z0, s(s(0')))) IFFACT(z0, true) -> c10(*'(z0, fact(-(z0, s(0')))), FACT(-(z0, s(0'))), -'(z0, s(0'))) IFFACT(z0, false) -> c11 +'(z0, 0') -> z0 +'(z0, s(z1)) -> s(+'(z0, z1)) *'(z0, 0') -> 0' *'(z0, s(z1)) -> +'(*'(z0, z1), z0) ge(z0, 0') -> true ge(0', s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) -(z0, 0') -> z0 -(s(z0), s(z1)) -> -(z0, z1) fact(z0) -> iffact(z0, ge(z0, s(s(0')))) iffact(z0, true) -> *'(z0, fact(-(z0, s(0')))) iffact(z0, false) -> s(0') Types: +' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 0' :: 0':c:s:c1:c2:c3 c :: 0':c:s:c1:c2:c3 s :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c1 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 *' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 c2 :: 0':c:s:c1:c2:c3 c3 :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 GE :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 -' :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> c7:c8 c7 :: c7:c8 c8 :: c7:c8 -> c7:c8 FACT :: 0':c:s:c1:c2:c3 -> c9 c9 :: c10:c11 -> c4:c5:c6 -> c9 IFFACT :: 0':c:s:c1:c2:c3 -> true:false -> c10:c11 ge :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> true:false true :: true:false c10 :: 0':c:s:c1:c2:c3 -> c9 -> c7:c8 -> c10:c11 fact :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 - :: 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 -> 0':c:s:c1:c2:c3 false :: true:false c11 :: c10:c11 iffact :: 0':c:s:c1:c2:c3 -> true:false -> 0':c:s:c1:c2:c3 hole_0':c:s:c1:c2:c31_12 :: 0':c:s:c1:c2:c3 hole_c4:c5:c62_12 :: c4:c5:c6 hole_c7:c83_12 :: c7:c8 hole_c94_12 :: c9 hole_c10:c115_12 :: c10:c11 hole_true:false6_12 :: true:false gen_0':c:s:c1:c2:c37_12 :: Nat -> 0':c:s:c1:c2:c3 gen_c4:c5:c68_12 :: Nat -> c4:c5:c6 gen_c7:c89_12 :: Nat -> c7:c8 Lemmas: +'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n11_12))) -> *10_12, rt in Omega(n11_12) Generator Equations: gen_0':c:s:c1:c2:c37_12(0) <=> 0' gen_0':c:s:c1:c2:c37_12(+(x, 1)) <=> s(gen_0':c:s:c1:c2:c37_12(x)) gen_c4:c5:c68_12(0) <=> c4 gen_c4:c5:c68_12(+(x, 1)) <=> c6(gen_c4:c5:c68_12(x)) gen_c7:c89_12(0) <=> c7 gen_c7:c89_12(+(x, 1)) <=> c8(gen_c7:c89_12(x)) The following defined symbols remain to be analysed: *', GE, -', FACT, ge, fact, - They will be analysed ascendingly in the following order: *' < FACT *' < fact GE < FACT -' < FACT ge < FACT fact < FACT - < FACT ge < fact - < fact ---------------------------------------- (17) RewriteLemmaProof (FINISHED) Proved the following rewrite lemma: *'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n2277_12))) -> *10_12, rt in Omega(EXP) Induction Base: *'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, 0))) Induction Step: *'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, +(n2277_12, 1)))) ->_R^Omega(1) c3(+'(*'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n2277_12))), gen_0':c:s:c1:c2:c37_12(a)), *'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n2277_12)))) ->_IH c3(+'(*10_12, gen_0':c:s:c1:c2:c37_12(a)), *'(gen_0':c:s:c1:c2:c37_12(a), gen_0':c:s:c1:c2:c37_12(+(1, n2277_12)))) ->_IH c3(+'(*10_12, gen_0':c:s:c1:c2:c37_12(a)), *10_12) We have rt in EXP and sz in O(n). Thus, we have irc_R in EXP ---------------------------------------- (18) BOUNDS(EXP, INF)