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