YES
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔, 0 ms)
↳7 QDP
↳8 MNOCProof (⇔, 0 ms)
↳9 QDP
↳10 MRRProof (⇔, 0 ms)
↳11 QDP
↳12 PisEmptyProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 MNOCProof (⇔, 0 ms)
↳18 QDP
↳19 MRRProof (⇔, 0 ms)
↳20 QDP
↳21 PisEmptyProof (⇔, 0 ms)
↳22 YES
↳23 QDP
↳24 QDPOrderProof (⇔, 22 ms)
↳25 QDP
↳26 PisEmptyProof (⇔, 0 ms)
↳27 YES
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
GEQ2 > s1 > ns1 > 0 > activate1 > n0
n__0=1
0=1
activate_1=1
n__s_1=1
s_1=1
GEQ_2=0
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
MINUS2 > s1 > ns1 > 0 > activate1 > n0
n__0=1
0=1
activate_1=1
n__s_1=1
s_1=1
MINUS_2=0
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)))
s > minus > 0 > n0
s=1
0=1
minus=1
n__0=1
minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
0 → n__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