-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))
↳ QTRS
↳ DependencyPairsProof
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))
-1(s(x), s(y)) → -1(x, y)
F(x, s(y)) → P(-(s(y), x))
F(x, s(y)) → P(-(x, s(y)))
F(x, s(y)) → F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) → -1(y, s(x))
F(s(x), y) → -1(s(x), y)
F(x, s(y)) → -1(s(y), x)
F(x, s(y)) → -1(x, s(y))
F(s(x), y) → F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x), y) → P(-(y, s(x)))
F(s(x), y) → P(-(s(x), y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
-1(s(x), s(y)) → -1(x, y)
F(x, s(y)) → P(-(s(y), x))
F(x, s(y)) → P(-(x, s(y)))
F(x, s(y)) → F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) → -1(y, s(x))
F(s(x), y) → -1(s(x), y)
F(x, s(y)) → -1(s(y), x)
F(x, s(y)) → -1(x, s(y))
F(s(x), y) → F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x), y) → P(-(y, s(x)))
F(s(x), y) → P(-(s(x), y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
-1(s(x), s(y)) → -1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
-1(s(x), s(y)) → -1(x, y)
The value of delta used in the strict ordering is 3.
POL(-1(x1, x2)) = (3)x_2
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
F(x, s(y)) → F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) → F(p(-(s(x), y)), p(-(y, s(x))))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
p(s(x)) → x
f(s(x), y) → f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) → f(p(-(x, s(y))), p(-(s(y), x)))