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