YES(O(1), O(1)) 0.00/0.55 YES(O(1), O(1)) 0.00/0.57 0.00/0.57 0.00/0.57
0.00/0.57 0.00/0.580 CpxTRS0.00/0.58
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.58
↳2 CdtProblem0.00/0.58
↳3 CdtUnreachableProof (⇔)0.00/0.58
↳4 CdtProblem0.00/0.58
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.58
↳6 CdtProblem0.00/0.58
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.58
↳8 CdtProblem0.00/0.58
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.58
↳10 BOUNDS(O(1), O(1))0.00/0.58
f(f(X)) → c(n__f(g(n__f(X)))) 0.00/0.58
c(X) → d(activate(X)) 0.00/0.58
h(X) → c(n__d(X)) 0.00/0.58
f(X) → n__f(X) 0.00/0.58
d(X) → n__d(X) 0.00/0.58
activate(n__f(X)) → f(X) 0.00/0.58
activate(n__d(X)) → d(X) 0.00/0.58
activate(X) → X
Tuples:
f(f(z0)) → c(n__f(g(n__f(z0)))) 0.00/0.58
f(z0) → n__f(z0) 0.00/0.58
c(z0) → d(activate(z0)) 0.00/0.58
h(z0) → c(n__d(z0)) 0.00/0.58
d(z0) → n__d(z0) 0.00/0.58
activate(n__f(z0)) → f(z0) 0.00/0.58
activate(n__d(z0)) → d(z0) 0.00/0.58
activate(z0) → z0
S tuples:
F(f(z0)) → c1(C(n__f(g(n__f(z0))))) 0.00/0.58
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
K tuples:none
F(f(z0)) → c1(C(n__f(g(n__f(z0))))) 0.00/0.58
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
f, c, h, d, activate
F, C, H, ACTIVATE
c1, c3, c4, c6, c7
F(f(z0)) → c1(C(n__f(g(n__f(z0)))))
Tuples:
f(f(z0)) → c(n__f(g(n__f(z0)))) 0.00/0.58
f(z0) → n__f(z0) 0.00/0.58
c(z0) → d(activate(z0)) 0.00/0.58
h(z0) → c(n__d(z0)) 0.00/0.58
d(z0) → n__d(z0) 0.00/0.58
activate(n__f(z0)) → f(z0) 0.00/0.58
activate(n__d(z0)) → d(z0) 0.00/0.58
activate(z0) → z0
S tuples:
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
K tuples:none
C(z0) → c3(D(activate(z0)), ACTIVATE(z0)) 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
ACTIVATE(n__f(z0)) → c6(F(z0)) 0.00/0.58
ACTIVATE(n__d(z0)) → c7(D(z0))
f, c, h, d, activate
C, H, ACTIVATE
c3, c4, c6, c7
Tuples:
f(f(z0)) → c(n__f(g(n__f(z0)))) 0.00/0.58
f(z0) → n__f(z0) 0.00/0.58
c(z0) → d(activate(z0)) 0.00/0.58
h(z0) → c(n__d(z0)) 0.00/0.58
d(z0) → n__d(z0) 0.00/0.58
activate(n__f(z0)) → f(z0) 0.00/0.58
activate(n__d(z0)) → d(z0) 0.00/0.58
activate(z0) → z0
S tuples:
H(z0) → c4(C(n__d(z0))) 0.00/0.58
C(z0) → c3(ACTIVATE(z0)) 0.00/0.58
ACTIVATE(n__f(z0)) → c6 0.00/0.58
ACTIVATE(n__d(z0)) → c7
K tuples:none
H(z0) → c4(C(n__d(z0))) 0.00/0.58
C(z0) → c3(ACTIVATE(z0)) 0.00/0.58
ACTIVATE(n__f(z0)) → c6 0.00/0.58
ACTIVATE(n__d(z0)) → c7
f, c, h, d, activate
H, C, ACTIVATE
c4, c3, c6, c7
ACTIVATE(n__f(z0)) → c6 0.00/0.58
ACTIVATE(n__d(z0)) → c7 0.00/0.58
H(z0) → c4(C(n__d(z0))) 0.00/0.58
C(z0) → c3(ACTIVATE(z0))
Tuples:none
f(f(z0)) → c(n__f(g(n__f(z0)))) 0.00/0.58
f(z0) → n__f(z0) 0.00/0.58
c(z0) → d(activate(z0)) 0.00/0.58
h(z0) → c(n__d(z0)) 0.00/0.58
d(z0) → n__d(z0) 0.00/0.58
activate(n__f(z0)) → f(z0) 0.00/0.58
activate(n__d(z0)) → d(z0) 0.00/0.58
activate(z0) → z0
f, c, h, d, activate