YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 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 NonMonReductionPairProof (⇔, 96 ms)
↳12 QDP
↳13 PisEmptyProof (⇔, 0 ms)
↳14 YES
↳15 QDP
↳16 NonMonReductionPairProof (⇔, 70 ms)
↳17 QDP
↳18 PisEmptyProof (⇔, 0 ms)
↳19 YES
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
MINUS(s(x), s(y)) → MINUS(x, y)
MINUS(x, s(y)) → P(minus(x, y))
MINUS(x, s(y)) → MINUS(x, y)
DIV(s(x), s(y)) → DIV(minus(s(x), s(y)), s(y))
DIV(s(x), s(y)) → MINUS(s(x), s(y))
LOG(s(s(x)), s(s(y))) → LOG(div(minus(x, y), s(s(y))), s(s(y)))
LOG(s(s(x)), s(s(y))) → DIV(minus(x, y), s(s(y)))
LOG(s(s(x)), s(s(y))) → MINUS(x, y)
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
MINUS(x, s(y)) → MINUS(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
MINUS(x, s(y)) → MINUS(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
DIV(s(x), s(y)) → DIV(minus(s(x), s(y)), s(y))
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
POL(0) = 0
POL(DIV(x1, x2)) = x1
POL(div(x1, x2)) = 0
POL(log(x1, x2)) = 0
POL(minus(x1, x2)) = max(0, x1 - x2)
POL(p(x1)) = max(0, -1 + x1)
POL(s(x1)) = 1 + x1
The remaining pairs can at least be oriented weakly.
DIV(s(x), s(y)) → DIV(minus(s(x), s(y)), s(y))
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
LOG(s(s(x)), s(s(y))) → LOG(div(minus(x, y), s(s(y))), s(s(y)))
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))
POL(0) = 0
POL(LOG(x1, x2)) = x1
POL(div(x1, x2)) = x1
POL(log(x1, x2)) = 1 + x1 + x2
POL(minus(x1, x2)) = max(0, x1 - x2)
POL(p(x1)) = max(0, -1 + x1)
POL(s(x1)) = 1 + x1
The remaining pairs can at least be oriented weakly.
LOG(s(s(x)), s(s(y))) → LOG(div(minus(x, y), s(s(y))), s(s(y)))
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
p(0) → 0
p(s(x)) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x, s(y)) → p(minus(x, y))
div(0, s(y)) → 0
div(s(x), s(y)) → s(div(minus(s(x), s(y)), s(y)))
log(s(0), s(s(y))) → 0
log(s(s(x)), s(s(y))) → s(log(div(minus(x, y), s(s(y))), s(s(y))))