(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(from(z0)) → mark(cons(z0, from(s(z0))))
active(2ndspos(0, z0)) → mark(rnil)
active(2ndspos(s(z0), cons(z1, z2))) → mark(2ndspos(s(z0), cons2(z1, z2)))
active(2ndspos(s(z0), cons2(z1, cons(z2, z3)))) → mark(rcons(posrecip(z2), 2ndsneg(z0, z3)))
active(2ndsneg(0, z0)) → mark(rnil)
active(2ndsneg(s(z0), cons(z1, z2))) → mark(2ndsneg(s(z0), cons2(z1, z2)))
active(2ndsneg(s(z0), cons2(z1, cons(z2, z3)))) → mark(rcons(negrecip(z2), 2ndspos(z0, z3)))
active(pi(z0)) → mark(2ndspos(z0, from(0)))
active(plus(0, z0)) → mark(z0)
active(plus(s(z0), z1)) → mark(s(plus(z0, z1)))
active(times(0, z0)) → mark(0)
active(times(s(z0), z1)) → mark(plus(z1, times(z0, z1)))
active(square(z0)) → mark(times(z0, z0))
mark(from(z0)) → active(from(mark(z0)))
mark(cons(z0, z1)) → active(cons(mark(z0), z1))
mark(s(z0)) → active(s(mark(z0)))
mark(2ndspos(z0, z1)) → active(2ndspos(mark(z0), mark(z1)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(z0, z1)) → active(cons2(z0, mark(z1)))
mark(rcons(z0, z1)) → active(rcons(mark(z0), mark(z1)))
mark(posrecip(z0)) → active(posrecip(mark(z0)))
mark(2ndsneg(z0, z1)) → active(2ndsneg(mark(z0), mark(z1)))
mark(negrecip(z0)) → active(negrecip(mark(z0)))
mark(pi(z0)) → active(pi(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(times(z0, z1)) → active(times(mark(z0), mark(z1)))
mark(square(z0)) → active(square(mark(z0)))
from(mark(z0)) → from(z0)
from(active(z0)) → from(z0)
cons(mark(z0), z1) → cons(z0, z1)
cons(z0, mark(z1)) → cons(z0, z1)
cons(active(z0), z1) → cons(z0, z1)
cons(z0, active(z1)) → cons(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
2ndspos(mark(z0), z1) → 2ndspos(z0, z1)
2ndspos(z0, mark(z1)) → 2ndspos(z0, z1)
2ndspos(active(z0), z1) → 2ndspos(z0, z1)
2ndspos(z0, active(z1)) → 2ndspos(z0, z1)
cons2(mark(z0), z1) → cons2(z0, z1)
cons2(z0, mark(z1)) → cons2(z0, z1)
cons2(active(z0), z1) → cons2(z0, z1)
cons2(z0, active(z1)) → cons2(z0, z1)
rcons(mark(z0), z1) → rcons(z0, z1)
rcons(z0, mark(z1)) → rcons(z0, z1)
rcons(active(z0), z1) → rcons(z0, z1)
rcons(z0, active(z1)) → rcons(z0, z1)
posrecip(mark(z0)) → posrecip(z0)
posrecip(active(z0)) → posrecip(z0)
2ndsneg(mark(z0), z1) → 2ndsneg(z0, z1)
2ndsneg(z0, mark(z1)) → 2ndsneg(z0, z1)
2ndsneg(active(z0), z1) → 2ndsneg(z0, z1)
2ndsneg(z0, active(z1)) → 2ndsneg(z0, z1)
negrecip(mark(z0)) → negrecip(z0)
negrecip(active(z0)) → negrecip(z0)
pi(mark(z0)) → pi(z0)
pi(active(z0)) → pi(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
times(mark(z0), z1) → times(z0, z1)
times(z0, mark(z1)) → times(z0, z1)
times(active(z0), z1) → times(z0, z1)
times(z0, active(z1)) → times(z0, z1)
square(mark(z0)) → square(z0)
square(active(z0)) → square(z0)
Tuples:
ACTIVE(from(z0)) → c(MARK(cons(z0, from(s(z0)))), CONS(z0, from(s(z0))), FROM(s(z0)), S(z0))
ACTIVE(2ndspos(0, z0)) → c1(MARK(rnil))
ACTIVE(2ndspos(s(z0), cons(z1, z2))) → c2(MARK(2ndspos(s(z0), cons2(z1, z2))), 2NDSPOS(s(z0), cons2(z1, z2)), S(z0), CONS2(z1, z2))
ACTIVE(2ndspos(s(z0), cons2(z1, cons(z2, z3)))) → c3(MARK(rcons(posrecip(z2), 2ndsneg(z0, z3))), RCONS(posrecip(z2), 2ndsneg(z0, z3)), POSRECIP(z2), 2NDSNEG(z0, z3))
ACTIVE(2ndsneg(0, z0)) → c4(MARK(rnil))
ACTIVE(2ndsneg(s(z0), cons(z1, z2))) → c5(MARK(2ndsneg(s(z0), cons2(z1, z2))), 2NDSNEG(s(z0), cons2(z1, z2)), S(z0), CONS2(z1, z2))
ACTIVE(2ndsneg(s(z0), cons2(z1, cons(z2, z3)))) → c6(MARK(rcons(negrecip(z2), 2ndspos(z0, z3))), RCONS(negrecip(z2), 2ndspos(z0, z3)), NEGRECIP(z2), 2NDSPOS(z0, z3))
ACTIVE(pi(z0)) → c7(MARK(2ndspos(z0, from(0))), 2NDSPOS(z0, from(0)), FROM(0))
ACTIVE(plus(0, z0)) → c8(MARK(z0))
ACTIVE(plus(s(z0), z1)) → c9(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
ACTIVE(times(0, z0)) → c10(MARK(0))
ACTIVE(times(s(z0), z1)) → c11(MARK(plus(z1, times(z0, z1))), PLUS(z1, times(z0, z1)), TIMES(z0, z1))
ACTIVE(square(z0)) → c12(MARK(times(z0, z0)), TIMES(z0, z0))
MARK(from(z0)) → c13(ACTIVE(from(mark(z0))), FROM(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c14(ACTIVE(cons(mark(z0), z1)), CONS(mark(z0), z1), MARK(z0))
MARK(s(z0)) → c15(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(2ndspos(z0, z1)) → c16(ACTIVE(2ndspos(mark(z0), mark(z1))), 2NDSPOS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c17(ACTIVE(0))
MARK(rnil) → c18(ACTIVE(rnil))
MARK(cons2(z0, z1)) → c19(ACTIVE(cons2(z0, mark(z1))), CONS2(z0, mark(z1)), MARK(z1))
MARK(rcons(z0, z1)) → c20(ACTIVE(rcons(mark(z0), mark(z1))), RCONS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(posrecip(z0)) → c21(ACTIVE(posrecip(mark(z0))), POSRECIP(mark(z0)), MARK(z0))
MARK(2ndsneg(z0, z1)) → c22(ACTIVE(2ndsneg(mark(z0), mark(z1))), 2NDSNEG(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(negrecip(z0)) → c23(ACTIVE(negrecip(mark(z0))), NEGRECIP(mark(z0)), MARK(z0))
MARK(pi(z0)) → c24(ACTIVE(pi(mark(z0))), PI(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c25(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(times(z0, z1)) → c26(ACTIVE(times(mark(z0), mark(z1))), TIMES(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(square(z0)) → c27(ACTIVE(square(mark(z0))), SQUARE(mark(z0)), MARK(z0))
FROM(mark(z0)) → c28(FROM(z0))
FROM(active(z0)) → c29(FROM(z0))
CONS(mark(z0), z1) → c30(CONS(z0, z1))
CONS(z0, mark(z1)) → c31(CONS(z0, z1))
CONS(active(z0), z1) → c32(CONS(z0, z1))
CONS(z0, active(z1)) → c33(CONS(z0, z1))
S(mark(z0)) → c34(S(z0))
S(active(z0)) → c35(S(z0))
2NDSPOS(mark(z0), z1) → c36(2NDSPOS(z0, z1))
2NDSPOS(z0, mark(z1)) → c37(2NDSPOS(z0, z1))
2NDSPOS(active(z0), z1) → c38(2NDSPOS(z0, z1))
2NDSPOS(z0, active(z1)) → c39(2NDSPOS(z0, z1))
CONS2(mark(z0), z1) → c40(CONS2(z0, z1))
CONS2(z0, mark(z1)) → c41(CONS2(z0, z1))
CONS2(active(z0), z1) → c42(CONS2(z0, z1))
CONS2(z0, active(z1)) → c43(CONS2(z0, z1))
RCONS(mark(z0), z1) → c44(RCONS(z0, z1))
RCONS(z0, mark(z1)) → c45(RCONS(z0, z1))
RCONS(active(z0), z1) → c46(RCONS(z0, z1))
RCONS(z0, active(z1)) → c47(RCONS(z0, z1))
POSRECIP(mark(z0)) → c48(POSRECIP(z0))
POSRECIP(active(z0)) → c49(POSRECIP(z0))
2NDSNEG(mark(z0), z1) → c50(2NDSNEG(z0, z1))
2NDSNEG(z0, mark(z1)) → c51(2NDSNEG(z0, z1))
2NDSNEG(active(z0), z1) → c52(2NDSNEG(z0, z1))
2NDSNEG(z0, active(z1)) → c53(2NDSNEG(z0, z1))
NEGRECIP(mark(z0)) → c54(NEGRECIP(z0))
NEGRECIP(active(z0)) → c55(NEGRECIP(z0))
PI(mark(z0)) → c56(PI(z0))
PI(active(z0)) → c57(PI(z0))
PLUS(mark(z0), z1) → c58(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c59(PLUS(z0, z1))
PLUS(active(z0), z1) → c60(PLUS(z0, z1))
PLUS(z0, active(z1)) → c61(PLUS(z0, z1))
TIMES(mark(z0), z1) → c62(TIMES(z0, z1))
TIMES(z0, mark(z1)) → c63(TIMES(z0, z1))
TIMES(active(z0), z1) → c64(TIMES(z0, z1))
TIMES(z0, active(z1)) → c65(TIMES(z0, z1))
SQUARE(mark(z0)) → c66(SQUARE(z0))
SQUARE(active(z0)) → c67(SQUARE(z0))
S tuples:
ACTIVE(from(z0)) → c(MARK(cons(z0, from(s(z0)))), CONS(z0, from(s(z0))), FROM(s(z0)), S(z0))
ACTIVE(2ndspos(0, z0)) → c1(MARK(rnil))
ACTIVE(2ndspos(s(z0), cons(z1, z2))) → c2(MARK(2ndspos(s(z0), cons2(z1, z2))), 2NDSPOS(s(z0), cons2(z1, z2)), S(z0), CONS2(z1, z2))
ACTIVE(2ndspos(s(z0), cons2(z1, cons(z2, z3)))) → c3(MARK(rcons(posrecip(z2), 2ndsneg(z0, z3))), RCONS(posrecip(z2), 2ndsneg(z0, z3)), POSRECIP(z2), 2NDSNEG(z0, z3))
ACTIVE(2ndsneg(0, z0)) → c4(MARK(rnil))
ACTIVE(2ndsneg(s(z0), cons(z1, z2))) → c5(MARK(2ndsneg(s(z0), cons2(z1, z2))), 2NDSNEG(s(z0), cons2(z1, z2)), S(z0), CONS2(z1, z2))
ACTIVE(2ndsneg(s(z0), cons2(z1, cons(z2, z3)))) → c6(MARK(rcons(negrecip(z2), 2ndspos(z0, z3))), RCONS(negrecip(z2), 2ndspos(z0, z3)), NEGRECIP(z2), 2NDSPOS(z0, z3))
ACTIVE(pi(z0)) → c7(MARK(2ndspos(z0, from(0))), 2NDSPOS(z0, from(0)), FROM(0))
ACTIVE(plus(0, z0)) → c8(MARK(z0))
ACTIVE(plus(s(z0), z1)) → c9(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
ACTIVE(times(0, z0)) → c10(MARK(0))
ACTIVE(times(s(z0), z1)) → c11(MARK(plus(z1, times(z0, z1))), PLUS(z1, times(z0, z1)), TIMES(z0, z1))
ACTIVE(square(z0)) → c12(MARK(times(z0, z0)), TIMES(z0, z0))
MARK(from(z0)) → c13(ACTIVE(from(mark(z0))), FROM(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c14(ACTIVE(cons(mark(z0), z1)), CONS(mark(z0), z1), MARK(z0))
MARK(s(z0)) → c15(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(2ndspos(z0, z1)) → c16(ACTIVE(2ndspos(mark(z0), mark(z1))), 2NDSPOS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c17(ACTIVE(0))
MARK(rnil) → c18(ACTIVE(rnil))
MARK(cons2(z0, z1)) → c19(ACTIVE(cons2(z0, mark(z1))), CONS2(z0, mark(z1)), MARK(z1))
MARK(rcons(z0, z1)) → c20(ACTIVE(rcons(mark(z0), mark(z1))), RCONS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(posrecip(z0)) → c21(ACTIVE(posrecip(mark(z0))), POSRECIP(mark(z0)), MARK(z0))
MARK(2ndsneg(z0, z1)) → c22(ACTIVE(2ndsneg(mark(z0), mark(z1))), 2NDSNEG(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(negrecip(z0)) → c23(ACTIVE(negrecip(mark(z0))), NEGRECIP(mark(z0)), MARK(z0))
MARK(pi(z0)) → c24(ACTIVE(pi(mark(z0))), PI(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c25(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(times(z0, z1)) → c26(ACTIVE(times(mark(z0), mark(z1))), TIMES(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(square(z0)) → c27(ACTIVE(square(mark(z0))), SQUARE(mark(z0)), MARK(z0))
FROM(mark(z0)) → c28(FROM(z0))
FROM(active(z0)) → c29(FROM(z0))
CONS(mark(z0), z1) → c30(CONS(z0, z1))
CONS(z0, mark(z1)) → c31(CONS(z0, z1))
CONS(active(z0), z1) → c32(CONS(z0, z1))
CONS(z0, active(z1)) → c33(CONS(z0, z1))
S(mark(z0)) → c34(S(z0))
S(active(z0)) → c35(S(z0))
2NDSPOS(mark(z0), z1) → c36(2NDSPOS(z0, z1))
2NDSPOS(z0, mark(z1)) → c37(2NDSPOS(z0, z1))
2NDSPOS(active(z0), z1) → c38(2NDSPOS(z0, z1))
2NDSPOS(z0, active(z1)) → c39(2NDSPOS(z0, z1))
CONS2(mark(z0), z1) → c40(CONS2(z0, z1))
CONS2(z0, mark(z1)) → c41(CONS2(z0, z1))
CONS2(active(z0), z1) → c42(CONS2(z0, z1))
CONS2(z0, active(z1)) → c43(CONS2(z0, z1))
RCONS(mark(z0), z1) → c44(RCONS(z0, z1))
RCONS(z0, mark(z1)) → c45(RCONS(z0, z1))
RCONS(active(z0), z1) → c46(RCONS(z0, z1))
RCONS(z0, active(z1)) → c47(RCONS(z0, z1))
POSRECIP(mark(z0)) → c48(POSRECIP(z0))
POSRECIP(active(z0)) → c49(POSRECIP(z0))
2NDSNEG(mark(z0), z1) → c50(2NDSNEG(z0, z1))
2NDSNEG(z0, mark(z1)) → c51(2NDSNEG(z0, z1))
2NDSNEG(active(z0), z1) → c52(2NDSNEG(z0, z1))
2NDSNEG(z0, active(z1)) → c53(2NDSNEG(z0, z1))
NEGRECIP(mark(z0)) → c54(NEGRECIP(z0))
NEGRECIP(active(z0)) → c55(NEGRECIP(z0))
PI(mark(z0)) → c56(PI(z0))
PI(active(z0)) → c57(PI(z0))
PLUS(mark(z0), z1) → c58(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c59(PLUS(z0, z1))
PLUS(active(z0), z1) → c60(PLUS(z0, z1))
PLUS(z0, active(z1)) → c61(PLUS(z0, z1))
TIMES(mark(z0), z1) → c62(TIMES(z0, z1))
TIMES(z0, mark(z1)) → c63(TIMES(z0, z1))
TIMES(active(z0), z1) → c64(TIMES(z0, z1))
TIMES(z0, active(z1)) → c65(TIMES(z0, z1))
SQUARE(mark(z0)) → c66(SQUARE(z0))
SQUARE(active(z0)) → c67(SQUARE(z0))
K tuples:none
Defined Rule Symbols:
active, mark, from, cons, s, 2ndspos, cons2, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square
Defined Pair Symbols:
ACTIVE, MARK, FROM, CONS, S, 2NDSPOS, CONS2, RCONS, POSRECIP, 2NDSNEG, NEGRECIP, PI, PLUS, TIMES, SQUARE
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
ACTIVE(from(z0)) → c(MARK(cons(z0, from(s(z0)))), CONS(z0, from(s(z0))), FROM(s(z0)), S(z0))
ACTIVE(2ndspos(0, z0)) → c1(MARK(rnil))
ACTIVE(2ndspos(s(z0), cons(z1, z2))) → c2(MARK(2ndspos(s(z0), cons2(z1, z2))), 2NDSPOS(s(z0), cons2(z1, z2)), S(z0), CONS2(z1, z2))
ACTIVE(2ndspos(s(z0), cons2(z1, cons(z2, z3)))) → c3(MARK(rcons(posrecip(z2), 2ndsneg(z0, z3))), RCONS(posrecip(z2), 2ndsneg(z0, z3)), POSRECIP(z2), 2NDSNEG(z0, z3))
ACTIVE(2ndsneg(0, z0)) → c4(MARK(rnil))
ACTIVE(2ndsneg(s(z0), cons(z1, z2))) → c5(MARK(2ndsneg(s(z0), cons2(z1, z2))), 2NDSNEG(s(z0), cons2(z1, z2)), S(z0), CONS2(z1, z2))
ACTIVE(2ndsneg(s(z0), cons2(z1, cons(z2, z3)))) → c6(MARK(rcons(negrecip(z2), 2ndspos(z0, z3))), RCONS(negrecip(z2), 2ndspos(z0, z3)), NEGRECIP(z2), 2NDSPOS(z0, z3))
ACTIVE(pi(z0)) → c7(MARK(2ndspos(z0, from(0))), 2NDSPOS(z0, from(0)), FROM(0))
ACTIVE(plus(0, z0)) → c8(MARK(z0))
ACTIVE(plus(s(z0), z1)) → c9(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
ACTIVE(times(0, z0)) → c10(MARK(0))
ACTIVE(times(s(z0), z1)) → c11(MARK(plus(z1, times(z0, z1))), PLUS(z1, times(z0, z1)), TIMES(z0, z1))
ACTIVE(square(z0)) → c12(MARK(times(z0, z0)), TIMES(z0, z0))
MARK(from(z0)) → c13(ACTIVE(from(mark(z0))), FROM(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c14(ACTIVE(cons(mark(z0), z1)), CONS(mark(z0), z1), MARK(z0))
MARK(s(z0)) → c15(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(2ndspos(z0, z1)) → c16(ACTIVE(2ndspos(mark(z0), mark(z1))), 2NDSPOS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(cons2(z0, z1)) → c19(ACTIVE(cons2(z0, mark(z1))), CONS2(z0, mark(z1)), MARK(z1))
MARK(rcons(z0, z1)) → c20(ACTIVE(rcons(mark(z0), mark(z1))), RCONS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(posrecip(z0)) → c21(ACTIVE(posrecip(mark(z0))), POSRECIP(mark(z0)), MARK(z0))
MARK(2ndsneg(z0, z1)) → c22(ACTIVE(2ndsneg(mark(z0), mark(z1))), 2NDSNEG(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(negrecip(z0)) → c23(ACTIVE(negrecip(mark(z0))), NEGRECIP(mark(z0)), MARK(z0))
MARK(pi(z0)) → c24(ACTIVE(pi(mark(z0))), PI(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c25(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(times(z0, z1)) → c26(ACTIVE(times(mark(z0), mark(z1))), TIMES(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(square(z0)) → c27(ACTIVE(square(mark(z0))), SQUARE(mark(z0)), MARK(z0))
FROM(mark(z0)) → c28(FROM(z0))
FROM(active(z0)) → c29(FROM(z0))
CONS(mark(z0), z1) → c30(CONS(z0, z1))
CONS(z0, mark(z1)) → c31(CONS(z0, z1))
CONS(active(z0), z1) → c32(CONS(z0, z1))
CONS(z0, active(z1)) → c33(CONS(z0, z1))
S(mark(z0)) → c34(S(z0))
S(active(z0)) → c35(S(z0))
2NDSPOS(mark(z0), z1) → c36(2NDSPOS(z0, z1))
2NDSPOS(z0, mark(z1)) → c37(2NDSPOS(z0, z1))
2NDSPOS(active(z0), z1) → c38(2NDSPOS(z0, z1))
2NDSPOS(z0, active(z1)) → c39(2NDSPOS(z0, z1))
CONS2(mark(z0), z1) → c40(CONS2(z0, z1))
CONS2(z0, mark(z1)) → c41(CONS2(z0, z1))
CONS2(active(z0), z1) → c42(CONS2(z0, z1))
CONS2(z0, active(z1)) → c43(CONS2(z0, z1))
RCONS(mark(z0), z1) → c44(RCONS(z0, z1))
RCONS(z0, mark(z1)) → c45(RCONS(z0, z1))
RCONS(active(z0), z1) → c46(RCONS(z0, z1))
RCONS(z0, active(z1)) → c47(RCONS(z0, z1))
POSRECIP(mark(z0)) → c48(POSRECIP(z0))
POSRECIP(active(z0)) → c49(POSRECIP(z0))
2NDSNEG(mark(z0), z1) → c50(2NDSNEG(z0, z1))
2NDSNEG(z0, mark(z1)) → c51(2NDSNEG(z0, z1))
2NDSNEG(active(z0), z1) → c52(2NDSNEG(z0, z1))
2NDSNEG(z0, active(z1)) → c53(2NDSNEG(z0, z1))
NEGRECIP(mark(z0)) → c54(NEGRECIP(z0))
NEGRECIP(active(z0)) → c55(NEGRECIP(z0))
PI(mark(z0)) → c56(PI(z0))
PI(active(z0)) → c57(PI(z0))
PLUS(mark(z0), z1) → c58(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c59(PLUS(z0, z1))
PLUS(active(z0), z1) → c60(PLUS(z0, z1))
PLUS(z0, active(z1)) → c61(PLUS(z0, z1))
TIMES(mark(z0), z1) → c62(TIMES(z0, z1))
TIMES(z0, mark(z1)) → c63(TIMES(z0, z1))
TIMES(active(z0), z1) → c64(TIMES(z0, z1))
TIMES(z0, active(z1)) → c65(TIMES(z0, z1))
SQUARE(mark(z0)) → c66(SQUARE(z0))
SQUARE(active(z0)) → c67(SQUARE(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(from(z0)) → mark(cons(z0, from(s(z0))))
active(2ndspos(0, z0)) → mark(rnil)
active(2ndspos(s(z0), cons(z1, z2))) → mark(2ndspos(s(z0), cons2(z1, z2)))
active(2ndspos(s(z0), cons2(z1, cons(z2, z3)))) → mark(rcons(posrecip(z2), 2ndsneg(z0, z3)))
active(2ndsneg(0, z0)) → mark(rnil)
active(2ndsneg(s(z0), cons(z1, z2))) → mark(2ndsneg(s(z0), cons2(z1, z2)))
active(2ndsneg(s(z0), cons2(z1, cons(z2, z3)))) → mark(rcons(negrecip(z2), 2ndspos(z0, z3)))
active(pi(z0)) → mark(2ndspos(z0, from(0)))
active(plus(0, z0)) → mark(z0)
active(plus(s(z0), z1)) → mark(s(plus(z0, z1)))
active(times(0, z0)) → mark(0)
active(times(s(z0), z1)) → mark(plus(z1, times(z0, z1)))
active(square(z0)) → mark(times(z0, z0))
mark(from(z0)) → active(from(mark(z0)))
mark(cons(z0, z1)) → active(cons(mark(z0), z1))
mark(s(z0)) → active(s(mark(z0)))
mark(2ndspos(z0, z1)) → active(2ndspos(mark(z0), mark(z1)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(z0, z1)) → active(cons2(z0, mark(z1)))
mark(rcons(z0, z1)) → active(rcons(mark(z0), mark(z1)))
mark(posrecip(z0)) → active(posrecip(mark(z0)))
mark(2ndsneg(z0, z1)) → active(2ndsneg(mark(z0), mark(z1)))
mark(negrecip(z0)) → active(negrecip(mark(z0)))
mark(pi(z0)) → active(pi(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(times(z0, z1)) → active(times(mark(z0), mark(z1)))
mark(square(z0)) → active(square(mark(z0)))
from(mark(z0)) → from(z0)
from(active(z0)) → from(z0)
cons(mark(z0), z1) → cons(z0, z1)
cons(z0, mark(z1)) → cons(z0, z1)
cons(active(z0), z1) → cons(z0, z1)
cons(z0, active(z1)) → cons(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
2ndspos(mark(z0), z1) → 2ndspos(z0, z1)
2ndspos(z0, mark(z1)) → 2ndspos(z0, z1)
2ndspos(active(z0), z1) → 2ndspos(z0, z1)
2ndspos(z0, active(z1)) → 2ndspos(z0, z1)
cons2(mark(z0), z1) → cons2(z0, z1)
cons2(z0, mark(z1)) → cons2(z0, z1)
cons2(active(z0), z1) → cons2(z0, z1)
cons2(z0, active(z1)) → cons2(z0, z1)
rcons(mark(z0), z1) → rcons(z0, z1)
rcons(z0, mark(z1)) → rcons(z0, z1)
rcons(active(z0), z1) → rcons(z0, z1)
rcons(z0, active(z1)) → rcons(z0, z1)
posrecip(mark(z0)) → posrecip(z0)
posrecip(active(z0)) → posrecip(z0)
2ndsneg(mark(z0), z1) → 2ndsneg(z0, z1)
2ndsneg(z0, mark(z1)) → 2ndsneg(z0, z1)
2ndsneg(active(z0), z1) → 2ndsneg(z0, z1)
2ndsneg(z0, active(z1)) → 2ndsneg(z0, z1)
negrecip(mark(z0)) → negrecip(z0)
negrecip(active(z0)) → negrecip(z0)
pi(mark(z0)) → pi(z0)
pi(active(z0)) → pi(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
times(mark(z0), z1) → times(z0, z1)
times(z0, mark(z1)) → times(z0, z1)
times(active(z0), z1) → times(z0, z1)
times(z0, active(z1)) → times(z0, z1)
square(mark(z0)) → square(z0)
square(active(z0)) → square(z0)
Tuples:
MARK(0) → c17(ACTIVE(0))
MARK(rnil) → c18(ACTIVE(rnil))
S tuples:
MARK(0) → c17(ACTIVE(0))
MARK(rnil) → c18(ACTIVE(rnil))
K tuples:none
Defined Rule Symbols:
active, mark, from, cons, s, 2ndspos, cons2, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square
Defined Pair Symbols:
MARK
Compound Symbols:
c17, c18
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
MARK(0) → c17(ACTIVE(0))
MARK(rnil) → c18(ACTIVE(rnil))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(from(z0)) → mark(cons(z0, from(s(z0))))
active(2ndspos(0, z0)) → mark(rnil)
active(2ndspos(s(z0), cons(z1, z2))) → mark(2ndspos(s(z0), cons2(z1, z2)))
active(2ndspos(s(z0), cons2(z1, cons(z2, z3)))) → mark(rcons(posrecip(z2), 2ndsneg(z0, z3)))
active(2ndsneg(0, z0)) → mark(rnil)
active(2ndsneg(s(z0), cons(z1, z2))) → mark(2ndsneg(s(z0), cons2(z1, z2)))
active(2ndsneg(s(z0), cons2(z1, cons(z2, z3)))) → mark(rcons(negrecip(z2), 2ndspos(z0, z3)))
active(pi(z0)) → mark(2ndspos(z0, from(0)))
active(plus(0, z0)) → mark(z0)
active(plus(s(z0), z1)) → mark(s(plus(z0, z1)))
active(times(0, z0)) → mark(0)
active(times(s(z0), z1)) → mark(plus(z1, times(z0, z1)))
active(square(z0)) → mark(times(z0, z0))
mark(from(z0)) → active(from(mark(z0)))
mark(cons(z0, z1)) → active(cons(mark(z0), z1))
mark(s(z0)) → active(s(mark(z0)))
mark(2ndspos(z0, z1)) → active(2ndspos(mark(z0), mark(z1)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(z0, z1)) → active(cons2(z0, mark(z1)))
mark(rcons(z0, z1)) → active(rcons(mark(z0), mark(z1)))
mark(posrecip(z0)) → active(posrecip(mark(z0)))
mark(2ndsneg(z0, z1)) → active(2ndsneg(mark(z0), mark(z1)))
mark(negrecip(z0)) → active(negrecip(mark(z0)))
mark(pi(z0)) → active(pi(mark(z0)))
mark(plus(z0, z1)) → active(plus(mark(z0), mark(z1)))
mark(times(z0, z1)) → active(times(mark(z0), mark(z1)))
mark(square(z0)) → active(square(mark(z0)))
from(mark(z0)) → from(z0)
from(active(z0)) → from(z0)
cons(mark(z0), z1) → cons(z0, z1)
cons(z0, mark(z1)) → cons(z0, z1)
cons(active(z0), z1) → cons(z0, z1)
cons(z0, active(z1)) → cons(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
2ndspos(mark(z0), z1) → 2ndspos(z0, z1)
2ndspos(z0, mark(z1)) → 2ndspos(z0, z1)
2ndspos(active(z0), z1) → 2ndspos(z0, z1)
2ndspos(z0, active(z1)) → 2ndspos(z0, z1)
cons2(mark(z0), z1) → cons2(z0, z1)
cons2(z0, mark(z1)) → cons2(z0, z1)
cons2(active(z0), z1) → cons2(z0, z1)
cons2(z0, active(z1)) → cons2(z0, z1)
rcons(mark(z0), z1) → rcons(z0, z1)
rcons(z0, mark(z1)) → rcons(z0, z1)
rcons(active(z0), z1) → rcons(z0, z1)
rcons(z0, active(z1)) → rcons(z0, z1)
posrecip(mark(z0)) → posrecip(z0)
posrecip(active(z0)) → posrecip(z0)
2ndsneg(mark(z0), z1) → 2ndsneg(z0, z1)
2ndsneg(z0, mark(z1)) → 2ndsneg(z0, z1)
2ndsneg(active(z0), z1) → 2ndsneg(z0, z1)
2ndsneg(z0, active(z1)) → 2ndsneg(z0, z1)
negrecip(mark(z0)) → negrecip(z0)
negrecip(active(z0)) → negrecip(z0)
pi(mark(z0)) → pi(z0)
pi(active(z0)) → pi(z0)
plus(mark(z0), z1) → plus(z0, z1)
plus(z0, mark(z1)) → plus(z0, z1)
plus(active(z0), z1) → plus(z0, z1)
plus(z0, active(z1)) → plus(z0, z1)
times(mark(z0), z1) → times(z0, z1)
times(z0, mark(z1)) → times(z0, z1)
times(active(z0), z1) → times(z0, z1)
times(z0, active(z1)) → times(z0, z1)
square(mark(z0)) → square(z0)
square(active(z0)) → square(z0)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
active, mark, from, cons, s, 2ndspos, cons2, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))