0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 PisEmptyProof (⇔)
↳23 TRUE
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 PisEmptyProof (⇔)
↳28 TRUE
↳29 QDP
↳30 QDPOrderProof (⇔)
↳31 QDP
↳32 QDPOrderProof (⇔)
↳33 QDP
↳34 PisEmptyProof (⇔)
↳35 TRUE
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 QDPOrderProof (⇔)
↳40 QDP
↳41 QDPOrderProof (⇔)
↳42 QDP
↳43 DependencyGraphProof (⇔)
↳44 TRUE
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
ACTIVE(minus(0, Y)) → MARK(0)
ACTIVE(minus(s(X), s(Y))) → MARK(minus(X, Y))
ACTIVE(minus(s(X), s(Y))) → MINUS(X, Y)
ACTIVE(geq(X, 0)) → MARK(true)
ACTIVE(geq(0, s(Y))) → MARK(false)
ACTIVE(geq(s(X), s(Y))) → MARK(geq(X, Y))
ACTIVE(geq(s(X), s(Y))) → GEQ(X, Y)
ACTIVE(div(0, s(Y))) → MARK(0)
ACTIVE(div(s(X), s(Y))) → MARK(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
ACTIVE(div(s(X), s(Y))) → IF(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
ACTIVE(div(s(X), s(Y))) → GEQ(X, Y)
ACTIVE(div(s(X), s(Y))) → S(div(minus(X, Y), s(Y)))
ACTIVE(div(s(X), s(Y))) → DIV(minus(X, Y), s(Y))
ACTIVE(div(s(X), s(Y))) → MINUS(X, Y)
ACTIVE(if(true, X, Y)) → MARK(X)
ACTIVE(if(false, X, Y)) → MARK(Y)
MARK(minus(X1, X2)) → ACTIVE(minus(X1, X2))
MARK(0) → ACTIVE(0)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(X)
MARK(geq(X1, X2)) → ACTIVE(geq(X1, X2))
MARK(true) → ACTIVE(true)
MARK(false) → ACTIVE(false)
MARK(div(X1, X2)) → ACTIVE(div(mark(X1), X2))
MARK(div(X1, X2)) → DIV(mark(X1), X2)
MARK(div(X1, X2)) → MARK(X1)
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), X2, X3))
MARK(if(X1, X2, X3)) → IF(mark(X1), X2, X3)
MARK(if(X1, X2, X3)) → MARK(X1)
MINUS(mark(X1), X2) → MINUS(X1, X2)
MINUS(X1, mark(X2)) → MINUS(X1, X2)
MINUS(active(X1), X2) → MINUS(X1, X2)
MINUS(X1, active(X2)) → MINUS(X1, X2)
S(mark(X)) → S(X)
S(active(X)) → S(X)
GEQ(mark(X1), X2) → GEQ(X1, X2)
GEQ(X1, mark(X2)) → GEQ(X1, X2)
GEQ(active(X1), X2) → GEQ(X1, X2)
GEQ(X1, active(X2)) → GEQ(X1, X2)
DIV(mark(X1), X2) → DIV(X1, X2)
DIV(X1, mark(X2)) → DIV(X1, X2)
DIV(active(X1), X2) → DIV(X1, X2)
DIV(X1, active(X2)) → DIV(X1, X2)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
IF(active(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, active(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, active(X3)) → IF(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
IF(active(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, active(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, active(X3)) → IF(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
IF(active(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, active(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, active(X3)) → IF(X1, X2, X3)
div > minus > [IF3, mark1, active1, if2] > 0
div > minus > [IF3, mark1, active1, if2] > s
div > [geq, true, false] > [IF3, mark1, active1, if2] > 0
div > [geq, true, false] > [IF3, mark1, active1, if2] > s
active1: [1]
minus: []
if2: [1,2]
div: []
true: []
mark1: [1]
false: []
s: []
geq: []
IF3: [3,2,1]
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
DIV(X1, mark(X2)) → DIV(X1, X2)
DIV(mark(X1), X2) → DIV(X1, X2)
DIV(active(X1), X2) → DIV(X1, X2)
DIV(X1, active(X2)) → DIV(X1, X2)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(mark(X1), X2) → DIV(X1, X2)
DIV(active(X1), X2) → DIV(X1, X2)
minus > 0 > [mark1, active1] > div1 > if2
s > 0 > [mark1, active1] > div1 > if2
s > [geq, true, false] > [mark1, active1] > div1 > if2
active1: [1]
minus: []
if2: [2,1]
true: []
div1: [1]
mark1: [1]
false: []
s: []
geq: []
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
DIV(X1, mark(X2)) → DIV(X1, X2)
DIV(X1, active(X2)) → DIV(X1, X2)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DIV(X1, mark(X2)) → DIV(X1, X2)
DIV(X1, active(X2)) → DIV(X1, X2)
[mark1, active1, geq, false] > DIV2 > [minus, 0, s, if2]
[mark1, active1, geq, false] > true > [minus, 0, s, if2]
[mark1, active1, geq, false] > div > [minus, 0, s, if2]
active1: [1]
minus: []
if2: [2,1]
div: []
DIV2: [2,1]
true: []
mark1: [1]
false: []
s: []
geq: []
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
GEQ(X1, mark(X2)) → GEQ(X1, X2)
GEQ(mark(X1), X2) → GEQ(X1, X2)
GEQ(active(X1), X2) → GEQ(X1, X2)
GEQ(X1, active(X2)) → GEQ(X1, X2)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GEQ(X1, mark(X2)) → GEQ(X1, X2)
GEQ(X1, active(X2)) → GEQ(X1, X2)
[mark1, active1] > [minus, s] > 0 > [false, if2]
[mark1, active1] > [minus, s] > [geq, true] > [false, if2]
[mark1, active1] > [minus, s] > div1 > [false, if2]
active1: [1]
minus: []
if2: [1,2]
true: []
div1: [1]
mark1: [1]
false: []
s: []
geq: []
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
GEQ(mark(X1), X2) → GEQ(X1, X2)
GEQ(active(X1), X2) → GEQ(X1, X2)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GEQ(mark(X1), X2) → GEQ(X1, X2)
GEQ(active(X1), X2) → GEQ(X1, X2)
[mark1, active1] > GEQ2
[mark1, active1] > div1 > minus > [0, s, false]
[mark1, active1] > div1 > geq > [0, s, false]
[mark1, active1] > div1 > geq > true
[mark1, active1] > div1 > if2
active1: [1]
minus: []
if2: [1,2]
true: []
div1: [1]
mark1: [1]
false: []
s: []
geq: []
0: []
GEQ2: [1,2]
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
S(active(X)) → S(X)
S(mark(X)) → S(X)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(active(X)) → S(X)
S(mark(X)) → S(X)
[S1, active1, mark1, minus, geq, true, false] > div > s > 0
[S1, active1, mark1, minus, geq, true, false] > div > s > if2
active1: [1]
minus: []
if2: [1,2]
div: []
true: []
mark1: [1]
false: []
s: []
geq: []
0: []
S1: [1]
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
MINUS(X1, mark(X2)) → MINUS(X1, X2)
MINUS(mark(X1), X2) → MINUS(X1, X2)
MINUS(active(X1), X2) → MINUS(X1, X2)
MINUS(X1, active(X2)) → MINUS(X1, X2)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(X1, mark(X2)) → MINUS(X1, X2)
MINUS(X1, active(X2)) → MINUS(X1, X2)
[mark1, active1] > [minus, s] > 0 > [false, if2]
[mark1, active1] > [minus, s] > [geq, true] > [false, if2]
[mark1, active1] > [minus, s] > div1 > [false, if2]
active1: [1]
minus: []
if2: [1,2]
true: []
div1: [1]
mark1: [1]
false: []
s: []
geq: []
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
MINUS(mark(X1), X2) → MINUS(X1, X2)
MINUS(active(X1), X2) → MINUS(X1, X2)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(mark(X1), X2) → MINUS(X1, X2)
MINUS(active(X1), X2) → MINUS(X1, X2)
[mark1, active1] > MINUS2
[mark1, active1] > div1 > minus > [0, s, false]
[mark1, active1] > div1 > geq > [0, s, false]
[mark1, active1] > div1 > geq > true
[mark1, active1] > div1 > if2
active1: [1]
minus: []
if2: [1,2]
true: []
div1: [1]
MINUS2: [1,2]
mark1: [1]
false: []
s: []
geq: []
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
ACTIVE(minus(s(X), s(Y))) → MARK(minus(X, Y))
MARK(minus(X1, X2)) → ACTIVE(minus(X1, X2))
ACTIVE(geq(s(X), s(Y))) → MARK(geq(X, Y))
MARK(s(X)) → ACTIVE(s(mark(X)))
ACTIVE(div(s(X), s(Y))) → MARK(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
MARK(s(X)) → MARK(X)
MARK(geq(X1, X2)) → ACTIVE(geq(X1, X2))
ACTIVE(if(true, X, Y)) → MARK(X)
MARK(div(X1, X2)) → ACTIVE(div(mark(X1), X2))
ACTIVE(if(false, X, Y)) → MARK(Y)
MARK(div(X1, X2)) → MARK(X1)
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), X2, X3))
MARK(if(X1, X2, X3)) → MARK(X1)
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(geq(s(X), s(Y))) → MARK(geq(X, Y))
ACTIVE(div(s(X), s(Y))) → MARK(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
MARK(s(X)) → MARK(X)
ACTIVE(if(true, X, Y)) → MARK(X)
ACTIVE(if(false, X, Y)) → MARK(Y)
MARK(div(X1, X2)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X1)
div1 > [minus, s1, 0]
div1 > [geq1, false] > true
div1 > if3
if3: [1,3,2]
minus: []
true: []
div1: [1]
geq1: [1]
false: []
s1: [1]
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
ACTIVE(minus(s(X), s(Y))) → MARK(minus(X, Y))
MARK(minus(X1, X2)) → ACTIVE(minus(X1, X2))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(geq(X1, X2)) → ACTIVE(geq(X1, X2))
MARK(div(X1, X2)) → ACTIVE(div(mark(X1), X2))
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), X2, X3))
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(s(X)) → ACTIVE(s(mark(X)))
[minus, MARK, mark, geq, div, if, 0, false] > s
[minus, MARK, mark, geq, div, if, 0, false] > true
MARK: []
minus: []
if: []
div: []
true: []
mark: []
false: []
s: []
geq: []
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
ACTIVE(minus(s(X), s(Y))) → MARK(minus(X, Y))
MARK(minus(X1, X2)) → ACTIVE(minus(X1, X2))
MARK(geq(X1, X2)) → ACTIVE(geq(X1, X2))
MARK(div(X1, X2)) → ACTIVE(div(mark(X1), X2))
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), X2, X3))
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(minus(s(X), s(Y))) → MARK(minus(X, Y))
div1 > [s1, if3] > minus1 > [0, true, false]
if3: [1,2,3]
minus1: [1]
true: []
div1: [1]
false: []
s1: [1]
0: []
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
MARK(minus(X1, X2)) → ACTIVE(minus(X1, X2))
MARK(geq(X1, X2)) → ACTIVE(geq(X1, X2))
MARK(div(X1, X2)) → ACTIVE(div(mark(X1), X2))
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), X2, X3))
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)