WORST_CASE(?,O(n^2))
proof of input_CLS7Y4RJiS.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

(0) CpxTRS
(1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(2) CdtProblem
(3) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(4) CdtProblem
(5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
(7) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) CdtProblem
(11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 137 ms]
(12) CdtProblem
(13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 37 ms]
(14) CdtProblem
(15) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CdtProblem
(17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 127 ms]
(18) CdtProblem
(19) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) BOUNDS(1, 1)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).


The TRS R consists of the following rules:

   from(X) -> cons(X, n__from(s(X)))
   2ndspos(0, Z) -> rnil
   2ndspos(s(N), cons(X, Z)) -> 2ndspos(s(N), cons2(X, activate(Z)))
   2ndspos(s(N), cons2(X, cons(Y, Z))) -> rcons(posrecip(Y), 2ndsneg(N, activate(Z)))
   2ndsneg(0, Z) -> rnil
   2ndsneg(s(N), cons(X, Z)) -> 2ndsneg(s(N), cons2(X, activate(Z)))
   2ndsneg(s(N), cons2(X, cons(Y, Z))) -> rcons(negrecip(Y), 2ndspos(N, activate(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)
   from(X) -> n__from(X)
   activate(n__from(X)) -> from(X)
   activate(X) -> X

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(2)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   2ndspos(0, z0) -> rnil
   2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, activate(z2)))
   2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, activate(z3)))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, activate(z2)))
   2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, activate(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)
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
Tuples:
   FROM(z0) -> c
   FROM(z0) -> c1
   2NDSPOS(0, z0) -> c2
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)), ACTIVATE(z3))
   2NDSNEG(0, z0) -> c5
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)), ACTIVATE(z3))
   PI(z0) -> c8(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(0, z0) -> c9
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(0, z0) -> c11
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   SQUARE(z0) -> c13(TIMES(z0, z0))
   ACTIVATE(n__from(z0)) -> c14(FROM(z0))
   ACTIVATE(z0) -> c15
S tuples:
   FROM(z0) -> c
   FROM(z0) -> c1
   2NDSPOS(0, z0) -> c2
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)), ACTIVATE(z3))
   2NDSNEG(0, z0) -> c5
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)), ACTIVATE(z3))
   PI(z0) -> c8(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(0, z0) -> c9
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(0, z0) -> c11
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   SQUARE(z0) -> c13(TIMES(z0, z0))
   ACTIVATE(n__from(z0)) -> c14(FROM(z0))
   ACTIVATE(z0) -> c15
K tuples:none
Defined Rule Symbols:   from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1, activate_1

Defined Pair Symbols:   FROM_1, 2NDSPOS_2, 2NDSNEG_2, PI_1, PLUS_2, TIMES_2, SQUARE_1, ACTIVATE_1

Compound Symbols:   c, c1, c2, c3_2, c4_2, c5, c6_2, c7_2, c8_2, c9, c10_1, c11, c12_2, c13_1, c14_1, c15


----------------------------------------

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   SQUARE(z0) -> c13(TIMES(z0, z0))
Removed 8 trailing nodes:
   FROM(z0) -> c1
   TIMES(0, z0) -> c11
   FROM(z0) -> c
   ACTIVATE(z0) -> c15
   PLUS(0, z0) -> c9
   2NDSNEG(0, z0) -> c5
   ACTIVATE(n__from(z0)) -> c14(FROM(z0))
   2NDSPOS(0, z0) -> c2

----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   2ndspos(0, z0) -> rnil
   2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, activate(z2)))
   2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, activate(z3)))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, activate(z2)))
   2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, activate(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)
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
Tuples:
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)), ACTIVATE(z3))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)), ACTIVATE(z3))
   PI(z0) -> c8(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
S tuples:
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)), ACTIVATE(z3))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))), ACTIVATE(z2))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)), ACTIVATE(z3))
   PI(z0) -> c8(2NDSPOS(z0, from(0)), FROM(0))
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(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, activate_1

Defined Pair Symbols:   2NDSPOS_2, 2NDSNEG_2, PI_1, PLUS_2, TIMES_2

Compound Symbols:   c3_2, c4_2, c6_2, c7_2, c8_2, c10_1, c12_2


----------------------------------------

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 5 trailing tuple parts
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   2ndspos(0, z0) -> rnil
   2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, activate(z2)))
   2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, activate(z3)))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, activate(z2)))
   2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, activate(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)
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
K tuples:none
Defined Rule Symbols:   from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1, activate_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))

----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
   2ndspos(0, z0) -> rnil
   2ndspos(s(z0), cons(z1, z2)) -> 2ndspos(s(z0), cons2(z1, activate(z2)))
   2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, activate(z3)))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, activate(z2)))
   2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, activate(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)
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
K tuples:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
Defined Rule Symbols:   from_1, 2ndspos_2, 2ndsneg_2, pi_1, plus_2, times_2, square_1, activate_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(9) 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, activate(z2)))
   2ndspos(s(z0), cons2(z1, cons(z2, z3))) -> rcons(posrecip(z2), 2ndsneg(z0, activate(z3)))
   2ndsneg(0, z0) -> rnil
   2ndsneg(s(z0), cons(z1, z2)) -> 2ndsneg(s(z0), cons2(z1, activate(z2)))
   2ndsneg(s(z0), cons2(z1, cons(z2, z3))) -> rcons(negrecip(z2), 2ndspos(z0, activate(z3)))
   pi(z0) -> 2ndspos(z0, from(0))
   square(z0) -> times(z0, z0)

----------------------------------------

(10)
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))
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
K tuples:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
Defined Rule Symbols:   times_2, plus_2, activate_1, from_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(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)) = 0
   POL(2NDSPOS(x_1, x_2)) = 0
   POL(PI(x_1)) = 0
   POL(PLUS(x_1, x_2)) = 0
   POL(TIMES(x_1, x_2)) = x_1
   POL(activate(x_1)) = x_1
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(cons(x_1, x_2)) = [1] + x_1
   POL(cons2(x_1, x_2)) = [1] + x_1
   POL(from(x_1)) = [1] + x_1
   POL(n__from(x_1)) = [1] + x_1
   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

----------------------------------------

(12)
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))
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
K tuples:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
Defined Rule Symbols:   times_2, plus_2, activate_1, from_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(13) 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))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
We considered the (Usable) Rules:none
And the Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(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)) = x_1
   POL(2NDSPOS(x_1, x_2)) = x_1
   POL(PI(x_1)) = x_1
   POL(PLUS(x_1, x_2)) = 0
   POL(TIMES(x_1, x_2)) = [2]x_1
   POL(activate(x_1)) = 0
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(cons(x_1, x_2)) = x_1
   POL(cons2(x_1, x_2)) = x_1
   POL(from(x_1)) = 0
   POL(n__from(x_1)) = [3] + x_1
   POL(plus(x_1, x_2)) = [3] + [3]x_1
   POL(s(x_1)) = [1] + x_1
   POL(times(x_1, x_2)) = [3] + [3]x_1 + [3]x_2

----------------------------------------

(14)
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))
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
K tuples:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
Defined Rule Symbols:   times_2, plus_2, activate_1, from_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID))
The following tuples could be moved from S to K by knowledge propagation:
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))

----------------------------------------

(16)
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))
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
K tuples:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
Defined Rule Symbols:   times_2, plus_2, activate_1, from_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(17) 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) -> c10(PLUS(z0, z1))
We considered the (Usable) Rules:none
And the Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(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(PI(x_1)) = [2] + [2]x_1^2
   POL(PLUS(x_1, x_2)) = x_1
   POL(TIMES(x_1, x_2)) = x_1*x_2
   POL(activate(x_1)) = 0
   POL(c10(x_1)) = x_1
   POL(c12(x_1, x_2)) = x_1 + x_2
   POL(c3(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c6(x_1)) = x_1
   POL(c7(x_1)) = x_1
   POL(c8(x_1)) = x_1
   POL(cons(x_1, x_2)) = 0
   POL(cons2(x_1, x_2)) = 0
   POL(from(x_1)) = 0
   POL(n__from(x_1)) = 0
   POL(plus(x_1, x_2)) = [1] + x_1^2
   POL(s(x_1)) = [1] + x_1
   POL(times(x_1, x_2)) = [2]x_2^2

----------------------------------------

(18)
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))
   activate(n__from(z0)) -> from(z0)
   activate(z0) -> z0
   from(z0) -> cons(z0, n__from(s(z0)))
   from(z0) -> n__from(z0)
Tuples:
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
S tuples:none
K tuples:
   PI(z0) -> c8(2NDSPOS(z0, from(0)))
   TIMES(s(z0), z1) -> c12(PLUS(z1, times(z0, z1)), TIMES(z0, z1))
   2NDSPOS(s(z0), cons2(z1, cons(z2, z3))) -> c4(2NDSNEG(z0, activate(z3)))
   2NDSNEG(s(z0), cons2(z1, cons(z2, z3))) -> c7(2NDSPOS(z0, activate(z3)))
   2NDSPOS(s(z0), cons(z1, z2)) -> c3(2NDSPOS(s(z0), cons2(z1, activate(z2))))
   2NDSNEG(s(z0), cons(z1, z2)) -> c6(2NDSNEG(s(z0), cons2(z1, activate(z2))))
   PLUS(s(z0), z1) -> c10(PLUS(z0, z1))
Defined Rule Symbols:   times_2, plus_2, activate_1, from_1

Defined Pair Symbols:   PLUS_2, TIMES_2, 2NDSPOS_2, 2NDSNEG_2, PI_1

Compound Symbols:   c10_1, c12_2, c3_1, c4_1, c6_1, c7_1, c8_1


----------------------------------------

(19) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(20)
BOUNDS(1, 1)