YES(O(1), O(n^1)) 0.00/0.73 YES(O(1), O(n^1)) 0.00/0.74 0.00/0.74 0.00/0.74
0.00/0.74 0.00/0.740 CpxTRS0.00/0.74
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.74
↳2 CdtProblem0.00/0.74
↳3 CdtUnreachableProof (⇔)0.00/0.74
↳4 CdtProblem0.00/0.74
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.74
↳6 CdtProblem0.00/0.74
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.74
↳8 CdtProblem0.00/0.74
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.74
↳10 CdtProblem0.00/0.74
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.74
↳12 BOUNDS(O(1), O(1))0.00/0.74
f(0) → cons(0, n__f(n__s(n__0))) 0.00/0.74
f(s(0)) → f(p(s(0))) 0.00/0.74
p(s(X)) → X 0.00/0.74
f(X) → n__f(X) 0.00/0.74
s(X) → n__s(X) 0.00/0.74
0 → n__0 0.00/0.74
activate(n__f(X)) → f(activate(X)) 0.00/0.74
activate(n__s(X)) → s(activate(X)) 0.00/0.74
activate(n__0) → 0 0.00/0.74
activate(X) → X
Tuples:
f(0) → cons(0, n__f(n__s(n__0))) 0.00/0.74
f(s(0)) → f(p(s(0))) 0.00/0.74
f(z0) → n__f(z0) 0.00/0.74
p(s(z0)) → z0 0.00/0.74
s(z0) → n__s(z0) 0.00/0.74
0 → n__0 0.00/0.74
activate(n__f(z0)) → f(activate(z0)) 0.00/0.74
activate(n__s(z0)) → s(activate(z0)) 0.00/0.74
activate(n__0) → 0 0.00/0.74
activate(z0) → z0
S tuples:
F(0) → c(0') 0.00/0.74
F(s(0)) → c1(F(p(s(0))), P(s(0)), S(0), 0') 0.00/0.74
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(S(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8(0')
K tuples:none
F(0) → c(0') 0.00/0.74
F(s(0)) → c1(F(p(s(0))), P(s(0)), S(0), 0') 0.00/0.74
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(S(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8(0')
f, p, s, 0, activate
F, ACTIVATE
c, c1, c6, c7, c8
F(0) → c(0') 0.00/0.74
F(s(0)) → c1(F(p(s(0))), P(s(0)), S(0), 0')
Tuples:
f(0) → cons(0, n__f(n__s(n__0))) 0.00/0.74
f(s(0)) → f(p(s(0))) 0.00/0.74
f(z0) → n__f(z0) 0.00/0.74
p(s(z0)) → z0 0.00/0.74
s(z0) → n__s(z0) 0.00/0.74
0 → n__0 0.00/0.74
activate(n__f(z0)) → f(activate(z0)) 0.00/0.74
activate(n__s(z0)) → s(activate(z0)) 0.00/0.74
activate(n__0) → 0 0.00/0.74
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(S(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8(0')
K tuples:none
ACTIVATE(n__f(z0)) → c6(F(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(S(activate(z0)), ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8(0')
f, p, s, 0, activate
ACTIVATE
c6, c7, c8
Tuples:
f(0) → cons(0, n__f(n__s(n__0))) 0.00/0.74
f(s(0)) → f(p(s(0))) 0.00/0.74
f(z0) → n__f(z0) 0.00/0.74
p(s(z0)) → z0 0.00/0.74
s(z0) → n__s(z0) 0.00/0.74
0 → n__0 0.00/0.74
activate(n__f(z0)) → f(activate(z0)) 0.00/0.74
activate(n__s(z0)) → s(activate(z0)) 0.00/0.74
activate(n__0) → 0 0.00/0.74
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
K tuples:none
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
f, p, s, 0, activate
ACTIVATE
c6, c7, c8
ACTIVATE(n__0) → c8
Tuples:
f(0) → cons(0, n__f(n__s(n__0))) 0.00/0.74
f(s(0)) → f(p(s(0))) 0.00/0.74
f(z0) → n__f(z0) 0.00/0.74
p(s(z0)) → z0 0.00/0.74
s(z0) → n__s(z0) 0.00/0.74
0 → n__0 0.00/0.74
activate(n__f(z0)) → f(activate(z0)) 0.00/0.74
activate(n__s(z0)) → s(activate(z0)) 0.00/0.74
activate(n__0) → 0 0.00/0.74
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
K tuples:none
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
f, p, s, 0, activate
ACTIVATE
c6, c7, c8
We considered the (Usable) Rules:none
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
The order we found is given by the following interpretation:
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
POL(ACTIVATE(x1)) = [5] + [3]x1 0.00/0.74
POL(c6(x1)) = x1 0.00/0.74
POL(c7(x1)) = x1 0.00/0.74
POL(c8) = 0 0.00/0.74
POL(n__0) = [5] 0.00/0.74
POL(n__f(x1)) = [5] + x1 0.00/0.74
POL(n__s(x1)) = [5] + x1
Tuples:
f(0) → cons(0, n__f(n__s(n__0))) 0.00/0.74
f(s(0)) → f(p(s(0))) 0.00/0.74
f(z0) → n__f(z0) 0.00/0.74
p(s(z0)) → z0 0.00/0.74
s(z0) → n__s(z0) 0.00/0.74
0 → n__0 0.00/0.74
activate(n__f(z0)) → f(activate(z0)) 0.00/0.74
activate(n__s(z0)) → s(activate(z0)) 0.00/0.74
activate(n__0) → 0 0.00/0.74
activate(z0) → z0
S tuples:none
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
Defined Rule Symbols:
ACTIVATE(n__f(z0)) → c6(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__s(z0)) → c7(ACTIVATE(z0)) 0.00/0.74
ACTIVATE(n__0) → c8
f, p, s, 0, activate
ACTIVATE
c6, c7, c8