(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, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(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(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)
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, cons(z2, z3)))) → mark(rcons(posrecip(z2), 2ndsneg(z0, z3)))
active(2ndsneg(0, z0)) → mark(rnil)
active(2ndsneg(s(z0), cons(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(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)
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, cons(z2, z3)))) → c2(MARK(rcons(posrecip(z2), 2ndsneg(z0, z3))), RCONS(posrecip(z2), 2ndsneg(z0, z3)), POSRECIP(z2), 2NDSNEG(z0, z3))
ACTIVE(2ndsneg(0, z0)) → c3(MARK(rnil))
ACTIVE(2ndsneg(s(z0), cons(z1, cons(z2, z3)))) → c4(MARK(rcons(negrecip(z2), 2ndspos(z0, z3))), RCONS(negrecip(z2), 2ndspos(z0, z3)), NEGRECIP(z2), 2NDSPOS(z0, z3))
ACTIVE(pi(z0)) → c5(MARK(2ndspos(z0, from(0))), 2NDSPOS(z0, from(0)), FROM(0))
ACTIVE(plus(0, z0)) → c6(MARK(z0))
ACTIVE(plus(s(z0), z1)) → c7(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
ACTIVE(times(0, z0)) → c8(MARK(0))
ACTIVE(times(s(z0), z1)) → c9(MARK(plus(z1, times(z0, z1))), PLUS(z1, times(z0, z1)), TIMES(z0, z1))
ACTIVE(square(z0)) → c10(MARK(times(z0, z0)), TIMES(z0, z0))
MARK(from(z0)) → c11(ACTIVE(from(mark(z0))), FROM(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c12(ACTIVE(cons(mark(z0), z1)), CONS(mark(z0), z1), MARK(z0))
MARK(s(z0)) → c13(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(2ndspos(z0, z1)) → c14(ACTIVE(2ndspos(mark(z0), mark(z1))), 2NDSPOS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c15(ACTIVE(0))
MARK(rnil) → c16(ACTIVE(rnil))
MARK(rcons(z0, z1)) → c17(ACTIVE(rcons(mark(z0), mark(z1))), RCONS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(posrecip(z0)) → c18(ACTIVE(posrecip(mark(z0))), POSRECIP(mark(z0)), MARK(z0))
MARK(2ndsneg(z0, z1)) → c19(ACTIVE(2ndsneg(mark(z0), mark(z1))), 2NDSNEG(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(negrecip(z0)) → c20(ACTIVE(negrecip(mark(z0))), NEGRECIP(mark(z0)), MARK(z0))
MARK(pi(z0)) → c21(ACTIVE(pi(mark(z0))), PI(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c22(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(times(z0, z1)) → c23(ACTIVE(times(mark(z0), mark(z1))), TIMES(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(square(z0)) → c24(ACTIVE(square(mark(z0))), SQUARE(mark(z0)), MARK(z0))
FROM(mark(z0)) → c25(FROM(z0))
FROM(active(z0)) → c26(FROM(z0))
CONS(mark(z0), z1) → c27(CONS(z0, z1))
CONS(z0, mark(z1)) → c28(CONS(z0, z1))
CONS(active(z0), z1) → c29(CONS(z0, z1))
CONS(z0, active(z1)) → c30(CONS(z0, z1))
S(mark(z0)) → c31(S(z0))
S(active(z0)) → c32(S(z0))
2NDSPOS(mark(z0), z1) → c33(2NDSPOS(z0, z1))
2NDSPOS(z0, mark(z1)) → c34(2NDSPOS(z0, z1))
2NDSPOS(active(z0), z1) → c35(2NDSPOS(z0, z1))
2NDSPOS(z0, active(z1)) → c36(2NDSPOS(z0, z1))
RCONS(mark(z0), z1) → c37(RCONS(z0, z1))
RCONS(z0, mark(z1)) → c38(RCONS(z0, z1))
RCONS(active(z0), z1) → c39(RCONS(z0, z1))
RCONS(z0, active(z1)) → c40(RCONS(z0, z1))
POSRECIP(mark(z0)) → c41(POSRECIP(z0))
POSRECIP(active(z0)) → c42(POSRECIP(z0))
2NDSNEG(mark(z0), z1) → c43(2NDSNEG(z0, z1))
2NDSNEG(z0, mark(z1)) → c44(2NDSNEG(z0, z1))
2NDSNEG(active(z0), z1) → c45(2NDSNEG(z0, z1))
2NDSNEG(z0, active(z1)) → c46(2NDSNEG(z0, z1))
NEGRECIP(mark(z0)) → c47(NEGRECIP(z0))
NEGRECIP(active(z0)) → c48(NEGRECIP(z0))
PI(mark(z0)) → c49(PI(z0))
PI(active(z0)) → c50(PI(z0))
PLUS(mark(z0), z1) → c51(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c52(PLUS(z0, z1))
PLUS(active(z0), z1) → c53(PLUS(z0, z1))
PLUS(z0, active(z1)) → c54(PLUS(z0, z1))
TIMES(mark(z0), z1) → c55(TIMES(z0, z1))
TIMES(z0, mark(z1)) → c56(TIMES(z0, z1))
TIMES(active(z0), z1) → c57(TIMES(z0, z1))
TIMES(z0, active(z1)) → c58(TIMES(z0, z1))
SQUARE(mark(z0)) → c59(SQUARE(z0))
SQUARE(active(z0)) → c60(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, cons(z2, z3)))) → c2(MARK(rcons(posrecip(z2), 2ndsneg(z0, z3))), RCONS(posrecip(z2), 2ndsneg(z0, z3)), POSRECIP(z2), 2NDSNEG(z0, z3))
ACTIVE(2ndsneg(0, z0)) → c3(MARK(rnil))
ACTIVE(2ndsneg(s(z0), cons(z1, cons(z2, z3)))) → c4(MARK(rcons(negrecip(z2), 2ndspos(z0, z3))), RCONS(negrecip(z2), 2ndspos(z0, z3)), NEGRECIP(z2), 2NDSPOS(z0, z3))
ACTIVE(pi(z0)) → c5(MARK(2ndspos(z0, from(0))), 2NDSPOS(z0, from(0)), FROM(0))
ACTIVE(plus(0, z0)) → c6(MARK(z0))
ACTIVE(plus(s(z0), z1)) → c7(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
ACTIVE(times(0, z0)) → c8(MARK(0))
ACTIVE(times(s(z0), z1)) → c9(MARK(plus(z1, times(z0, z1))), PLUS(z1, times(z0, z1)), TIMES(z0, z1))
ACTIVE(square(z0)) → c10(MARK(times(z0, z0)), TIMES(z0, z0))
MARK(from(z0)) → c11(ACTIVE(from(mark(z0))), FROM(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c12(ACTIVE(cons(mark(z0), z1)), CONS(mark(z0), z1), MARK(z0))
MARK(s(z0)) → c13(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(2ndspos(z0, z1)) → c14(ACTIVE(2ndspos(mark(z0), mark(z1))), 2NDSPOS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(0) → c15(ACTIVE(0))
MARK(rnil) → c16(ACTIVE(rnil))
MARK(rcons(z0, z1)) → c17(ACTIVE(rcons(mark(z0), mark(z1))), RCONS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(posrecip(z0)) → c18(ACTIVE(posrecip(mark(z0))), POSRECIP(mark(z0)), MARK(z0))
MARK(2ndsneg(z0, z1)) → c19(ACTIVE(2ndsneg(mark(z0), mark(z1))), 2NDSNEG(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(negrecip(z0)) → c20(ACTIVE(negrecip(mark(z0))), NEGRECIP(mark(z0)), MARK(z0))
MARK(pi(z0)) → c21(ACTIVE(pi(mark(z0))), PI(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c22(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(times(z0, z1)) → c23(ACTIVE(times(mark(z0), mark(z1))), TIMES(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(square(z0)) → c24(ACTIVE(square(mark(z0))), SQUARE(mark(z0)), MARK(z0))
FROM(mark(z0)) → c25(FROM(z0))
FROM(active(z0)) → c26(FROM(z0))
CONS(mark(z0), z1) → c27(CONS(z0, z1))
CONS(z0, mark(z1)) → c28(CONS(z0, z1))
CONS(active(z0), z1) → c29(CONS(z0, z1))
CONS(z0, active(z1)) → c30(CONS(z0, z1))
S(mark(z0)) → c31(S(z0))
S(active(z0)) → c32(S(z0))
2NDSPOS(mark(z0), z1) → c33(2NDSPOS(z0, z1))
2NDSPOS(z0, mark(z1)) → c34(2NDSPOS(z0, z1))
2NDSPOS(active(z0), z1) → c35(2NDSPOS(z0, z1))
2NDSPOS(z0, active(z1)) → c36(2NDSPOS(z0, z1))
RCONS(mark(z0), z1) → c37(RCONS(z0, z1))
RCONS(z0, mark(z1)) → c38(RCONS(z0, z1))
RCONS(active(z0), z1) → c39(RCONS(z0, z1))
RCONS(z0, active(z1)) → c40(RCONS(z0, z1))
POSRECIP(mark(z0)) → c41(POSRECIP(z0))
POSRECIP(active(z0)) → c42(POSRECIP(z0))
2NDSNEG(mark(z0), z1) → c43(2NDSNEG(z0, z1))
2NDSNEG(z0, mark(z1)) → c44(2NDSNEG(z0, z1))
2NDSNEG(active(z0), z1) → c45(2NDSNEG(z0, z1))
2NDSNEG(z0, active(z1)) → c46(2NDSNEG(z0, z1))
NEGRECIP(mark(z0)) → c47(NEGRECIP(z0))
NEGRECIP(active(z0)) → c48(NEGRECIP(z0))
PI(mark(z0)) → c49(PI(z0))
PI(active(z0)) → c50(PI(z0))
PLUS(mark(z0), z1) → c51(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c52(PLUS(z0, z1))
PLUS(active(z0), z1) → c53(PLUS(z0, z1))
PLUS(z0, active(z1)) → c54(PLUS(z0, z1))
TIMES(mark(z0), z1) → c55(TIMES(z0, z1))
TIMES(z0, mark(z1)) → c56(TIMES(z0, z1))
TIMES(active(z0), z1) → c57(TIMES(z0, z1))
TIMES(z0, active(z1)) → c58(TIMES(z0, z1))
SQUARE(mark(z0)) → c59(SQUARE(z0))
SQUARE(active(z0)) → c60(SQUARE(z0))
K tuples:none
Defined Rule Symbols:
active, mark, from, cons, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square
Defined Pair Symbols:
ACTIVE, MARK, FROM, CONS, S, 2NDSPOS, 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
(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, cons(z2, z3)))) → c2(MARK(rcons(posrecip(z2), 2ndsneg(z0, z3))), RCONS(posrecip(z2), 2ndsneg(z0, z3)), POSRECIP(z2), 2NDSNEG(z0, z3))
ACTIVE(2ndsneg(0, z0)) → c3(MARK(rnil))
ACTIVE(2ndsneg(s(z0), cons(z1, cons(z2, z3)))) → c4(MARK(rcons(negrecip(z2), 2ndspos(z0, z3))), RCONS(negrecip(z2), 2ndspos(z0, z3)), NEGRECIP(z2), 2NDSPOS(z0, z3))
ACTIVE(pi(z0)) → c5(MARK(2ndspos(z0, from(0))), 2NDSPOS(z0, from(0)), FROM(0))
ACTIVE(plus(0, z0)) → c6(MARK(z0))
ACTIVE(plus(s(z0), z1)) → c7(MARK(s(plus(z0, z1))), S(plus(z0, z1)), PLUS(z0, z1))
ACTIVE(times(0, z0)) → c8(MARK(0))
ACTIVE(times(s(z0), z1)) → c9(MARK(plus(z1, times(z0, z1))), PLUS(z1, times(z0, z1)), TIMES(z0, z1))
ACTIVE(square(z0)) → c10(MARK(times(z0, z0)), TIMES(z0, z0))
MARK(from(z0)) → c11(ACTIVE(from(mark(z0))), FROM(mark(z0)), MARK(z0))
MARK(cons(z0, z1)) → c12(ACTIVE(cons(mark(z0), z1)), CONS(mark(z0), z1), MARK(z0))
MARK(s(z0)) → c13(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(2ndspos(z0, z1)) → c14(ACTIVE(2ndspos(mark(z0), mark(z1))), 2NDSPOS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(rcons(z0, z1)) → c17(ACTIVE(rcons(mark(z0), mark(z1))), RCONS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(posrecip(z0)) → c18(ACTIVE(posrecip(mark(z0))), POSRECIP(mark(z0)), MARK(z0))
MARK(2ndsneg(z0, z1)) → c19(ACTIVE(2ndsneg(mark(z0), mark(z1))), 2NDSNEG(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(negrecip(z0)) → c20(ACTIVE(negrecip(mark(z0))), NEGRECIP(mark(z0)), MARK(z0))
MARK(pi(z0)) → c21(ACTIVE(pi(mark(z0))), PI(mark(z0)), MARK(z0))
MARK(plus(z0, z1)) → c22(ACTIVE(plus(mark(z0), mark(z1))), PLUS(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(times(z0, z1)) → c23(ACTIVE(times(mark(z0), mark(z1))), TIMES(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(square(z0)) → c24(ACTIVE(square(mark(z0))), SQUARE(mark(z0)), MARK(z0))
FROM(mark(z0)) → c25(FROM(z0))
FROM(active(z0)) → c26(FROM(z0))
CONS(mark(z0), z1) → c27(CONS(z0, z1))
CONS(z0, mark(z1)) → c28(CONS(z0, z1))
CONS(active(z0), z1) → c29(CONS(z0, z1))
CONS(z0, active(z1)) → c30(CONS(z0, z1))
S(mark(z0)) → c31(S(z0))
S(active(z0)) → c32(S(z0))
2NDSPOS(mark(z0), z1) → c33(2NDSPOS(z0, z1))
2NDSPOS(z0, mark(z1)) → c34(2NDSPOS(z0, z1))
2NDSPOS(active(z0), z1) → c35(2NDSPOS(z0, z1))
2NDSPOS(z0, active(z1)) → c36(2NDSPOS(z0, z1))
RCONS(mark(z0), z1) → c37(RCONS(z0, z1))
RCONS(z0, mark(z1)) → c38(RCONS(z0, z1))
RCONS(active(z0), z1) → c39(RCONS(z0, z1))
RCONS(z0, active(z1)) → c40(RCONS(z0, z1))
POSRECIP(mark(z0)) → c41(POSRECIP(z0))
POSRECIP(active(z0)) → c42(POSRECIP(z0))
2NDSNEG(mark(z0), z1) → c43(2NDSNEG(z0, z1))
2NDSNEG(z0, mark(z1)) → c44(2NDSNEG(z0, z1))
2NDSNEG(active(z0), z1) → c45(2NDSNEG(z0, z1))
2NDSNEG(z0, active(z1)) → c46(2NDSNEG(z0, z1))
NEGRECIP(mark(z0)) → c47(NEGRECIP(z0))
NEGRECIP(active(z0)) → c48(NEGRECIP(z0))
PI(mark(z0)) → c49(PI(z0))
PI(active(z0)) → c50(PI(z0))
PLUS(mark(z0), z1) → c51(PLUS(z0, z1))
PLUS(z0, mark(z1)) → c52(PLUS(z0, z1))
PLUS(active(z0), z1) → c53(PLUS(z0, z1))
PLUS(z0, active(z1)) → c54(PLUS(z0, z1))
TIMES(mark(z0), z1) → c55(TIMES(z0, z1))
TIMES(z0, mark(z1)) → c56(TIMES(z0, z1))
TIMES(active(z0), z1) → c57(TIMES(z0, z1))
TIMES(z0, active(z1)) → c58(TIMES(z0, z1))
SQUARE(mark(z0)) → c59(SQUARE(z0))
SQUARE(active(z0)) → c60(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, cons(z2, z3)))) → mark(rcons(posrecip(z2), 2ndsneg(z0, z3)))
active(2ndsneg(0, z0)) → mark(rnil)
active(2ndsneg(s(z0), cons(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(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)
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) → c15(ACTIVE(0))
MARK(rnil) → c16(ACTIVE(rnil))
S tuples:
MARK(0) → c15(ACTIVE(0))
MARK(rnil) → c16(ACTIVE(rnil))
K tuples:none
Defined Rule Symbols:
active, mark, from, cons, s, 2ndspos, rcons, posrecip, 2ndsneg, negrecip, pi, plus, times, square
Defined Pair Symbols:
MARK
Compound Symbols:
c15, c16
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
MARK(0) → c15(ACTIVE(0))
MARK(rnil) → c16(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, cons(z2, z3)))) → mark(rcons(posrecip(z2), 2ndsneg(z0, z3)))
active(2ndsneg(0, z0)) → mark(rnil)
active(2ndsneg(s(z0), cons(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(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)
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, 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))