YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.55 0.00/0.55 0.00/0.55
0.00/0.55 0.00/0.550 CpxTRS0.00/0.55
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳2 CdtProblem0.00/0.55
↳3 CdtUnreachableProof (⇔)0.00/0.55
↳4 CdtProblem0.00/0.55
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳6 CdtProblem0.00/0.55
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳8 CdtProblem0.00/0.55
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳10 BOUNDS(O(1), O(1))0.00/0.55
f(f(a)) → f(g(n__f(a))) 0.00/0.55
f(X) → n__f(X) 0.00/0.55
activate(n__f(X)) → f(X) 0.00/0.55
activate(X) → X
Tuples:
f(f(a)) → f(g(n__f(a))) 0.00/0.55
f(z0) → n__f(z0) 0.00/0.55
activate(n__f(z0)) → f(z0) 0.00/0.55
activate(z0) → z0
S tuples:
F(f(a)) → c(F(g(n__f(a)))) 0.00/0.55
ACTIVATE(n__f(z0)) → c2(F(z0))
K tuples:none
F(f(a)) → c(F(g(n__f(a)))) 0.00/0.55
ACTIVATE(n__f(z0)) → c2(F(z0))
f, activate
F, ACTIVATE
c, c2
F(f(a)) → c(F(g(n__f(a))))
Tuples:
f(f(a)) → f(g(n__f(a))) 0.00/0.55
f(z0) → n__f(z0) 0.00/0.55
activate(n__f(z0)) → f(z0) 0.00/0.55
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c2(F(z0))
K tuples:none
ACTIVATE(n__f(z0)) → c2(F(z0))
f, activate
ACTIVATE
c2
Tuples:
f(f(a)) → f(g(n__f(a))) 0.00/0.55
f(z0) → n__f(z0) 0.00/0.55
activate(n__f(z0)) → f(z0) 0.00/0.55
activate(z0) → z0
S tuples:
ACTIVATE(n__f(z0)) → c2
K tuples:none
ACTIVATE(n__f(z0)) → c2
f, activate
ACTIVATE
c2
ACTIVATE(n__f(z0)) → c2
Tuples:none
f(f(a)) → f(g(n__f(a))) 0.00/0.55
f(z0) → n__f(z0) 0.00/0.55
activate(n__f(z0)) → f(z0) 0.00/0.55
activate(z0) → z0
f, activate