KILLED proof of input_jh1LYSIfo1.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), 880 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 188 ms] (24) CpxRNTS (25) CompletionProof [UPPER BOUND(ID), 0 ms] (26) CpxTypedWeightedCompleteTrs (27) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (28) CpxRNTS (29) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (30) CdtProblem (31) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (32) CdtProblem (33) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (36) CdtProblem (37) CdtKnowledgeProof [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)), 109 ms] (42) CdtProblem (43) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (44) CdtProblem (45) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 83 ms] (46) CdtProblem (47) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtNarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CdtProblem (51) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CdtProblem (53) CdtInstantiationProof [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), 0 ms] (60) CdtProblem (61) CdtRewritingProof [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) CdtRewritingProof [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 (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), 0 ms] (86) 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: from(X) -> cons(X, from(s(X))) 2ndspos(0, Z) -> rnil 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) 2ndsneg(0, Z) -> rnil 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) pi(X) -> 2ndspos(X, from(0)) plus(0, Y) -> Y plus(s(X), Y) -> s(plus(X, Y)) times(0, Y) -> 0 times(s(X), Y) -> plus(Y, times(X, Y)) square(X) -> times(X, X) 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: from(X) -> cons(X, from(s(X))) 2ndspos(0', Z) -> rnil 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) 2ndsneg(0', Z) -> rnil 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) pi(X) -> 2ndspos(X, from(0')) plus(0', Y) -> Y plus(s(X), Y) -> s(plus(X, Y)) times(0', Y) -> 0' times(s(X), Y) -> plus(Y, times(X, Y)) square(X) -> times(X, X) 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: from(X) -> cons(X, from(s(X))) 2ndspos(0, Z) -> rnil 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) 2ndsneg(0, Z) -> rnil 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) pi(X) -> 2ndspos(X, from(0)) plus(0, Y) -> Y plus(s(X), Y) -> s(plus(X, Y)) times(0, Y) -> 0 times(s(X), Y) -> plus(Y, times(X, Y)) square(X) -> times(X, X) 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: from(X) -> cons(X, from(s(X))) [1] 2ndspos(0, Z) -> rnil [1] 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) [1] 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) [1] 2ndsneg(0, Z) -> rnil [1] 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) [1] 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) [1] pi(X) -> 2ndspos(X, from(0)) [1] plus(0, Y) -> Y [1] plus(s(X), Y) -> s(plus(X, Y)) [1] times(0, Y) -> 0 [1] times(s(X), Y) -> plus(Y, times(X, Y)) [1] square(X) -> times(X, X) [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: from(X) -> cons(X, from(s(X))) [1] 2ndspos(0, Z) -> rnil [1] 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) [1] 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) [1] 2ndsneg(0, Z) -> rnil [1] 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) [1] 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) [1] pi(X) -> 2ndspos(X, from(0)) [1] plus(0, Y) -> Y [1] plus(s(X), Y) -> s(plus(X, Y)) [1] times(0, Y) -> 0 [1] times(s(X), Y) -> plus(Y, times(X, Y)) [1] square(X) -> times(X, X) [1] The TRS has the following type information: from :: s:0 -> cons:cons2 cons :: s:0 -> cons:cons2 -> cons:cons2 s :: s:0 -> s:0 2ndspos :: s:0 -> cons:cons2 -> rnil:rcons 0 :: s:0 rnil :: rnil:rcons cons2 :: s:0 -> cons:cons2 -> cons:cons2 rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons posrecip :: s:0 -> posrecip:negrecip 2ndsneg :: s:0 -> cons:cons2 -> rnil:rcons negrecip :: s:0 -> posrecip:negrecip pi :: s:0 -> rnil:rcons plus :: s:0 -> s:0 -> s:0 times :: s:0 -> s:0 -> s:0 square :: s:0 -> 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: 2ndspos_2 2ndsneg_2 pi_1 square_1 (c) The following functions are completely defined: times_2 from_1 plus_2 Due to the following rules being added: none And the following fresh constants: const, const1 ---------------------------------------- (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: from(X) -> cons(X, from(s(X))) [1] 2ndspos(0, Z) -> rnil [1] 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) [1] 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) [1] 2ndsneg(0, Z) -> rnil [1] 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) [1] 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) [1] pi(X) -> 2ndspos(X, from(0)) [1] plus(0, Y) -> Y [1] plus(s(X), Y) -> s(plus(X, Y)) [1] times(0, Y) -> 0 [1] times(s(X), Y) -> plus(Y, times(X, Y)) [1] square(X) -> times(X, X) [1] The TRS has the following type information: from :: s:0 -> cons:cons2 cons :: s:0 -> cons:cons2 -> cons:cons2 s :: s:0 -> s:0 2ndspos :: s:0 -> cons:cons2 -> rnil:rcons 0 :: s:0 rnil :: rnil:rcons cons2 :: s:0 -> cons:cons2 -> cons:cons2 rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons posrecip :: s:0 -> posrecip:negrecip 2ndsneg :: s:0 -> cons:cons2 -> rnil:rcons negrecip :: s:0 -> posrecip:negrecip pi :: s:0 -> rnil:rcons plus :: s:0 -> s:0 -> s:0 times :: s:0 -> s:0 -> s:0 square :: s:0 -> s:0 const :: cons:cons2 const1 :: posrecip:negrecip 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: from(X) -> cons(X, from(s(X))) [1] 2ndspos(0, Z) -> rnil [1] 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) [1] 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) [1] 2ndsneg(0, Z) -> rnil [1] 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) [1] 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) [1] pi(X) -> 2ndspos(X, cons(0, from(s(0)))) [2] plus(0, Y) -> Y [1] plus(s(X), Y) -> s(plus(X, Y)) [1] times(0, Y) -> 0 [1] times(s(0), Y) -> plus(Y, 0) [2] times(s(s(X')), Y) -> plus(Y, plus(Y, times(X', Y))) [2] square(X) -> times(X, X) [1] The TRS has the following type information: from :: s:0 -> cons:cons2 cons :: s:0 -> cons:cons2 -> cons:cons2 s :: s:0 -> s:0 2ndspos :: s:0 -> cons:cons2 -> rnil:rcons 0 :: s:0 rnil :: rnil:rcons cons2 :: s:0 -> cons:cons2 -> cons:cons2 rcons :: posrecip:negrecip -> rnil:rcons -> rnil:rcons posrecip :: s:0 -> posrecip:negrecip 2ndsneg :: s:0 -> cons:cons2 -> rnil:rcons negrecip :: s:0 -> posrecip:negrecip pi :: s:0 -> rnil:rcons plus :: s:0 -> s:0 -> s:0 times :: s:0 -> s:0 -> s:0 square :: s:0 -> s:0 const :: cons:cons2 const1 :: posrecip:negrecip 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 rnil => 0 const => 0 const1 => 0 ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + N, 1 + X + Z) :|: Z >= 0, z = 1 + N, X >= 0, z' = 1 + X + Z, N >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: Z >= 0, z' = Z, z = 0 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(N, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, z = 1 + N, X >= 0, N >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + N, 1 + X + Z) :|: Z >= 0, z = 1 + N, X >= 0, z' = 1 + X + Z, N >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: Z >= 0, z' = Z, z = 0 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(N, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, z = 1 + N, X >= 0, N >= 0 from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X pi(z) -{ 2 }-> 2ndspos(X, 1 + 0 + from(1 + 0)) :|: X >= 0, z = X plus(z, z') -{ 1 }-> Y :|: z' = Y, Y >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0 square(z) -{ 1 }-> times(X, X) :|: X >= 0, z = X times(z, z') -{ 2 }-> plus(Y, plus(Y, times(X', Y))) :|: z' = Y, Y >= 0, X' >= 0, z = 1 + (1 + X') times(z, z') -{ 2 }-> plus(Y, 0) :|: z' = Y, Y >= 0, z = 1 + 0 times(z, z') -{ 1 }-> 0 :|: z' = Y, Y >= 0, z = 0 ---------------------------------------- (15) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 pi(z) -{ 2 }-> 2ndspos(z, 1 + 0 + from(1 + 0)) :|: z >= 0 plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0 square(z) -{ 1 }-> times(z, z) :|: z >= 0 times(z, z') -{ 2 }-> plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0 times(z, z') -{ 2 }-> plus(z', 0) :|: z' >= 0, z = 1 + 0 times(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 ---------------------------------------- (17) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { from } { 2ndspos, 2ndsneg } { plus } { pi } { times } { square } ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 pi(z) -{ 2 }-> 2ndspos(z, 1 + 0 + from(1 + 0)) :|: z >= 0 plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0 square(z) -{ 1 }-> times(z, z) :|: z >= 0 times(z, z') -{ 2 }-> plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0 times(z, z') -{ 2 }-> plus(z', 0) :|: z' >= 0, z = 1 + 0 times(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 Function symbols to be analyzed: {from}, {2ndspos,2ndsneg}, {plus}, {pi}, {times}, {square} ---------------------------------------- (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: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 pi(z) -{ 2 }-> 2ndspos(z, 1 + 0 + from(1 + 0)) :|: z >= 0 plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0 square(z) -{ 1 }-> times(z, z) :|: z >= 0 times(z, z') -{ 2 }-> plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0 times(z, z') -{ 2 }-> plus(z', 0) :|: z' >= 0, z = 1 + 0 times(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 Function symbols to be analyzed: {from}, {2ndspos,2ndsneg}, {plus}, {pi}, {times}, {square} ---------------------------------------- (21) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: from after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 0 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 pi(z) -{ 2 }-> 2ndspos(z, 1 + 0 + from(1 + 0)) :|: z >= 0 plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0 square(z) -{ 1 }-> times(z, z) :|: z >= 0 times(z, z') -{ 2 }-> plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0 times(z, z') -{ 2 }-> plus(z', 0) :|: z' >= 0, z = 1 + 0 times(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 Function symbols to be analyzed: {from}, {2ndspos,2ndsneg}, {plus}, {pi}, {times}, {square} Previous analysis results are: from: runtime: ?, size: O(1) [0] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: from after applying outer abstraction to obtain an ITS, resulting in: INF with polynomial bound: ? ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + (z - 1), 1 + X + Z) :|: Z >= 0, X >= 0, z' = 1 + X + Z, z - 1 >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(z - 1, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, X >= 0, z - 1 >= 0 from(z) -{ 1 }-> 1 + z + from(1 + z) :|: z >= 0 pi(z) -{ 2 }-> 2ndspos(z, 1 + 0 + from(1 + 0)) :|: z >= 0 plus(z, z') -{ 1 }-> z' :|: z' >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(z - 1, z') :|: z' >= 0, z - 1 >= 0 square(z) -{ 1 }-> times(z, z) :|: z >= 0 times(z, z') -{ 2 }-> plus(z', plus(z', times(z - 2, z'))) :|: z' >= 0, z - 2 >= 0 times(z, z') -{ 2 }-> plus(z', 0) :|: z' >= 0, z = 1 + 0 times(z, z') -{ 1 }-> 0 :|: z' >= 0, z = 0 Function symbols to be analyzed: {from}, {2ndspos,2ndsneg}, {plus}, {pi}, {times}, {square} Previous analysis results are: from: runtime: INF, size: O(1) [0] ---------------------------------------- (25) 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: 2ndspos(v0, v1) -> null_2ndspos [0] 2ndsneg(v0, v1) -> null_2ndsneg [0] And the following fresh constants: null_2ndspos, null_2ndsneg, const, const1 ---------------------------------------- (26) 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: from(X) -> cons(X, from(s(X))) [1] 2ndspos(0, Z) -> rnil [1] 2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, Z)) [1] 2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, Z)) [1] 2ndsneg(0, Z) -> rnil [1] 2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, Z)) [1] 2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, Z)) [1] pi(X) -> 2ndspos(X, from(0)) [1] plus(0, Y) -> Y [1] plus(s(X), Y) -> s(plus(X, Y)) [1] times(0, Y) -> 0 [1] times(s(X), Y) -> plus(Y, times(X, Y)) [1] square(X) -> times(X, X) [1] 2ndspos(v0, v1) -> null_2ndspos [0] 2ndsneg(v0, v1) -> null_2ndsneg [0] The TRS has the following type information: from :: s:0 -> cons:cons2 cons :: s:0 -> cons:cons2 -> cons:cons2 s :: s:0 -> s:0 2ndspos :: s:0 -> cons:cons2 -> rnil:rcons:null_2ndspos:null_2ndsneg 0 :: s:0 rnil :: rnil:rcons:null_2ndspos:null_2ndsneg cons2 :: s:0 -> cons:cons2 -> cons:cons2 rcons :: posrecip:negrecip -> rnil:rcons:null_2ndspos:null_2ndsneg -> rnil:rcons:null_2ndspos:null_2ndsneg posrecip :: s:0 -> posrecip:negrecip 2ndsneg :: s:0 -> cons:cons2 -> rnil:rcons:null_2ndspos:null_2ndsneg negrecip :: s:0 -> posrecip:negrecip pi :: s:0 -> rnil:rcons:null_2ndspos:null_2ndsneg plus :: s:0 -> s:0 -> s:0 times :: s:0 -> s:0 -> s:0 square :: s:0 -> s:0 null_2ndspos :: rnil:rcons:null_2ndspos:null_2ndsneg null_2ndsneg :: rnil:rcons:null_2ndspos:null_2ndsneg const :: cons:cons2 const1 :: posrecip:negrecip Rewrite Strategy: INNERMOST ---------------------------------------- (27) 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 rnil => 0 null_2ndspos => 0 null_2ndsneg => 0 const => 0 const1 => 0 ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: 2ndsneg(z, z') -{ 1 }-> 2ndsneg(1 + N, 1 + X + Z) :|: Z >= 0, z = 1 + N, X >= 0, z' = 1 + X + Z, N >= 0 2ndsneg(z, z') -{ 1 }-> 0 :|: Z >= 0, z' = Z, z = 0 2ndsneg(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 2ndsneg(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndspos(N, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, z = 1 + N, X >= 0, N >= 0 2ndspos(z, z') -{ 1 }-> 2ndspos(1 + N, 1 + X + Z) :|: Z >= 0, z = 1 + N, X >= 0, z' = 1 + X + Z, N >= 0 2ndspos(z, z') -{ 1 }-> 0 :|: Z >= 0, z' = Z, z = 0 2ndspos(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 2ndspos(z, z') -{ 1 }-> 1 + (1 + Y) + 2ndsneg(N, Z) :|: Z >= 0, z' = 1 + X + (1 + Y + Z), Y >= 0, z = 1 + N, X >= 0, N >= 0 from(z) -{ 1 }-> 1 + X + from(1 + X) :|: X >= 0, z = X pi(z) -{ 1 }-> 2ndspos(X, from(0)) :|: X >= 0, z = X plus(z, z') -{ 1 }-> Y :|: z' = Y, Y >= 0, z = 0 plus(z, z') -{ 1 }-> 1 + plus(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0 square(z) -{ 1 }-> times(X, X) :|: X >= 0, z = X times(z, z') -{ 1 }-> plus(Y, times(X, Y)) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0 times(z, z') -{ 1 }-> 0 :|: z' = Y, Y >= 0, z = 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (29) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) 2ndspos(0, z0) -> rnil 2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, z2)) 2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3)) 2ndsneg(0, z0) -> rnil 2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, z2)) 2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3)) pi(z0) -> 2ndspos(z0, from(0)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) square(z0) -> times(z0, z0) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(0, z0) -> c1 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(0, z0) -> c4 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PI(z0) -> c7(2NDSPOS(z0, from(0)), FROM(0)) PLUS(0, z0) -> c8 PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(0, z0) -> c10 TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) SQUARE(z0) -> c12(TIMES(z0, z0)) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(0, z0) -> c1 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(0, z0) -> c4 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PI(z0) -> c7(2NDSPOS(z0, from(0)), FROM(0)) PLUS(0, z0) -> c8 PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(0, z0) -> c10 TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) SQUARE(z0) -> c12(TIMES(z0, z0)) K tuples:none Defined Rule Symbols: from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PI_1, PLUS_2, TIMES_2, SQUARE_1 Compound Symbols: c_1, c1, c2_1, c3_1, c4, c5_1, c6_1, c7_2, c8, c9_1, c10, c11_2, c12_1 ---------------------------------------- (31) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: SQUARE(z0) -> c12(TIMES(z0, z0)) Removed 4 trailing nodes: PLUS(0, z0) -> c8 2NDSPOS(0, z0) -> c1 2NDSNEG(0, z0) -> c4 TIMES(0, z0) -> c10 ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) 2ndspos(0, z0) -> rnil 2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, z2)) 2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3)) 2ndsneg(0, z0) -> rnil 2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, z2)) 2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3)) pi(z0) -> 2ndspos(z0, from(0)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) square(z0) -> times(z0, z0) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PI(z0) -> c7(2NDSPOS(z0, from(0)), FROM(0)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PI(z0) -> c7(2NDSPOS(z0, from(0)), FROM(0)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) K tuples:none Defined Rule Symbols: from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PI_1, PLUS_2, TIMES_2 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c7_2, c9_1, c11_2 ---------------------------------------- (33) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) 2ndspos(0, z0) -> rnil 2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, z2)) 2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3)) 2ndsneg(0, z0) -> rnil 2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, z2)) 2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3)) pi(z0) -> 2ndspos(z0, from(0)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) square(z0) -> times(z0, z0) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) PI(z0) -> c1(FROM(0)) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) PI(z0) -> c1(FROM(0)) K tuples:none Defined Rule Symbols: from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (35) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: PI(z0) -> c1(FROM(0)) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) 2ndspos(0, z0) -> rnil 2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, z2)) 2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3)) 2ndsneg(0, z0) -> rnil 2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, z2)) 2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3)) pi(z0) -> 2ndspos(z0, from(0)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) square(z0) -> times(z0, z0) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) K tuples:none Defined Rule Symbols: from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (37) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: PI(z0) -> c1(2NDSPOS(z0, from(0))) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: from(z0) -> cons(z0, from(s(z0))) 2ndspos(0, z0) -> rnil 2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, z2)) 2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3)) 2ndsneg(0, z0) -> rnil 2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, z2)) 2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3)) pi(z0) -> 2ndspos(z0, from(0)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) square(z0) -> times(z0, z0) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) Defined Rule Symbols: from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (39) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: 2ndspos(0, z0) -> rnil 2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, z2)) 2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, z3)) 2ndsneg(0, z0) -> rnil 2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, z2)) 2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, z3)) pi(z0) -> 2ndspos(z0, from(0)) square(z0) -> times(z0, z0) ---------------------------------------- (40) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (41) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) We considered the (Usable) Rules: from(z0) -> cons(z0, from(s(z0))) And the Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(2NDSNEG(x_1, x_2)) = [1] + x_1 + x_2 POL(2NDSPOS(x_1, x_2)) = [1] + x_1 + x_2 POL(FROM(x_1)) = 0 POL(PI(x_1)) = [1] + x_1 POL(PLUS(x_1, x_2)) = 0 POL(TIMES(x_1, x_2)) = x_1 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c11(x_1, x_2)) = x_1 + x_2 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = x_2 POL(cons2(x_1, x_2)) = x_2 POL(from(x_1)) = 0 POL(plus(x_1, x_2)) = [1] + x_1 + x_2 POL(s(x_1)) = [1] + x_1 POL(times(x_1, x_2)) = [1] + x_1 + x_2 ---------------------------------------- (42) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (43) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) ---------------------------------------- (44) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (45) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) We considered the (Usable) Rules:none And the Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(2NDSNEG(x_1, x_2)) = 0 POL(2NDSPOS(x_1, x_2)) = 0 POL(FROM(x_1)) = 0 POL(PI(x_1)) = [1] + [2]x_1^2 POL(PLUS(x_1, x_2)) = [2]x_1 POL(TIMES(x_1, x_2)) = x_1*x_2 POL(c(x_1)) = x_1 POL(c1(x_1)) = x_1 POL(c11(x_1, x_2)) = x_1 + x_2 POL(c2(x_1)) = x_1 POL(c3(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c9(x_1)) = x_1 POL(cons(x_1, x_2)) = 0 POL(cons2(x_1, x_2)) = 0 POL(from(x_1)) = 0 POL(plus(x_1, x_2)) = [2] + x_1^2 POL(s(x_1)) = [2] + x_1 POL(times(x_1, x_2)) = [2]x_2^2 ---------------------------------------- (46) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(z0) -> c1(2NDSPOS(z0, from(0))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (47) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace PI(z0) -> c1(2NDSPOS(z0, from(0))) by PI(x0) -> c1(2NDSPOS(x0, cons(0, from(s(0))))) ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, from(s(0))))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (49) CdtNarrowingProof (BOTH BOUNDS(ID, ID)) Use narrowing to replace PI(x0) -> c1(2NDSPOS(x0, cons(0, from(s(0))))) by PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) ---------------------------------------- (50) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: FROM(z0) -> c(FROM(s(z0))) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) S tuples: FROM(z0) -> c(FROM(s(z0))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1 Compound Symbols: c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1 ---------------------------------------- (51) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace FROM(z0) -> c(FROM(s(z0))) by FROM(s(x0)) -> c(FROM(s(s(x0)))) ---------------------------------------- (52) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) FROM(s(x0)) -> c(FROM(s(s(x0)))) S tuples: FROM(s(x0)) -> c(FROM(s(s(x0)))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1, FROM_1 Compound Symbols: c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1, c_1 ---------------------------------------- (53) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace FROM(s(x0)) -> c(FROM(s(s(x0)))) by FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) ---------------------------------------- (54) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1, FROM_1 Compound Symbols: c2_1, c3_1, c5_1, c6_1, c9_1, c11_2, c1_1, c_1 ---------------------------------------- (55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSPOS(s(z0), cons(z1, z2)) -> c2(2NDSPOS(s(z0), cons2(z1, z2))) by 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) ---------------------------------------- (56) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: 2NDSPOS_2, 2NDSNEG_2, PLUS_2, TIMES_2, PI_1, FROM_1 Compound Symbols: c3_1, c5_1, c6_1, c9_1, c11_2, c1_1, c_1, c2_1 ---------------------------------------- (57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c3(2NDSNEG(z0, z3)) by 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) ---------------------------------------- (58) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: 2NDSNEG_2, PLUS_2, TIMES_2, PI_1, FROM_1, 2NDSPOS_2 Compound Symbols: c5_1, c6_1, c9_1, c11_2, c1_1, c_1, c2_1, c3_1 ---------------------------------------- (59) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSNEG(s(z0), cons(z1, z2)) -> c5(2NDSNEG(s(z0), cons2(z1, z2))) by 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) ---------------------------------------- (60) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: 2NDSNEG_2, PLUS_2, TIMES_2, PI_1, FROM_1, 2NDSPOS_2 Compound Symbols: c6_1, c9_1, c11_2, c1_1, c_1, c2_1, c3_1, c5_1 ---------------------------------------- (61) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace PI(x0) -> c1(2NDSPOS(x0, cons(0, cons(s(0), from(s(s(0))))))) by PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), from(s(s(s(0))))))))) ---------------------------------------- (62) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), from(s(s(s(0))))))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: 2NDSNEG_2, PLUS_2, TIMES_2, FROM_1, 2NDSPOS_2, PI_1 Compound Symbols: c6_1, c9_1, c11_2, c_1, c2_1, c3_1, c5_1, c1_1 ---------------------------------------- (63) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c6(2NDSPOS(z0, z3)) by 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) ---------------------------------------- (64) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), from(s(s(s(0))))))))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: PLUS_2, TIMES_2, FROM_1, 2NDSPOS_2, 2NDSNEG_2, PI_1 Compound Symbols: c9_1, c11_2, c_1, c2_1, c3_1, c5_1, c1_1, c6_1 ---------------------------------------- (65) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace PLUS(s(z0), z1) -> c9(PLUS(z0, z1)) by PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) ---------------------------------------- (66) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), from(s(s(s(0))))))))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSPOS_2, 2NDSNEG_2, PI_1, PLUS_2 Compound Symbols: c11_2, c_1, c2_1, c3_1, c5_1, c1_1, c6_1, c9_1 ---------------------------------------- (67) CdtRewritingProof (BOTH BOUNDS(ID, ID)) Used rewriting to replace PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), from(s(s(s(0))))))))) by PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) ---------------------------------------- (68) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, PI_1 Compound Symbols: c11_2, c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c1_1 ---------------------------------------- (69) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSPOS(s(z0), cons(z1, cons(y2, y3))) -> c2(2NDSPOS(s(z0), cons2(z1, cons(y2, y3)))) by 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) ---------------------------------------- (70) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, PI_1 Compound Symbols: c11_2, c_1, c3_1, c5_1, c6_1, c9_1, c1_1, c2_1 ---------------------------------------- (71) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y1, y2)))) -> c3(2NDSNEG(s(y0), cons(y1, y2))) by 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) ---------------------------------------- (72) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, PI_1 Compound Symbols: c11_2, c_1, c3_1, c5_1, c6_1, c9_1, c1_1, c2_1 ---------------------------------------- (73) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y1, cons(y2, y3))))) -> c3(2NDSNEG(s(y0), cons2(y1, cons(y2, y3)))) by 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) ---------------------------------------- (74) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSNEG_2, PLUS_2, PI_1, 2NDSPOS_2 Compound Symbols: c11_2, c_1, c5_1, c6_1, c9_1, c1_1, c2_1, c3_1 ---------------------------------------- (75) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSNEG(s(z0), cons(z1, cons(y2, y3))) -> c5(2NDSNEG(s(z0), cons2(z1, cons(y2, y3)))) by 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) ---------------------------------------- (76) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSNEG_2, PLUS_2, PI_1, 2NDSPOS_2 Compound Symbols: c11_2, c_1, c6_1, c9_1, c1_1, c2_1, c3_1, c5_1 ---------------------------------------- (77) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y1, cons(y2, y3))))) -> c6(2NDSPOS(s(y0), cons(y1, cons(y2, y3)))) by 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) ---------------------------------------- (78) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSNEG_2, PLUS_2, PI_1, 2NDSPOS_2 Compound Symbols: c11_2, c_1, c6_1, c9_1, c1_1, c2_1, c3_1, c5_1 ---------------------------------------- (79) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons(y3, y4))))) by 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) ---------------------------------------- (80) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSNEG_2, PLUS_2, PI_1, 2NDSPOS_2 Compound Symbols: c11_2, c_1, c6_1, c9_1, c1_1, c2_1, c3_1, c5_1 ---------------------------------------- (81) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y1, cons(y2, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons2(y1, cons(y2, cons2(y3, cons(y4, y5)))))) by 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) ---------------------------------------- (82) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, PLUS_2, PI_1, 2NDSPOS_2, 2NDSNEG_2 Compound Symbols: c11_2, c_1, c9_1, c1_1, c2_1, c3_1, c5_1, c6_1 ---------------------------------------- (83) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace PLUS(s(s(y0)), z1) -> c9(PLUS(s(y0), z1)) by PLUS(s(s(s(y0))), z1) -> c9(PLUS(s(s(y0)), z1)) ---------------------------------------- (84) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) PLUS(s(s(s(y0))), z1) -> c9(PLUS(s(s(y0)), z1)) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) PLUS(s(s(s(y0))), z1) -> c9(PLUS(s(s(y0)), z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, PI_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2 Compound Symbols: c11_2, c_1, c1_1, c2_1, c3_1, c5_1, c6_1, c9_1 ---------------------------------------- (85) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace PI(z0) -> c1(2NDSPOS(z0, cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) by PI(s(s(y0))) -> c1(2NDSPOS(s(s(y0)), cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) ---------------------------------------- (86) Obligation: Complexity Dependency Tuples Problem Rules: times(0, z0) -> 0 times(s(z0), z1) -> plus(z1, times(z0, z1)) plus(0, z0) -> z0 plus(s(z0), z1) -> s(plus(z0, z1)) from(z0) -> cons(z0, from(s(z0))) Tuples: TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) PLUS(s(s(s(y0))), z1) -> c9(PLUS(s(s(y0)), z1)) PI(s(s(y0))) -> c1(2NDSPOS(s(s(y0)), cons(0, cons(s(0), cons(s(s(0)), cons(s(s(s(0))), from(s(s(s(s(0))))))))))) S tuples: FROM(s(s(x0))) -> c(FROM(s(s(s(x0))))) K tuples: PI(z0) -> c1(2NDSPOS(z0, from(0))) TIMES(s(z0), z1) -> c11(PLUS(z1, times(z0, z1)), TIMES(z0, z1)) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons(y3, y4)))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons(y3, y4))))) 2NDSPOS(s(s(y0)), cons(z1, cons(z2, cons2(y3, cons(y4, y5))))) -> c2(2NDSPOS(s(s(y0)), cons2(z1, cons(z2, cons2(y3, cons(y4, y5)))))) 2NDSPOS(s(s(z0)), cons2(z1, cons(z2, cons(z3, cons(y2, y3))))) -> c3(2NDSNEG(s(z0), cons(z3, cons(y2, y3)))) 2NDSPOS(s(s(s(y0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(y3, cons(y4, y5))))))) -> c3(2NDSNEG(s(s(y0)), cons2(z3, cons(z4, cons(y3, cons(y4, y5)))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6)))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSPOS(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))))) -> c3(2NDSNEG(s(s(s(y0))), cons2(z3, cons(z4, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(y0)), cons(z1, cons(z2, cons(y3, cons(y4, y5))))) -> c5(2NDSNEG(s(s(y0)), cons2(z1, cons(z2, cons(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6)))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons(y5, y6))))))) 2NDSNEG(s(s(s(y0))), cons(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7))))))) -> c5(2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons2(y3, cons(y4, cons2(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons(y3, y4)))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons(y3, y4))))) 2NDSNEG(s(s(s(y0))), cons2(z1, cons(z2, cons(z3, cons(z4, cons2(y3, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(y0)), cons(z3, cons(z4, cons2(y3, cons(y4, y5)))))) 2NDSNEG(s(s(s(z0))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons(z5, cons(y4, y5))))))) -> c6(2NDSPOS(s(s(z0)), cons2(z3, cons(z4, cons(z5, cons(y4, y5)))))) 2NDSNEG(s(s(s(s(y0)))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7))))))))) -> c6(2NDSPOS(s(s(s(y0))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons(y5, cons(y6, y7)))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8)))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons(y7, y8))))))))) 2NDSNEG(s(s(s(s(s(y0))))), cons2(z1, cons(z2, cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9))))))))))) -> c6(2NDSPOS(s(s(s(s(y0)))), cons2(z3, cons(z4, cons2(z5, cons(z6, cons2(y5, cons(y6, cons2(y7, cons(y8, y9)))))))))) PLUS(s(s(s(y0))), z1) -> c9(PLUS(s(s(y0)), z1)) Defined Rule Symbols: times_2, plus_2, from_1 Defined Pair Symbols: TIMES_2, FROM_1, 2NDSPOS_2, 2NDSNEG_2, PLUS_2, PI_1 Compound Symbols: c11_2, c_1, c2_1, c3_1, c5_1, c6_1, c9_1, c1_1