YES(O(1), O(n^1)) 0.00/0.78 YES(O(1), O(n^1)) 0.00/0.80 0.00/0.80 0.00/0.80
0.00/0.80 0.00/0.800 CpxTRS0.00/0.80
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.80
↳2 CdtProblem0.00/0.80
↳3 CdtUnreachableProof (⇔)0.00/0.80
↳4 CdtProblem0.00/0.80
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.80
↳6 CdtProblem0.00/0.80
↳7 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.80
↳8 CdtProblem0.00/0.80
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.80
↳10 CdtProblem0.00/0.80
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.80
↳12 CdtProblem0.00/0.80
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.80
↳14 BOUNDS(O(1), O(1))0.00/0.80
f(f(X)) → c(n__f(n__g(n__f(X)))) 0.00/0.80
c(X) → d(activate(X)) 0.00/0.80
h(X) → c(n__d(X)) 0.00/0.80
f(X) → n__f(X) 0.00/0.80
g(X) → n__g(X) 0.00/0.80
d(X) → n__d(X) 0.00/0.80
activate(n__f(X)) → f(activate(X)) 0.00/0.80
activate(n__g(X)) → g(X) 0.00/0.80
activate(n__d(X)) → d(X) 0.00/0.80
activate(X) → X
Tuples:
f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
S tuples:
F(f(z0)) → c1(C(n__f(n__g(n__f(z0))))) 0.00/0.80
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
K tuples:none
F(f(z0)) → c1(C(n__f(n__g(n__f(z0))))) 0.00/0.80
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
f, c, h, g, d, activate
F, C, H, ACTIVATE
c1, c3, c4, c7, c8, c9
F(f(z0)) → c1(C(n__f(n__g(n__f(z0)))))
Tuples:
f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
S tuples:
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
K tuples:none
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.80
H(z0) → c4(C(n__d(z0))) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(F(activate(z0)), ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8(G(z0)) 0.00/0.80
ACTIVATE(n__d(z0)) → c9(D(z0))
f, c, h, g, d, activate
C, H, ACTIVATE
c3, c4, c7, c8, c9
Tuples:
f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
S tuples:
H(z0) → c4(C(n__d(z0))) 0.00/0.80
C(z0) → c3(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
K tuples:none
H(z0) → c4(C(n__d(z0))) 0.00/0.80
C(z0) → c3(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
f, c, h, g, d, activate
H, C, ACTIVATE
c4, c3, c7, c8, c9
Removed 2 trailing nodes:
H(z0) → c4(C(n__d(z0))) 0.00/0.80
C(z0) → c3(ACTIVATE(z0))
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
Tuples:
f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
K tuples:none
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
f, c, h, g, d, activate
ACTIVATE
c7, c8, c9
We considered the (Usable) Rules:none
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
The order we found is given by the following interpretation:
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
POL(ACTIVATE(x1)) = [1] 0.00/0.80
POL(c7(x1)) = x1 0.00/0.80
POL(c8) = 0 0.00/0.80
POL(c9) = 0 0.00/0.80
POL(n__d(x1)) = [1] 0.00/0.80
POL(n__f(x1)) = [1] + x1 0.00/0.80
POL(n__g(x1)) = [1]
Tuples:
f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
K tuples:
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0))
Defined Rule Symbols:
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
f, c, h, g, d, activate
ACTIVATE
c7, c8, c9
We considered the (Usable) Rules:none
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0))
The order we found is given by the following interpretation:
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
POL(ACTIVATE(x1)) = [3]x1 0.00/0.80
POL(c7(x1)) = x1 0.00/0.80
POL(c8) = 0 0.00/0.80
POL(c9) = 0 0.00/0.80
POL(n__d(x1)) = 0 0.00/0.80
POL(n__f(x1)) = [1] + x1 0.00/0.80
POL(n__g(x1)) = 0
Tuples:
f(f(z0)) → c(n__f(n__g(n__f(z0)))) 0.00/0.80
f(z0) → n__f(z0) 0.00/0.80
c(z0) → d(activate(z0)) 0.00/0.80
h(z0) → c(n__d(z0)) 0.00/0.80
g(z0) → n__g(z0) 0.00/0.80
d(z0) → n__d(z0) 0.00/0.80
activate(n__f(z0)) → f(activate(z0)) 0.00/0.80
activate(n__g(z0)) → g(z0) 0.00/0.80
activate(n__d(z0)) → d(z0) 0.00/0.80
activate(z0) → z0
S tuples:none
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0)) 0.00/0.80
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9
Defined Rule Symbols:
ACTIVATE(n__g(z0)) → c8 0.00/0.80
ACTIVATE(n__d(z0)) → c9 0.00/0.80
ACTIVATE(n__f(z0)) → c7(ACTIVATE(z0))
f, c, h, g, d, activate
ACTIVATE
c7, c8, c9