Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 ITRStoIDPProof (⇔)
↳6 IDP
↳7 UsableRulesProof (⇔)
↳8 IDP
↳9 IDPNonInfProof (⇐)
↳10 AND
    ↳11 IDP
        ↳12 IDependencyGraphProof (⇔)
        ↳13 TRUE
    ↳14 IDP
        ↳15 IDPNonInfProof (⇐)
        ↳16 AND
            ↳17 IDP
                ↳18 IDependencyGraphProof (⇔)
                ↳19 TRUE
            ↳20 IDP
                ↳21 IDependencyGraphProof (⇔)
                ↳22 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaC3 
/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaC3 {
    public static void main(String[] args) {
        Random.args = args;
        int x = Random.random();
        int y = Random.random();
        int z = Random.random();

        while (x < y) {
            if (x < z) {
                x++;
            } else {
                z++;
            }
        }
    }
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 253 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1224(i11, i23, i62) → Cond_Load1224(i11 >= i62 && i11 < i23, i11, i23, i62)
Cond_Load1224(TRUE, i11, i23, i62) → Load1224(i11, i23, i62 + 1)
Load1224(i11, i23, i62) → Cond_Load12241(i11 < i62 && i11 < i23, i11, i23, i62)
Cond_Load12241(TRUE, i11, i23, i62) → Load1224(i11 + 1, i23, i62)
The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

(5) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(6) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


The ITRS R consists of the following rules:
Load1224(i11, i23, i62) → Cond_Load1224(i11 >= i62 && i11 < i23, i11, i23, i62)
Cond_Load1224(TRUE, i11, i23, i62) → Load1224(i11, i23, i62 + 1)
Load1224(i11, i23, i62) → Cond_Load12241(i11 < i62 && i11 < i23, i11, i23, i62)
Cond_Load12241(TRUE, i11, i23, i62) → Load1224(i11 + 1, i23, i62)

The integer pair graph contains the following rules and edges:
(0): LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(i11[0] >= i62[0] && i11[0] < i23[0], i11[0], i23[0], i62[0])
(1): COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], i62[1] + 1)
(2): LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(i11[2] < i62[2] && i11[2] < i23[2], i11[2], i23[2], i62[2])
(3): COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(i11[3] + 1, i23[3], i62[3])

(0) -> (1), if ((i62[0] →* i62[1])∧(i23[0] →* i23[1])∧(i11[0] >= i62[0] && i11[0] < i23[0] →* TRUE)∧(i11[0] →* i11[1]))


(1) -> (0), if ((i23[1] →* i23[0])∧(i62[1] + 1 →* i62[0])∧(i11[1] →* i11[0]))


(1) -> (2), if ((i11[1] →* i11[2])∧(i23[1] →* i23[2])∧(i62[1] + 1 →* i62[2]))


(2) -> (3), if ((i11[2] < i62[2] && i11[2] < i23[2] →* TRUE)∧(i11[2] →* i11[3])∧(i62[2] →* i62[3])∧(i23[2] →* i23[3]))


(3) -> (0), if ((i23[3] →* i23[0])∧(i11[3] + 1 →* i11[0])∧(i62[3] →* i62[0]))


(3) -> (2), if ((i11[3] + 1 →* i11[2])∧(i23[3] →* i23[2])∧(i62[3] →* i62[2]))



The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

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

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(i11[0] >= i62[0] && i11[0] < i23[0], i11[0], i23[0], i62[0])
(1): COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], i62[1] + 1)
(2): LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(i11[2] < i62[2] && i11[2] < i23[2], i11[2], i23[2], i62[2])
(3): COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(i11[3] + 1, i23[3], i62[3])

(0) -> (1), if ((i62[0] →* i62[1])∧(i23[0] →* i23[1])∧(i11[0] >= i62[0] && i11[0] < i23[0] →* TRUE)∧(i11[0] →* i11[1]))


(1) -> (0), if ((i23[1] →* i23[0])∧(i62[1] + 1 →* i62[0])∧(i11[1] →* i11[0]))


(1) -> (2), if ((i11[1] →* i11[2])∧(i23[1] →* i23[2])∧(i62[1] + 1 →* i62[2]))


(2) -> (3), if ((i11[2] < i62[2] && i11[2] < i23[2] →* TRUE)∧(i11[2] →* i11[3])∧(i62[2] →* i62[3])∧(i23[2] →* i23[3]))


(3) -> (0), if ((i23[3] →* i23[0])∧(i11[3] + 1 →* i11[0])∧(i62[3] →* i62[0]))


(3) -> (2), if ((i11[3] + 1 →* i11[2])∧(i23[3] →* i23[2])∧(i62[3] →* i62[2]))



The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

(9) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
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 LOAD1224(i11, i23, i62) → COND_LOAD1224(&&(>=(i11, i62), <(i11, i23)), i11, i23, i62) the following chains were created:
  • We consider the chain LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0]), COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], +(i62[1], 1)) which results in the following constraint:

    (1)    (i62[0]=i62[1]∧i23[0]=i23[1]∧&&(>=(i11[0], i62[0]), <(i11[0], i23[0]))=TRUE∧i11[0]=i11[1] ⇒ LOAD1224(i11[0], i23[0], i62[0])≥NonInfC∧LOAD1224(i11[0], i23[0], i62[0])≥COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])∧(UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥))



    We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>=(i11[0], i62[0])=TRUE∧<(i11[0], i23[0])=TRUE ⇒ LOAD1224(i11[0], i23[0], i62[0])≥NonInfC∧LOAD1224(i11[0], i23[0], i62[0])≥COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])∧(UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i62[0] + [(2)bni_20]i23[0] + [(-1)bni_20]i11[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i62[0] + [(2)bni_20]i23[0] + [(-1)bni_20]i11[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i62[0] + [(2)bni_20]i23[0] + [(-1)bni_20]i11[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (i11[0] ≥ 0∧i23[0] + [-1] + [-1]i62[0] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-2)bni_20]i62[0] + [(2)bni_20]i23[0] + [(-1)bni_20]i11[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i11[0] ≥ 0∧i62[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)Bound*bni_20 + bni_20] + [bni_20]i11[0] + [(2)bni_20]i62[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (8)    (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)Bound*bni_20 + bni_20] + [bni_20]i11[0] + [(2)bni_20]i62[0] ≥ 0∧[(-1)bso_21] ≥ 0)


    (9)    (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)Bound*bni_20 + bni_20] + [bni_20]i11[0] + [(2)bni_20]i62[0] ≥ 0∧[(-1)bso_21] ≥ 0)







For Pair COND_LOAD1224(TRUE, i11, i23, i62) → LOAD1224(i11, i23, +(i62, 1)) the following chains were created:
  • We consider the chain LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0]), COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], +(i62[1], 1)), LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0]) which results in the following constraint:

    (10)    (i62[0]=i62[1]∧i23[0]=i23[1]∧&&(>=(i11[0], i62[0]), <(i11[0], i23[0]))=TRUE∧i11[0]=i11[1]∧i23[1]=i23[0]1∧+(i62[1], 1)=i62[0]1∧i11[1]=i11[0]1 ⇒ COND_LOAD1224(TRUE, i11[1], i23[1], i62[1])≥NonInfC∧COND_LOAD1224(TRUE, i11[1], i23[1], i62[1])≥LOAD1224(i11[1], i23[1], +(i62[1], 1))∧(UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥))



    We simplified constraint (10) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (11)    (>=(i11[0], i62[0])=TRUE∧<(i11[0], i23[0])=TRUE ⇒ COND_LOAD1224(TRUE, i11[0], i23[0], i62[0])≥NonInfC∧COND_LOAD1224(TRUE, i11[0], i23[0], i62[0])≥LOAD1224(i11[0], i23[0], +(i62[0], 1))∧(UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥))



    We simplified constraint (11) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (12)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (12) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (13)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (13) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (14)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (15)    (i11[0] ≥ 0∧i23[0] + [-1] + [-1]i62[0] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-2)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (16)    (i11[0] ≥ 0∧i62[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (17)    (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)


    (18)    (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



  • We consider the chain LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0]), COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], +(i62[1], 1)), LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]) which results in the following constraint:

    (19)    (i62[0]=i62[1]∧i23[0]=i23[1]∧&&(>=(i11[0], i62[0]), <(i11[0], i23[0]))=TRUE∧i11[0]=i11[1]∧i11[1]=i11[2]∧i23[1]=i23[2]∧+(i62[1], 1)=i62[2] ⇒ COND_LOAD1224(TRUE, i11[1], i23[1], i62[1])≥NonInfC∧COND_LOAD1224(TRUE, i11[1], i23[1], i62[1])≥LOAD1224(i11[1], i23[1], +(i62[1], 1))∧(UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥))



    We simplified constraint (19) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (20)    (>=(i11[0], i62[0])=TRUE∧<(i11[0], i23[0])=TRUE ⇒ COND_LOAD1224(TRUE, i11[0], i23[0], i62[0])≥NonInfC∧COND_LOAD1224(TRUE, i11[0], i23[0], i62[0])≥LOAD1224(i11[0], i23[0], +(i62[0], 1))∧(UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥))



    We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (21)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (22)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (23)    (i11[0] + [-1]i62[0] ≥ 0∧i23[0] + [-1] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (23) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (24)    (i11[0] ≥ 0∧i23[0] + [-1] + [-1]i62[0] + [-1]i11[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-2)bni_22]i62[0] + [(2)bni_22]i23[0] + [(-1)bni_22]i11[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (24) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (25)    (i11[0] ≥ 0∧i62[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (25) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (26)    (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)


    (27)    (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)







For Pair LOAD1224(i11, i23, i62) → COND_LOAD12241(&&(<(i11, i62), <(i11, i23)), i11, i23, i62) the following chains were created:
  • We consider the chain LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]), COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3]) which results in the following constraint:

    (28)    (&&(<(i11[2], i62[2]), <(i11[2], i23[2]))=TRUE∧i11[2]=i11[3]∧i62[2]=i62[3]∧i23[2]=i23[3] ⇒ LOAD1224(i11[2], i23[2], i62[2])≥NonInfC∧LOAD1224(i11[2], i23[2], i62[2])≥COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])∧(UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥))



    We simplified constraint (28) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (29)    (<(i11[2], i62[2])=TRUE∧<(i11[2], i23[2])=TRUE ⇒ LOAD1224(i11[2], i23[2], i62[2])≥NonInfC∧LOAD1224(i11[2], i23[2], i62[2])≥COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])∧(UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥))



    We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (30)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i62[2] + [(2)bni_24]i23[2] + [(-1)bni_24]i11[2] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (31)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i62[2] + [(2)bni_24]i23[2] + [(-1)bni_24]i11[2] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (32)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i62[2] + [(2)bni_24]i23[2] + [(-1)bni_24]i11[2] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (33)    (i62[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-2)bni_24 + (-1)Bound*bni_24] + [(-2)bni_24]i11[2] + [(-1)bni_24]i62[2] + [(2)bni_24]i23[2] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (33) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (34)    (i62[2] ≥ 0∧i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i11[2] + [(-1)bni_24]i62[2] ≥ 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (34) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (35)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i11[2] + [(-1)bni_24]i62[2] ≥ 0∧[(-1)bso_25] ≥ 0)


    (36)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i11[2] + [(-1)bni_24]i62[2] ≥ 0∧[(-1)bso_25] ≥ 0)







For Pair COND_LOAD12241(TRUE, i11, i23, i62) → LOAD1224(+(i11, 1), i23, i62) the following chains were created:
  • We consider the chain LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]), COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3]), LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0]) which results in the following constraint:

    (37)    (&&(<(i11[2], i62[2]), <(i11[2], i23[2]))=TRUE∧i11[2]=i11[3]∧i62[2]=i62[3]∧i23[2]=i23[3]∧i23[3]=i23[0]∧+(i11[3], 1)=i11[0]∧i62[3]=i62[0] ⇒ COND_LOAD12241(TRUE, i11[3], i23[3], i62[3])≥NonInfC∧COND_LOAD12241(TRUE, i11[3], i23[3], i62[3])≥LOAD1224(+(i11[3], 1), i23[3], i62[3])∧(UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥))



    We simplified constraint (37) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (38)    (<(i11[2], i62[2])=TRUE∧<(i11[2], i23[2])=TRUE ⇒ COND_LOAD12241(TRUE, i11[2], i23[2], i62[2])≥NonInfC∧COND_LOAD12241(TRUE, i11[2], i23[2], i62[2])≥LOAD1224(+(i11[2], 1), i23[2], i62[2])∧(UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥))



    We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (39)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] + [(-1)bni_26]i11[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (40)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] + [(-1)bni_26]i11[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (41)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] + [(-1)bni_26]i11[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (41) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (42)    (i62[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [(-2)bni_26]i11[2] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (42) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (43)    (i62[2] ≥ 0∧i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (43) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (44)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)


    (45)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



  • We consider the chain LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]), COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3]), LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]) which results in the following constraint:

    (46)    (&&(<(i11[2], i62[2]), <(i11[2], i23[2]))=TRUE∧i11[2]=i11[3]∧i62[2]=i62[3]∧i23[2]=i23[3]∧+(i11[3], 1)=i11[2]1∧i23[3]=i23[2]1∧i62[3]=i62[2]1 ⇒ COND_LOAD12241(TRUE, i11[3], i23[3], i62[3])≥NonInfC∧COND_LOAD12241(TRUE, i11[3], i23[3], i62[3])≥LOAD1224(+(i11[3], 1), i23[3], i62[3])∧(UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥))



    We simplified constraint (46) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (47)    (<(i11[2], i62[2])=TRUE∧<(i11[2], i23[2])=TRUE ⇒ COND_LOAD12241(TRUE, i11[2], i23[2], i62[2])≥NonInfC∧COND_LOAD12241(TRUE, i11[2], i23[2], i62[2])≥LOAD1224(+(i11[2], 1), i23[2], i62[2])∧(UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥))



    We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (48)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] + [(-1)bni_26]i11[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (49)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] + [(-1)bni_26]i11[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (50)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] + [(-1)bni_26]i11[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (50) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (51)    (i62[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [(-2)bni_26]i11[2] + [(-1)bni_26]i62[2] + [(2)bni_26]i23[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (51) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (52)    (i62[2] ≥ 0∧i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)



    We simplified constraint (52) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (53)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)


    (54)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1224(i11, i23, i62) → COND_LOAD1224(&&(>=(i11, i62), <(i11, i23)), i11, i23, i62)
    • (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)Bound*bni_20 + bni_20] + [bni_20]i11[0] + [(2)bni_20]i62[0] ≥ 0∧[(-1)bso_21] ≥ 0)
    • (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])), ≥)∧[(-1)Bound*bni_20 + bni_20] + [bni_20]i11[0] + [(2)bni_20]i62[0] ≥ 0∧[(-1)bso_21] ≥ 0)

  • COND_LOAD1224(TRUE, i11, i23, i62) → LOAD1224(i11, i23, +(i62, 1))
    • (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
    • (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
    • (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
    • (i11[0] ≥ 0∧i62[0] ≥ 0∧i23[0] ≥ 0 ⇒ (UIncreasing(LOAD1224(i11[1], i23[1], +(i62[1], 1))), ≥)∧[(-1)Bound*bni_22 + bni_22] + [bni_22]i11[0] + [(2)bni_22]i62[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

  • LOAD1224(i11, i23, i62) → COND_LOAD12241(&&(<(i11, i62), <(i11, i23)), i11, i23, i62)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i11[2] + [(-1)bni_24]i62[2] ≥ 0∧[(-1)bso_25] ≥ 0)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i11[2] + [(-1)bni_24]i62[2] ≥ 0∧[(-1)bso_25] ≥ 0)

  • COND_LOAD12241(TRUE, i11, i23, i62) → LOAD1224(+(i11, 1), i23, i62)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 0)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_26] + [(2)bni_26]i11[2] + [(-1)bni_26]i62[2] ≥ 0∧[1 + (-1)bso_27] ≥ 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 over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD1224(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + [-1]x1   
POL(COND_LOAD1224(x1, x2, x3, x4)) = [-1] + [-1]x4 + [2]x3 + [-1]x2   
POL(&&(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(COND_LOAD12241(x1, x2, x3, x4)) = [-1] + [-1]x4 + [2]x3 + [-1]x2   

The following pairs are in P>:

COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], +(i62[1], 1))
COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3])

The following pairs are in Pbound:

LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])
COND_LOAD1224(TRUE, i11[1], i23[1], i62[1]) → LOAD1224(i11[1], i23[1], +(i62[1], 1))

The following pairs are in P≥:

LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(&&(>=(i11[0], i62[0]), <(i11[0], i23[0])), i11[0], i23[0], i62[0])
LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(10) Complex Obligation (AND)

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1224(i11[0], i23[0], i62[0]) → COND_LOAD1224(i11[0] >= i62[0] && i11[0] < i23[0], i11[0], i23[0], i62[0])
(2): LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(i11[2] < i62[2] && i11[2] < i23[2], i11[2], i23[2], i62[2])


The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

(12) IDependencyGraphProof (EQUIVALENT transformation)

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

(13) TRUE

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(i11[2] < i62[2] && i11[2] < i23[2], i11[2], i23[2], i62[2])
(3): COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(i11[3] + 1, i23[3], i62[3])

(3) -> (2), if ((i11[3] + 1 →* i11[2])∧(i23[3] →* i23[2])∧(i62[3] →* i62[2]))


(2) -> (3), if ((i11[2] < i62[2] && i11[2] < i23[2] →* TRUE)∧(i11[2] →* i11[3])∧(i62[2] →* i62[3])∧(i23[2] →* i23[3]))



The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

(15) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
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 LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]) the following chains were created:
  • We consider the chain LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]), COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3]) which results in the following constraint:

    (1)    (&&(<(i11[2], i62[2]), <(i11[2], i23[2]))=TRUE∧i11[2]=i11[3]∧i62[2]=i62[3]∧i23[2]=i23[3] ⇒ LOAD1224(i11[2], i23[2], i62[2])≥NonInfC∧LOAD1224(i11[2], i23[2], i62[2])≥COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])∧(UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥))



    We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (<(i11[2], i62[2])=TRUE∧<(i11[2], i23[2])=TRUE ⇒ LOAD1224(i11[2], i23[2], i62[2])≥NonInfC∧LOAD1224(i11[2], i23[2], i62[2])≥COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])∧(UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14] + [bni_14]i23[2] + [(-1)bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14] + [bni_14]i23[2] + [(-1)bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14] + [bni_14]i23[2] + [(-1)bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (i62[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14] + [(-1)bni_14]i11[2] + [bni_14]i23[2] ≥ 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (7)    (i62[2] ≥ 0∧i11[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14 + bni_14] + [bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)



    We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (8)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14 + bni_14] + [bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)


    (9)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14 + bni_14] + [bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)







For Pair COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3]) the following chains were created:
  • We consider the chain LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]), COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3]), LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2]) which results in the following constraint:

    (10)    (&&(<(i11[2], i62[2]), <(i11[2], i23[2]))=TRUE∧i11[2]=i11[3]∧i62[2]=i62[3]∧i23[2]=i23[3]∧+(i11[3], 1)=i11[2]1∧i23[3]=i23[2]1∧i62[3]=i62[2]1 ⇒ COND_LOAD12241(TRUE, i11[3], i23[3], i62[3])≥NonInfC∧COND_LOAD12241(TRUE, i11[3], i23[3], i62[3])≥LOAD1224(+(i11[3], 1), i23[3], i62[3])∧(UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥))



    We simplified constraint (10) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (11)    (<(i11[2], i62[2])=TRUE∧<(i11[2], i23[2])=TRUE ⇒ COND_LOAD12241(TRUE, i11[2], i23[2], i62[2])≥NonInfC∧COND_LOAD12241(TRUE, i11[2], i23[2], i62[2])≥LOAD1224(+(i11[2], 1), i23[2], i62[2])∧(UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥))



    We simplified constraint (11) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (12)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16] + [bni_16]i23[2] + [(-1)bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (12) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (13)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16] + [bni_16]i23[2] + [(-1)bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (13) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (14)    (i62[2] + [-1] + [-1]i11[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16] + [bni_16]i23[2] + [(-1)bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (15)    (i62[2] ≥ 0∧i23[2] + [-1] + [-1]i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]i11[2] + [bni_16]i23[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (16)    (i62[2] ≥ 0∧i11[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)



    We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (17)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)


    (18)    (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14 + bni_14] + [bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])), ≥)∧[(-1)Bound*bni_14 + bni_14] + [bni_14]i11[2] ≥ 0∧[(-1)bso_15] ≥ 0)

  • COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3])
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 0)
    • (i62[2] ≥ 0∧i11[2] ≥ 0∧i23[2] ≥ 0 ⇒ (UIncreasing(LOAD1224(+(i11[3], 1), i23[3], i62[3])), ≥)∧[(-1)Bound*bni_16 + bni_16] + [bni_16]i11[2] ≥ 0∧[1 + (-1)bso_17] ≥ 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 over integers[POLO]:

POL(TRUE) = [1]   
POL(FALSE) = [1]   
POL(LOAD1224(x1, x2, x3)) = x2 + [-1]x1   
POL(COND_LOAD12241(x1, x2, x3, x4)) = x3 + [-1]x2   
POL(&&(x1, x2)) = [-1]   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   

The following pairs are in P>:

COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3])

The following pairs are in Pbound:

LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])
COND_LOAD12241(TRUE, i11[3], i23[3], i62[3]) → LOAD1224(+(i11[3], 1), i23[3], i62[3])

The following pairs are in P≥:

LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(&&(<(i11[2], i62[2]), <(i11[2], i23[2])), i11[2], i23[2], i62[2])

At least the following rules have been oriented under context sensitive arithmetic replacement:

FALSE1 → &&(FALSE, TRUE)1

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1224(i11[2], i23[2], i62[2]) → COND_LOAD12241(i11[2] < i62[2] && i11[2] < i23[2], i11[2], i23[2], i62[2])


The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

(18) IDependencyGraphProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Load1224(x0, x1, x2)
Cond_Load1224(TRUE, x0, x1, x2)
Cond_Load12241(TRUE, x0, x1, x2)

(21) IDependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE