implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
↳ QTRS
↳ DependencyPairsProof
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
IMPLIES(x, or(y, z)) → IMPLIES(x, z)
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
IMPLIES(x, or(y, z)) → IMPLIES(x, z)
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IMPLIES(not(x), or(y, z)) → IMPLIES(y, or(x, z))
IMPLIES(x, or(y, z)) → IMPLIES(x, z)
The value of delta used in the strict ordering is 1.
POL(IMPLIES(x1, x2)) = (4)x_1 + x_2
POL(not(x1)) = 4 + x_1
POL(or(x1, x2)) = 1 + (4)x_1 + x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
implies(not(x), y) → or(x, y)
implies(not(x), or(y, z)) → implies(y, or(x, z))
implies(x, or(y, z)) → or(y, implies(x, z))