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 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.54
↳6 BOUNDS(O(1), O(1))0.00/0.54
f(f(x, y, z), u, f(x, y, v)) → f(x, y, f(z, u, v)) 0.00/0.54
f(x, y, y) → y 0.00/0.54
f(x, y, g(y)) → x 0.00/0.54
f(x, x, y) → x 0.00/0.54
f(g(x), x, y) → y
Tuples:
f(f(z0, z1, z2), z3, f(z0, z1, z4)) → f(z0, z1, f(z2, z3, z4)) 0.00/0.54
f(z0, z1, z1) → z1 0.00/0.54
f(z0, z1, g(z1)) → z0 0.00/0.54
f(z0, z0, z1) → z0 0.00/0.54
f(g(z0), z0, z1) → z1
S tuples:
F(f(z0, z1, z2), z3, f(z0, z1, z4)) → c(F(z0, z1, f(z2, z3, z4)), F(z2, z3, z4))
K tuples:none
F(f(z0, z1, z2), z3, f(z0, z1, z4)) → c(F(z0, z1, f(z2, z3, z4)), F(z2, z3, z4))
f
F
c
F(f(z0, z1, z2), z3, f(z0, z1, z4)) → c(F(z0, z1, f(z2, z3, z4)), F(z2, z3, z4))
Tuples:none
f(f(z0, z1, z2), z3, f(z0, z1, z4)) → f(z0, z1, f(z2, z3, z4)) 0.00/0.54
f(z0, z1, z1) → z1 0.00/0.54
f(z0, z1, g(z1)) → z0 0.00/0.54
f(z0, z0, z1) → z0 0.00/0.54
f(g(z0), z0, z1) → z1
f