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