Termination w.r.t. Q proof of AProVE_07

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS

↳1 Overlay + Local Confluence (⇔, 0 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QReductionProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 QDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 QReductionProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 NonInfProof (⇔, 59 ms)

        ↳20 AND

            ↳21 QDP

                ↳22 NonInfProof (⇔, 9 ms)

                ↳23 AND

                    ↳24 QDP

                        ↳25 DependencyGraphProof (⇔, 0 ms)

                        ↳26 TRUE

                    ↳27 QDP

                        ↳28 DependencyGraphProof (⇔, 0 ms)

                        ↳29 TRUE

            ↳30 QDP

                ↳31 DependencyGraphProof (⇔, 0 ms)

                ↳32 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
mod(x, 0) → modZeroErro
mod(x, s(y)) → modIter(x, s(y), 0, 0)
modIter(x, s(y), z, u) → if(le(x, z), x, s(y), z, u)
if(true, x, y, z, u) → u
if(false, x, y, z, u) → if2(le(y, s(u)), x, y, s(z), s(u))
if2(false, x, y, z, u) → modIter(x, y, z, u)
if2(true, x, y, z, u) → modIter(x, y, z, 0)

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
mod(x, 0) → modZeroErro
mod(x, s(y)) → modIter(x, s(y), 0, 0)
modIter(x, s(y), z, u) → if(le(x, z), x, s(y), z, u)
if(true, x, y, z, u) → u
if(false, x, y, z, u) → if2(le(y, s(u)), x, y, s(z), s(u))
if2(false, x, y, z, u) → modIter(x, y, z, u)
if2(true, x, y, z, u) → modIter(x, y, z, 0)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)
MOD(x, s(y)) → MODITER(x, s(y), 0, 0)
MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u)
MODITER(x, s(y), z, u) → LE(x, z)
IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
IF(false, x, y, z, u) → LE(y, s(u))
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
IF2(true, x, y, z, u) → MODITER(x, y, z, 0)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
mod(x, 0) → modZeroErro
mod(x, s(y)) → modIter(x, s(y), 0, 0)
modIter(x, s(y), z, u) → if(le(x, z), x, s(y), z, u)
if(true, x, y, z, u) → u
if(false, x, y, z, u) → if2(le(y, s(u)), x, y, s(z), s(u))
if2(false, x, y, z, u) → modIter(x, y, z, u)
if2(true, x, y, z, u) → modIter(x, y, z, 0)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 3 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
mod(x, 0) → modZeroErro
mod(x, s(y)) → modIter(x, s(y), 0, 0)
modIter(x, s(y), z, u) → if(le(x, z), x, s(y), z, u)
if(true, x, y, z, u) → u
if(false, x, y, z, u) → if2(le(y, s(u)), x, y, s(z), s(u))
if2(false, x, y, z, u) → modIter(x, y, z, u)
if2(true, x, y, z, u) → modIter(x, y, z, 0)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

R is empty.
The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LE(s(x), s(y)) → LE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u)
IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
IF2(true, x, y, z, u) → MODITER(x, y, z, 0)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
mod(x, 0) → modZeroErro
mod(x, s(y)) → modIter(x, s(y), 0, 0)
modIter(x, s(y), z, u) → if(le(x, z), x, s(y), z, u)
if(true, x, y, z, u) → u
if(false, x, y, z, u) → if2(le(y, s(u)), x, y, s(z), s(u))
if2(false, x, y, z, u) → modIter(x, y, z, u)
if2(true, x, y, z, u) → modIter(x, y, z, 0)

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u)
IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
IF2(true, x, y, z, u) → MODITER(x, y, z, 0)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

We have to consider all minimal (P,Q,R)-chains.

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

mod(x0, 0)
mod(x0, s(x1))
modIter(x0, s(x1), x2, x3)
if(true, x0, x1, x2, x3)
if(false, x0, x1, x2, x3)
if2(false, x0, x1, x2, x3)
if2(true, x0, x1, x2, x3)

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u)
IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
IF2(true, x, y, z, u) → MODITER(x, y, z, 0)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(19) NonInfProof (EQUIVALENT transformation)

The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u) the following chains were created:

We consider the chain IF2(false, x8, x9, x10, x11) → MODITER(x8, x9, x10, x11), MODITER(x12, s(x13), x14, x15) → IF(le(x12, x14), x12, s(x13), x14, x15) which results in the following constraint:
(1) (MODITER(x8, x9, x10, x11)=MODITER(x12, s(x13), x14, x15) ⇒ MODITER(x12, s(x13), x14, x15)≥IF(le(x12, x14), x12, s(x13), x14, x15))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (MODITER(x8, s(x13), x10, x11)≥IF(le(x8, x10), x8, s(x13), x10, x11))
We consider the chain IF2(true, x16, x17, x18, x19) → MODITER(x16, x17, x18, 0), MODITER(x20, s(x21), x22, x23) → IF(le(x20, x22), x20, s(x21), x22, x23) which results in the following constraint:
(1) (MODITER(x16, x17, x18, 0)=MODITER(x20, s(x21), x22, x23) ⇒ MODITER(x20, s(x21), x22, x23)≥IF(le(x20, x22), x20, s(x21), x22, x23))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (MODITER(x16, s(x21), x18, 0)≥IF(le(x16, x18), x16, s(x21), x18, 0))

For Pair IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u)) the following chains were created:

We consider the chain MODITER(x24, s(x25), x26, x27) → IF(le(x24, x26), x24, s(x25), x26, x27), IF(false, x28, x29, x30, x31) → IF2(le(x29, s(x31)), x28, x29, s(x30), s(x31)) which results in the following constraint:

(1) (IF(le(x24, x26), x24, s(x25), x26, x27)=IF(false, x28, x29, x30, x31) ⇒ IF(false, x28, x29, x30, x31)≥IF2(le(x29, s(x31)), x28, x29, s(x30), s(x31)))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:

(2) (le(x24, x26)=false ⇒ IF(false, x24, s(x25), x26, x27)≥IF2(le(s(x25), s(x27)), x24, s(x25), s(x26), s(x27)))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x24, x26)=false which results in the following new constraints:

(3) (le(x86, x85)=false∧(∀x87,x88:le(x86, x85)=false ⇒ IF(false, x86, s(x87), x85, x88)≥IF2(le(s(x87), s(x88)), x86, s(x87), s(x85), s(x88))) ⇒ IF(false, s(x86), s(x25), s(x85), x27)≥IF2(le(s(x25), s(x27)), s(x86), s(x25), s(s(x85)), s(x27)))

(4) (false=false ⇒ IF(false, s(x89), s(x25), 0, x27)≥IF2(le(s(x25), s(x27)), s(x89), s(x25), s(0), s(x27)))

We simplified constraint (3) using rule (VI) where we applied the induction hypothesis (∀x87,x88:le(x86, x85)=false ⇒ IF(false, x86, s(x87), x85, x88)≥IF2(le(s(x87), s(x88)), x86, s(x87), s(x85), s(x88))) with σ = [x87 / x25, x88 / x27] which results in the following new constraint:

(5) (IF(false, x86, s(x25), x85, x27)≥IF2(le(s(x25), s(x27)), x86, s(x25), s(x85), s(x27)) ⇒ IF(false, s(x86), s(x25), s(x85), x27)≥IF2(le(s(x25), s(x27)), s(x86), s(x25), s(s(x85)), s(x27)))

We simplified constraint (4) using rules (I), (II) which results in the following new constraint:

(6) (IF(false, s(x89), s(x25), 0, x27)≥IF2(le(s(x25), s(x27)), s(x89), s(x25), s(0), s(x27)))

For Pair IF2(false, x, y, z, u) → MODITER(x, y, z, u) the following chains were created:

We consider the chain IF(false, x48, x49, x50, x51) → IF2(le(x49, s(x51)), x48, x49, s(x50), s(x51)), IF2(false, x52, x53, x54, x55) → MODITER(x52, x53, x54, x55) which results in the following constraint:

(1) (IF2(le(x49, s(x51)), x48, x49, s(x50), s(x51))=IF2(false, x52, x53, x54, x55) ⇒ IF2(false, x52, x53, x54, x55)≥MODITER(x52, x53, x54, x55))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:

(2) (s(x51)=x90∧le(x49, x90)=false ⇒ IF2(false, x48, x49, s(x50), s(x51))≥MODITER(x48, x49, s(x50), s(x51)))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x49, x90)=false which results in the following new constraints:

(3) (le(x93, x92)=false∧s(x51)=s(x92)∧(∀x94,x95,x96:le(x93, x92)=false∧s(x94)=x92 ⇒ IF2(false, x95, x93, s(x96), s(x94))≥MODITER(x95, x93, s(x96), s(x94))) ⇒ IF2(false, x48, s(x93), s(x50), s(x51))≥MODITER(x48, s(x93), s(x50), s(x51)))

(4) (false=false∧s(x51)=0 ⇒ IF2(false, x48, s(x97), s(x50), s(x51))≥MODITER(x48, s(x97), s(x50), s(x51)))

We simplified constraint (3) using rules (I), (II), (III), (IV) which results in the following new constraint:

(5) (le(x93, x92)=false ⇒ IF2(false, x48, s(x93), s(x50), s(x92))≥MODITER(x48, s(x93), s(x50), s(x92)))

We solved constraint (4) using rules (I), (II).We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on le(x93, x92)=false which results in the following new constraints:

(6) (le(x100, x99)=false∧(∀x101,x102:le(x100, x99)=false ⇒ IF2(false, x101, s(x100), s(x102), s(x99))≥MODITER(x101, s(x100), s(x102), s(x99))) ⇒ IF2(false, x48, s(s(x100)), s(x50), s(s(x99)))≥MODITER(x48, s(s(x100)), s(x50), s(s(x99))))

(7) (false=false ⇒ IF2(false, x48, s(s(x103)), s(x50), s(0))≥MODITER(x48, s(s(x103)), s(x50), s(0)))

We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (∀x101,x102:le(x100, x99)=false ⇒ IF2(false, x101, s(x100), s(x102), s(x99))≥MODITER(x101, s(x100), s(x102), s(x99))) with σ = [x101 / x48, x102 / x50] which results in the following new constraint:

(8) (IF2(false, x48, s(x100), s(x50), s(x99))≥MODITER(x48, s(x100), s(x50), s(x99)) ⇒ IF2(false, x48, s(s(x100)), s(x50), s(s(x99)))≥MODITER(x48, s(s(x100)), s(x50), s(s(x99))))

We simplified constraint (7) using rules (I), (II) which results in the following new constraint:

(9) (IF2(false, x48, s(s(x103)), s(x50), s(0))≥MODITER(x48, s(s(x103)), s(x50), s(0)))

For Pair IF2(true, x, y, z, u) → MODITER(x, y, z, 0) the following chains were created:

We consider the chain IF(false, x68, x69, x70, x71) → IF2(le(x69, s(x71)), x68, x69, s(x70), s(x71)), IF2(true, x72, x73, x74, x75) → MODITER(x72, x73, x74, 0) which results in the following constraint:

(1) (IF2(le(x69, s(x71)), x68, x69, s(x70), s(x71))=IF2(true, x72, x73, x74, x75) ⇒ IF2(true, x72, x73, x74, x75)≥MODITER(x72, x73, x74, 0))

We simplified constraint (1) using rules (I), (II), (III), (VII) which results in the following new constraint:

(2) (s(x71)=x104∧le(x69, x104)=true ⇒ IF2(true, x68, x69, s(x70), s(x71))≥MODITER(x68, x69, s(x70), 0))

We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x69, x104)=true which results in the following new constraints:

(3) (true=true∧s(x71)=x105 ⇒ IF2(true, x68, 0, s(x70), s(x71))≥MODITER(x68, 0, s(x70), 0))

(4) (le(x107, x106)=true∧s(x71)=s(x106)∧(∀x108,x109,x110:le(x107, x106)=true∧s(x108)=x106 ⇒ IF2(true, x109, x107, s(x110), s(x108))≥MODITER(x109, x107, s(x110), 0)) ⇒ IF2(true, x68, s(x107), s(x70), s(x71))≥MODITER(x68, s(x107), s(x70), 0))

We simplified constraint (3) using rules (I), (II), (IV) which results in the following new constraint:

(5) (IF2(true, x68, 0, s(x70), s(x71))≥MODITER(x68, 0, s(x70), 0))

We simplified constraint (4) using rules (I), (II), (III), (IV) which results in the following new constraint:

(6) (le(x107, x106)=true ⇒ IF2(true, x68, s(x107), s(x70), s(x106))≥MODITER(x68, s(x107), s(x70), 0))

We simplified constraint (6) using rule (V) (with possible (I) afterwards) using induction on le(x107, x106)=true which results in the following new constraints:

(7) (true=true ⇒ IF2(true, x68, s(0), s(x70), s(x112))≥MODITER(x68, s(0), s(x70), 0))

(8) (le(x114, x113)=true∧(∀x115,x116:le(x114, x113)=true ⇒ IF2(true, x115, s(x114), s(x116), s(x113))≥MODITER(x115, s(x114), s(x116), 0)) ⇒ IF2(true, x68, s(s(x114)), s(x70), s(s(x113)))≥MODITER(x68, s(s(x114)), s(x70), 0))

We simplified constraint (7) using rules (I), (II) which results in the following new constraint:

(9) (IF2(true, x68, s(0), s(x70), s(x112))≥MODITER(x68, s(0), s(x70), 0))

We simplified constraint (8) using rule (VI) where we applied the induction hypothesis (∀x115,x116:le(x114, x113)=true ⇒ IF2(true, x115, s(x114), s(x116), s(x113))≥MODITER(x115, s(x114), s(x116), 0)) with σ = [x115 / x68, x116 / x70] which results in the following new constraint:

(10) (IF2(true, x68, s(x114), s(x70), s(x113))≥MODITER(x68, s(x114), s(x70), 0) ⇒ IF2(true, x68, s(s(x114)), s(x70), s(s(x113)))≥MODITER(x68, s(s(x114)), s(x70), 0))

To summarize, we get the following constraints P_≥ for the following pairs.

MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u)
- (MODITER(x8, s(x13), x10, x11)≥IF(le(x8, x10), x8, s(x13), x10, x11))
- (MODITER(x16, s(x21), x18, 0)≥IF(le(x16, x18), x16, s(x21), x18, 0))
IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
- (IF(false, x86, s(x25), x85, x27)≥IF2(le(s(x25), s(x27)), x86, s(x25), s(x85), s(x27)) ⇒ IF(false, s(x86), s(x25), s(x85), x27)≥IF2(le(s(x25), s(x27)), s(x86), s(x25), s(s(x85)), s(x27)))
- (IF(false, s(x89), s(x25), 0, x27)≥IF2(le(s(x25), s(x27)), s(x89), s(x25), s(0), s(x27)))
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
- (IF2(false, x48, s(x100), s(x50), s(x99))≥MODITER(x48, s(x100), s(x50), s(x99)) ⇒ IF2(false, x48, s(s(x100)), s(x50), s(s(x99)))≥MODITER(x48, s(s(x100)), s(x50), s(s(x99))))
- (IF2(false, x48, s(s(x103)), s(x50), s(0))≥MODITER(x48, s(s(x103)), s(x50), s(0)))
IF2(true, x, y, z, u) → MODITER(x, y, z, 0)
- (IF2(true, x68, 0, s(x70), s(x71))≥MODITER(x68, 0, s(x70), 0))
- (IF2(true, x68, s(0), s(x70), s(x112))≥MODITER(x68, s(0), s(x70), 0))
- (IF2(true, x68, s(x114), s(x70), s(x113))≥MODITER(x68, s(x114), s(x70), 0) ⇒ IF2(true, x68, s(s(x114)), s(x70), s(s(x113)))≥MODITER(x68, s(s(x114)), s(x70), 0))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0
POL(IF(x₁, x₂, x₃, x₄, x₅)) = x₂ - x₄ + x₅
POL(IF2(x₁, x₂, x₃, x₄, x₅)) = 1 - x₁ + x₂ - x₄ + x₅
POL(MODITER(x₁, x₂, x₃, x₄)) = x₁ - x₃ + x₄
POL(c) = -1
POL(false) = 1
POL(le(x₁, x₂)) = 1
POL(s(x₁)) = 1 + x₁
POL(true) = 1

The following pairs are in P_>:

IF2(true, x, y, z, u) → MODITER(x, y, z, 0)

The following pairs are in P_bound:

IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))

The following rules are usable:

true → le(0, y)
le(x, y) → le(s(x), s(y))
false → le(s(x), 0)

(20) Complex Obligation (AND)

(21) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u)
IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
IF2(false, x, y, z, u) → MODITER(x, y, z, u)

The TRS R consists of the following rules:

le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x), 0) → false

The set Q consists of the following terms:

le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(22) NonInfProof (EQUIVALENT transformation)

We consider the chain IF2(false, x8, x9, x10, x11) → MODITER(x8, x9, x10, x11), MODITER(x12, s(x13), x14, x15) → IF(le(x12, x14), x12, s(x13), x14, x15) which results in the following constraint:
(1) (MODITER(x8, x9, x10, x11)=MODITER(x12, s(x13), x14, x15) ⇒ MODITER(x12, s(x13), x14, x15)≥IF(le(x12, x14), x12, s(x13), x14, x15))

We simplified constraint (1) using rules (I), (II), (III) which results in the following new constraint:
(2) (MODITER(x8, s(x13), x10, x11)≥IF(le(x8, x10), x8, s(x13), x10, x11))