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