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

0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳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 Instantiation (⇔)
        ↳20 QDP
      ↳21 NonInfProof (⇔)
        ↳22 AND
          ↳23 QDP
            ↳24 Instantiation (⇔)
              ↳25 QDP
            ↳26 NonInfProof (⇔)
              ↳27 AND
                ↳28 QDP
                  ↳29 DependencyGraphProof (⇔)
                  ↳30 TRUE
                ↳31 QDP
                  ↳32 DependencyGraphProof (⇔)
                  ↳33 TRUE
          ↳34 QDP
            ↳35 DependencyGraphProof (⇔)
            ↳36 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) TRUE

(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) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u)) we obtained the following new rules [LPAR04]:

IF(false, z0, s(z1), z2, z3) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3))

(20) 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)
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
IF2(true, x, y, z, u) → MODITER(x, y, z, 0)
IF(false, z0, s(z1), z2, z3) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3))

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.

(21) 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, x, y, z, u) → MODITER(x, y, z, u), MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u) 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, x, y, z, u) → MODITER(x, y, z, 0), MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u) which results in the following constraint:

    (3)    (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 (3) using rules (I), (II), (III) which results in the following new constraint:

    (4)    (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(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)) which results in the following constraint:

    (5)    (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 (5) using rules (I), (II), (III) which results in the following new constraint:

    (6)    (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 (6) using rule (V) (with possible (I) afterwards) using induction on le(x24, x26)=false which results in the following new constraints:

    (7)    (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)))


    (8)    (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 (7) 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:

    (9)    (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 (8) using rules (I), (II) which results in the following new constraint:

    (10)    (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, 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) which results in the following constraint:

    (11)    (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 (11) using rules (I), (II), (III), (VII) which results in the following new constraint:

    (12)    (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 (12) using rule (V) (with possible (I) afterwards) using induction on le(x49, x90)=false which results in the following new constraints:

    (13)    (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)))


    (14)    (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 (13) using rules (I), (II), (III), (IV) which results in the following new constraint:

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



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

    (16)    (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))))


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



    We simplified constraint (16) 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:

    (18)    (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 (17) using rules (I), (II) which results in the following new constraint:

    (19)    (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, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u)), IF2(true, x, y, z, u) → MODITER(x, y, z, 0) which results in the following constraint:

    (20)    (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 (20) using rules (I), (II), (III), (VII) which results in the following new constraint:

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



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

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


    (23)    (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 (22) using rules (I), (II), (IV) which results in the following new constraint:

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



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

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



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

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


    (27)    (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 (26) using rules (I), (II) which results in the following new constraint:

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



    We simplified constraint (27) 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:

    (29)    (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 Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF(x1, x2, x3, x4, x5)) = -1 + x2 - x4 + x5   
POL(IF2(x1, x2, x3, x4, x5)) = -1 + x2 - x4 + x5   
POL(MODITER(x1, x2, x3, x4)) = -1 + x1 - x3 + x4   
POL(c) = -1   
POL(false) = 0   
POL(le(x1, x2)) = x2   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following pairs are in P>:

IF2(true, x, y, z, u) → MODITER(x, y, z, 0)
The following pairs are in Pbound:

IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
There are no usable rules

(22) Complex Obligation (AND)

(23) 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.

(24) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u)) we obtained the following new rules [LPAR04]:

IF(false, z0, s(z1), z2, z3) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3))

(25) 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)
IF2(false, x, y, z, u) → MODITER(x, y, z, u)
IF(false, z0, s(z1), z2, z3) → IF2(le(s(z1), s(z3)), z0, s(z1), s(z2), s(z3))

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.

(26) 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, x, y, z, u) → MODITER(x, y, z, u), MODITER(x, s(y), z, u) → IF(le(x, z), x, s(y), z, u) 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))







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(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)) which results in the following constraint:

    (3)    (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 (3) using rules (I), (II), (III) which results in the following new constraint:

    (4)    (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 (4) using rule (V) (with possible (I) afterwards) using induction on le(x24, x26)=false which results in the following new constraints:

    (5)    (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)))


    (6)    (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 (5) 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:

    (7)    (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 (6) using rules (I), (II) which results in the following new constraint:

    (8)    (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, 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) which results in the following constraint:

    (9)    (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 (9) using rules (I), (II), (III), (VII) which results in the following new constraint:

    (10)    (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 (10) using rule (V) (with possible (I) afterwards) using induction on le(x49, x90)=false which results in the following new constraints:

    (11)    (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)))


    (12)    (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 (11) using rules (I), (II), (III), (IV) which results in the following new constraint:

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



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

    (14)    (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))))


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



    We simplified constraint (14) 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:

    (16)    (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 (15) using rules (I), (II) which results in the following new constraint:

    (17)    (IF2(false, x48, s(s(x103)), s(x50), s(0))≥MODITER(x48, s(s(x103)), s(x50), s(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))

  • 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)))




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:

POL(0) = 0   
POL(IF(x1, x2, x3, x4, x5)) = 1 + x3 - x5   
POL(IF2(x1, x2, x3, x4, x5)) = 1 + x3 - x5   
POL(MODITER(x1, x2, x3, x4)) = 1 + x2 - x4   
POL(c) = -1   
POL(false) = 0   
POL(le(x1, x2)) = x2   
POL(s(x1)) = 1 + x1   
POL(true) = 0   

The following pairs are in P>:

IF(false, x, y, z, u) → IF2(le(y, s(u)), x, y, s(z), s(u))
The following pairs are in Pbound:

IF2(false, x, y, z, u) → MODITER(x, y, z, u)
There are no usable rules

(27) Complex Obligation (AND)

(28) 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)
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.

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(30) TRUE

(31) 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))

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.

(32) DependencyGraphProof (EQUIVALENT transformation)

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

(33) TRUE

(34) 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)
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.

(35) DependencyGraphProof (EQUIVALENT transformation)

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

(36) TRUE