0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPOrderProof (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 TRUE
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
MINUS(s(x), y) → IF_MINUS(le(s(x), y), s(x), y)
MINUS(s(x), y) → LE(s(x), y)
IF_MINUS(false, s(x), y) → MINUS(x, y)
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
MOD(s(x), s(y)) → LE(y, x)
IF_MOD(true, s(x), s(y)) → MOD(minus(x, y), s(y))
IF_MOD(true, s(x), s(y)) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
MINUS(s(x), y) → IF_MINUS(le(s(x), y), s(x), y)
IF_MINUS(false, s(x), y) → MINUS(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
MINUS(s(x), y) → IF_MINUS(le(s(x), y), s(x), y)
IF_MINUS(false, s(x), y) → MINUS(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, y) → true
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
MINUS(s(x), y) → IF_MINUS(le(s(x), y), s(x), y)
IF_MINUS(false, s(x), y) → MINUS(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
le(0, y) → true
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
IF_MOD(true, s(x), s(y)) → MOD(minus(x, y), s(y))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
mod(0, y) → 0
mod(s(x), 0) → 0
mod(s(x), s(y)) → if_mod(le(y, x), s(x), s(y))
if_mod(true, s(x), s(y)) → mod(minus(x, y), s(y))
if_mod(false, s(x), s(y)) → s(x)
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
IF_MOD(true, s(x), s(y)) → MOD(minus(x, y), s(y))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
mod(0, x0)
mod(s(x0), 0)
mod(s(x0), s(x1))
if_mod(true, s(x0), s(x1))
if_mod(false, s(x0), s(x1))
IF_MOD(true, s(x), s(y)) → MOD(minus(x, y), s(y))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_MOD(true, s(x), s(y)) → MOD(minus(x, y), s(y))
POL(0) = 0
POL(IF_MOD(x1, x2, x3)) = x2 + x3
POL(MOD(x1, x2)) = x1 + x2
POL(false) = 0
POL(if_minus(x1, x2, x3)) = x2
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
MOD(s(x), s(y)) → IF_MOD(le(y, x), s(x), s(y))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
minus(0, y) → 0
minus(s(x), y) → if_minus(le(s(x), y), s(x), y)
if_minus(true, s(x), y) → 0
if_minus(false, s(x), y) → s(minus(x, y))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
if_minus(true, s(x0), x1)
if_minus(false, s(x0), x1)