0 CpxTRS
↳1 NestedDefinedSymbolProof (BOTH BOUNDS(ID, ID), 13 ms)
↳2 CpxTRS
↳3 RcToIrcProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTRS
↳5 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳10 BOUNDS(1, 1)
f(f(x, y, z), u, f(x, y, v)) → f(x, y, f(z, u, v))
f(x, y, y) → y
f(x, y, g(y)) → x
f(x, x, y) → x
f(g(x), x, y) → y
f(x, x, y) → x
f(x, y, y) → y
f(x, y, g(y)) → x
f(g(x), x, y) → y
As the TRS does not nest defined symbols, we have rc = irc.
f(x, x, y) → x
f(x, y, y) → y
f(x, y, g(y)) → x
f(g(x), x, y) → y
Tuples:
f(z0, z0, z1) → z0
f(z0, z1, z1) → z1
f(z0, z1, g(z1)) → z0
f(g(z0), z0, z1) → z1
S tuples:
F(z0, z0, z1) → c
F(z0, z1, z1) → c1
F(z0, z1, g(z1)) → c2
F(g(z0), z0, z1) → c3
K tuples:none
F(z0, z0, z1) → c
F(z0, z1, z1) → c1
F(z0, z1, g(z1)) → c2
F(g(z0), z0, z1) → c3
f
F
c, c1, c2, c3
F(z0, z1, z1) → c1
F(z0, z0, z1) → c
F(z0, z1, g(z1)) → c2
F(g(z0), z0, z1) → c3
Tuples:none
f(z0, z0, z1) → z0
f(z0, z1, z1) → z1
f(z0, z1, g(z1)) → z0
f(g(z0), z0, z1) → z1
f