0 QTRS
↳1 AAECC Innermost (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
↳20 PisEmptyProof (⇔)
↳21 TRUE
↳22 QDP
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
-1(s(x), s(y)) → -1(x, y)
+1(s(x), y) → +1(x, y)
*1(x, s(y)) → +1(x, *(x, y))
*1(x, s(y)) → *1(x, y)
F(s(x), y) → F(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
F(s(x), y) → -1(*(s(x), s(y)), s(*(s(x), y)))
F(s(x), y) → *1(s(x), s(y))
F(s(x), y) → *1(s(x), y)
F(s(x), y) → *1(y, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
+1(s(x), y) → +1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+1(s(x), y) → +1(x, y)
s1 > +^12
+^12: [1,2]
s1: multiset
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
*1(x, s(y)) → *1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*1(x, s(y)) → *1(x, y)
s1 > *^12
*^12: [2,1]
s1: multiset
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
-1(s(x), s(y)) → -1(x, y)
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
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)
trivial
-^11: [1]
s1: multiset
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)
F(s(x), y) → F(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x, 0) → x
-(s(x), s(y)) → -(x, y)
+(0, y) → y
+(s(x), y) → s(+(x, y))
*(x, 0) → 0
*(x, s(y)) → +(x, *(x, y))
f(s(x), y) → f(-(*(s(x), s(y)), s(*(s(x), y))), *(y, y))
-(x0, 0)
-(s(x0), s(x1))
+(0, x0)
+(s(x0), x1)
*(x0, 0)
*(x0, s(x1))
f(s(x0), x1)