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