KILLED proof of input_ns70pIwNAq.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), 1 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) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CdtProblem (27) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 105 ms] (28) CdtProblem (29) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CdtProblem (31) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 2 ms] (40) CdtProblem (41) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (42) CdtProblem (43) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (60) CdtProblem (61) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (66) CdtProblem (67) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CdtProblem (69) CdtRewritingProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CdtProblem (73) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 13 ms] (74) CdtProblem (75) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (76) CdtProblem (77) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (78) CdtProblem (79) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (80) CdtProblem (81) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (82) CdtProblem (83) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (84) CdtProblem (85) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 40 ms] (86) CdtProblem (87) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (88) 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: app(nil, k) -> k app(l, nil) -> l app(cons(x, l), k) -> cons(x, app(l, k)) sum(cons(x, nil)) -> cons(x, nil) sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) a(h, h, x) -> s(x) a(x, s(y), h) -> a(x, y, s(h)) a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) a(s(x), h, z) -> a(x, z, z) 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: app(nil, k) -> k app(l, nil) -> l app(cons(x, l), k) -> cons(x, app(l, k)) sum(cons(x, nil)) -> cons(x, nil) sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) a(h, h, x) -> s(x) a(x, s(y), h) -> a(x, y, s(h)) a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) a(s(x), h, z) -> a(x, z, z) 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: app(nil, k) -> k app(l, nil) -> l app(cons(x, l), k) -> cons(x, app(l, k)) sum(cons(x, nil)) -> cons(x, nil) sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) a(h, h, x) -> s(x) a(x, s(y), h) -> a(x, y, s(h)) a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) a(s(x), h, z) -> a(x, z, z) 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: app(nil, k) -> k [1] app(l, nil) -> l [1] app(cons(x, l), k) -> cons(x, app(l, k)) [1] sum(cons(x, nil)) -> cons(x, nil) [1] sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) [1] a(h, h, x) -> s(x) [1] a(x, s(y), h) -> a(x, y, s(h)) [1] a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) [1] a(s(x), h, z) -> a(x, z, z) [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: app(nil, k) -> k [1] app(l, nil) -> l [1] app(cons(x, l), k) -> cons(x, app(l, k)) [1] sum(cons(x, nil)) -> cons(x, nil) [1] sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) [1] a(h, h, x) -> s(x) [1] a(x, s(y), h) -> a(x, y, s(h)) [1] a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) [1] a(s(x), h, z) -> a(x, z, z) [1] The TRS has the following type information: app :: nil:cons -> nil:cons -> nil:cons nil :: nil:cons cons :: h:s -> nil:cons -> nil:cons sum :: nil:cons -> nil:cons a :: h:s -> h:s -> h:s -> h:s h :: h:s s :: h:s -> h: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: app_2 sum_1 (c) The following functions are completely defined: a_3 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: app(nil, k) -> k [1] app(l, nil) -> l [1] app(cons(x, l), k) -> cons(x, app(l, k)) [1] sum(cons(x, nil)) -> cons(x, nil) [1] sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) [1] a(h, h, x) -> s(x) [1] a(x, s(y), h) -> a(x, y, s(h)) [1] a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) [1] a(s(x), h, z) -> a(x, z, z) [1] The TRS has the following type information: app :: nil:cons -> nil:cons -> nil:cons nil :: nil:cons cons :: h:s -> nil:cons -> nil:cons sum :: nil:cons -> nil:cons a :: h:s -> h:s -> h:s -> h:s h :: h:s s :: h:s -> h: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: app(nil, k) -> k [1] app(l, nil) -> l [1] app(cons(x, l), k) -> cons(x, app(l, k)) [1] sum(cons(x, nil)) -> cons(x, nil) [1] sum(cons(h, cons(h, l))) -> sum(cons(s(h), l)) [2] sum(cons(x, cons(s(y'), l))) -> sum(cons(a(x, y', s(h)), l)) [2] sum(cons(s(x'), cons(h, l))) -> sum(cons(a(x', h, h), l)) [2] a(h, h, x) -> s(x) [1] a(x, s(y), h) -> a(x, y, s(h)) [1] a(x, s(y), s(h)) -> a(x, y, a(x, y, s(h))) [2] a(x, s(y), s(s(z'))) -> a(x, y, a(x, y, a(x, s(y), z'))) [2] a(s(x), h, z) -> a(x, z, z) [1] The TRS has the following type information: app :: nil:cons -> nil:cons -> nil:cons nil :: nil:cons cons :: h:s -> nil:cons -> nil:cons sum :: nil:cons -> nil:cons a :: h:s -> h:s -> h:s -> h:s h :: h:s s :: h:s -> h: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: nil => 0 h => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: a(z'', z1, z2) -{ 2 }-> a(x, y, a(x, y, a(x, 1 + y, z'))) :|: x >= 0, y >= 0, z' >= 0, z'' = x, z1 = 1 + y, z2 = 1 + (1 + z') a(z'', z1, z2) -{ 2 }-> a(x, y, a(x, y, 1 + 0)) :|: z2 = 1 + 0, x >= 0, y >= 0, z'' = x, z1 = 1 + y a(z'', z1, z2) -{ 1 }-> a(x, y, 1 + 0) :|: z2 = 0, x >= 0, y >= 0, z'' = x, z1 = 1 + y a(z'', z1, z2) -{ 1 }-> a(x, z, z) :|: z1 = 0, z >= 0, z2 = z, x >= 0, z'' = 1 + x a(z'', z1, z2) -{ 1 }-> 1 + x :|: z'' = 0, z1 = 0, z2 = x, x >= 0 app(z'', z1) -{ 1 }-> k :|: z'' = 0, z1 = k, k >= 0 app(z'', z1) -{ 1 }-> l :|: z1 = 0, l >= 0, z'' = l app(z'', z1) -{ 1 }-> 1 + x + app(l, k) :|: z'' = 1 + x + l, z1 = k, x >= 0, l >= 0, k >= 0 sum(z'') -{ 2 }-> sum(1 + a(x, y', 1 + 0) + l) :|: z'' = 1 + x + (1 + (1 + y') + l), x >= 0, y' >= 0, l >= 0 sum(z'') -{ 2 }-> sum(1 + a(x', 0, 0) + l) :|: x' >= 0, z'' = 1 + (1 + x') + (1 + 0 + l), l >= 0 sum(z'') -{ 2 }-> sum(1 + (1 + 0) + l) :|: l >= 0, z'' = 1 + 0 + (1 + 0 + l) sum(z'') -{ 1 }-> 1 + x + 0 :|: z'' = 1 + x + 0, x >= 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: a(z'', z1, z2) -{ 2 }-> a(z'', z1 - 1, a(z'', z1 - 1, a(z'', 1 + (z1 - 1), z2 - 2))) :|: z'' >= 0, z1 - 1 >= 0, z2 - 2 >= 0 a(z'', z1, z2) -{ 2 }-> a(z'', z1 - 1, a(z'', z1 - 1, 1 + 0)) :|: z2 = 1 + 0, z'' >= 0, z1 - 1 >= 0 a(z'', z1, z2) -{ 1 }-> a(z'', z1 - 1, 1 + 0) :|: z2 = 0, z'' >= 0, z1 - 1 >= 0 a(z'', z1, z2) -{ 1 }-> a(z'' - 1, z2, z2) :|: z1 = 0, z2 >= 0, z'' - 1 >= 0 a(z'', z1, z2) -{ 1 }-> 1 + z2 :|: z'' = 0, z1 = 0, z2 >= 0 app(z'', z1) -{ 1 }-> z'' :|: z1 = 0, z'' >= 0 app(z'', z1) -{ 1 }-> z1 :|: z'' = 0, z1 >= 0 app(z'', z1) -{ 1 }-> 1 + x + app(l, z1) :|: z'' = 1 + x + l, x >= 0, l >= 0, z1 >= 0 sum(z'') -{ 2 }-> sum(1 + a(x, y', 1 + 0) + l) :|: z'' = 1 + x + (1 + (1 + y') + l), x >= 0, y' >= 0, l >= 0 sum(z'') -{ 2 }-> sum(1 + a(x', 0, 0) + l) :|: x' >= 0, z'' = 1 + (1 + x') + (1 + 0 + l), l >= 0 sum(z'') -{ 2 }-> sum(1 + (1 + 0) + (z'' - 2)) :|: z'' - 2 >= 0 sum(z'') -{ 1 }-> 1 + (z'' - 1) + 0 :|: z'' - 1 >= 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: sum(v0) -> null_sum [0] app(v0, v1) -> null_app [0] And the following fresh constants: null_sum, null_app ---------------------------------------- (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: app(nil, k) -> k [1] app(l, nil) -> l [1] app(cons(x, l), k) -> cons(x, app(l, k)) [1] sum(cons(x, nil)) -> cons(x, nil) [1] sum(cons(x, cons(y, l))) -> sum(cons(a(x, y, h), l)) [1] a(h, h, x) -> s(x) [1] a(x, s(y), h) -> a(x, y, s(h)) [1] a(x, s(y), s(z)) -> a(x, y, a(x, s(y), z)) [1] a(s(x), h, z) -> a(x, z, z) [1] sum(v0) -> null_sum [0] app(v0, v1) -> null_app [0] The TRS has the following type information: app :: nil:cons:null_sum:null_app -> nil:cons:null_sum:null_app -> nil:cons:null_sum:null_app nil :: nil:cons:null_sum:null_app cons :: h:s -> nil:cons:null_sum:null_app -> nil:cons:null_sum:null_app sum :: nil:cons:null_sum:null_app -> nil:cons:null_sum:null_app a :: h:s -> h:s -> h:s -> h:s h :: h:s s :: h:s -> h:s null_sum :: nil:cons:null_sum:null_app null_app :: nil:cons:null_sum:null_app 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 h => 0 null_sum => 0 null_app => 0 ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: a(z', z'', z1) -{ 1 }-> a(x, y, a(x, 1 + y, z)) :|: z >= 0, z' = x, x >= 0, y >= 0, z'' = 1 + y, z1 = 1 + z a(z', z'', z1) -{ 1 }-> a(x, y, 1 + 0) :|: z1 = 0, z' = x, x >= 0, y >= 0, z'' = 1 + y a(z', z'', z1) -{ 1 }-> a(x, z, z) :|: z'' = 0, z' = 1 + x, z1 = z, z >= 0, x >= 0 a(z', z'', z1) -{ 1 }-> 1 + x :|: z'' = 0, x >= 0, z1 = x, z' = 0 app(z', z'') -{ 1 }-> k :|: k >= 0, z'' = k, z' = 0 app(z', z'') -{ 1 }-> l :|: z' = l, z'' = 0, l >= 0 app(z', z'') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z'' = v1, z' = v0 app(z', z'') -{ 1 }-> 1 + x + app(l, k) :|: x >= 0, z' = 1 + x + l, l >= 0, k >= 0, z'' = k sum(z') -{ 1 }-> sum(1 + a(x, y, 0) + l) :|: z' = 1 + x + (1 + y + l), x >= 0, y >= 0, l >= 0 sum(z') -{ 0 }-> 0 :|: v0 >= 0, z' = v0 sum(z') -{ 1 }-> 1 + x + 0 :|: x >= 0, z' = 1 + x + 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: app(nil, z0) -> z0 app(z0, nil) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) sum(cons(z0, nil)) -> cons(z0, nil) sum(cons(z0, cons(z1, z2))) -> sum(cons(a(z0, z1, h), z2)) a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) a(s(z0), h, z1) -> a(z0, z1, z1) Tuples: APP(nil, z0) -> c APP(z0, nil) -> c1 APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, nil)) -> c3 SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(h, h, z0) -> c5 A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) S tuples: APP(nil, z0) -> c APP(z0, nil) -> c1 APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, nil)) -> c3 SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(h, h, z0) -> c5 A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples:none Defined Rule Symbols: app_2, sum_1, a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c, c1, c2_1, c3, c4_2, c5, c6_1, c7_2, c8_1 ---------------------------------------- (23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 4 trailing nodes: APP(z0, nil) -> c1 SUM(cons(z0, nil)) -> c3 APP(nil, z0) -> c A(h, h, z0) -> c5 ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: app(nil, z0) -> z0 app(z0, nil) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) sum(cons(z0, nil)) -> cons(z0, nil) sum(cons(z0, cons(z1, z2))) -> sum(cons(a(z0, z1, h), z2)) a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) a(s(z0), h, z1) -> a(z0, z1, z1) Tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) S tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples:none Defined Rule Symbols: app_2, sum_1, a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c7_2, c8_1 ---------------------------------------- (25) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: app(nil, z0) -> z0 app(z0, nil) -> z0 app(cons(z0, z1), z2) -> cons(z0, app(z1, z2)) sum(cons(z0, nil)) -> cons(z0, nil) sum(cons(z0, cons(z1, z2))) -> sum(cons(a(z0, z1, h), z2)) ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) S tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples:none Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c7_2, c8_1 ---------------------------------------- (27) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) We considered the (Usable) Rules:none And the Tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(A(x_1, x_2, x_3)) = 0 POL(APP(x_1, x_2)) = [3]x_1 POL(SUM(x_1)) = [2]x_1 POL(a(x_1, x_2, x_3)) = 0 POL(c2(x_1)) = x_1 POL(c4(x_1, x_2)) = x_1 + x_2 POL(c6(x_1)) = x_1 POL(c7(x_1, x_2)) = x_1 + x_2 POL(c8(x_1)) = x_1 POL(cons(x_1, x_2)) = [1] + x_2 POL(h) = 0 POL(s(x_1)) = [3] + x_1 ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) S tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples: APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c7_2, c8_1 ---------------------------------------- (29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace APP(cons(z0, z1), z2) -> c2(APP(z1, z2)) by APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) S tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples: SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_2, c8_1, c2_1 ---------------------------------------- (31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(z0, cons(z1, z2))) -> c4(SUM(cons(a(z0, z1, h), z2)), A(z0, z1, h)) by SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) S tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: A_3, APP_2, SUM_1 Compound Symbols: c6_1, c7_2, c8_1, c2_1, c4_2 ---------------------------------------- (33) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) by SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) S tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: A_3, APP_2, SUM_1 Compound Symbols: c6_1, c7_2, c8_1, c2_1, c4_2 ---------------------------------------- (35) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) by SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) S tuples: A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: A_3, APP_2, SUM_1 Compound Symbols: c6_1, c7_2, c8_1, c2_1, c4_2 ---------------------------------------- (37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(z0, s(z1), h) -> c6(A(z0, z1, s(h))) by A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) S tuples: A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(s(z0), h, z1) -> c8(A(z0, z1, z1)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: A_3, APP_2, SUM_1 Compound Symbols: c7_2, c8_1, c2_1, c4_2, c6_1 ---------------------------------------- (39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(s(z0), h, z1) -> c8(A(z0, z1, z1)) by A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) S tuples: A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: A_3, APP_2, SUM_1 Compound Symbols: c7_2, c2_1, c4_2, c6_1, c8_1 ---------------------------------------- (41) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace A(z0, s(z1), s(z2)) -> c7(A(z0, z1, a(z0, s(z1), z2)), A(z0, s(z1), z2)) by A(z0, s(z1), s(h)) -> c7(A(z0, z1, a(z0, z1, s(h))), A(z0, s(z1), h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(z1), s(h)) -> c7(A(z0, z1, a(z0, z1, s(h))), A(z0, s(z1), h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(z1), s(h)) -> c7(A(z0, z1, a(z0, z1, s(h))), A(z0, s(z1), h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_2 ---------------------------------------- (43) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace A(z0, s(z1), s(h)) -> c7(A(z0, z1, a(z0, z1, s(h))), A(z0, s(z1), h)) by A(h, s(h), s(h)) -> c7(A(h, h, s(s(h))), A(h, s(h), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) A(h, s(h), s(h)) -> c7(A(h, h, s(s(h))), A(h, s(h), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) A(h, s(h), s(h)) -> c7(A(h, h, s(s(h))), A(h, s(h), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(y1), z2))) -> c4(SUM(cons(a(z0, s(y1), h), z2)), A(z0, s(y1), h)) SUM(cons(s(y0), cons(h, z2))) -> c4(SUM(cons(a(s(y0), h, h), z2)), A(s(y0), h, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_2, c7_1 ---------------------------------------- (45) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing nodes: A(h, s(h), s(h)) -> c7(A(h, h, s(s(h))), A(h, s(h), h)) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_2, c7_1 ---------------------------------------- (47) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace A(z0, s(z1), s(s(z2))) -> c7(A(z0, z1, a(z0, z1, a(z0, s(z1), z2))), A(z0, s(z1), s(z2))) by A(h, s(h), s(s(x2))) -> c7(A(h, h, s(a(h, s(h), x2))), A(h, s(h), s(x2))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(h, s(h), s(s(x2))) -> c7(A(h, h, s(a(h, s(h), x2))), A(h, s(h), s(x2))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(h, s(h), s(s(x2))) -> c7(A(h, h, s(a(h, s(h), x2))), A(h, s(h), s(x2))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_2, c7_1 ---------------------------------------- (49) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 1 trailing tuple parts ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_2, c7_1 ---------------------------------------- (51) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, s(h), s(h))), A(s(z0), s(h), h)) by A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, s(h), h))), A(s(z0), s(h), h)) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, s(h), h))), A(s(z0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, s(h), h))), A(s(z0), s(h), h)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_2, c7_1 ---------------------------------------- (53) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, s(z1), h))), A(z0, s(s(z1)), h)) by A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, s(h), h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, s(h), h))), A(s(z0), s(h), h)) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_1, c7_2 ---------------------------------------- (55) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, s(h), h))), A(s(z0), s(h), h)) by A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) Defined Rule Symbols: a_3 Defined Pair Symbols: APP_2, SUM_1, A_3 Compound Symbols: c2_1, c4_2, c6_1, c8_1, c7_1, c7_2 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace APP(cons(z0, cons(y0, y1)), z2) -> c2(APP(cons(y0, y1), z2)) by APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(z0, cons(s(z1), x2))) -> c4(SUM(cons(a(z0, z1, s(h)), x2)), A(z0, s(z1), h)) by SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(s(y1)), z2))) -> c4(SUM(cons(a(z0, s(y1), s(h)), z2)), A(z0, s(s(y1)), h)) SUM(cons(s(y0), cons(s(h), z2))) -> c4(SUM(cons(a(s(y0), h, s(h)), z2)), A(s(y0), s(h), h)) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(s(y1)), z2))) -> c4(SUM(cons(a(z0, s(y1), s(h)), z2)), A(z0, s(s(y1)), h)) SUM(cons(s(y0), cons(s(h), z2))) -> c4(SUM(cons(a(s(y0), h, s(h)), z2)), A(s(y0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1 ---------------------------------------- (61) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SUM(cons(z0, cons(s(s(y1)), z2))) -> c4(SUM(cons(a(z0, s(y1), s(h)), z2)), A(z0, s(s(y1)), h)) by SUM(cons(z0, cons(s(s(z1)), x2))) -> c4(SUM(cons(a(z0, z1, a(z0, s(z1), h)), x2)), A(z0, s(s(z1)), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(s(y0), cons(s(h), z2))) -> c4(SUM(cons(a(s(y0), h, s(h)), z2)), A(s(y0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), x2))) -> c4(SUM(cons(a(z0, z1, a(z0, s(z1), h)), x2)), A(z0, s(s(z1)), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (63) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SUM(cons(s(y0), cons(s(h), z2))) -> c4(SUM(cons(a(s(y0), h, s(h)), z2)), A(s(y0), s(h), h)) by SUM(cons(s(z0), cons(s(h), x1))) -> c4(SUM(cons(a(z0, s(h), s(h)), x1)), A(s(z0), s(h), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(s(z1)), x2))) -> c4(SUM(cons(a(z0, z1, a(z0, s(z1), h)), x2)), A(z0, s(s(z1)), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(z0), cons(s(h), x1))) -> c4(SUM(cons(a(z0, s(h), s(h)), x1)), A(s(z0), s(h), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (65) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace SUM(cons(z0, cons(s(s(z1)), x2))) -> c4(SUM(cons(a(z0, z1, a(z0, s(z1), h)), x2)), A(z0, s(s(z1)), h)) by SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(z0), cons(s(h), x1))) -> c4(SUM(cons(a(z0, s(h), s(h)), x1)), A(s(z0), s(h), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (67) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace SUM(cons(s(z0), cons(s(h), x1))) -> c4(SUM(cons(a(z0, s(h), s(h)), x1)), A(s(z0), s(h), h)) by SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, s(h), h)), z1)), A(s(z0), s(h), h)) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, s(h), h)), z1)), A(s(z0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (69) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, s(h), h)), z1)), A(s(z0), s(h), h)) by SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (71) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(z0), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(z0), h, h)) by SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(s(y0)), cons(h, z1))) -> c4(SUM(cons(a(s(y0), h, h), z1)), A(s(s(y0)), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(s(y0)), cons(h, z1))) -> c4(SUM(cons(a(s(y0), h, h), z1)), A(s(s(y0)), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (73) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace SUM(cons(s(s(y0)), cons(h, z1))) -> c4(SUM(cons(a(s(y0), h, h), z1)), A(s(s(y0)), h, h)) by SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (75) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(s(z0), h, s(y1)) -> c8(A(z0, s(y1), s(y1))) by A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c8_1, c7_1, c7_2, c2_1, c4_1 ---------------------------------------- (77) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(s(s(y0)), h, h) -> c8(A(s(y0), h, h)) by A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_1, c7_2, c2_1, c4_1, c8_1 ---------------------------------------- (79) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(x0, s(x1), s(h)) -> c7(A(x0, s(x1), h)) by A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) S tuples: A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_2, c7_1, c2_1, c4_1, c8_1 ---------------------------------------- (81) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(z0, s(s(y1)), h) -> c6(A(z0, s(y1), s(h))) by A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) S tuples: A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_2, c7_1, c2_1, c4_1, c8_1 ---------------------------------------- (83) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(h, s(h), s(s(x2))) -> c7(A(h, s(h), s(x2))) by A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(h, s(h), s(s(s(y0)))) -> c7(A(h, s(h), s(s(y0)))) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(h, s(h), s(s(s(y0)))) -> c7(A(h, s(h), s(s(y0)))) S tuples: A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(h, s(h), s(s(s(y0)))) -> c7(A(h, s(h), s(s(y0)))) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_2, c2_1, c4_1, c8_1, c7_1 ---------------------------------------- (85) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(z0, s(s(y1)), s(h)) -> c7(A(z0, s(s(y1)), h)) by A(z0, s(s(s(y1))), s(h)) -> c7(A(z0, s(s(s(y1))), h)) A(s(y0), s(s(h)), s(h)) -> c7(A(s(y0), s(s(h)), h)) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(h, s(h), s(s(s(y0)))) -> c7(A(h, s(h), s(s(y0)))) A(z0, s(s(s(y1))), s(h)) -> c7(A(z0, s(s(s(y1))), h)) A(s(y0), s(s(h)), s(h)) -> c7(A(s(y0), s(s(h)), h)) S tuples: A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(h, s(h), s(s(s(y0)))) -> c7(A(h, s(h), s(s(y0)))) A(z0, s(s(s(y1))), s(h)) -> c7(A(z0, s(s(s(y1))), h)) A(s(y0), s(s(h)), s(h)) -> c7(A(s(y0), s(s(h)), h)) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_2, c2_1, c4_1, c8_1, c7_1 ---------------------------------------- (87) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace A(h, s(h), s(s(s(y0)))) -> c7(A(h, s(h), s(s(y0)))) by A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(h, s(h), s(s(s(s(h))))) -> c7(A(h, s(h), s(s(s(h))))) A(h, s(h), s(s(s(s(s(y0)))))) -> c7(A(h, s(h), s(s(s(s(y0)))))) ---------------------------------------- (88) Obligation: Complexity Dependency Tuples Problem Rules: a(h, h, z0) -> s(z0) a(z0, s(z1), h) -> a(z0, z1, s(h)) a(s(z0), h, z1) -> a(z0, z1, z1) a(z0, s(z1), s(z2)) -> a(z0, z1, a(z0, s(z1), z2)) Tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) SUM(cons(z0, cons(s(z1), cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y1, cons(y2, y3)))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(y2, y3)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(y2, y3))), A(z0, s(z1), h)) SUM(cons(z0, cons(s(z1), cons(h, y2)))) -> c4(SUM(cons(a(z0, z1, s(h)), cons(h, y2))), A(z0, s(z1), h)) SUM(cons(x0, cons(s(s(x1)), x2))) -> c4(A(x0, s(s(x1)), h)) SUM(cons(s(x0), cons(s(h), x1))) -> c4(A(s(x0), s(h), h)) SUM(cons(z0, cons(s(s(z1)), z2))) -> c4(SUM(cons(a(z0, z1, a(z0, z1, s(h))), z2)), A(z0, s(s(z1)), h)) SUM(cons(s(z0), cons(s(h), z1))) -> c4(SUM(cons(a(z0, h, a(z0, h, s(h))), z1)), A(s(z0), s(h), h)) SUM(cons(s(z0), cons(h, cons(y1, cons(y2, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y1, cons(y2, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(h, y2)))) -> c4(SUM(cons(a(z0, h, h), cons(h, y2))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(y3, cons(y4, y5)))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(y3, cons(y4, y5))))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y2, cons(h, y3))))) -> c4(SUM(cons(a(z0, h, h), cons(y2, cons(h, y3)))), A(s(z0), h, h)) SUM(cons(s(z0), cons(h, cons(y3, y4)))) -> c4(SUM(cons(a(z0, h, h), cons(y3, y4))), A(s(z0), h, h)) SUM(cons(s(s(z0)), cons(h, x1))) -> c4(SUM(cons(a(z0, h, h), x1)), A(s(s(z0)), h, h)) SUM(cons(s(s(x0)), cons(h, x1))) -> c4(A(s(s(x0)), h, h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(z0, s(s(s(y1))), s(h)) -> c7(A(z0, s(s(s(y1))), h)) A(s(y0), s(s(h)), s(h)) -> c7(A(s(y0), s(s(h)), h)) A(h, s(h), s(s(s(s(h))))) -> c7(A(h, s(h), s(s(s(h))))) A(h, s(h), s(s(s(s(s(y0)))))) -> c7(A(h, s(h), s(s(s(s(y0)))))) S tuples: A(s(y0), s(h), h) -> c6(A(s(y0), h, s(h))) A(s(z0), s(h), s(s(x2))) -> c7(A(s(z0), h, a(z0, a(s(z0), s(h), x2), a(s(z0), s(h), x2))), A(s(z0), s(h), s(x2))) A(z0, s(z1), s(s(h))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, s(h)))), A(z0, s(z1), s(h))) A(z0, s(z1), s(s(s(z2)))) -> c7(A(z0, z1, a(z0, z1, a(z0, z1, a(z0, s(z1), z2)))), A(z0, s(z1), s(s(z2)))) A(z0, s(s(z1)), s(h)) -> c7(A(z0, s(z1), a(z0, z1, a(z0, z1, s(h)))), A(z0, s(s(z1)), h)) A(s(z0), s(h), s(h)) -> c7(A(s(z0), h, a(z0, h, a(z0, h, s(h)))), A(s(z0), s(h), h)) A(s(z0), h, s(h)) -> c8(A(z0, s(h), s(h))) A(s(z0), h, s(s(h))) -> c8(A(z0, s(s(h)), s(s(h)))) A(s(z0), h, s(s(s(y2)))) -> c8(A(z0, s(s(s(y2))), s(s(s(y2))))) A(s(s(y0)), h, s(h)) -> c8(A(s(y0), s(h), s(h))) A(s(s(s(y0))), h, h) -> c8(A(s(s(y0)), h, h)) A(s(y0), s(h), s(h)) -> c7(A(s(y0), s(h), h)) A(z0, s(s(s(y1))), h) -> c6(A(z0, s(s(y1)), s(h))) A(s(y0), s(s(h)), h) -> c6(A(s(y0), s(h), s(h))) A(h, s(h), s(s(s(h)))) -> c7(A(h, s(h), s(s(h)))) A(h, s(h), s(s(s(s(y2))))) -> c7(A(h, s(h), s(s(s(y2))))) A(z0, s(s(s(y1))), s(h)) -> c7(A(z0, s(s(s(y1))), h)) A(s(y0), s(s(h)), s(h)) -> c7(A(s(y0), s(s(h)), h)) A(h, s(h), s(s(s(s(h))))) -> c7(A(h, s(h), s(s(s(h))))) A(h, s(h), s(s(s(s(s(y0)))))) -> c7(A(h, s(h), s(s(s(s(y0)))))) K tuples: SUM(cons(z0, cons(z1, cons(y1, y2)))) -> c4(SUM(cons(a(z0, z1, h), cons(y1, y2))), A(z0, z1, h)) APP(cons(z0, cons(z1, cons(y1, y2))), z3) -> c2(APP(cons(z1, cons(y1, y2)), z3)) Defined Rule Symbols: a_3 Defined Pair Symbols: SUM_1, A_3, APP_2 Compound Symbols: c4_2, c6_1, c7_2, c2_1, c4_1, c8_1, c7_1