KILLED proof of input_vkXr3JcEb3.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) CompletionProof [UPPER BOUND(ID), 0 ms] (18) CpxTypedWeightedCompleteTrs (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (22) CdtProblem (23) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (24) CdtProblem (25) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CdtProblem (29) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CdtProblem (31) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 0 ms] (40) CdtProblem (41) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 4 ms] (48) CdtProblem (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 11 ms] (54) CdtProblem (55) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (60) CdtProblem (61) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 8 ms] (64) CdtProblem (65) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (66) CdtProblem (67) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CdtProblem (69) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CdtProblem (73) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CdtProblem (75) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (76) CdtProblem (77) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (78) CdtProblem (79) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (80) CdtProblem (81) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (82) CdtProblem (83) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CdtProblem (85) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (86) CdtProblem (87) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (88) CdtProblem (89) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (90) CdtProblem (91) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (92) CdtProblem (93) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (94) CdtProblem (95) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (96) CdtProblem (97) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (98) CdtProblem (99) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (100) CdtProblem (101) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (102) CdtProblem (103) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (104) 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: empty(nil) -> true empty(cons(x, l)) -> false head(cons(x, l)) -> x tail(nil) -> nil tail(cons(x, l)) -> l rev(nil) -> nil rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) last(x, l) -> if(empty(l), x, l) if(true, x, l) -> x if(false, x, l) -> last(head(l), tail(l)) rev2(x, nil) -> nil rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 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: empty(nil) -> true empty(cons(x, l)) -> false head(cons(x, l)) -> x tail(nil) -> nil tail(cons(x, l)) -> l rev(nil) -> nil rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) last(x, l) -> if(empty(l), x, l) if(true, x, l) -> x if(false, x, l) -> last(head(l), tail(l)) rev2(x, nil) -> nil rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 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: empty(nil) -> true empty(cons(x, l)) -> false head(cons(x, l)) -> x tail(nil) -> nil tail(cons(x, l)) -> l rev(nil) -> nil rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) last(x, l) -> if(empty(l), x, l) if(true, x, l) -> x if(false, x, l) -> last(head(l), tail(l)) rev2(x, nil) -> nil rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) 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: empty(nil) -> true [1] empty(cons(x, l)) -> false [1] head(cons(x, l)) -> x [1] tail(nil) -> nil [1] tail(cons(x, l)) -> l [1] rev(nil) -> nil [1] rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1] last(x, l) -> if(empty(l), x, l) [1] if(true, x, l) -> x [1] if(false, x, l) -> last(head(l), tail(l)) [1] rev2(x, nil) -> nil [1] rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [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: empty(nil) -> true [1] empty(cons(x, l)) -> false [1] head(cons(x, l)) -> x [1] tail(nil) -> nil [1] tail(cons(x, l)) -> l [1] rev(nil) -> nil [1] rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1] last(x, l) -> if(empty(l), x, l) [1] if(true, x, l) -> x [1] if(false, x, l) -> last(head(l), tail(l)) [1] rev2(x, nil) -> nil [1] rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1] The TRS has the following type information: empty :: nil:cons -> true:false nil :: nil:cons true :: true:false cons :: rev1 -> nil:cons -> nil:cons false :: true:false head :: nil:cons -> rev1 tail :: nil:cons -> nil:cons rev :: nil:cons -> nil:cons rev1 :: rev1 -> nil:cons -> rev1 rev2 :: rev1 -> nil:cons -> nil:cons last :: rev1 -> nil:cons -> rev1 if :: true:false -> rev1 -> nil:cons -> rev1 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: last_2 if_3 (c) The following functions are completely defined: rev2_2 head_1 tail_1 empty_1 rev_1 Due to the following rules being added: head(v0) -> const [0] And the following fresh constants: const ---------------------------------------- (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: empty(nil) -> true [1] empty(cons(x, l)) -> false [1] head(cons(x, l)) -> x [1] tail(nil) -> nil [1] tail(cons(x, l)) -> l [1] rev(nil) -> nil [1] rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1] last(x, l) -> if(empty(l), x, l) [1] if(true, x, l) -> x [1] if(false, x, l) -> last(head(l), tail(l)) [1] rev2(x, nil) -> nil [1] rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1] head(v0) -> const [0] The TRS has the following type information: empty :: nil:cons -> true:false nil :: nil:cons true :: true:false cons :: rev1:const -> nil:cons -> nil:cons false :: true:false head :: nil:cons -> rev1:const tail :: nil:cons -> nil:cons rev :: nil:cons -> nil:cons rev1 :: rev1:const -> nil:cons -> rev1:const rev2 :: rev1:const -> nil:cons -> nil:cons last :: rev1:const -> nil:cons -> rev1:const if :: true:false -> rev1:const -> nil:cons -> rev1:const const :: rev1:const 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: empty(nil) -> true [1] empty(cons(x, l)) -> false [1] head(cons(x, l)) -> x [1] tail(nil) -> nil [1] tail(cons(x, l)) -> l [1] rev(nil) -> nil [1] rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1] last(x, nil) -> if(true, x, nil) [2] last(x, cons(x', l')) -> if(false, x, cons(x', l')) [2] if(true, x, l) -> x [1] if(false, x, cons(x'', l'')) -> last(x'', l'') [3] if(false, x, nil) -> last(const, nil) [2] if(false, x, cons(x1, l1)) -> last(const, l1) [2] rev2(x, nil) -> nil [1] rev2(x, cons(y, nil)) -> rev(cons(x, nil)) [2] rev2(x, cons(y, cons(y', l2))) -> rev(cons(x, rev(cons(y, rev2(y', l2))))) [2] head(v0) -> const [0] The TRS has the following type information: empty :: nil:cons -> true:false nil :: nil:cons true :: true:false cons :: rev1:const -> nil:cons -> nil:cons false :: true:false head :: nil:cons -> rev1:const tail :: nil:cons -> nil:cons rev :: nil:cons -> nil:cons rev1 :: rev1:const -> nil:cons -> rev1:const rev2 :: rev1:const -> nil:cons -> nil:cons last :: rev1:const -> nil:cons -> rev1:const if :: true:false -> rev1:const -> nil:cons -> rev1:const const :: rev1:const 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: nil => 0 true => 1 false => 0 const => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: empty(z) -{ 1 }-> 1 :|: z = 0 empty(z) -{ 1 }-> 0 :|: x >= 0, l >= 0, z = 1 + x + l head(z) -{ 1 }-> x :|: x >= 0, l >= 0, z = 1 + x + l head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 if(z, z', z'') -{ 1 }-> x :|: z' = x, z = 1, x >= 0, l >= 0, z'' = l if(z, z', z'') -{ 3 }-> last(x'', l'') :|: z' = x, l'' >= 0, z'' = 1 + x'' + l'', x >= 0, x'' >= 0, z = 0 if(z, z', z'') -{ 2 }-> last(0, l1) :|: x1 >= 0, z' = x, x >= 0, l1 >= 0, z = 0, z'' = 1 + x1 + l1 if(z, z', z'') -{ 2 }-> last(0, 0) :|: z'' = 0, z' = x, x >= 0, z = 0 last(z, z') -{ 2 }-> if(1, x, 0) :|: x >= 0, z = x, z' = 0 last(z, z') -{ 2 }-> if(0, x, 1 + x' + l') :|: x >= 0, x' >= 0, l' >= 0, z' = 1 + x' + l', z = x rev(z) -{ 1 }-> 0 :|: z = 0 rev(z) -{ 1 }-> 1 + (1 + x + l) + rev2(x, l) :|: x >= 0, l >= 0, z = 1 + x + l rev2(z, z') -{ 2 }-> rev(1 + x + rev(1 + y + rev2(y', l2))) :|: x >= 0, y >= 0, y' >= 0, z = x, l2 >= 0, z' = 1 + y + (1 + y' + l2) rev2(z, z') -{ 2 }-> rev(1 + x + 0) :|: x >= 0, y >= 0, z' = 1 + y + 0, z = x rev2(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0 tail(z) -{ 1 }-> l :|: x >= 0, l >= 0, z = 1 + x + l tail(z) -{ 1 }-> 0 :|: z = 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: empty(z) -{ 1 }-> 1 :|: z = 0 empty(z) -{ 1 }-> 0 :|: x >= 0, l >= 0, z = 1 + x + l head(z) -{ 1 }-> x :|: x >= 0, l >= 0, z = 1 + x + l head(z) -{ 0 }-> 0 :|: z >= 0 if(z, z', z'') -{ 1 }-> z' :|: z = 1, z' >= 0, z'' >= 0 if(z, z', z'') -{ 3 }-> last(x'', l'') :|: l'' >= 0, z'' = 1 + x'' + l'', z' >= 0, x'' >= 0, z = 0 if(z, z', z'') -{ 2 }-> last(0, l1) :|: x1 >= 0, z' >= 0, l1 >= 0, z = 0, z'' = 1 + x1 + l1 if(z, z', z'') -{ 2 }-> last(0, 0) :|: z'' = 0, z' >= 0, z = 0 last(z, z') -{ 2 }-> if(1, z, 0) :|: z >= 0, z' = 0 last(z, z') -{ 2 }-> if(0, z, 1 + x' + l') :|: z >= 0, x' >= 0, l' >= 0, z' = 1 + x' + l' rev(z) -{ 1 }-> 0 :|: z = 0 rev(z) -{ 1 }-> 1 + (1 + x + l) + rev2(x, l) :|: x >= 0, l >= 0, z = 1 + x + l rev2(z, z') -{ 2 }-> rev(1 + z + rev(1 + y + rev2(y', l2))) :|: z >= 0, y >= 0, y' >= 0, l2 >= 0, z' = 1 + y + (1 + y' + l2) rev2(z, z') -{ 2 }-> rev(1 + z + 0) :|: z >= 0, z' - 1 >= 0 rev2(z, z') -{ 1 }-> 0 :|: z >= 0, z' = 0 tail(z) -{ 1 }-> l :|: x >= 0, l >= 0, z = 1 + x + l tail(z) -{ 1 }-> 0 :|: z = 0 ---------------------------------------- (17) 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: head(v0) -> null_head [0] And the following fresh constants: null_head ---------------------------------------- (18) 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: empty(nil) -> true [1] empty(cons(x, l)) -> false [1] head(cons(x, l)) -> x [1] tail(nil) -> nil [1] tail(cons(x, l)) -> l [1] rev(nil) -> nil [1] rev(cons(x, l)) -> cons(rev1(x, l), rev2(x, l)) [1] last(x, l) -> if(empty(l), x, l) [1] if(true, x, l) -> x [1] if(false, x, l) -> last(head(l), tail(l)) [1] rev2(x, nil) -> nil [1] rev2(x, cons(y, l)) -> rev(cons(x, rev2(y, l))) [1] head(v0) -> null_head [0] The TRS has the following type information: empty :: nil:cons -> true:false nil :: nil:cons true :: true:false cons :: rev1:null_head -> nil:cons -> nil:cons false :: true:false head :: nil:cons -> rev1:null_head tail :: nil:cons -> nil:cons rev :: nil:cons -> nil:cons rev1 :: rev1:null_head -> nil:cons -> rev1:null_head rev2 :: rev1:null_head -> nil:cons -> nil:cons last :: rev1:null_head -> nil:cons -> rev1:null_head if :: true:false -> rev1:null_head -> nil:cons -> rev1:null_head null_head :: rev1:null_head Rewrite Strategy: INNERMOST ---------------------------------------- (19) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: nil => 0 true => 1 false => 0 null_head => 0 ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: empty(z) -{ 1 }-> 1 :|: z = 0 empty(z) -{ 1 }-> 0 :|: x >= 0, l >= 0, z = 1 + x + l head(z) -{ 1 }-> x :|: x >= 0, l >= 0, z = 1 + x + l head(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 if(z, z', z'') -{ 1 }-> x :|: z' = x, z = 1, x >= 0, l >= 0, z'' = l if(z, z', z'') -{ 1 }-> last(head(l), tail(l)) :|: z' = x, x >= 0, l >= 0, z = 0, z'' = l last(z, z') -{ 1 }-> if(empty(l), x, l) :|: z' = l, x >= 0, l >= 0, z = x rev(z) -{ 1 }-> 0 :|: z = 0 rev(z) -{ 1 }-> 1 + (1 + x + l) + rev2(x, l) :|: x >= 0, l >= 0, z = 1 + x + l rev2(z, z') -{ 1 }-> rev(1 + x + rev2(y, l)) :|: x >= 0, y >= 0, z' = 1 + y + l, l >= 0, z = x rev2(z, z') -{ 1 }-> 0 :|: x >= 0, z = x, z' = 0 tail(z) -{ 1 }-> l :|: x >= 0, l >= 0, z = 1 + x + l tail(z) -{ 1 }-> 0 :|: z = 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (21) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: empty(nil) -> true empty(cons(z0, z1)) -> false head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 rev(nil) -> nil rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) last(z0, z1) -> if(empty(z1), z0, z1) if(true, z0, z1) -> z0 if(false, z0, z1) -> last(head(z1), tail(z1)) rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) Tuples: EMPTY(nil) -> c EMPTY(cons(z0, z1)) -> c1 HEAD(cons(z0, z1)) -> c2 TAIL(nil) -> c3 TAIL(cons(z0, z1)) -> c4 REV(nil) -> c5 REV(cons(z0, z1)) -> c6(REV2(z0, z1)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1)) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1)) REV2(z0, nil) -> c11 REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) S tuples: EMPTY(nil) -> c EMPTY(cons(z0, z1)) -> c1 HEAD(cons(z0, z1)) -> c2 TAIL(nil) -> c3 TAIL(cons(z0, z1)) -> c4 REV(nil) -> c5 REV(cons(z0, z1)) -> c6(REV2(z0, z1)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1)) IF(true, z0, z1) -> c8 IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1)) REV2(z0, nil) -> c11 REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) K tuples:none Defined Rule Symbols: empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2 Defined Pair Symbols: EMPTY_1, HEAD_1, TAIL_1, REV_1, LAST_2, IF_3, REV2_2 Compound Symbols: c, c1, c2, c3, c4, c5, c6_1, c7_2, c8, c9_2, c10_2, c11, c12_2 ---------------------------------------- (23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 8 trailing nodes: EMPTY(cons(z0, z1)) -> c1 REV2(z0, nil) -> c11 HEAD(cons(z0, z1)) -> c2 IF(true, z0, z1) -> c8 TAIL(cons(z0, z1)) -> c4 REV(nil) -> c5 EMPTY(nil) -> c TAIL(nil) -> c3 ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: empty(nil) -> true empty(cons(z0, z1)) -> false head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 rev(nil) -> nil rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) last(z0, z1) -> if(empty(z1), z0, z1) if(true, z0, z1) -> z0 if(false, z0, z1) -> last(head(z1), tail(z1)) rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1), EMPTY(z1)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1)), HEAD(z1)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1)), TAIL(z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) K tuples:none Defined Rule Symbols: empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2 Defined Pair Symbols: REV_1, LAST_2, IF_3, REV2_2 Compound Symbols: c6_1, c7_2, c9_2, c10_2, c12_2 ---------------------------------------- (25) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing tuple parts ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: empty(nil) -> true empty(cons(z0, z1)) -> false head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 rev(nil) -> nil rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) last(z0, z1) -> if(empty(z1), z0, z1) if(true, z0, z1) -> z0 if(false, z0, z1) -> last(head(z1), tail(z1)) rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) K tuples:none Defined Rule Symbols: empty_1, head_1, tail_1, rev_1, last_2, if_3, rev2_2 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (27) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: rev(nil) -> nil last(z0, z1) -> if(empty(z1), z0, z1) if(true, z0, z1) -> z0 if(false, z0, z1) -> last(head(z1), tail(z1)) ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) empty(nil) -> true empty(cons(z0, z1)) -> false head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) K tuples:none Defined Rule Symbols: rev2_2, rev_1, empty_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (29) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace LAST(z0, z1) -> c7(IF(empty(z1), z0, z1)) by LAST(x0, nil) -> c7(IF(true, x0, nil)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) empty(nil) -> true empty(cons(z0, z1)) -> false head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, nil) -> c7(IF(true, x0, nil)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, nil) -> c7(IF(true, x0, nil)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) K tuples:none Defined Rule Symbols: rev2_2, rev_1, empty_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, IF_3, LAST_2 Compound Symbols: c6_1, c12_2, c9_1, c10_1, c7_1 ---------------------------------------- (31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: LAST(x0, nil) -> c7(IF(true, x0, nil)) ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) empty(nil) -> true empty(cons(z0, z1)) -> false head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) K tuples:none Defined Rule Symbols: rev2_2, rev_1, empty_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, IF_3, LAST_2 Compound Symbols: c6_1, c12_2, c9_1, c10_1, c7_1 ---------------------------------------- (33) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: empty(nil) -> true empty(cons(z0, z1)) -> false ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) K tuples:none Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, IF_3, LAST_2 Compound Symbols: c6_1, c12_2, c9_1, c10_1, c7_1 ---------------------------------------- (35) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace IF(false, z0, z1) -> c9(LAST(head(z1), tail(z1))) by IF(false, x0, nil) -> c9(LAST(head(nil), nil)) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, nil) -> c9(LAST(head(nil), nil)) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, nil) -> c9(LAST(head(nil), nil)) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) K tuples:none Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, IF_3, LAST_2 Compound Symbols: c6_1, c12_2, c10_1, c7_1, c9_1 ---------------------------------------- (37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: IF(false, x0, nil) -> c9(LAST(head(nil), nil)) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) K tuples:none Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, IF_3, LAST_2 Compound Symbols: c6_1, c12_2, c10_1, c7_1, c9_1 ---------------------------------------- (39) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) We considered the (Usable) Rules: tail(cons(z0, z1)) -> z1 tail(nil) -> nil And the Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) The order we found is given by the following interpretation: Polynomial interpretation : POL(IF(x_1, x_2, x_3)) = x_3 POL(LAST(x_1, x_2)) = x_2 POL(REV(x_1)) = 0 POL(REV2(x_1, x_2)) = 0 POL(c10(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(false) = [1] POL(head(x_1)) = [1] + x_1 POL(nil) = [1] POL(rev(x_1)) = [1] POL(rev1(x_1, x_2)) = [1] + x_1 + x_2 POL(rev2(x_1, x_2)) = [1] + x_1 + x_2 POL(tail(x_1)) = x_1 ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, IF_3, LAST_2 Compound Symbols: c6_1, c12_2, c10_1, c7_1, c9_1 ---------------------------------------- (41) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace IF(false, z0, z1) -> c10(LAST(head(z1), tail(z1))) by IF(false, x0, nil) -> c10(LAST(head(nil), nil)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, nil) -> c10(LAST(head(nil), nil)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, nil) -> c10(LAST(head(nil), nil)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (43) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: IF(false, x0, nil) -> c10(LAST(head(nil), nil)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(nil) -> nil tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (45) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: tail(nil) -> nil ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (47) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) We considered the (Usable) Rules: tail(cons(z0, z1)) -> z1 And the Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) The order we found is given by the following interpretation: Polynomial interpretation : POL(IF(x_1, x_2, x_3)) = x_3 POL(LAST(x_1, x_2)) = x_2 POL(REV(x_1)) = 0 POL(REV2(x_1, x_2)) = 0 POL(c10(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(false) = [1] POL(head(x_1)) = [1] + x_1 POL(nil) = [1] POL(rev(x_1)) = [1] POL(rev1(x_1, x_2)) = [1] + x_1 + x_2 POL(rev2(x_1, x_2)) = [1] + x_1 + x_2 POL(tail(x_1)) = x_1 ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) by IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (51) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, tail(cons(z0, z1)))) by IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c10_1, c9_1 ---------------------------------------- (53) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) We considered the (Usable) Rules: tail(cons(z0, z1)) -> z1 And the Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(IF(x_1, x_2, x_3)) = x_3 POL(LAST(x_1, x_2)) = x_2 POL(REV(x_1)) = 0 POL(REV2(x_1, x_2)) = 0 POL(c10(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(false) = [1] POL(head(x_1)) = [1] + x_1 POL(nil) = [1] POL(rev(x_1)) = [1] + x_1 POL(rev1(x_1, x_2)) = [1] + x_1 + x_2 POL(rev2(x_1, x_2)) = [1] + x_1 + x_2 POL(tail(x_1)) = x_1 ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c10_1, c9_1 ---------------------------------------- (55) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) by IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) head(cons(z0, z1)) -> z0 tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1, head_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c10_1, c9_1 ---------------------------------------- (57) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: head(cons(z0, z1)) -> z0 ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c10_1, c9_1 ---------------------------------------- (59) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, tail(cons(z0, z1)))) by IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) tail(cons(z0, z1)) -> z1 Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1, tail_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (61) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: tail(cons(z0, z1)) -> z1 ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (63) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) We considered the (Usable) Rules:none And the Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(IF(x_1, x_2, x_3)) = x_2 + x_3 POL(LAST(x_1, x_2)) = [1] + x_1 + x_2 POL(REV(x_1)) = 0 POL(REV2(x_1, x_2)) = 0 POL(c10(x_1)) = x_1 POL(c12(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(false) = [1] POL(nil) = [1] POL(rev(x_1)) = [1] + x_1 POL(rev1(x_1, x_2)) = [1] + x_1 + x_2 POL(rev2(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (65) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) S tuples: REV(cons(z0, z1)) -> c6(REV2(z0, z1)) REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV_1, REV2_2, LAST_2, IF_3 Compound Symbols: c6_1, c12_2, c7_1, c9_1, c10_1 ---------------------------------------- (67) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace REV(cons(z0, z1)) -> c6(REV2(z0, z1)) by REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) S tuples: REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, LAST_2, IF_3, REV_1 Compound Symbols: c12_2, c7_1, c9_1, c10_1, c6_1 ---------------------------------------- (69) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace REV2(z0, cons(z1, z2)) -> c12(REV(cons(z0, rev2(z1, z2))), REV2(z1, z2)) by REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil)) REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil)) REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil)) REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(head(cons(z0, z1)), z1)) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2 ---------------------------------------- (71) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: REV2(x0, cons(z0, nil)) -> c12(REV(cons(x0, nil)), REV2(z0, nil)) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2 ---------------------------------------- (73) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace REV2(x0, cons(z0, cons(z1, z2))) -> c12(REV(cons(x0, rev(cons(z0, rev2(z1, z2))))), REV2(z0, cons(z1, z2))) by REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))), REV2(x1, cons(z0, nil))) REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))), REV2(x1, cons(z0, nil))) REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil)))), REV2(x1, cons(z0, nil))) REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2 ---------------------------------------- (75) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil))))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil))))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2, c12_1 ---------------------------------------- (77) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace REV2(x0, cons(x1, cons(z0, cons(z1, z2)))) -> c12(REV(cons(x0, rev(cons(x1, rev(cons(z0, rev2(z1, z2))))))), REV2(x1, cons(z0, cons(z1, z2)))) by REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil))))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil))))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2, c12_1 ---------------------------------------- (79) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace REV2(x0, cons(x1, cons(z0, nil))) -> c12(REV(cons(x0, rev(cons(x1, nil))))) by REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2, c12_1 ---------------------------------------- (81) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, rev(cons(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) by REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2, c12_1 ---------------------------------------- (83) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), rev2(z1, nil))))) by REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) K tuples: IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c9_1, c10_1, c6_1, c12_2, c12_1 ---------------------------------------- (85) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace IF(false, x0, cons(z0, z1)) -> c9(LAST(z0, z1)) by IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) S tuples: REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) K tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV_1, REV2_2 Compound Symbols: c7_1, c10_1, c6_1, c12_2, c12_1, c9_1 ---------------------------------------- (87) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace REV(cons(z0, cons(y1, y2))) -> c6(REV2(z0, cons(y1, y2))) by REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil))) ---------------------------------------- (88) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil))) K tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV2_2, REV_1 Compound Symbols: c7_1, c10_1, c12_2, c12_1, c9_1, c6_1 ---------------------------------------- (89) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: REV(cons(x0, cons(rev1(x1, nil), nil))) -> c6(REV2(x0, cons(rev1(x1, nil), nil))) ---------------------------------------- (90) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) K tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, IF_3, REV2_2, REV_1 Compound Symbols: c7_1, c10_1, c12_2, c12_1, c9_1, c6_1 ---------------------------------------- (91) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace IF(false, x0, cons(z0, z1)) -> c10(LAST(z0, z1)) by IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) ---------------------------------------- (92) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) K tuples: LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: LAST_2, REV2_2, IF_3, REV_1 Compound Symbols: c7_1, c12_2, c12_1, c9_1, c6_1, c10_1 ---------------------------------------- (93) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace LAST(x0, cons(z0, z1)) -> c7(IF(false, x0, cons(z0, z1))) by LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) ---------------------------------------- (94) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) K tuples: IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, IF_3, REV_1, LAST_2 Compound Symbols: c12_2, c12_1, c9_1, c6_1, c10_1, c7_1 ---------------------------------------- (95) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace IF(false, z0, cons(z1, cons(y1, y2))) -> c9(LAST(z1, cons(y1, y2))) by IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) ---------------------------------------- (96) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) K tuples: IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, REV_1, IF_3, LAST_2 Compound Symbols: c12_2, c12_1, c6_1, c10_1, c7_1, c9_1 ---------------------------------------- (97) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace REV(cons(x0, cons(rev1(x1, y0), y2))) -> c6(REV2(x0, cons(rev1(x1, y0), y2))) by REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) ---------------------------------------- (98) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) K tuples: IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, IF_3, LAST_2, REV_1 Compound Symbols: c12_2, c12_1, c10_1, c7_1, c9_1, c6_1 ---------------------------------------- (99) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: REV2(z0, cons(z1, cons(z2, nil))) -> c12(REV(cons(z0, cons(rev1(z1, nil), nil)))) ---------------------------------------- (100) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) K tuples: IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, IF_3, LAST_2, REV_1 Compound Symbols: c12_2, c10_1, c7_1, c9_1, c6_1 ---------------------------------------- (101) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace IF(false, z0, cons(z1, cons(y1, y2))) -> c10(LAST(z1, cons(y1, y2))) by IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3)))) ---------------------------------------- (102) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3)))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) K tuples: LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3)))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, LAST_2, IF_3, REV_1 Compound Symbols: c12_2, c7_1, c9_1, c6_1, c10_1 ---------------------------------------- (103) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace LAST(z0, cons(z1, cons(y2, y3))) -> c7(IF(false, z0, cons(z1, cons(y2, y3)))) by LAST(z0, cons(z1, cons(z2, cons(y3, y4)))) -> c7(IF(false, z0, cons(z1, cons(z2, cons(y3, y4))))) ---------------------------------------- (104) Obligation: Complexity Dependency Tuples Problem Rules: rev2(z0, nil) -> nil rev2(z0, cons(z1, z2)) -> rev(cons(z0, rev2(z1, z2))) rev(cons(z0, z1)) -> cons(rev1(z0, z1), rev2(z0, z1)) Tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3)))) LAST(z0, cons(z1, cons(z2, cons(y3, y4)))) -> c7(IF(false, z0, cons(z1, cons(z2, cons(y3, y4))))) S tuples: REV2(x0, cons(z0, cons(x2, x3))) -> c12(REV(cons(x0, cons(rev1(z0, rev2(x2, x3)), rev2(z0, rev2(x2, x3))))), REV2(z0, cons(x2, x3))) REV2(z0, cons(z1, cons(z2, cons(z3, z4)))) -> c12(REV(cons(z0, cons(rev1(z1, rev(cons(z2, rev2(z3, z4)))), rev2(z1, cons(rev1(z2, rev2(z3, z4)), rev2(z2, rev2(z3, z4))))))), REV2(z1, cons(z2, cons(z3, z4)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, y3)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, y3)))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, cons(y3, y4))))) REV(cons(z0, cons(rev1(z1, z2), cons(y2, nil)))) -> c6(REV2(z0, cons(rev1(z1, z2), cons(y2, nil)))) K tuples: IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c9(LAST(z1, cons(z2, cons(y2, y3)))) IF(false, z0, cons(z1, cons(z2, cons(y2, y3)))) -> c10(LAST(z1, cons(z2, cons(y2, y3)))) LAST(z0, cons(z1, cons(z2, cons(y3, y4)))) -> c7(IF(false, z0, cons(z1, cons(z2, cons(y3, y4))))) Defined Rule Symbols: rev2_2, rev_1 Defined Pair Symbols: REV2_2, IF_3, REV_1, LAST_2 Compound Symbols: c12_2, c9_1, c6_1, c10_1, c7_1