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 PisEmptyProof (⇔)
↳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) → ifMinus(le(s(X), Y), s(X), Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), 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) → ifMinus(le(s(X), Y), s(X), Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
LE(s(X), s(Y)) → LE(X, Y)
MINUS(s(X), Y) → IFMINUS(le(s(X), Y), s(X), Y)
MINUS(s(X), Y) → LE(s(X), Y)
IFMINUS(false, s(X), Y) → MINUS(X, Y)
QUOT(s(X), s(Y)) → QUOT(minus(X, Y), s(Y))
QUOT(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) → ifMinus(le(s(X), Y), s(X), Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(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) → ifMinus(le(s(X), Y), s(X), Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(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)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(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) → IFMINUS(le(s(X), Y), s(X), Y)
IFMINUS(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) → ifMinus(le(s(X), Y), s(X), Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
MINUS(s(X), Y) → IFMINUS(le(s(X), Y), s(X), Y)
IFMINUS(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)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
MINUS(s(X), Y) → IFMINUS(le(s(X), Y), s(X), Y)
IFMINUS(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:
QUOT(s(X), s(Y)) → QUOT(minus(X, Y), 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) → ifMinus(le(s(X), Y), s(X), Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
quot(0, s(Y)) → 0
quot(s(X), s(Y)) → s(quot(minus(X, Y), s(Y)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
minus(0, x0)
minus(s(x0), x1)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
QUOT(s(X), s(Y)) → QUOT(minus(X, Y), s(Y))
minus(0, Y) → 0
minus(s(X), Y) → ifMinus(le(s(X), Y), s(X), Y)
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(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)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
quot(0, s(x0))
quot(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
QUOT(s(X), s(Y)) → QUOT(minus(X, Y), s(Y))
minus(0, Y) → 0
minus(s(X), Y) → ifMinus(le(s(X), Y), s(X), Y)
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(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)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(X), s(Y)) → QUOT(minus(X, Y), s(Y))
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(false) = 0
POL(ifMinus(x1, x2, x3)) = x2
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
ifMinus(false, s(X), Y) → s(minus(X, Y))
ifMinus(true, s(X), Y) → 0
minus(s(X), Y) → ifMinus(le(s(X), Y), s(X), Y)
minus(0, Y) → 0
minus(0, Y) → 0
minus(s(X), Y) → ifMinus(le(s(X), Y), s(X), Y)
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
ifMinus(true, s(X), Y) → 0
ifMinus(false, s(X), Y) → s(minus(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)
ifMinus(true, s(x0), x1)
ifMinus(false, s(x0), x1)