### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaB15
`/** * 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 PastaB15 {    public static void main(String[] args) {        Random.args = args;        int x = Random.random();        int y = Random.random();        int z = Random.random();        while (x == y && x > z) {            while (y > z) {                x--;                y--;            }        }    }}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 265 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:
Load848(i20, i37) → Cond_Load848(i20 <= i37 && i20 > i37, i20, i37)
Inc1074(i55, i20, i37) → Cond_Inc1074(i20 + -1 <= i37, i55, i20, i37)
Cond_Inc1074(TRUE, i55, i20, i37) → Load848(i55, i37)
Load848(i20, i37) → Cond_Load8481(i20 + -1 <= i37 && i20 > i37, i20, i37)
Inc1074(i55, i20, i37) → Cond_Inc10741(i20 + -1 > i37, i55, i20, i37)
Cond_Inc10741(TRUE, i55, i20, i37) → Inc1074(i55 + -1, i20 + -1, i37)
Load848(i20, i37) → Cond_Load8482(i20 + -1 > i37 && i20 > i37, i20, i37)
Cond_Load8482(TRUE, i20, i37) → Inc1074(i20 + -1 + -1, i20 + -1, i37)
The set Q consists of the following terms:
Inc1074(x0, x1, x2)
Cond_Inc1074(TRUE, x0, x1, x2)
Cond_Inc10741(TRUE, x0, x1, x2)

### (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:
Load848(i20, i37) → Cond_Load848(i20 <= i37 && i20 > i37, i20, i37)
Inc1074(i55, i20, i37) → Cond_Inc1074(i20 + -1 <= i37, i55, i20, i37)
Cond_Inc1074(TRUE, i55, i20, i37) → Load848(i55, i37)
Load848(i20, i37) → Cond_Load8481(i20 + -1 <= i37 && i20 > i37, i20, i37)
Inc1074(i55, i20, i37) → Cond_Inc10741(i20 + -1 > i37, i55, i20, i37)
Cond_Inc10741(TRUE, i55, i20, i37) → Inc1074(i55 + -1, i20 + -1, i37)
Load848(i20, i37) → Cond_Load8482(i20 + -1 > i37 && i20 > i37, i20, i37)
Cond_Load8482(TRUE, i20, i37) → Inc1074(i20 + -1 + -1, i20 + -1, i37)

The integer pair graph contains the following rules and edges:
(0): LOAD848(i20[0], i37[0]) → COND_LOAD848(i20[0] <= i37[0] && i20[0] > i37[0], i20[0], i37[0])
(2): INC1074(i55[2], i20[2], i37[2]) → COND_INC1074(i20[2] + -1 <= i37[2], i55[2], i20[2], i37[2])
(3): COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3])
(4): LOAD848(i20[4], i37[4]) → COND_LOAD8481(i20[4] + -1 <= i37[4] && i20[4] > i37[4], i20[4], i37[4])
(6): INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(i20[6] + -1 > i37[6], i55[6], i20[6], i37[6])
(7): COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(i55[7] + -1, i20[7] + -1, i37[7])
(8): LOAD848(i20[8], i37[8]) → COND_LOAD8482(i20[8] + -1 > i37[8] && i20[8] > i37[8], i20[8], i37[8])
(9): COND_LOAD8482(TRUE, i20[9], i37[9]) → INC1074(i20[9] + -1 + -1, i20[9] + -1, i37[9])

(0) -> (1), if ((i20[0] <= i37[0] && i20[0] > i37[0]* TRUE)∧(i20[0]* i20[1])∧(i37[0]* i37[1]))

(1) -> (0), if ((i37[1]* i37[0])∧(i20[1]* i20[0]))

(1) -> (4), if ((i37[1]* i37[4])∧(i20[1]* i20[4]))

(1) -> (8), if ((i37[1]* i37[8])∧(i20[1]* i20[8]))

(2) -> (3), if ((i37[2]* i37[3])∧(i55[2]* i55[3])∧(i20[2]* i20[3])∧(i20[2] + -1 <= i37[2]* TRUE))

(3) -> (0), if ((i37[3]* i37[0])∧(i55[3]* i20[0]))

(3) -> (4), if ((i37[3]* i37[4])∧(i55[3]* i20[4]))

(3) -> (8), if ((i55[3]* i20[8])∧(i37[3]* i37[8]))

(4) -> (5), if ((i20[4]* i20[5])∧(i20[4] + -1 <= i37[4] && i20[4] > i37[4]* TRUE)∧(i37[4]* i37[5]))

(5) -> (0), if ((i37[5]* i37[0])∧(i20[5] + -1* i20[0]))

(5) -> (4), if ((i20[5] + -1* i20[4])∧(i37[5]* i37[4]))

(5) -> (8), if ((i37[5]* i37[8])∧(i20[5] + -1* i20[8]))

(6) -> (7), if ((i55[6]* i55[7])∧(i20[6] + -1 > i37[6]* TRUE)∧(i37[6]* i37[7])∧(i20[6]* i20[7]))

(7) -> (2), if ((i55[7] + -1* i55[2])∧(i37[7]* i37[2])∧(i20[7] + -1* i20[2]))

(7) -> (6), if ((i55[7] + -1* i55[6])∧(i20[7] + -1* i20[6])∧(i37[7]* i37[6]))

(8) -> (9), if ((i20[8] + -1 > i37[8] && i20[8] > i37[8]* TRUE)∧(i37[8]* i37[9])∧(i20[8]* i20[9]))

(9) -> (2), if ((i20[9] + -1 + -1* i55[2])∧(i37[9]* i37[2])∧(i20[9] + -1* i20[2]))

(9) -> (6), if ((i20[9] + -1 + -1* i55[6])∧(i37[9]* i37[6])∧(i20[9] + -1* i20[6]))

The set Q consists of the following terms:
Inc1074(x0, x1, x2)
Cond_Inc1074(TRUE, x0, x1, x2)
Cond_Inc10741(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): LOAD848(i20[0], i37[0]) → COND_LOAD848(i20[0] <= i37[0] && i20[0] > i37[0], i20[0], i37[0])
(2): INC1074(i55[2], i20[2], i37[2]) → COND_INC1074(i20[2] + -1 <= i37[2], i55[2], i20[2], i37[2])
(3): COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3])
(4): LOAD848(i20[4], i37[4]) → COND_LOAD8481(i20[4] + -1 <= i37[4] && i20[4] > i37[4], i20[4], i37[4])
(6): INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(i20[6] + -1 > i37[6], i55[6], i20[6], i37[6])
(7): COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(i55[7] + -1, i20[7] + -1, i37[7])
(8): LOAD848(i20[8], i37[8]) → COND_LOAD8482(i20[8] + -1 > i37[8] && i20[8] > i37[8], i20[8], i37[8])
(9): COND_LOAD8482(TRUE, i20[9], i37[9]) → INC1074(i20[9] + -1 + -1, i20[9] + -1, i37[9])

(0) -> (1), if ((i20[0] <= i37[0] && i20[0] > i37[0]* TRUE)∧(i20[0]* i20[1])∧(i37[0]* i37[1]))

(1) -> (0), if ((i37[1]* i37[0])∧(i20[1]* i20[0]))

(1) -> (4), if ((i37[1]* i37[4])∧(i20[1]* i20[4]))

(1) -> (8), if ((i37[1]* i37[8])∧(i20[1]* i20[8]))

(2) -> (3), if ((i37[2]* i37[3])∧(i55[2]* i55[3])∧(i20[2]* i20[3])∧(i20[2] + -1 <= i37[2]* TRUE))

(3) -> (0), if ((i37[3]* i37[0])∧(i55[3]* i20[0]))

(3) -> (4), if ((i37[3]* i37[4])∧(i55[3]* i20[4]))

(3) -> (8), if ((i55[3]* i20[8])∧(i37[3]* i37[8]))

(4) -> (5), if ((i20[4]* i20[5])∧(i20[4] + -1 <= i37[4] && i20[4] > i37[4]* TRUE)∧(i37[4]* i37[5]))

(5) -> (0), if ((i37[5]* i37[0])∧(i20[5] + -1* i20[0]))

(5) -> (4), if ((i20[5] + -1* i20[4])∧(i37[5]* i37[4]))

(5) -> (8), if ((i37[5]* i37[8])∧(i20[5] + -1* i20[8]))

(6) -> (7), if ((i55[6]* i55[7])∧(i20[6] + -1 > i37[6]* TRUE)∧(i37[6]* i37[7])∧(i20[6]* i20[7]))

(7) -> (2), if ((i55[7] + -1* i55[2])∧(i37[7]* i37[2])∧(i20[7] + -1* i20[2]))

(7) -> (6), if ((i55[7] + -1* i55[6])∧(i20[7] + -1* i20[6])∧(i37[7]* i37[6]))

(8) -> (9), if ((i20[8] + -1 > i37[8] && i20[8] > i37[8]* TRUE)∧(i37[8]* i37[9])∧(i20[8]* i20[9]))

(9) -> (2), if ((i20[9] + -1 + -1* i55[2])∧(i37[9]* i37[2])∧(i20[9] + -1* i20[2]))

(9) -> (6), if ((i20[9] + -1 + -1* i55[6])∧(i37[9]* i37[6])∧(i20[9] + -1* i20[6]))

The set Q consists of the following terms:
Inc1074(x0, x1, x2)
Cond_Inc1074(TRUE, x0, x1, x2)
Cond_Inc10741(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 LOAD848(i20, i37) → COND_LOAD848(&&(<=(i20, i37), >(i20, i37)), i20, i37) the following chains were created:
• We consider the chain LOAD848(i20[0], i37[0]) → COND_LOAD848(&&(<=(i20[0], i37[0]), >(i20[0], i37[0])), i20[0], i37[0]), COND_LOAD848(TRUE, i20[1], i37[1]) → LOAD848(i20[1], i37[1]) which results in the following constraint:

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

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

(3)    (i37[0] + [-1]i20[0] ≥ 0∧i20[0] + [-1] + [-1]i37[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD848(&&(<=(i20[0], i37[0]), >(i20[0], i37[0])), i20[0], i37[0])), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i37[0] + [bni_16]i20[0] ≥ 0∧[-2 + (-1)bso_17] ≥ 0)

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

(4)    (i37[0] + [-1]i20[0] ≥ 0∧i20[0] + [-1] + [-1]i37[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD848(&&(<=(i20[0], i37[0]), >(i20[0], i37[0])), i20[0], i37[0])), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i37[0] + [bni_16]i20[0] ≥ 0∧[-2 + (-1)bso_17] ≥ 0)

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

(5)    (i37[0] + [-1]i20[0] ≥ 0∧i20[0] + [-1] + [-1]i37[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD848(&&(<=(i20[0], i37[0]), >(i20[0], i37[0])), i20[0], i37[0])), ≥)∧[(-1)bni_16 + (-1)Bound*bni_16] + [(-1)bni_16]i37[0] + [bni_16]i20[0] ≥ 0∧[-2 + (-1)bso_17] ≥ 0)

We solved constraint (5) using rule (IDP_SMT_SPLIT).

For Pair COND_LOAD848(TRUE, i20, i37) → LOAD848(i20, i37) the following chains were created:
• We consider the chain COND_LOAD848(TRUE, i20[1], i37[1]) → LOAD848(i20[1], i37[1]), LOAD848(i20[0], i37[0]) → COND_LOAD848(&&(<=(i20[0], i37[0]), >(i20[0], i37[0])), i20[0], i37[0]) which results in the following constraint:

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

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

(8)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(9)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(10)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(11)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_19] ≥ 0)

• We consider the chain COND_LOAD848(TRUE, i20[1], i37[1]) → LOAD848(i20[1], i37[1]), LOAD848(i20[4], i37[4]) → COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4]) which results in the following constraint:

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

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

(14)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(15)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(16)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(17)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_19] ≥ 0)

• We consider the chain COND_LOAD848(TRUE, i20[1], i37[1]) → LOAD848(i20[1], i37[1]), LOAD848(i20[8], i37[8]) → COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8]) which results in the following constraint:

We simplified constraint (18) using rule (IV) which results in the following new constraint:

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

(20)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(21)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(22)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧[2 + (-1)bso_19] ≥ 0)

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

(23)    ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_19] ≥ 0)

For Pair INC1074(i55, i20, i37) → COND_INC1074(<=(+(i20, -1), i37), i55, i20, i37) the following chains were created:
• We consider the chain INC1074(i55[2], i20[2], i37[2]) → COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2]), COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3]) which results in the following constraint:

(24)    (i37[2]=i37[3]i55[2]=i55[3]i20[2]=i20[3]<=(+(i20[2], -1), i37[2])=TRUEINC1074(i55[2], i20[2], i37[2])≥NonInfC∧INC1074(i55[2], i20[2], i37[2])≥COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])∧(UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥))

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

(25)    (<=(+(i20[2], -1), i37[2])=TRUEINC1074(i55[2], i20[2], i37[2])≥NonInfC∧INC1074(i55[2], i20[2], i37[2])≥COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])∧(UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥))

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

(26)    (i37[2] + [1] + [-1]i20[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] + [bni_20]i55[2] ≥ 0∧[(-1)bso_21] ≥ 0)

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

(27)    (i37[2] + [1] + [-1]i20[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] + [bni_20]i55[2] ≥ 0∧[(-1)bso_21] ≥ 0)

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

(28)    (i37[2] + [1] + [-1]i20[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] + [bni_20]i55[2] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(29)    (i37[2] + [1] + [-1]i20[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[bni_20] = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

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

(30)    (i20[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[bni_20] = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

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

(31)    (i20[2] ≥ 0∧i37[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[bni_20] = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]i37[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

(32)    (i20[2] ≥ 0∧i37[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[bni_20] = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair COND_INC1074(TRUE, i55, i20, i37) → LOAD848(i55, i37) the following chains were created:
• We consider the chain COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3]), LOAD848(i20[0], i37[0]) → COND_LOAD848(&&(<=(i20[0], i37[0]), >(i20[0], i37[0])), i20[0], i37[0]) which results in the following constraint:

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

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

(35)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(36)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(37)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(38)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• We consider the chain COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3]), LOAD848(i20[4], i37[4]) → COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4]) which results in the following constraint:

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

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

(41)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(42)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(43)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(44)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• We consider the chain COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3]), LOAD848(i20[8], i37[8]) → COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8]) which results in the following constraint:

We simplified constraint (45) using rule (IV) which results in the following new constraint:

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

(47)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(48)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(49)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧[(-1)bso_23] ≥ 0)

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

(50)    ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

For Pair LOAD848(i20, i37) → COND_LOAD8481(&&(<=(+(i20, -1), i37), >(i20, i37)), i20, i37) the following chains were created:
• We consider the chain LOAD848(i20[4], i37[4]) → COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4]), COND_LOAD8481(TRUE, i20[5], i37[5]) → LOAD848(+(i20[5], -1), i37[5]) which results in the following constraint:

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

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

(53)    (i37[4] + [1] + [-1]i20[4] ≥ 0∧i20[4] + [-1] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i37[4] + [bni_24]i20[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(54)    (i37[4] + [1] + [-1]i20[4] ≥ 0∧i20[4] + [-1] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i37[4] + [bni_24]i20[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(55)    (i37[4] + [1] + [-1]i20[4] ≥ 0∧i20[4] + [-1] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i37[4] + [bni_24]i20[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(56)    ([-1]i37[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i37[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(57)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(58)    (0 ≥ 0∧0 ≥ 0∧i20[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

(59)    (0 ≥ 0∧0 ≥ 0∧i20[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

For Pair COND_LOAD8481(TRUE, i20, i37) → LOAD848(+(i20, -1), i37) the following chains were created:
• We consider the chain COND_LOAD8481(TRUE, i20[5], i37[5]) → LOAD848(+(i20[5], -1), i37[5]) which results in the following constraint:

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

(61)    ((UIncreasing(LOAD848(+(i20[5], -1), i37[5])), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(62)    ((UIncreasing(LOAD848(+(i20[5], -1), i37[5])), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(63)    ((UIncreasing(LOAD848(+(i20[5], -1), i37[5])), ≥)∧[1 + (-1)bso_27] ≥ 0)

We simplified constraint (63) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(64)    ((UIncreasing(LOAD848(+(i20[5], -1), i37[5])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

For Pair INC1074(i55, i20, i37) → COND_INC10741(>(+(i20, -1), i37), i55, i20, i37) the following chains were created:
• We consider the chain INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6]), COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7]) which results in the following constraint:

(65)    (i55[6]=i55[7]>(+(i20[6], -1), i37[6])=TRUEi37[6]=i37[7]i20[6]=i20[7]INC1074(i55[6], i20[6], i37[6])≥NonInfC∧INC1074(i55[6], i20[6], i37[6])≥COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])∧(UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥))

We simplified constraint (65) using rule (IV) which results in the following new constraint:

(66)    (>(+(i20[6], -1), i37[6])=TRUEINC1074(i55[6], i20[6], i37[6])≥NonInfC∧INC1074(i55[6], i20[6], i37[6])≥COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])∧(UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥))

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

(67)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] + [bni_28]i55[6] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(68)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] + [bni_28]i55[6] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(69)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] + [bni_28]i55[6] ≥ 0∧[(-1)bso_29] ≥ 0)

We simplified constraint (69) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(70)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

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

(71)    (i20[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

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

(72)    (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

(73)    (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i37[6] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair COND_INC10741(TRUE, i55, i20, i37) → INC1074(+(i55, -1), +(i20, -1), i37) the following chains were created:
• We consider the chain COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7]) which results in the following constraint:

(74)    (COND_INC10741(TRUE, i55[7], i20[7], i37[7])≥NonInfC∧COND_INC10741(TRUE, i55[7], i20[7], i37[7])≥INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])∧(UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥))

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

(75)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧[1 + (-1)bso_31] ≥ 0)

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

(76)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧[1 + (-1)bso_31] ≥ 0)

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

(77)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧[1 + (-1)bso_31] ≥ 0)

We simplified constraint (77) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(78)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

For Pair LOAD848(i20, i37) → COND_LOAD8482(&&(>(+(i20, -1), i37), >(i20, i37)), i20, i37) the following chains were created:
• We consider the chain LOAD848(i20[8], i37[8]) → COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8]), COND_LOAD8482(TRUE, i20[9], i37[9]) → INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9]) which results in the following constraint:

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

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

(81)    (i20[8] + [-2] + [-1]i37[8] ≥ 0∧i20[8] + [-1] + [-1]i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]i37[8] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(82)    (i20[8] + [-2] + [-1]i37[8] ≥ 0∧i20[8] + [-1] + [-1]i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]i37[8] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(83)    (i20[8] + [-2] + [-1]i37[8] ≥ 0∧i20[8] + [-1] + [-1]i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[(-1)bni_32 + (-1)Bound*bni_32] + [(-1)bni_32]i37[8] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(84)    (i20[8] ≥ 0∧[1] + i20[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(85)    (i20[8] ≥ 0∧[1] + i20[8] ≥ 0∧i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

(86)    (i20[8] ≥ 0∧[1] + i20[8] ≥ 0∧i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

For Pair COND_LOAD8482(TRUE, i20, i37) → INC1074(+(+(i20, -1), -1), +(i20, -1), i37) the following chains were created:
• We consider the chain COND_LOAD8482(TRUE, i20[9], i37[9]) → INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9]) which results in the following constraint:

(87)    (COND_LOAD8482(TRUE, i20[9], i37[9])≥NonInfC∧COND_LOAD8482(TRUE, i20[9], i37[9])≥INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])∧(UIncreasing(INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])), ≥))

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

(88)    ((UIncreasing(INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])), ≥)∧[2 + (-1)bso_35] ≥ 0)

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

(89)    ((UIncreasing(INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])), ≥)∧[2 + (-1)bso_35] ≥ 0)

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

(90)    ((UIncreasing(INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])), ≥)∧[2 + (-1)bso_35] ≥ 0)

We simplified constraint (90) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(91)    ((UIncreasing(INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_35] ≥ 0)

To summarize, we get the following constraints P for the following pairs.

• ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_19] ≥ 0)
• ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_19] ≥ 0)
• ((UIncreasing(LOAD848(i20[1], i37[1])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_19] ≥ 0)

• INC1074(i55, i20, i37) → COND_INC1074(<=(+(i20, -1), i37), i55, i20, i37)
• (i20[2] ≥ 0∧i37[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[bni_20] = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [bni_20]i37[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)
• (i20[2] ≥ 0∧i37[2] ≥ 0 ⇒ (UIncreasing(COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])), ≥)∧[bni_20] = 0∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]i37[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

• COND_INC1074(TRUE, i55, i20, i37) → LOAD848(i55, i37)
• ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)
• ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)
• ((UIncreasing(LOAD848(i55[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• (0 ≥ 0∧0 ≥ 0∧i20[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)
• (0 ≥ 0∧0 ≥ 0∧i20[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD8481(&&(<=(+(i20[4], -1), i37[4]), >(i20[4], i37[4])), i20[4], i37[4])), ≥)∧[(-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

• ((UIncreasing(LOAD848(+(i20[5], -1), i37[5])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

• INC1074(i55, i20, i37) → COND_INC10741(>(+(i20, -1), i37), i55, i20, i37)
• (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i37[6] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)
• (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[bni_28] = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i37[6] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

• COND_INC10741(TRUE, i55, i20, i37) → INC1074(+(i55, -1), +(i20, -1), i37)
• ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

• (i20[8] ≥ 0∧[1] + i20[8] ≥ 0∧i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)
• (i20[8] ≥ 0∧[1] + i20[8] ≥ 0∧i37[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD8482(&&(>(+(i20[8], -1), i37[8]), >(i20[8], i37[8])), i20[8], i37[8])), ≥)∧[bni_32 + (-1)Bound*bni_32] + [bni_32]i20[8] ≥ 0∧[(-1)bso_33] ≥ 0)

• COND_LOAD8482(TRUE, i20, i37) → INC1074(+(+(i20, -1), -1), +(i20, -1), i37)
• ((UIncreasing(INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])), ≥)∧0 = 0∧0 = 0∧[2 + (-1)bso_35] ≥ 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(LOAD848(x1, x2)) = [-1] + [-1]x2 + x1
POL(COND_LOAD848(x1, x2, x3)) = [1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(INC1074(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(COND_INC1074(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_LOAD8481(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(COND_INC10741(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(COND_LOAD8482(x1, x2, x3)) = [-1] + [-1]x3 + x2

The following pairs are in P>:

COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])
COND_LOAD8482(TRUE, i20[9], i37[9]) → INC1074(+(+(i20[9], -1), -1), +(i20[9], -1), i37[9])

The following pairs are in Pbound:

The following pairs are in P:

INC1074(i55[2], i20[2], i37[2]) → COND_INC1074(<=(+(i20[2], -1), i37[2]), i55[2], i20[2], i37[2])
COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3])
INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])

There are no usable rules.

### (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:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1074(i55[2], i20[2], i37[2]) → COND_INC1074(i20[2] + -1 <= i37[2], i55[2], i20[2], i37[2])
(3): COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3])
(4): LOAD848(i20[4], i37[4]) → COND_LOAD8481(i20[4] + -1 <= i37[4] && i20[4] > i37[4], i20[4], i37[4])
(6): INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(i20[6] + -1 > i37[6], i55[6], i20[6], i37[6])
(8): LOAD848(i20[8], i37[8]) → COND_LOAD8482(i20[8] + -1 > i37[8] && i20[8] > i37[8], i20[8], i37[8])

(2) -> (3), if ((i37[2]* i37[3])∧(i55[2]* i55[3])∧(i20[2]* i20[3])∧(i20[2] + -1 <= i37[2]* TRUE))

(3) -> (4), if ((i37[3]* i37[4])∧(i55[3]* i20[4]))

(3) -> (8), if ((i55[3]* i20[8])∧(i37[3]* i37[8]))

The set Q consists of the following terms:
Inc1074(x0, x1, x2)
Cond_Inc1074(TRUE, x0, x1, x2)
Cond_Inc10741(TRUE, x0, x1, x2)

### (12) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1074(i55[2], i20[2], i37[2]) → COND_INC1074(i20[2] + -1 <= i37[2], i55[2], i20[2], i37[2])
(3): COND_INC1074(TRUE, i55[3], i20[3], i37[3]) → LOAD848(i55[3], i37[3])
(6): INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(i20[6] + -1 > i37[6], i55[6], i20[6], i37[6])
(7): COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(i55[7] + -1, i20[7] + -1, i37[7])
(9): COND_LOAD8482(TRUE, i20[9], i37[9]) → INC1074(i20[9] + -1 + -1, i20[9] + -1, i37[9])

(7) -> (2), if ((i55[7] + -1* i55[2])∧(i37[7]* i37[2])∧(i20[7] + -1* i20[2]))

(9) -> (2), if ((i20[9] + -1 + -1* i55[2])∧(i37[9]* i37[2])∧(i20[9] + -1* i20[2]))

(2) -> (3), if ((i37[2]* i37[3])∧(i55[2]* i55[3])∧(i20[2]* i20[3])∧(i20[2] + -1 <= i37[2]* TRUE))

(7) -> (6), if ((i55[7] + -1* i55[6])∧(i20[7] + -1* i20[6])∧(i37[7]* i37[6]))

(9) -> (6), if ((i20[9] + -1 + -1* i55[6])∧(i37[9]* i37[6])∧(i20[9] + -1* i20[6]))

(6) -> (7), if ((i55[6]* i55[7])∧(i20[6] + -1 > i37[6]* TRUE)∧(i37[6]* i37[7])∧(i20[6]* i20[7]))

The set Q consists of the following terms:
Inc1074(x0, x1, x2)
Cond_Inc1074(TRUE, x0, x1, x2)
Cond_Inc10741(TRUE, x0, x1, x2)

### (15) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 5 less nodes.

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

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(7): COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(i55[7] + -1, i20[7] + -1, i37[7])
(6): INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(i20[6] + -1 > i37[6], i55[6], i20[6], i37[6])

(7) -> (6), if ((i55[7] + -1* i55[6])∧(i20[7] + -1* i20[6])∧(i37[7]* i37[6]))

(6) -> (7), if ((i55[6]* i55[7])∧(i20[6] + -1 > i37[6]* TRUE)∧(i37[6]* i37[7])∧(i20[6]* i20[7]))

The set Q consists of the following terms:
Inc1074(x0, x1, x2)
Cond_Inc1074(TRUE, x0, x1, x2)
Cond_Inc10741(TRUE, x0, x1, x2)

### (17) 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 COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7]) the following chains were created:
• We consider the chain COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7]) which results in the following constraint:

(1)    (COND_INC10741(TRUE, i55[7], i20[7], i37[7])≥NonInfC∧COND_INC10741(TRUE, i55[7], i20[7], i37[7])≥INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])∧(UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥))

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

(2)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧[(-1)bso_8] ≥ 0)

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

(3)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧[(-1)bso_8] ≥ 0)

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

(4)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧[(-1)bso_8] ≥ 0)

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

(5)    ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_8] ≥ 0)

For Pair INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6]) the following chains were created:
• We consider the chain INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6]), COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7]) which results in the following constraint:

(6)    (i55[6]=i55[7]>(+(i20[6], -1), i37[6])=TRUEi37[6]=i37[7]i20[6]=i20[7]INC1074(i55[6], i20[6], i37[6])≥NonInfC∧INC1074(i55[6], i20[6], i37[6])≥COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])∧(UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥))

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

(7)    (>(+(i20[6], -1), i37[6])=TRUEINC1074(i55[6], i20[6], i37[6])≥NonInfC∧INC1074(i55[6], i20[6], i37[6])≥COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])∧(UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥))

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

(8)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[(-1)Bound*bni_9] + [bni_9]i20[6] + [(-1)bni_9]i37[6] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

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

(9)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[(-1)Bound*bni_9] + [bni_9]i20[6] + [(-1)bni_9]i37[6] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

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

(10)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧[(-1)Bound*bni_9] + [bni_9]i20[6] + [(-1)bni_9]i37[6] ≥ 0∧[1 + (-1)bso_10] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(11)    (i20[6] + [-2] + [-1]i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧0 = 0∧[(-1)Bound*bni_9] + [bni_9]i20[6] + [(-1)bni_9]i37[6] ≥ 0∧0 = 0∧[1 + (-1)bso_10] ≥ 0)

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

(12)    (i20[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧0 = 0∧[(-1)Bound*bni_9 + (2)bni_9] + [bni_9]i20[6] ≥ 0∧0 = 0∧[1 + (-1)bso_10] ≥ 0)

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

(13)    (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧0 = 0∧[(-1)Bound*bni_9 + (2)bni_9] + [bni_9]i20[6] ≥ 0∧0 = 0∧[1 + (-1)bso_10] ≥ 0)

(14)    (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧0 = 0∧[(-1)Bound*bni_9 + (2)bni_9] + [bni_9]i20[6] ≥ 0∧0 = 0∧[1 + (-1)bso_10] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])
• ((UIncreasing(INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_8] ≥ 0)

• INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])
• (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧0 = 0∧[(-1)Bound*bni_9 + (2)bni_9] + [bni_9]i20[6] ≥ 0∧0 = 0∧[1 + (-1)bso_10] ≥ 0)
• (i20[6] ≥ 0∧i37[6] ≥ 0 ⇒ (UIncreasing(COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])), ≥)∧0 = 0∧[(-1)Bound*bni_9 + (2)bni_9] + [bni_9]i20[6] ≥ 0∧0 = 0∧[1 + (-1)bso_10] ≥ 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(COND_INC10741(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(INC1074(x1, x2, x3)) = x2 + [-1]x3
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]

The following pairs are in P>:

INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])

The following pairs are in Pbound:

INC1074(i55[6], i20[6], i37[6]) → COND_INC10741(>(+(i20[6], -1), i37[6]), i55[6], i20[6], i37[6])

The following pairs are in P:

COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(+(i55[7], -1), +(i20[7], -1), i37[7])

There are no usable rules.

### (18) 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:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(7): COND_INC10741(TRUE, i55[7], i20[7], i37[7]) → INC1074(i55[7] + -1, i20[7] + -1, i37[7])

The set Q consists of the following terms: