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