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 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳4 CdtProblem0.00/0.55
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳6 CdtProblem0.00/0.55
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳8 BOUNDS(O(1), O(1))0.00/0.55
f(s(X), X) → f(X, a(X)) 0.00/0.55
f(X, c(X)) → f(s(X), X) 0.00/0.55
f(X, X) → c(X)
Tuples:
f(s(z0), z0) → f(z0, a(z0)) 0.00/0.55
f(z0, c(z0)) → f(s(z0), z0) 0.00/0.55
f(z0, z0) → c(z0)
S tuples:
F(s(z0), z0) → c1(F(z0, a(z0))) 0.00/0.55
F(z0, c(z0)) → c2(F(s(z0), z0))
K tuples:none
F(s(z0), z0) → c1(F(z0, a(z0))) 0.00/0.55
F(z0, c(z0)) → c2(F(s(z0), z0))
f
F
c1, c2
Tuples:
f(s(z0), z0) → f(z0, a(z0)) 0.00/0.55
f(z0, c(z0)) → f(s(z0), z0) 0.00/0.55
f(z0, z0) → c(z0)
S tuples:
F(z0, c(z0)) → c2(F(s(z0), z0)) 0.00/0.55
F(s(z0), z0) → c1
K tuples:none
F(z0, c(z0)) → c2(F(s(z0), z0)) 0.00/0.55
F(s(z0), z0) → c1
f
F
c2, c1
F(s(z0), z0) → c1 0.00/0.55
F(z0, c(z0)) → c2(F(s(z0), z0))
Tuples:none
f(s(z0), z0) → f(z0, a(z0)) 0.00/0.55
f(z0, c(z0)) → f(s(z0), z0) 0.00/0.55
f(z0, z0) → c(z0)
f