0 QTRS
↳1 AAECC Innermost (⇔)
↳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 Instantiation (⇔)
↳27 QDP
↳28 NonInfProof (⇔)
↳29 QDP
↳30 DependencyGraphProof (⇔)
↳31 TRUE
↳32 QDP
↳33 UsableRulesProof (⇔)
↳34 QDP
↳35 QReductionProof (⇔)
↳36 QDP
↳37 QDPSizeChangeProof (⇔)
↳38 TRUE
↳39 QDP
↳40 UsableRulesProof (⇔)
↳41 QDP
↳42 QReductionProof (⇔)
↳43 QDP
↳44 Rewriting (⇔)
↳45 QDP
↳46 UsableRulesProof (⇔)
↳47 QDP
↳48 QReductionProof (⇔)
↳49 QDP
↳50 Rewriting (⇔)
↳51 QDP
↳52 Narrowing (⇔)
↳53 QDP
↳54 DependencyGraphProof (⇔)
↳55 QDP
↳56 Instantiation (⇔)
↳57 QDP
↳58 Instantiation (⇔)
↳59 QDP
↳60 ForwardInstantiation (⇔)
↳61 QDP
↳62 Narrowing (⇔)
↳63 QDP
↳64 DependencyGraphProof (⇔)
↳65 QDP
↳66 Narrowing (⇔)
↳67 QDP
↳68 DependencyGraphProof (⇔)
↳69 QDP
↳70 Instantiation (⇔)
↳71 QDP
↳72 QDPOrderProof (⇔)
↳73 QDP
↳74 DependencyGraphProof (⇔)
↳75 TRUE
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
a → c
a → d
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
DIV(x, y) → DIV2(x, y, 0)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
DIV2(x, y, i) → LE(y, 0)
DIV2(x, y, i) → LE(y, x)
DIV2(x, y, i) → PLUS(i, 0)
DIV2(x, y, i) → INC(i)
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
IF2(true, x, y, i, j) → MINUS(x, y)
INC(s(i)) → INC(i)
LE(s(x), s(y)) → LE(x, y)
MINUS(s(x), s(y)) → MINUS(x, y)
PLUS(x, y) → PLUSITER(x, y, 0)
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
PLUSITER(x, y, z) → LE(x, z)
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
MINUS(s(x), s(y)) → MINUS(x, y)
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
MINUS(s(x), s(y)) → MINUS(x, y)
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
LE(s(x), s(y)) → LE(x, y)
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
PLUSITER(z0, s(z1), s(z2)) → IFPLUS(le(z0, s(z2)), z0, s(z1), s(z2))
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
PLUSITER(z0, s(z1), s(z2)) → IFPLUS(le(z0, s(z2)), z0, s(z1), s(z2))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
(1) (PLUSITER(x3, s(x4), s(x5))=PLUSITER(x6, x7, x8) ⇒ PLUSITER(x6, x7, x8)≥IFPLUS(le(x6, x8), x6, x7, x8))
(2) (PLUSITER(x3, s(x4), s(x5))≥IFPLUS(le(x3, s(x5)), x3, s(x4), s(x5)))
(3) (IFPLUS(le(x9, x11), x9, x10, x11)=IFPLUS(false, x12, x13, x14) ⇒ IFPLUS(false, x12, x13, x14)≥PLUSITER(x12, s(x13), s(x14)))
(4) (le(x9, x11)=false ⇒ IFPLUS(false, x9, x10, x11)≥PLUSITER(x9, s(x10), s(x11)))
(5) (false=false ⇒ IFPLUS(false, s(x18), x10, 0)≥PLUSITER(s(x18), s(x10), s(0)))
(6) (le(x21, x20)=false∧(∀x22:le(x21, x20)=false ⇒ IFPLUS(false, x21, x22, x20)≥PLUSITER(x21, s(x22), s(x20))) ⇒ IFPLUS(false, s(x21), x10, s(x20))≥PLUSITER(s(x21), s(x10), s(s(x20))))
(7) (IFPLUS(false, s(x18), x10, 0)≥PLUSITER(s(x18), s(x10), s(0)))
(8) (IFPLUS(false, x21, x10, x20)≥PLUSITER(x21, s(x10), s(x20)) ⇒ IFPLUS(false, s(x21), x10, s(x20))≥PLUSITER(s(x21), s(x10), s(s(x20))))
POL(0) = 0
POL(IFPLUS(x1, x2, x3, x4)) = -1 - x1 + x2 - x4
POL(PLUSITER(x1, x2, x3)) = -1 + x1 - x3
POL(c) = -2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in Pbound:
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
The following rules are usable:
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
le(x, y) → le(s(x), s(y))
false → le(s(x), 0)
true → le(0, y)
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
INC(s(i)) → INC(i)
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
INC(s(i)) → INC(i)
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
INC(s(i)) → INC(i)
From the DPs we obtained the following set of size-change graphs:
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
div(x, y) → div2(x, y, 0)
div2(x, y, i) → if1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
if1(true, b, x, y, i, j) → divZeroError
if1(false, b, x, y, i, j) → if2(b, x, y, i, j)
if2(true, x, y, i, j) → div2(minus(x, y), y, j)
if2(false, x, y, i, j) → i
inc(0) → 0
inc(s(i)) → s(inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
a → c
a → d
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(x, y) → plusIter(x, y, 0)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
a
div(x0, x1)
div2(x0, x1, x2)
if1(true, x0, x1, x2, x3, x4)
if1(false, x0, x1, x2, x3, x4)
if2(true, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
a
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plus(i, 0), inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(x, y) → plusIter(x, y, 0)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plusIter(i, 0, 0), inc(i))
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plusIter(i, 0, 0), inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(x, y) → plusIter(x, y, 0)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plusIter(i, 0, 0), inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
plus(x0, x1)
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, plusIter(i, 0, 0), inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, ifPlus(le(i, 0), i, 0, 0), inc(i))
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(x, y, i) → IF1(le(y, 0), le(y, x), x, y, ifPlus(le(i, 0), i, 0, 0), inc(i))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
DIV2(y0, s(x0), y2) → IF1(false, le(s(x0), y0), y0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
DIV2(y0, 0, y2) → IF1(true, le(0, y0), y0, 0, ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(y0, s(x0), y2) → IF1(false, le(s(x0), y0), y0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
DIV2(y0, 0, y2) → IF1(true, le(0, y0), y0, 0, ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(y0, s(x0), y2) → IF1(false, le(s(x0), y0), y0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, b, x, y, i, j) → IF2(b, x, y, i, j)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF1(false, y_0, z0, s(z1), y_2, y_3) → IF2(y_0, z0, s(z1), y_2, y_3)
IF2(true, x, y, i, j) → DIV2(minus(x, y), y, j)
DIV2(y0, s(x0), y2) → IF1(false, le(s(x0), y0), y0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, y_0, z0, s(z1), y_2, y_3) → IF2(y_0, z0, s(z1), y_2, y_3)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF2(true, z1, s(z2), z3, z4) → DIV2(minus(z1, s(z2)), s(z2), z4)
DIV2(y0, s(x0), y2) → IF1(false, le(s(x0), y0), y0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, y_0, z0, s(z1), y_2, y_3) → IF2(y_0, z0, s(z1), y_2, y_3)
IF2(true, z1, s(z2), z3, z4) → DIV2(minus(z1, s(z2)), s(z2), z4)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF1(false, true, x1, s(x2), x3, x4) → IF2(true, x1, s(x2), x3, x4)
DIV2(y0, s(x0), y2) → IF1(false, le(s(x0), y0), y0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF2(true, z1, s(z2), z3, z4) → DIV2(minus(z1, s(z2)), s(z2), z4)
IF1(false, true, x1, s(x2), x3, x4) → IF2(true, x1, s(x2), x3, x4)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
DIV2(0, s(x0), y2) → IF1(false, false, 0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF2(true, z1, s(z2), z3, z4) → DIV2(minus(z1, s(z2)), s(z2), z4)
IF1(false, true, x1, s(x2), x3, x4) → IF2(true, x1, s(x2), x3, x4)
DIV2(0, s(x0), y2) → IF1(false, false, 0, s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, true, x1, s(x2), x3, x4) → IF2(true, x1, s(x2), x3, x4)
IF2(true, z1, s(z2), z3, z4) → DIV2(minus(z1, s(z2)), s(z2), z4)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF2(true, 0, s(y1), y2, y3) → DIV2(0, s(y1), y3)
IF2(true, s(x0), s(x1), y2, y3) → DIV2(minus(x0, x1), s(x1), y3)
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, true, x1, s(x2), x3, x4) → IF2(true, x1, s(x2), x3, x4)
IF2(true, 0, s(y1), y2, y3) → DIV2(0, s(y1), y3)
IF2(true, s(x0), s(x1), y2, y3) → DIV2(minus(x0, x1), s(x1), y3)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF1(false, true, x1, s(x2), x3, x4) → IF2(true, x1, s(x2), x3, x4)
IF2(true, s(x0), s(x1), y2, y3) → DIV2(minus(x0, x1), s(x1), y3)
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
IF1(false, true, s(z0), s(z1), y_2, y_3) → IF2(true, s(z0), s(z1), y_2, y_3)
IF2(true, s(x0), s(x1), y2, y3) → DIV2(minus(x0, x1), s(x1), y3)
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, true, s(z0), s(z1), y_2, y_3) → IF2(true, s(z0), s(z1), y_2, y_3)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF2(true, s(x0), s(x1), y2, y3) → DIV2(minus(x0, x1), s(x1), y3)
POL(0) = 0
POL(DIV2(x1, x2, x3)) = x1
POL(IF1(x1, x2, x3, x4, x5, x6)) = x3
POL(IF2(x1, x2, x3, x4, x5)) = x2
POL(false) = 0
POL(ifPlus(x1, x2, x3, x4)) = 0
POL(inc(x1)) = 0
POL(le(x1, x2)) = 0
POL(minus(x1, x2)) = x1
POL(plusIter(x1, x2, x3)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(0, y) → 0
DIV2(s(x1), s(x0), y2) → IF1(false, le(x0, x1), s(x1), s(x0), ifPlus(le(y2, 0), y2, 0, 0), inc(y2))
IF1(false, true, s(z0), s(z1), y_2, y_3) → IF2(true, s(z0), s(z1), y_2, y_3)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
inc(0) → 0
inc(s(i)) → s(inc(i))
ifPlus(true, x, y, z) → y
minus(x, 0) → x
minus(0, y) → 0
minus(s(x), s(y)) → minus(x, y)
inc(0)
inc(s(x0))
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
minus(x0, 0)
minus(0, x0)
minus(s(x0), s(x1))
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)