KILLED proof of input_EbalKFE3xU.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). (0) CpxTRS (1) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxTRS (3) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxTRS (5) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 0 ms] (10) CpxTypedWeightedCompleteTrs (11) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedCompleteTrs (13) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (14) CpxRNTS (15) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxRNTS (17) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) IntTrsBoundProof [UPPER BOUND(ID), 473 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 56 ms] (24) CpxRNTS (25) ResultPropagationProof [UPPER BOUND(ID), 2 ms] (26) CpxRNTS (27) IntTrsBoundProof [UPPER BOUND(ID), 1512 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 410 ms] (30) CpxRNTS (31) CompletionProof [UPPER BOUND(ID), 0 ms] (32) CpxTypedWeightedCompleteTrs (33) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (34) CpxRNTS (35) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (36) CdtProblem (37) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem (39) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (40) CdtProblem (41) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 112 ms] (42) CdtProblem (43) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 284 ms] (44) CdtProblem (45) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (46) CdtProblem (47) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (54) CdtProblem (55) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (56) CdtProblem (57) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (58) CdtProblem (59) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 3 ms] (60) CdtProblem (61) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (62) CdtProblem (63) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (64) CdtProblem (65) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (66) CdtProblem (67) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (68) CdtProblem (69) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (70) CdtProblem (71) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (72) CdtProblem (73) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (74) CdtProblem (75) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (76) CdtProblem (77) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (78) 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) sum(cons(0, x), y) -> sum(x, y) sum(nil, y) -> y weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x))) weight(cons(n, nil)) -> n 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) sum(cons(0', x), y) -> sum(x, y) sum(nil, y) -> y weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0', x))) weight(cons(n, nil)) -> n 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) sum(cons(0, x), y) -> sum(x, y) sum(nil, y) -> y weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x))) weight(cons(n, nil)) -> n 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) [1] sum(cons(0, x), y) -> sum(x, y) [1] sum(nil, y) -> y [1] weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x))) [1] weight(cons(n, nil)) -> n [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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) [1] sum(cons(0, x), y) -> sum(x, y) [1] sum(nil, y) -> y [1] weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x))) [1] weight(cons(n, nil)) -> n [1] The TRS has the following type information: sum :: cons:nil -> cons:nil -> cons:nil cons :: s:0 -> cons:nil -> cons:nil s :: s:0 -> s:0 0 :: s:0 nil :: cons:nil weight :: cons:nil -> s:0 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: weight_1 (c) The following functions are completely defined: sum_2 Due to the following rules being added: sum(v0, v1) -> nil [0] 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) [1] sum(cons(0, x), y) -> sum(x, y) [1] sum(nil, y) -> y [1] weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x))) [1] weight(cons(n, nil)) -> n [1] sum(v0, v1) -> nil [0] The TRS has the following type information: sum :: cons:nil -> cons:nil -> cons:nil cons :: s:0 -> cons:nil -> cons:nil s :: s:0 -> s:0 0 :: s:0 nil :: cons:nil weight :: cons:nil -> s:0 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) [1] sum(cons(0, x), y) -> sum(x, y) [1] sum(nil, y) -> y [1] weight(cons(s(n'), cons(m, x))) -> weight(sum(cons(n', cons(m, x)), cons(s(0), x))) [2] weight(cons(0, cons(m, x))) -> weight(sum(cons(m, x), cons(0, x))) [2] weight(cons(n, cons(m, x))) -> weight(nil) [1] weight(cons(n, nil)) -> n [1] sum(v0, v1) -> nil [0] The TRS has the following type information: sum :: cons:nil -> cons:nil -> cons:nil cons :: s:0 -> cons:nil -> cons:nil s :: s:0 -> s:0 0 :: s:0 nil :: cons:nil weight :: cons:nil -> s:0 Rewrite Strategy: INNERMOST ---------------------------------------- (13) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 nil => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 1 }-> y :|: y >= 0, z = 0, z' = y sum(z, z') -{ 1 }-> sum(x, y) :|: x >= 0, y >= 0, z = 1 + 0 + x, z' = y sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 weight(z) -{ 1 }-> n :|: z = 1 + n + 0, n >= 0 weight(z) -{ 2 }-> weight(sum(1 + m + x, 1 + 0 + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 2 }-> weight(sum(1 + n' + (1 + m + x), 1 + (1 + 0) + x)) :|: z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 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: sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 1 }-> sum(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 2 }-> weight(sum(1 + m + x, 1 + 0 + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 2 }-> weight(sum(1 + n' + (1 + m + x), 1 + (1 + 0) + x)) :|: z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { sum } { weight } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 1 }-> sum(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 2 }-> weight(sum(1 + m + x, 1 + 0 + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 2 }-> weight(sum(1 + n' + (1 + m + x), 1 + (1 + 0) + x)) :|: z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {sum}, {weight} ---------------------------------------- (19) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 1 }-> sum(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 2 }-> weight(sum(1 + m + x, 1 + 0 + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 2 }-> weight(sum(1 + n' + (1 + m + x), 1 + (1 + 0) + x)) :|: z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {sum}, {weight} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: sum after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z + z' ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 1 }-> sum(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 2 }-> weight(sum(1 + m + x, 1 + 0 + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 2 }-> weight(sum(1 + n' + (1 + m + x), 1 + (1 + 0) + x)) :|: z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {sum}, {weight} Previous analysis results are: sum: runtime: ?, size: O(n^1) [z + z'] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: sum after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 1 + z ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 1 }-> sum(z - 1, z') :|: z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 2 }-> weight(sum(1 + m + x, 1 + 0 + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 2 }-> weight(sum(1 + n' + (1 + m + x), 1 + (1 + 0) + x)) :|: z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {weight} Previous analysis results are: sum: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] ---------------------------------------- (25) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 3 + n + x }-> s :|: s >= 0, s <= 1 + n + x + (1 + (1 + m) + y), n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 1 + z }-> s' :|: s' >= 0, s' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 5 + m + n' + x }-> weight(s'') :|: s'' >= 0, s'' <= 1 + n' + (1 + m + x) + (1 + (1 + 0) + x), z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 4 + m + x }-> weight(s1) :|: s1 >= 0, s1 <= 1 + m + x + (1 + 0 + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {weight} Previous analysis results are: sum: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] ---------------------------------------- (27) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: weight after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 3 + n + x }-> s :|: s >= 0, s <= 1 + n + x + (1 + (1 + m) + y), n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 1 + z }-> s' :|: s' >= 0, s' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 5 + m + n' + x }-> weight(s'') :|: s'' >= 0, s'' <= 1 + n' + (1 + m + x) + (1 + (1 + 0) + x), z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 4 + m + x }-> weight(s1) :|: s1 >= 0, s1 <= 1 + m + x + (1 + 0 + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {weight} Previous analysis results are: sum: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] weight: runtime: ?, size: INF ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: weight after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 3 + n + x }-> s :|: s >= 0, s <= 1 + n + x + (1 + (1 + m) + y), n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 1 + z }-> s' :|: s' >= 0, s' <= z - 1 + z', z - 1 >= 0, z' >= 0 sum(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 sum(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 weight(z) -{ 5 + m + n' + x }-> weight(s'') :|: s'' >= 0, s'' <= 1 + n' + (1 + m + x) + (1 + (1 + 0) + x), z = 1 + (1 + n') + (1 + m + x), x >= 0, n' >= 0, m >= 0 weight(z) -{ 4 + m + x }-> weight(s1) :|: s1 >= 0, s1 <= 1 + m + x + (1 + 0 + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 weight(z) -{ 1 }-> weight(0) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 1 }-> z - 1 :|: z - 1 >= 0 Function symbols to be analyzed: {weight} Previous analysis results are: sum: runtime: O(n^1) [1 + z], size: O(n^1) [z + z'] weight: runtime: INF, size: INF ---------------------------------------- (31) 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, v1) -> null_sum [0] weight(v0) -> null_weight [0] And the following fresh constants: null_sum, null_weight ---------------------------------------- (32) 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: sum(cons(s(n), x), cons(m, y)) -> sum(cons(n, x), cons(s(m), y)) [1] sum(cons(0, x), y) -> sum(x, y) [1] sum(nil, y) -> y [1] weight(cons(n, cons(m, x))) -> weight(sum(cons(n, cons(m, x)), cons(0, x))) [1] weight(cons(n, nil)) -> n [1] sum(v0, v1) -> null_sum [0] weight(v0) -> null_weight [0] The TRS has the following type information: sum :: cons:nil:null_sum -> cons:nil:null_sum -> cons:nil:null_sum cons :: s:0:null_weight -> cons:nil:null_sum -> cons:nil:null_sum s :: s:0:null_weight -> s:0:null_weight 0 :: s:0:null_weight nil :: cons:nil:null_sum weight :: cons:nil:null_sum -> s:0:null_weight null_sum :: cons:nil:null_sum null_weight :: s:0:null_weight Rewrite Strategy: INNERMOST ---------------------------------------- (33) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 nil => 0 null_sum => 0 null_weight => 0 ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: sum(z, z') -{ 1 }-> y :|: y >= 0, z = 0, z' = y sum(z, z') -{ 1 }-> sum(x, y) :|: x >= 0, y >= 0, z = 1 + 0 + x, z' = y sum(z, z') -{ 1 }-> sum(1 + n + x, 1 + (1 + m) + y) :|: n >= 0, z' = 1 + m + y, x >= 0, y >= 0, z = 1 + (1 + n) + x, m >= 0 sum(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 weight(z) -{ 1 }-> n :|: z = 1 + n + 0, n >= 0 weight(z) -{ 1 }-> weight(sum(1 + n + (1 + m + x), 1 + 0 + x)) :|: n >= 0, x >= 0, z = 1 + n + (1 + m + x), m >= 0 weight(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (35) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 weight(cons(z0, cons(z1, z2))) -> weight(sum(cons(z0, cons(z1, z2)), cons(0, z2))) weight(cons(z0, nil)) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) SUM(nil, z0) -> c2 WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) WEIGHT(cons(z0, nil)) -> c4 S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) SUM(nil, z0) -> c2 WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) WEIGHT(cons(z0, nil)) -> c4 K tuples:none Defined Rule Symbols: sum_2, weight_1 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c2, c3_2, c4 ---------------------------------------- (37) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing nodes: SUM(nil, z0) -> c2 WEIGHT(cons(z0, nil)) -> c4 ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 weight(cons(z0, cons(z1, z2))) -> weight(sum(cons(z0, cons(z1, z2)), cons(0, z2))) weight(cons(z0, nil)) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) K tuples:none Defined Rule Symbols: sum_2, weight_1 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2 ---------------------------------------- (39) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: weight(cons(z0, cons(z1, z2))) -> weight(sum(cons(z0, cons(z1, z2)), cons(0, z2))) weight(cons(z0, nil)) -> z0 ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) K tuples:none Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2 ---------------------------------------- (41) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) We considered the (Usable) Rules: sum(nil, z0) -> z0 sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) And the Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(SUM(x_1, x_2)) = 0 POL(WEIGHT(x_1)) = x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2)) = x_1 + x_2 POL(cons(x_1, x_2)) = [1] + x_1 + x_2 POL(nil) = 0 POL(s(x_1)) = x_1 POL(sum(x_1, x_2)) = x_2 ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2 ---------------------------------------- (43) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) We considered the (Usable) Rules: sum(nil, z0) -> z0 sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) And the Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(SUM(x_1, x_2)) = [2]x_1 + [2]x_2 POL(WEIGHT(x_1)) = x_1^2 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c3(x_1, x_2)) = x_1 + x_2 POL(cons(x_1, x_2)) = [2] + x_2 POL(nil) = [2] POL(s(x_1)) = 0 POL(sum(x_1, x_2)) = x_2 ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2 ---------------------------------------- (45) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) by WEIGHT(cons(s(z0), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(0), z3))), SUM(cons(s(z0), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(0, cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(0, x2))), SUM(cons(0, cons(x1, x2)), cons(0, x2))) ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(s(z0), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(0), z3))), SUM(cons(s(z0), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(0, cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(0, x2))), SUM(cons(0, cons(x1, x2)), cons(0, x2))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2 ---------------------------------------- (47) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace WEIGHT(cons(s(z0), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(0), z3))), SUM(cons(s(z0), cons(x1, z3)), cons(0, z3))) by WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(s(x0), cons(x1, x2))) -> c3(SUM(cons(s(x0), cons(x1, x2)), cons(0, x2))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(0, cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(0, x2))), SUM(cons(0, cons(x1, x2)), cons(0, x2))) WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(s(x0), cons(x1, x2))) -> c3(SUM(cons(s(x0), cons(x1, x2)), cons(0, x2))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2, c3_1 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace WEIGHT(cons(0, cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(0, x2))), SUM(cons(0, cons(x1, x2)), cons(0, x2))) by WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(x0, x1))) -> c3(SUM(cons(0, cons(x0, x1)), cons(0, x1))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(s(x0), cons(x1, x2))) -> c3(SUM(cons(s(x0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(x0, x1))) -> c3(SUM(cons(0, cons(x0, x1)), cons(0, x1))) S tuples: SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c_1, c1_1, c3_2, c3_1 ---------------------------------------- (51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(z0), z1), cons(z2, z3)) -> c(SUM(cons(z0, z1), cons(s(z2), z3))) by SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(s(x0), cons(x1, x2))) -> c3(SUM(cons(s(x0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(x0, x1))) -> c3(SUM(cons(0, cons(x0, x1)), cons(0, x1))) SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) S tuples: SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) Defined Rule Symbols: sum_2 Defined Pair Symbols: SUM_2, WEIGHT_1 Compound Symbols: c1_1, c3_2, c3_1, c_1 ---------------------------------------- (53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, z0), z1) -> c1(SUM(z0, z1)) by SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(s(x0), cons(x1, x2))) -> c3(SUM(cons(s(x0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(x0, x1))) -> c3(SUM(cons(0, cons(x0, x1)), cons(0, x1))) SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) S tuples: SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(s(x0), cons(x1, x2))) -> c3(SUM(cons(s(x0), cons(x1, x2)), cons(0, x2))) by WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(x0, x1))) -> c3(SUM(cons(0, cons(x0, x1)), cons(0, x1))) SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) S tuples: SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(0, cons(x0, x1))) -> c3(SUM(cons(0, cons(x0, x1)), cons(0, x1))) by WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) S tuples: SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c_1, c1_1, c3_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(s(y0)), z1), cons(z2, z3)) -> c(SUM(cons(s(y0), z1), cons(s(z2), z3))) by SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) S tuples: SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c_1, c1_1, c3_1 ---------------------------------------- (61) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(s(0), z1), cons(z2, z3)) -> c(SUM(cons(0, z1), cons(s(z2), z3))) by SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c1_1, c3_1, c_1 ---------------------------------------- (63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, cons(0, y0)), z1) -> c1(SUM(cons(0, y0), z1)) by SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c1_1, c3_1, c_1 ---------------------------------------- (65) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3)) -> c1(SUM(cons(s(s(y0)), y1), cons(y2, y3))) by SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c1_1, c3_1, c_1 ---------------------------------------- (67) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace SUM(cons(0, cons(s(0), y0)), cons(y1, y2)) -> c1(SUM(cons(s(0), y0), cons(y1, y2))) by SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (69) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(s(s(y0)), cons(z1, z2))) -> c3(SUM(cons(s(s(y0)), cons(z1, z2)), cons(0, z2))) by WEIGHT(cons(s(s(s(y0))), cons(z1, z2))) -> c3(SUM(cons(s(s(s(y0))), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(s(0)), cons(z1, z2))) -> c3(SUM(cons(s(s(0)), cons(z1, z2)), cons(0, z2))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) WEIGHT(cons(s(s(s(y0))), cons(z1, z2))) -> c3(SUM(cons(s(s(s(y0))), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(s(0)), cons(z1, z2))) -> c3(SUM(cons(s(s(0)), cons(z1, z2)), cons(0, z2))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (71) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(s(0), cons(z1, z2))) -> c3(SUM(cons(s(0), cons(z1, z2)), cons(0, z2))) by WEIGHT(cons(s(0), cons(0, z1))) -> c3(SUM(cons(s(0), cons(0, z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(s(y0)), z1))) -> c3(SUM(cons(s(0), cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(0), z1))) -> c3(SUM(cons(s(0), cons(s(0), z1)), cons(0, z1))) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) WEIGHT(cons(s(s(s(y0))), cons(z1, z2))) -> c3(SUM(cons(s(s(s(y0))), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(s(0)), cons(z1, z2))) -> c3(SUM(cons(s(s(0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(0, z1))) -> c3(SUM(cons(s(0), cons(0, z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(s(y0)), z1))) -> c3(SUM(cons(s(0), cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(0), z1))) -> c3(SUM(cons(s(0), cons(s(0), z1)), cons(0, z1))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(0, cons(0, z1))) -> c3(SUM(cons(0, cons(0, z1)), cons(0, z1))) by WEIGHT(cons(0, cons(0, cons(0, y0)))) -> c3(SUM(cons(0, cons(0, cons(0, y0))), cons(0, cons(0, y0)))) WEIGHT(cons(0, cons(0, cons(s(s(y0)), y1)))) -> c3(SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(0, cons(s(s(y0)), y1)))) WEIGHT(cons(0, cons(0, cons(s(0), y0)))) -> c3(SUM(cons(0, cons(0, cons(s(0), y0))), cons(0, cons(s(0), y0)))) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) WEIGHT(cons(s(s(s(y0))), cons(z1, z2))) -> c3(SUM(cons(s(s(s(y0))), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(s(0)), cons(z1, z2))) -> c3(SUM(cons(s(s(0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(0, z1))) -> c3(SUM(cons(s(0), cons(0, z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(s(y0)), z1))) -> c3(SUM(cons(s(0), cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(0), z1))) -> c3(SUM(cons(s(0), cons(s(0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, cons(0, y0)))) -> c3(SUM(cons(0, cons(0, cons(0, y0))), cons(0, cons(0, y0)))) WEIGHT(cons(0, cons(0, cons(s(s(y0)), y1)))) -> c3(SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(0, cons(s(s(y0)), y1)))) WEIGHT(cons(0, cons(0, cons(s(0), y0)))) -> c3(SUM(cons(0, cons(0, cons(s(0), y0))), cons(0, cons(s(0), y0)))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (75) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(0, cons(s(s(y0)), z1))) -> c3(SUM(cons(0, cons(s(s(y0)), z1)), cons(0, z1))) by WEIGHT(cons(0, cons(s(s(s(y0))), z1))) -> c3(SUM(cons(0, cons(s(s(s(y0))), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(0)), z1))) -> c3(SUM(cons(0, cons(s(s(0)), z1)), cons(0, z1))) ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) WEIGHT(cons(s(s(s(y0))), cons(z1, z2))) -> c3(SUM(cons(s(s(s(y0))), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(s(0)), cons(z1, z2))) -> c3(SUM(cons(s(s(0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(0, z1))) -> c3(SUM(cons(s(0), cons(0, z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(s(y0)), z1))) -> c3(SUM(cons(s(0), cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(0), z1))) -> c3(SUM(cons(s(0), cons(s(0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, cons(0, y0)))) -> c3(SUM(cons(0, cons(0, cons(0, y0))), cons(0, cons(0, y0)))) WEIGHT(cons(0, cons(0, cons(s(s(y0)), y1)))) -> c3(SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(0, cons(s(s(y0)), y1)))) WEIGHT(cons(0, cons(0, cons(s(0), y0)))) -> c3(SUM(cons(0, cons(0, cons(s(0), y0))), cons(0, cons(s(0), y0)))) WEIGHT(cons(0, cons(s(s(s(y0))), z1))) -> c3(SUM(cons(0, cons(s(s(s(y0))), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(0)), z1))) -> c3(SUM(cons(0, cons(s(s(0)), z1)), cons(0, z1))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c3_1, c_1, c1_1 ---------------------------------------- (77) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace WEIGHT(cons(0, cons(s(0), z1))) -> c3(SUM(cons(0, cons(s(0), z1)), cons(0, z1))) by WEIGHT(cons(0, cons(s(0), cons(0, y0)))) -> c3(SUM(cons(0, cons(s(0), cons(0, y0))), cons(0, cons(0, y0)))) WEIGHT(cons(0, cons(s(0), cons(s(s(y0)), y1)))) -> c3(SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(0, cons(s(s(y0)), y1)))) WEIGHT(cons(0, cons(s(0), cons(s(0), y0)))) -> c3(SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(0, cons(s(0), y0)))) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: sum(cons(s(z0), z1), cons(z2, z3)) -> sum(cons(z0, z1), cons(s(z2), z3)) sum(cons(0, z0), z1) -> sum(z0, z1) sum(nil, z0) -> z0 Tuples: WEIGHT(cons(s(s(z0)), cons(x1, z3))) -> c3(WEIGHT(sum(cons(z0, cons(x1, z3)), cons(s(s(0)), z3))), SUM(cons(s(s(z0)), cons(x1, z3)), cons(0, z3))) WEIGHT(cons(s(0), cons(x1, x2))) -> c3(WEIGHT(sum(cons(x1, x2), cons(s(0), x2))), SUM(cons(s(0), cons(x1, x2)), cons(0, x2))) WEIGHT(cons(0, cons(s(z0), z1))) -> c3(WEIGHT(sum(cons(z0, z1), cons(s(0), z1))), SUM(cons(0, cons(s(z0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, z0))) -> c3(WEIGHT(sum(z0, cons(0, z0))), SUM(cons(0, cons(0, z0)), cons(0, z0))) SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) WEIGHT(cons(s(s(s(y0))), cons(z1, z2))) -> c3(SUM(cons(s(s(s(y0))), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(s(0)), cons(z1, z2))) -> c3(SUM(cons(s(s(0)), cons(z1, z2)), cons(0, z2))) WEIGHT(cons(s(0), cons(0, z1))) -> c3(SUM(cons(s(0), cons(0, z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(s(y0)), z1))) -> c3(SUM(cons(s(0), cons(s(s(y0)), z1)), cons(0, z1))) WEIGHT(cons(s(0), cons(s(0), z1))) -> c3(SUM(cons(s(0), cons(s(0), z1)), cons(0, z1))) WEIGHT(cons(0, cons(0, cons(0, y0)))) -> c3(SUM(cons(0, cons(0, cons(0, y0))), cons(0, cons(0, y0)))) WEIGHT(cons(0, cons(0, cons(s(s(y0)), y1)))) -> c3(SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(0, cons(s(s(y0)), y1)))) WEIGHT(cons(0, cons(0, cons(s(0), y0)))) -> c3(SUM(cons(0, cons(0, cons(s(0), y0))), cons(0, cons(s(0), y0)))) WEIGHT(cons(0, cons(s(s(s(y0))), z1))) -> c3(SUM(cons(0, cons(s(s(s(y0))), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(s(0)), z1))) -> c3(SUM(cons(0, cons(s(s(0)), z1)), cons(0, z1))) WEIGHT(cons(0, cons(s(0), cons(0, y0)))) -> c3(SUM(cons(0, cons(s(0), cons(0, y0))), cons(0, cons(0, y0)))) WEIGHT(cons(0, cons(s(0), cons(s(s(y0)), y1)))) -> c3(SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(0, cons(s(s(y0)), y1)))) WEIGHT(cons(0, cons(s(0), cons(s(0), y0)))) -> c3(SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(0, cons(s(0), y0)))) S tuples: SUM(cons(s(s(s(y0))), z1), cons(z2, z3)) -> c(SUM(cons(s(s(y0)), z1), cons(s(z2), z3))) SUM(cons(s(s(0)), z1), cons(z2, z3)) -> c(SUM(cons(s(0), z1), cons(s(z2), z3))) SUM(cons(s(0), cons(0, y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(0, y0)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(s(y0)), y1)), cons(s(z1), z2))) SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2)) -> c(SUM(cons(0, cons(s(0), y0)), cons(s(z1), z2))) K tuples: WEIGHT(cons(z0, cons(z1, z2))) -> c3(WEIGHT(sum(cons(z0, cons(z1, z2)), cons(0, z2))), SUM(cons(z0, cons(z1, z2)), cons(0, z2))) SUM(cons(0, cons(0, cons(0, y0))), z1) -> c1(SUM(cons(0, cons(0, y0)), z1)) SUM(cons(0, cons(0, cons(s(s(y0)), y1))), cons(y2, y3)) -> c1(SUM(cons(0, cons(s(s(y0)), y1)), cons(y2, y3))) SUM(cons(0, cons(0, cons(s(0), y0))), cons(y1, y2)) -> c1(SUM(cons(0, cons(s(0), y0)), cons(y1, y2))) SUM(cons(0, cons(s(s(s(y0))), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(s(y0))), z1), cons(z2, z3))) SUM(cons(0, cons(s(s(0)), z1)), cons(z2, z3)) -> c1(SUM(cons(s(s(0)), z1), cons(z2, z3))) SUM(cons(0, cons(s(0), cons(0, y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(0, y0)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(s(y0)), y1))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(s(y0)), y1)), cons(z1, z2))) SUM(cons(0, cons(s(0), cons(s(0), y0))), cons(z1, z2)) -> c1(SUM(cons(s(0), cons(s(0), y0)), cons(z1, z2))) Defined Rule Symbols: sum_2 Defined Pair Symbols: WEIGHT_1, SUM_2 Compound Symbols: c3_2, c_1, c1_1, c3_1