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, y) → f(y, x, s(x))
Tuples:
f(s(z0), z1, z1) → f(z1, z0, s(z0))
S tuples:
F(s(z0), z1, z1) → c(F(z1, z0, s(z0)))
K tuples:none
F(s(z0), z1, z1) → c(F(z1, z0, s(z0)))
f
F
c
Tuples:
f(s(z0), z1, z1) → f(z1, z0, s(z0))
S tuples:
F(s(z0), z1, z1) → c
K tuples:none
F(s(z0), z1, z1) → c
f
F
c
F(s(z0), z1, z1) → c
Tuples:none
f(s(z0), z1, z1) → f(z1, z0, s(z0))
f