KILLED proof of input_dmPkop8uwa.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxTRS (5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedCompleteTrs (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (14) CpxRNTS (15) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRNTS (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) ResultPropagationProof [UPPER BOUND(ID), 3 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 326 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 119 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 266 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 55 ms] (30) CpxRNTS (31) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (32) CpxRNTS (33) IntTrsBoundProof [UPPER BOUND(ID), 2843 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 529 ms] (36) CpxRNTS (37) CompletionProof [UPPER BOUND(ID), 0 ms] (38) CpxTypedWeightedCompleteTrs (39) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (40) CpxRNTS (41) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (42) CdtProblem (43) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (48) CdtProblem (49) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (56) CdtProblem (57) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (60) CdtProblem (61) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 19 ms] (66) CdtProblem (67) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 24 ms] (68) CdtProblem (69) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CdtProblem (73) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CdtProblem (75) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 18 ms] (76) CdtProblem (77) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (78) CdtProblem (79) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (80) CdtProblem (81) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (82) CdtProblem (83) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CdtProblem (85) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (86) CdtProblem (87) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (88) CdtProblem (89) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (90) CdtProblem (91) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (92) CdtProblem (93) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (94) CdtProblem (95) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (96) CdtProblem (97) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (98) CdtProblem (99) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (100) CdtProblem (101) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (102) CdtProblem (103) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (104) CdtProblem (105) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (106) CdtProblem (107) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (108) CdtProblem (109) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (110) CdtProblem (111) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (112) CdtProblem (113) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (114) CdtProblem (115) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (116) CdtProblem (117) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (118) CdtProblem (119) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (120) CdtProblem (121) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (122) CdtProblem ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) generate(x, y) -> gen(x, y, 0) gen(x, y, z) -> if(ge(z, x), x, y, z) if(true, x, y, z) -> nil if(false, x, y, z) -> cons(y, gen(x, y, s(z))) sum(nil) -> 0 sum(cons(0, xs)) -> sum(xs) sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) ge(x, 0) -> true ge(0, s(y)) -> false ge(s(x), s(y)) -> ge(x, y) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) generate(x, y) -> gen(x, y, 0') gen(x, y, z) -> if(ge(z, x), x, y, z) if(true, x, y, z) -> nil if(false, x, y, z) -> cons(y, gen(x, y, s(z))) sum(nil) -> 0' sum(cons(0', xs)) -> sum(xs) sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) ge(x, 0') -> true ge(0', s(y)) -> false ge(s(x), s(y)) -> ge(x, y) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) generate(x, y) -> gen(x, y, 0) gen(x, y, z) -> if(ge(z, x), x, y, z) if(true, x, y, z) -> nil if(false, x, y, z) -> cons(y, gen(x, y, s(z))) sum(nil) -> 0 sum(cons(0, xs)) -> sum(xs) sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) ge(x, 0) -> true ge(0, s(y)) -> false ge(s(x), s(y)) -> ge(x, y) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) [1] generate(x, y) -> gen(x, y, 0) [1] gen(x, y, z) -> if(ge(z, x), x, y, z) [1] if(true, x, y, z) -> nil [1] if(false, x, y, z) -> cons(y, gen(x, y, s(z))) [1] sum(nil) -> 0 [1] sum(cons(0, xs)) -> sum(xs) [1] sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) [1] ge(x, 0) -> true [1] ge(0, s(y)) -> false [1] ge(s(x), s(y)) -> ge(x, y) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) [1] generate(x, y) -> gen(x, y, 0) [1] gen(x, y, z) -> if(ge(z, x), x, y, z) [1] if(true, x, y, z) -> nil [1] if(false, x, y, z) -> cons(y, gen(x, y, s(z))) [1] sum(nil) -> 0 [1] sum(cons(0, xs)) -> sum(xs) [1] sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) [1] ge(x, 0) -> true [1] ge(0, s(y)) -> false [1] ge(s(x), s(y)) -> ge(x, y) [1] The TRS has the following type information: times :: 0:s -> 0:s -> 0:s sum :: nil:cons -> 0:s generate :: 0:s -> 0:s -> nil:cons gen :: 0:s -> 0:s -> 0:s -> nil:cons 0 :: 0:s if :: true:false -> 0:s -> 0:s -> 0:s -> nil:cons ge :: 0:s -> 0:s -> true:false true :: true:false nil :: nil:cons false :: true:false cons :: 0:s -> nil:cons -> nil:cons s :: 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (9) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: times_2 sum_1 (c) The following functions are completely defined: ge_2 generate_2 gen_3 if_4 Due to the following rules being added: none And the following fresh constants: none ---------------------------------------- (10) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) [1] generate(x, y) -> gen(x, y, 0) [1] gen(x, y, z) -> if(ge(z, x), x, y, z) [1] if(true, x, y, z) -> nil [1] if(false, x, y, z) -> cons(y, gen(x, y, s(z))) [1] sum(nil) -> 0 [1] sum(cons(0, xs)) -> sum(xs) [1] sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) [1] ge(x, 0) -> true [1] ge(0, s(y)) -> false [1] ge(s(x), s(y)) -> ge(x, y) [1] The TRS has the following type information: times :: 0:s -> 0:s -> 0:s sum :: nil:cons -> 0:s generate :: 0:s -> 0:s -> nil:cons gen :: 0:s -> 0:s -> 0:s -> nil:cons 0 :: 0:s if :: true:false -> 0:s -> 0:s -> 0:s -> nil:cons ge :: 0:s -> 0:s -> true:false true :: true:false nil :: nil:cons false :: true:false cons :: 0:s -> nil:cons -> nil:cons s :: 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (11) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: times(x, y) -> sum(gen(x, y, 0)) [2] generate(x, y) -> gen(x, y, 0) [1] gen(0, y, z) -> if(true, 0, y, z) [2] gen(s(y'), y, 0) -> if(false, s(y'), y, 0) [2] gen(s(y''), y, s(x')) -> if(ge(x', y''), s(y''), y, s(x')) [2] if(true, x, y, z) -> nil [1] if(false, x, y, z) -> cons(y, gen(x, y, s(z))) [1] sum(nil) -> 0 [1] sum(cons(0, xs)) -> sum(xs) [1] sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) [1] ge(x, 0) -> true [1] ge(0, s(y)) -> false [1] ge(s(x), s(y)) -> ge(x, y) [1] The TRS has the following type information: times :: 0:s -> 0:s -> 0:s sum :: nil:cons -> 0:s generate :: 0:s -> 0:s -> nil:cons gen :: 0:s -> 0:s -> 0:s -> nil:cons 0 :: 0:s if :: true:false -> 0:s -> 0:s -> 0:s -> nil:cons ge :: 0:s -> 0:s -> true:false true :: true:false nil :: nil:cons false :: true:false cons :: 0:s -> nil:cons -> nil:cons s :: 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 true => 1 nil => 0 false => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' = x, x >= 0 ge(z', z'') -{ 1 }-> 0 :|: y >= 0, z'' = 1 + y, z' = 0 gen(z', z'', z1) -{ 2 }-> if(ge(x', y''), 1 + y'', y, 1 + x') :|: z' = 1 + y'', z'' = y, y >= 0, x' >= 0, y'' >= 0, z1 = 1 + x' gen(z', z'', z1) -{ 2 }-> if(1, 0, y, z) :|: z1 = z, z >= 0, z'' = y, y >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + y', y, 0) :|: z1 = 0, z'' = y, y >= 0, y' >= 0, z' = 1 + y' generate(z', z'') -{ 1 }-> gen(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + y + gen(x, y, 1 + z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0 sum(z') -{ 1 }-> sum(xs) :|: xs >= 0, z' = 1 + 0 + xs sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(x, y, 0)) :|: z' = x, z'' = y, x >= 0, y >= 0 ---------------------------------------- (15) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(ge(z1 - 1, z' - 1), 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { ge } { sum } { if, gen } { generate } { times } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(ge(z1 - 1, z' - 1), 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {ge}, {sum}, {if,gen}, {generate}, {times} ---------------------------------------- (19) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(ge(z1 - 1, z' - 1), 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {ge}, {sum}, {if,gen}, {generate}, {times} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: ge after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(ge(z1 - 1, z' - 1), 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {ge}, {sum}, {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: ?, size: O(1) [1] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: ge after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 2 + z'' ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(z' - 1, z'' - 1) :|: z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(ge(z1 - 1, z' - 1), 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {sum}, {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] ---------------------------------------- (25) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 2 + z'' }-> s' :|: s' >= 0, s' <= 1, z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 3 + z' }-> if(s, 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: s >= 0, s <= 1, z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {sum}, {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: sum after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 2 + z'' }-> s' :|: s' >= 0, s' <= 1, z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 3 + z' }-> if(s, 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: s >= 0, s <= 1, z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {sum}, {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] sum: runtime: ?, size: O(n^1) [z'] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: sum after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z' ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 2 + z'' }-> s' :|: s' >= 0, s' <= 1, z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 3 + z' }-> if(s, 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: s >= 0, s <= 1, z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 }-> sum(z' - 1) :|: z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] sum: runtime: O(n^1) [1 + z'], size: O(n^1) [z'] ---------------------------------------- (31) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (32) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 2 + z'' }-> s' :|: s' >= 0, s' <= 1, z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 3 + z' }-> if(s, 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: s >= 0, s <= 1, z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 + z' }-> s'' :|: s'' >= 0, s'' <= z' - 1, z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 3 + x + xs }-> 1 + s1 :|: s1 >= 0, s1 <= 1 + x + xs, xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] sum: runtime: O(n^1) [1 + z'], size: O(n^1) [z'] ---------------------------------------- (33) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: if after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? Computed SIZE bound using CoFloCo for: gen after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 2 + z'' }-> s' :|: s' >= 0, s' <= 1, z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 3 + z' }-> if(s, 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: s >= 0, s <= 1, z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 + z' }-> s'' :|: s'' >= 0, s'' <= z' - 1, z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 3 + x + xs }-> 1 + s1 :|: s1 >= 0, s1 <= 1 + x + xs, xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] sum: runtime: O(n^1) [1 + z'], size: O(n^1) [z'] if: runtime: ?, size: INF gen: runtime: ?, size: INF ---------------------------------------- (35) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: if after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 2 + z'' }-> s' :|: s' >= 0, s' <= 1, z' - 1 >= 0, z'' - 1 >= 0 ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' >= 0 ge(z', z'') -{ 1 }-> 0 :|: z'' - 1 >= 0, z' = 0 gen(z', z'', z1) -{ 3 + z' }-> if(s, 1 + (z' - 1), z'', 1 + (z1 - 1)) :|: s >= 0, s <= 1, z'' >= 0, z1 - 1 >= 0, z' - 1 >= 0 gen(z', z'', z1) -{ 2 }-> if(1, 0, z'', z1) :|: z1 >= 0, z'' >= 0, z' = 0 gen(z', z'', z1) -{ 2 }-> if(0, 1 + (z' - 1), z'', 0) :|: z1 = 0, z'' >= 0, z' - 1 >= 0 generate(z', z'') -{ 1 }-> gen(z', z'', 0) :|: z' >= 0, z'' >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + z1 + gen(z'', z1, 1 + z2) :|: z2 >= 0, z'' >= 0, z1 >= 0, z' = 0 sum(z') -{ 1 + z' }-> s'' :|: s'' >= 0, s'' <= z' - 1, z' - 1 >= 0 sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 3 + x + xs }-> 1 + s1 :|: s1 >= 0, s1 <= 1 + x + xs, xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 2 }-> sum(gen(z', z'', 0)) :|: z' >= 0, z'' >= 0 Function symbols to be analyzed: {if,gen}, {generate}, {times} Previous analysis results are: ge: runtime: O(n^1) [2 + z''], size: O(1) [1] sum: runtime: O(n^1) [1 + z'], size: O(n^1) [z'] if: runtime: INF, size: INF gen: runtime: ?, size: INF ---------------------------------------- (37) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: none And the following fresh constants: none ---------------------------------------- (38) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: times(x, y) -> sum(generate(x, y)) [1] generate(x, y) -> gen(x, y, 0) [1] gen(x, y, z) -> if(ge(z, x), x, y, z) [1] if(true, x, y, z) -> nil [1] if(false, x, y, z) -> cons(y, gen(x, y, s(z))) [1] sum(nil) -> 0 [1] sum(cons(0, xs)) -> sum(xs) [1] sum(cons(s(x), xs)) -> s(sum(cons(x, xs))) [1] ge(x, 0) -> true [1] ge(0, s(y)) -> false [1] ge(s(x), s(y)) -> ge(x, y) [1] The TRS has the following type information: times :: 0:s -> 0:s -> 0:s sum :: nil:cons -> 0:s generate :: 0:s -> 0:s -> nil:cons gen :: 0:s -> 0:s -> 0:s -> nil:cons 0 :: 0:s if :: true:false -> 0:s -> 0:s -> 0:s -> nil:cons ge :: 0:s -> 0:s -> true:false true :: true:false nil :: nil:cons false :: true:false cons :: 0:s -> nil:cons -> nil:cons s :: 0:s -> 0:s Rewrite Strategy: INNERMOST ---------------------------------------- (39) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 true => 1 nil => 0 false => 0 ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: ge(z', z'') -{ 1 }-> ge(x, y) :|: z' = 1 + x, x >= 0, y >= 0, z'' = 1 + y ge(z', z'') -{ 1 }-> 1 :|: z'' = 0, z' = x, x >= 0 ge(z', z'') -{ 1 }-> 0 :|: y >= 0, z'' = 1 + y, z' = 0 gen(z', z'', z1) -{ 1 }-> if(ge(z, x), x, y, z) :|: z1 = z, z >= 0, z' = x, z'' = y, x >= 0, y >= 0 generate(z', z'') -{ 1 }-> gen(x, y, 0) :|: z' = x, z'' = y, x >= 0, y >= 0 if(z', z'', z1, z2) -{ 1 }-> 0 :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 1 if(z', z'', z1, z2) -{ 1 }-> 1 + y + gen(x, y, 1 + z) :|: z1 = y, z >= 0, z2 = z, x >= 0, y >= 0, z'' = x, z' = 0 sum(z') -{ 1 }-> sum(xs) :|: xs >= 0, z' = 1 + 0 + xs sum(z') -{ 1 }-> 0 :|: z' = 0 sum(z') -{ 1 }-> 1 + sum(1 + x + xs) :|: xs >= 0, x >= 0, z' = 1 + (1 + x) + xs times(z', z'') -{ 1 }-> sum(generate(x, y)) :|: z' = x, z'' = y, x >= 0, y >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (41) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: times(z0, z1) -> sum(generate(z0, z1)) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) sum(nil) -> 0 sum(cons(0, z0)) -> sum(z0) sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1))) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) Tuples: TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1)) GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(true, z0, z1, z2) -> c3 IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(nil) -> c5 SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(z0, 0) -> c8 GE(0, s(z0)) -> c9 GE(s(z0), s(z1)) -> c10(GE(z0, z1)) S tuples: TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1)) GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(true, z0, z1, z2) -> c3 IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(nil) -> c5 SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(z0, 0) -> c8 GE(0, s(z0)) -> c9 GE(s(z0), s(z1)) -> c10(GE(z0, z1)) K tuples:none Defined Rule Symbols: times_2, generate_2, gen_3, if_4, sum_1, ge_2 Defined Pair Symbols: TIMES_2, GENERATE_2, GEN_3, IF_4, SUM_1, GE_2 Compound Symbols: c_2, c1_1, c2_2, c3, c4_1, c5, c6_1, c7_1, c8, c9, c10_1 ---------------------------------------- (43) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: GE(z0, 0) -> c8 IF(true, z0, z1, z2) -> c3 GE(0, s(z0)) -> c9 SUM(nil) -> c5 ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: times(z0, z1) -> sum(generate(z0, z1)) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) sum(nil) -> 0 sum(cons(0, z0)) -> sum(z0) sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1))) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) Tuples: TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1)) GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) S tuples: TIMES(z0, z1) -> c(SUM(generate(z0, z1)), GENERATE(z0, z1)) GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) K tuples:none Defined Rule Symbols: times_2, generate_2, gen_3, if_4, sum_1, ge_2 Defined Pair Symbols: TIMES_2, GENERATE_2, GEN_3, IF_4, SUM_1, GE_2 Compound Symbols: c_2, c1_1, c2_2, c4_1, c6_1, c7_1, c10_1 ---------------------------------------- (45) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: times(z0, z1) -> sum(generate(z0, z1)) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) sum(nil) -> 0 sum(cons(0, z0)) -> sum(z0) sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1))) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) Tuples: GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) TIMES(z0, z1) -> c3(GENERATE(z0, z1)) S tuples: GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) TIMES(z0, z1) -> c3(GENERATE(z0, z1)) K tuples:none Defined Rule Symbols: times_2, generate_2, gen_3, if_4, sum_1, ge_2 Defined Pair Symbols: GENERATE_2, GEN_3, IF_4, SUM_1, GE_2, TIMES_2 Compound Symbols: c1_1, c2_2, c4_1, c6_1, c7_1, c10_1, c3_1 ---------------------------------------- (47) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 2 leading nodes: TIMES(z0, z1) -> c3(GENERATE(z0, z1)) GENERATE(z0, z1) -> c1(GEN(z0, z1, 0)) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: times(z0, z1) -> sum(generate(z0, z1)) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) sum(nil) -> 0 sum(cons(0, z0)) -> sum(z0) sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1))) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) Tuples: GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) S tuples: GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) K tuples:none Defined Rule Symbols: times_2, generate_2, gen_3, if_4, sum_1, ge_2 Defined Pair Symbols: GEN_3, IF_4, SUM_1, GE_2, TIMES_2 Compound Symbols: c2_2, c4_1, c6_1, c7_1, c10_1, c3_1 ---------------------------------------- (49) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: times(z0, z1) -> sum(generate(z0, z1)) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) sum(nil) -> 0 sum(cons(0, z0)) -> sum(z0) sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1))) ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) Tuples: GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) S tuples: GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: times_2, generate_2, gen_3, if_4, sum_1, ge_2 Defined Pair Symbols: GEN_3, IF_4, SUM_1, GE_2, TIMES_2 Compound Symbols: c2_2, c4_1, c6_1, c7_1, c10_1, c3_1 ---------------------------------------- (51) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: times(z0, z1) -> sum(generate(z0, z1)) sum(nil) -> 0 sum(cons(0, z0)) -> sum(z0) sum(cons(s(z0), z1)) -> s(sum(cons(z0, z1))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) S tuples: GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, generate_2, gen_3, if_4 Defined Pair Symbols: GEN_3, IF_4, SUM_1, GE_2, TIMES_2 Compound Symbols: c2_2, c4_1, c6_1, c7_1, c10_1, c3_1 ---------------------------------------- (53) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace GEN(z0, z1, z2) -> c2(IF(ge(z2, z0), z0, z1, z2), GE(z2, z0)) by GEN(0, x1, z0) -> c2(IF(true, 0, x1, z0), GE(z0, 0)) GEN(s(z0), x1, 0) -> c2(IF(false, s(z0), x1, 0), GE(0, s(z0))) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(0, x1, z0) -> c2(IF(true, 0, x1, z0), GE(z0, 0)) GEN(s(z0), x1, 0) -> c2(IF(false, s(z0), x1, 0), GE(0, s(z0))) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(0, x1, z0) -> c2(IF(true, 0, x1, z0), GE(z0, 0)) GEN(s(z0), x1, 0) -> c2(IF(false, s(z0), x1, 0), GE(0, s(z0))) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, generate_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, TIMES_2, GEN_3 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c3_1, c2_2 ---------------------------------------- (55) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: GEN(s(z0), x1, 0) -> c2(IF(false, s(z0), x1, 0), GE(0, s(z0))) Removed 1 trailing nodes: GEN(0, x1, z0) -> c2(IF(true, 0, x1, z0), GE(z0, 0)) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, generate_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, TIMES_2, GEN_3 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c3_1, c2_2 ---------------------------------------- (57) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) by TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) generate(z0, z1) -> gen(z0, z1, 0) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, generate_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c3_1 ---------------------------------------- (59) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: generate(z0, z1) -> gen(z0, z1, 0) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c3_1 ---------------------------------------- (61) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace GEN(s(z1), x1, s(z0)) -> c2(IF(ge(z0, z1), s(z1), x1, s(z0)), GE(s(z0), s(z1))) by GEN(s(0), x1, s(z0)) -> c2(IF(true, s(0), x1, s(z0)), GE(s(z0), s(0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) GEN(s(0), x1, s(z0)) -> c2(IF(true, s(0), x1, s(z0)), GE(s(z0), s(0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(0), x1, s(z0)) -> c2(IF(true, s(0), x1, s(z0)), GE(s(z0), s(0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, TIMES_2, GEN_3 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c3_1, c2_2, c2_1 ---------------------------------------- (63) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, TIMES_2, GEN_3 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c3_1, c2_2, c2_1 ---------------------------------------- (65) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) We considered the (Usable) Rules:none And the Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(GE(x_1, x_2)) = 0 POL(GEN(x_1, x_2, x_3)) = x_1 POL(IF(x_1, x_2, x_3, x_4)) = x_2 POL(SUM(x_1)) = [1] POL(TIMES(x_1, x_2)) = [1] POL(c10(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c2(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 POL(false) = [1] POL(ge(x_1, x_2)) = [1] + x_2 POL(gen(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(if(x_1, x_2, x_3, x_4)) = [1] + x_1 + x_2 + x_3 + x_4 POL(nil) = [1] POL(s(x_1)) = x_1 POL(true) = [1] ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, TIMES_2, GEN_3 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c3_1, c2_2, c2_1 ---------------------------------------- (67) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) We considered the (Usable) Rules:none And the Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(GE(x_1, x_2)) = 0 POL(GEN(x_1, x_2, x_3)) = [1] + x_1 POL(IF(x_1, x_2, x_3, x_4)) = [1] + x_2 POL(SUM(x_1)) = [1] POL(TIMES(x_1, x_2)) = [1] POL(c10(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c2(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 POL(false) = [1] POL(ge(x_1, x_2)) = x_2 POL(gen(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(if(x_1, x_2, x_3, x_4)) = [1] + x_1 + x_2 + x_3 + x_4 POL(nil) = [1] POL(s(x_1)) = x_1 POL(true) = [1] ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, TIMES_2, GEN_3 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c3_1, c2_2, c2_1 ---------------------------------------- (69) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace TIMES(z0, z1) -> c3(SUM(gen(z0, z1, 0))) by TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c2_1, c3_1 ---------------------------------------- (71) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace GEN(s(s(z1)), x1, s(s(z0))) -> c2(IF(ge(z0, z1), s(s(z1)), x1, s(s(z0))), GE(s(s(z0)), s(s(z1)))) by GEN(s(s(0)), x1, s(s(z0))) -> c2(IF(true, s(s(0)), x1, s(s(z0))), GE(s(s(z0)), s(s(0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) GEN(s(s(0)), x1, s(s(z0))) -> c2(IF(true, s(s(0)), x1, s(s(z0))), GE(s(s(z0)), s(s(0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(IF(true, s(s(0)), x1, s(s(z0))), GE(s(s(z0)), s(s(0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c2_1, c3_1 ---------------------------------------- (73) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c2_1, c3_1 ---------------------------------------- (75) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) We considered the (Usable) Rules: ge(s(z0), s(z1)) -> ge(z0, z1) ge(0, s(z0)) -> false ge(z0, 0) -> true And the Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(GE(x_1, x_2)) = 0 POL(GEN(x_1, x_2, x_3)) = [1] + x_1 + x_3 POL(IF(x_1, x_2, x_3, x_4)) = x_1 + x_2 POL(SUM(x_1)) = [1] POL(TIMES(x_1, x_2)) = [1] POL(c10(x_1)) = x_1 POL(c2(x_1)) = x_1 POL(c2(x_1, x_2)) = x_1 + x_2 POL(c3(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(cons(x_1, x_2)) = x_1 POL(false) = [1] POL(ge(x_1, x_2)) = [1] POL(gen(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(if(x_1, x_2, x_3, x_4)) = x_2 + x_3 + x_4 POL(nil) = 0 POL(s(x_1)) = 0 POL(true) = [1] ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c2_1, c3_1 ---------------------------------------- (77) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace TIMES(z0, z1) -> c3(SUM(if(ge(0, z0), z0, z1, 0))) by TIMES(0, x1) -> c3(SUM(if(true, 0, x1, 0))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) TIMES(0, x1) -> c3(SUM(if(true, 0, x1, 0))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) S tuples: IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: IF_4, SUM_1, GE_2, GEN_3, TIMES_2 Compound Symbols: c4_1, c6_1, c7_1, c10_1, c2_2, c2_1, c3_1 ---------------------------------------- (79) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace IF(false, z0, z1, z2) -> c4(GEN(z0, z1, s(z2))) by IF(false, s(s(x0)), x1, s(0)) -> c4(GEN(s(s(x0)), x1, s(s(0)))) IF(false, s(s(s(x0))), x1, s(s(0))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) TIMES(0, x1) -> c3(SUM(if(true, 0, x1, 0))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) IF(false, s(s(x0)), x1, s(0)) -> c4(GEN(s(s(x0)), x1, s(s(0)))) IF(false, s(s(s(x0))), x1, s(s(0))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) IF(false, s(s(x0)), x1, s(0)) -> c4(GEN(s(s(x0)), x1, s(s(0)))) IF(false, s(s(s(x0))), x1, s(s(0))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) K tuples: TIMES(z0, z1) -> c3(SUM(generate(z0, z1))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_2, c2_1, c3_1, c4_1 ---------------------------------------- (81) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 6 leading nodes: GEN(s(s(z0)), x1, s(0)) -> c2(IF(false, s(s(z0)), x1, s(0)), GE(s(0), s(s(z0)))) IF(false, s(s(x0)), x1, s(0)) -> c4(GEN(s(s(x0)), x1, s(s(0)))) GEN(s(s(s(z0))), x1, s(s(0))) -> c2(IF(false, s(s(s(z0))), x1, s(s(0))), GE(s(s(0)), s(s(s(z0))))) IF(false, s(s(s(x0))), x1, s(s(0))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(0))))) GEN(s(0), x1, s(z0)) -> c2(GE(s(z0), s(0))) GEN(s(s(0)), x1, s(s(z0))) -> c2(GE(s(s(z0)), s(s(0)))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) TIMES(0, x1) -> c3(SUM(if(true, 0, x1, 0))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) K tuples: GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_1, c2_2, c3_1, c4_1 ---------------------------------------- (83) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace GEN(s(x0), x1, s(x2)) -> c2(GE(s(x2), s(x0))) by GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) TIMES(0, x1) -> c3(SUM(if(true, 0, x1, 0))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) K tuples: GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_2, c2_1, c3_1, c4_1 ---------------------------------------- (85) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace TIMES(0, x1) -> c3(SUM(if(true, 0, x1, 0))) by TIMES(0, z0) -> c3(SUM(nil)) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(0, z0) -> c3(SUM(nil)) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) K tuples: GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_2, c2_1, c3_1, c4_1 ---------------------------------------- (87) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: TIMES(0, z0) -> c3(SUM(nil)) ---------------------------------------- (88) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) K tuples: GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_2, c2_1, c3_1, c4_1 ---------------------------------------- (89) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace GEN(s(s(s(z1))), x1, s(s(s(z0)))) -> c2(IF(ge(z0, z1), s(s(s(z1))), x1, s(s(s(z0)))), GE(s(s(s(z0))), s(s(s(z1))))) by GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) ---------------------------------------- (90) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) K tuples: GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_1, c3_1, c4_1, c2_2 ---------------------------------------- (91) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace TIMES(s(z0), x1) -> c3(SUM(if(false, s(z0), x1, 0))) by TIMES(s(z0), z1) -> c3(SUM(cons(z1, gen(s(z0), z1, s(0))))) ---------------------------------------- (92) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, gen(s(z0), z1, s(0))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) K tuples: GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, IF_4, TIMES_2 Compound Symbols: c6_1, c7_1, c10_1, c2_1, c4_1, c2_2, c3_1 ---------------------------------------- (93) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace GEN(s(s(x0)), x1, s(s(x2))) -> c2(GE(s(s(x2)), s(s(x0)))) by GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) ---------------------------------------- (94) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, gen(s(z0), z1, s(0))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, IF_4, GEN_3, TIMES_2 Compound Symbols: c6_1, c7_1, c10_1, c4_1, c2_1, c2_2, c3_1 ---------------------------------------- (95) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace TIMES(s(z0), z1) -> c3(SUM(cons(z1, gen(s(z0), z1, s(0))))) by TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) ---------------------------------------- (96) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, IF_4, GEN_3, TIMES_2 Compound Symbols: c6_1, c7_1, c10_1, c4_1, c2_1, c2_2, c3_1 ---------------------------------------- (97) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace IF(false, s(s(s(x0))), x1, s(s(s(x2)))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(x2)))))) by IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) ---------------------------------------- (98) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) S tuples: SUM(cons(0, z0)) -> c6(SUM(z0)) SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c6_1, c7_1, c10_1, c2_1, c2_2, c3_1, c4_1 ---------------------------------------- (99) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, z0)) -> c6(SUM(z0)) by SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) ---------------------------------------- (100) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) S tuples: SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c7_1, c10_1, c2_1, c2_2, c3_1, c4_1, c6_1 ---------------------------------------- (101) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) by GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) ---------------------------------------- (102) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) S tuples: SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c7_1, c10_1, c2_1, c2_2, c3_1, c4_1, c6_1 ---------------------------------------- (103) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(IF(ge(s(x2), x0), s(s(s(x0))), x1, s(s(s(s(x2))))), GE(s(s(s(s(x2)))), s(s(s(x0))))) by GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) ---------------------------------------- (104) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) S tuples: SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: SUM_1, GE_2, GEN_3, TIMES_2, IF_4 Compound Symbols: c7_1, c10_1, c2_1, c3_1, c4_1, c6_1, c2_2 ---------------------------------------- (105) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(z0), z1)) -> c7(SUM(cons(z0, z1))) by SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) ---------------------------------------- (106) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: GE(s(z0), s(z1)) -> c10(GE(z0, z1)) GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) S tuples: GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: GE_2, GEN_3, TIMES_2, IF_4, SUM_1 Compound Symbols: c10_1, c2_1, c3_1, c4_1, c6_1, c2_2, c7_1 ---------------------------------------- (107) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace GEN(s(s(s(x0))), x1, s(s(s(s(x2))))) -> c2(GE(s(s(s(s(x2)))), s(s(s(x0))))) by GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) ---------------------------------------- (108) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: GE(s(z0), s(z1)) -> c10(GE(z0, z1)) TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) S tuples: GE(s(z0), s(z1)) -> c10(GE(z0, z1)) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: GE_2, TIMES_2, IF_4, SUM_1, GEN_3 Compound Symbols: c10_1, c3_1, c4_1, c6_1, c2_1, c2_2, c7_1 ---------------------------------------- (109) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace GE(s(z0), s(z1)) -> c10(GE(z0, z1)) by GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) ---------------------------------------- (110) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, SUM_1, GEN_3, GE_2 Compound Symbols: c3_1, c4_1, c6_1, c2_1, c2_2, c7_1, c10_1 ---------------------------------------- (111) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, cons(0, y0))) -> c6(SUM(cons(0, y0))) by SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) ---------------------------------------- (112) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, SUM_1, GEN_3, GE_2 Compound Symbols: c3_1, c4_1, c6_1, c2_1, c2_2, c7_1, c10_1 ---------------------------------------- (113) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, cons(s(y0), y1))) -> c6(SUM(cons(s(y0), y1))) by SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) ---------------------------------------- (114) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, GEN_3, SUM_1, GE_2 Compound Symbols: c3_1, c4_1, c2_1, c2_2, c7_1, c10_1, c6_1 ---------------------------------------- (115) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(s(y0)), z1)) -> c7(SUM(cons(s(y0), z1))) by SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) ---------------------------------------- (116) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, GEN_3, SUM_1, GE_2 Compound Symbols: c3_1, c4_1, c2_1, c2_2, c7_1, c10_1, c6_1 ---------------------------------------- (117) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(0), cons(0, y0))) -> c7(SUM(cons(0, cons(0, y0)))) by SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) ---------------------------------------- (118) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, GEN_3, SUM_1, GE_2 Compound Symbols: c3_1, c4_1, c2_1, c2_2, c7_1, c10_1, c6_1 ---------------------------------------- (119) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(0), cons(s(y0), y1))) -> c7(SUM(cons(0, cons(s(y0), y1)))) by SUM(cons(s(0), cons(s(s(y0)), z1))) -> c7(SUM(cons(0, cons(s(s(y0)), z1)))) SUM(cons(s(0), cons(s(0), cons(0, y0)))) -> c7(SUM(cons(0, cons(s(0), cons(0, y0))))) SUM(cons(s(0), cons(s(0), cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(s(0), cons(s(y0), y1))))) ---------------------------------------- (120) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) SUM(cons(s(0), cons(s(s(y0)), z1))) -> c7(SUM(cons(0, cons(s(s(y0)), z1)))) SUM(cons(s(0), cons(s(0), cons(0, y0)))) -> c7(SUM(cons(0, cons(s(0), cons(0, y0))))) SUM(cons(s(0), cons(s(0), cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(s(0), cons(s(y0), y1))))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) SUM(cons(s(0), cons(s(s(y0)), z1))) -> c7(SUM(cons(0, cons(s(s(y0)), z1)))) SUM(cons(s(0), cons(s(0), cons(0, y0)))) -> c7(SUM(cons(0, cons(s(0), cons(0, y0))))) SUM(cons(s(0), cons(s(0), cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(s(0), cons(s(y0), y1))))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, GEN_3, GE_2, SUM_1 Compound Symbols: c3_1, c4_1, c2_1, c2_2, c10_1, c6_1, c7_1 ---------------------------------------- (121) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace GE(s(s(y0)), s(s(y1))) -> c10(GE(s(y0), s(y1))) by GE(s(s(s(y0))), s(s(s(y1)))) -> c10(GE(s(s(y0)), s(s(y1)))) ---------------------------------------- (122) Obligation: Complexity Dependency Tuples Problem Rules: ge(z0, 0) -> true ge(0, s(z0)) -> false ge(s(z0), s(z1)) -> ge(z0, z1) gen(z0, z1, z2) -> if(ge(z2, z0), z0, z1, z2) if(true, z0, z1, z2) -> nil if(false, z0, z1, z2) -> cons(z1, gen(z0, z1, s(z2))) Tuples: TIMES(s(z0), z1) -> c3(SUM(cons(z1, if(ge(s(0), s(z0)), s(z0), z1, s(0))))) IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) SUM(cons(s(0), cons(s(s(y0)), z1))) -> c7(SUM(cons(0, cons(s(s(y0)), z1)))) SUM(cons(s(0), cons(s(0), cons(0, y0)))) -> c7(SUM(cons(0, cons(s(0), cons(0, y0))))) SUM(cons(s(0), cons(s(0), cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(s(0), cons(s(y0), y1))))) GE(s(s(s(y0))), s(s(s(y1)))) -> c10(GE(s(s(y0)), s(s(y1)))) S tuples: IF(false, s(s(s(x0))), x1, s(s(s(s(x2))))) -> c4(GEN(s(s(s(x0))), x1, s(s(s(s(s(x2))))))) GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(IF(ge(s(s(x2)), x0), s(s(s(x0))), x1, s(s(s(s(s(x2)))))), GE(s(s(s(s(s(x2))))), s(s(s(x0))))) SUM(cons(0, cons(0, cons(0, y0)))) -> c6(SUM(cons(0, cons(0, y0)))) SUM(cons(0, cons(0, cons(s(y0), y1)))) -> c6(SUM(cons(0, cons(s(y0), y1)))) SUM(cons(0, cons(s(s(y0)), z1))) -> c6(SUM(cons(s(s(y0)), z1))) SUM(cons(0, cons(s(0), cons(0, y0)))) -> c6(SUM(cons(s(0), cons(0, y0)))) SUM(cons(0, cons(s(0), cons(s(y0), y1)))) -> c6(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(s(s(y0))), z1)) -> c7(SUM(cons(s(s(y0)), z1))) SUM(cons(s(s(0)), cons(0, y0))) -> c7(SUM(cons(s(0), cons(0, y0)))) SUM(cons(s(s(0)), cons(s(y0), y1))) -> c7(SUM(cons(s(0), cons(s(y0), y1)))) SUM(cons(s(0), cons(0, cons(0, y0)))) -> c7(SUM(cons(0, cons(0, cons(0, y0))))) SUM(cons(s(0), cons(0, cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(0, cons(s(y0), y1))))) SUM(cons(s(0), cons(s(s(y0)), z1))) -> c7(SUM(cons(0, cons(s(s(y0)), z1)))) SUM(cons(s(0), cons(s(0), cons(0, y0)))) -> c7(SUM(cons(0, cons(s(0), cons(0, y0))))) SUM(cons(s(0), cons(s(0), cons(s(y0), y1)))) -> c7(SUM(cons(0, cons(s(0), cons(s(y0), y1))))) GE(s(s(s(y0))), s(s(s(y1)))) -> c10(GE(s(s(y0)), s(s(y1)))) K tuples: GEN(s(s(s(x0))), x1, s(s(s(s(s(x2)))))) -> c2(GE(s(s(s(s(s(x2))))), s(s(s(x0))))) Defined Rule Symbols: ge_2, gen_3, if_4 Defined Pair Symbols: TIMES_2, IF_4, GEN_3, SUM_1, GE_2 Compound Symbols: c3_1, c4_1, c2_1, c2_2, c6_1, c7_1, c10_1