YES
0 QTRS
↳1 DependencyPairsProof (⇔, 11 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 QDPSizeChangeProof (⇔, 0 ms)
↳9 YES
↳10 QDP
↳11 UsableRulesProof (⇔, 0 ms)
↳12 QDP
↳13 MNOCProof (⇔, 0 ms)
↳14 QDP
↳15 DependencyGraphProof (⇔, 0 ms)
↳16 AND
↳17 QDP
↳18 UsableRulesProof (⇔, 0 ms)
↳19 QDP
↳20 QReductionProof (⇔, 0 ms)
↳21 QDP
↳22 QDPOrderProof (⇔, 0 ms)
↳23 QDP
↳24 PisEmptyProof (⇔, 0 ms)
↳25 YES
↳26 QDP
↳27 QDPSizeChangeProof (⇔, 0 ms)
↳28 YES
↳29 QDP
↳30 UsableRulesProof (⇔, 0 ms)
↳31 QDP
↳32 MNOCProof (⇔, 0 ms)
↳33 QDP
↳34 UsableRulesReductionPairsProof (⇔, 0 ms)
↳35 QDP
↳36 TransformationProof (⇔, 0 ms)
↳37 QDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 QDP
↳40 QDPOrderProof (⇔, 0 ms)
↳41 QDP
↳42 PisEmptyProof (⇔, 0 ms)
↳43 YES
↳44 QDP
↳45 QDPOrderProof (⇔, 0 ms)
↳46 QDP
↳47 QDPOrderProof (⇔, 0 ms)
↳48 QDP
↳49 PisEmptyProof (⇔, 0 ms)
↳50 YES
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
MINUS(s(x), s(y)) → P(s(x))
MINUS(s(x), s(y)) → P(s(y))
MINUS(x, plus(y, z)) → MINUS(minus(x, y), z)
MINUS(x, plus(y, z)) → MINUS(x, y)
P(s(s(x))) → P(s(x))
DIV(s(x), s(y)) → DIV(minus(x, y), s(y))
DIV(s(x), s(y)) → MINUS(x, y)
DIV(plus(x, y), z) → PLUS(div(x, z), div(y, z))
DIV(plus(x, y), z) → DIV(x, z)
DIV(plus(x, y), z) → DIV(y, z)
PLUS(s(x), y) → PLUS(y, minus(s(x), s(0)))
PLUS(s(x), y) → MINUS(s(x), s(0))
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
P(s(s(x))) → P(s(x))
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
P(s(s(x))) → P(s(x))
From the DPs we obtained the following set of size-change graphs:
MINUS(x, plus(y, z)) → MINUS(minus(x, y), z)
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
MINUS(x, plus(y, z)) → MINUS(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
MINUS(x, plus(y, z)) → MINUS(minus(x, y), z)
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
MINUS(x, plus(y, z)) → MINUS(x, y)
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
MINUS(x, plus(y, z)) → MINUS(minus(x, y), z)
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
MINUS(x, plus(y, z)) → MINUS(x, y)
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x0)))
minus(x0, 0)
minus(0, x0)
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x0)))
minus(x0, 0)
minus(0, x0)
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
p(s(s(x0)))
minus(x0, 0)
minus(0, x0)
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
p(s(s(x0)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(s(x), s(y)) → MINUS(p(s(x)), p(s(y)))
POL( MINUS(x1, x2) ) = x1 + 2x2 |
POL( p(x1) ) = max{0, x1 - 2} |
POL( s(x1) ) = 2x1 + 2 |
p(s(s(x))) → s(p(s(x)))
p(s(s(x))) → s(p(s(x)))
p(s(s(x0)))
MINUS(x, plus(y, z)) → MINUS(x, y)
MINUS(x, plus(y, z)) → MINUS(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x0)))
minus(x0, 0)
minus(0, x0)
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
PLUS(s(x), y) → PLUS(y, minus(s(x), s(0)))
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
PLUS(s(x), y) → PLUS(y, minus(s(x), s(0)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, 0) → x
minus(0, y) → 0
p(s(s(x))) → s(p(s(x)))
PLUS(s(x), y) → PLUS(y, minus(s(x), s(0)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, 0) → x
minus(0, y) → 0
p(s(s(x))) → s(p(s(x)))
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
p(s(s(x0)))
Used ordering: POLO with Polynomial interpretation [POLO]:
minus(x, plus(y, z)) → minus(minus(x, y), z)
POL(0) = 0
POL(PLUS(x1, x2)) = 2·x1 + 2·x2
POL(minus(x1, x2)) = x1 + x2
POL(p(x1)) = x1
POL(plus(x1, x2)) = 2 + x1 + x2
POL(s(x1)) = x1
PLUS(s(x), y) → PLUS(y, minus(s(x), s(0)))
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
p(s(s(x0)))
PLUS(s(x), y) → PLUS(y, minus(p(s(x)), p(s(0)))) → PLUS(s(x), y) → PLUS(y, minus(p(s(x)), p(s(0))))
PLUS(s(x), y) → PLUS(y, minus(p(s(x)), p(s(0))))
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
p(s(s(x0)))
PLUS(s(x), y) → PLUS(y, minus(p(s(x)), p(s(0))))
p(s(s(x))) → s(p(s(x)))
minus(0, y) → 0
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
p(s(s(x0)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(x), y) → PLUS(y, minus(p(s(x)), p(s(0))))
trivial
s=3
0=1
minus=2
PLUS_2=1
minus(0, y) → 0
p(s(s(x))) → s(p(s(x)))
minus(0, y) → 0
minus(x0, plus(x1, x2))
minus(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
p(s(s(x0)))
DIV(plus(x, y), z) → DIV(x, z)
DIV(s(x), s(y)) → DIV(minus(x, y), s(y))
DIV(plus(x, y), z) → DIV(y, z)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(plus(x, y), z) → DIV(x, z)
DIV(plus(x, y), z) → DIV(y, z)
trivial
0=2
p=1
plus_2=1
minus(x, 0) → x
minus(0, y) → 0
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
DIV(s(x), s(y)) → DIV(minus(x, y), s(y))
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(s(x), s(y)) → DIV(minus(x, y), s(y))
trivial
s_1=1
0=1
minus(x, 0) → x
minus(0, y) → 0
minus(x, plus(y, z)) → minus(minus(x, y), z)
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
p(s(s(x))) → s(p(s(x)))
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) → minus(minus(x, y), z)
p(s(s(x))) → s(p(s(x)))
p(0) → s(s(0))
div(s(x), s(y)) → s(div(minus(x, y), s(y)))
div(plus(x, y), z) → plus(div(x, z), div(y, z))
plus(0, y) → y
plus(s(x), y) → s(plus(y, minus(s(x), s(0))))