0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 MNOCProof (⇔)
↳9 QDP
↳10 MRRProof (⇔)
↳11 QDP
↳12 PisEmptyProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 MNOCProof (⇔)
↳18 QDP
↳19 MRRProof (⇔)
↳20 QDP
↳21 PisEmptyProof (⇔)
↳22 TRUE
↳23 QDP
↳24 QDPOrderProof (⇔)
↳25 QDP
↳26 PisEmptyProof (⇔)
↳27 TRUE
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
MINUS(n__0, Y) → 01
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
MINUS(n__s(X), n__s(Y)) → ACTIVATE(X)
MINUS(n__s(X), n__s(Y)) → ACTIVATE(Y)
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
GEQ(n__s(X), n__s(Y)) → ACTIVATE(X)
GEQ(n__s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → IF(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
DIV(s(X), n__s(Y)) → GEQ(X, activate(Y))
DIV(s(X), n__s(Y)) → ACTIVATE(Y)
DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))
DIV(s(X), n__s(Y)) → MINUS(X, activate(Y))
IF(true, X, Y) → ACTIVATE(X)
IF(false, X, Y) → ACTIVATE(Y)
ACTIVATE(n__0) → 01
ACTIVATE(n__s(X)) → S(X)
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
s(X) → n__s(X)
0 → n__0
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
s(X) → n__s(X)
0 → n__0
activate(x0)
s(x0)
0
GEQ(n__s(X), n__s(Y)) → GEQ(activate(X), activate(Y))
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
s(X) → n__s(X)
0 → n__0
POL(0) = 1
POL(GEQ(x1, x2)) = x1 + x2
POL(activate(x1)) = 2 + x1
POL(n__0) = 0
POL(n__s(x1)) = 3 + x1
POL(s(x1)) = 4 + x1
activate(x0)
s(x0)
0
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
s(X) → n__s(X)
0 → n__0
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
s(X) → n__s(X)
0 → n__0
activate(x0)
s(x0)
0
MINUS(n__s(X), n__s(Y)) → MINUS(activate(X), activate(Y))
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
s(X) → n__s(X)
0 → n__0
POL(0) = 1
POL(MINUS(x1, x2)) = x1 + x2
POL(activate(x1)) = 2 + x1
POL(n__0) = 0
POL(n__s(x1)) = 3 + x1
POL(s(x1)) = 4 + x1
activate(x0)
s(x0)
0
DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(s(X), n__s(Y)) → DIV(minus(X, activate(Y)), n__s(activate(Y)))
POL(0) = 0
POL(DIV(x1, x2)) = x1
POL(activate(x1)) = 1 + x1
POL(minus(x1, x2)) = 0
POL(n__0) = 0
POL(n__s(x1)) = 1 + x1
POL(s(x1)) = 1 + x1
0 → n__0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
minus(n__0, Y) → 0
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(div(minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
activate(n__0) → 0
activate(n__s(X)) → s(X)
activate(X) → X