### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: LogAG
`public class LogAG{  // adapted from Arts&Giesl, 2001  public static int half(int x) {    int res = 0;    while (x > 1) {      x = x-2;      res++;    }    return res;  }  public static int log(int x) {    int res = 0;    while (x > 1) {      x = half(x-2)+1;      res++;    }    return res;  }  public static void main(String[] args) {    Random.args = args;    int x  = Random.random();    log(x);  }}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 161 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:
Load1158(1, i70, i133, i123) → Cond_Load1158(i133 > 1 && i123 + 1 > 0, 1, i70, i133, i123)
Cond_Load1158(TRUE, 1, i70, i133, i123) → Load1158(1, i70, i133 - 2, i123 + 1)
Load1158(1, i70, i133, i123) → Cond_Load11581(i133 > 0 && i133 <= 1, 1, i70, i133, i123)
Load1158(1, i70, i132, i123) → Cond_Load11582(i132 <= 1 && i70 + 1 > 0 && i123 + 1 > 0, 1, i70, i132, i123)
Cond_Load11582(TRUE, 1, i70, i132, i123) → Load945(1, i123 + 1, i70 + 1)
The set Q consists of the following terms:

### (5) GroundTermsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they always contain the same ground term.
We removed the following ground terms:
• 1

We removed arguments according to the following replacements:

### (6) 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:
Load1158(i70, i133, i123) → Cond_Load1158(i133 > 1 && i123 + 1 > 0, i70, i133, i123)
Cond_Load1158(TRUE, i70, i133, i123) → Load1158(i70, i133 - 2, i123 + 1)
Load1158(i70, i133, i123) → Cond_Load11581(i133 > 0 && i133 <= 1, i70, i133, i123)
Load1158(i70, i132, i123) → Cond_Load11582(i132 <= 1 && i70 + 1 > 0 && i123 + 1 > 0, i70, i132, i123)
The set Q consists of the following terms:

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

Integer, Boolean

The ITRS R consists of the following rules:
Load1158(i70, i133, i123) → Cond_Load1158(i133 > 1 && i123 + 1 > 0, i70, i133, i123)
Cond_Load1158(TRUE, i70, i133, i123) → Load1158(i70, i133 - 2, i123 + 1)
Load1158(i70, i133, i123) → Cond_Load11581(i133 > 0 && i133 <= 1, i70, i133, i123)
Load1158(i70, i132, i123) → Cond_Load11582(i132 <= 1 && i70 + 1 > 0 && i123 + 1 > 0, i70, i132, i123)

The integer pair graph contains the following rules and edges:
(2): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])
(3): COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], i133[3] - 2, i123[3] + 1)
(4): LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(i133[4] > 0 && i133[4] <= 1, i70[4], i133[4], i123[4])
(7): LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0, i70[7], i132[7], i123[7])
(8): COND_LOAD11582(TRUE, i70[8], i132[8], i123[8]) → LOAD945(i123[8] + 1, i70[8] + 1)

(0) -> (1), if ((i80[0]* i80[1])∧(i80[0] > 1* TRUE)∧(i70[0]* i70[1]))

(1) -> (2), if ((0* i123[2])∧(i80[1] - 2* i133[2])∧(i70[1]* i70[2]))

(1) -> (4), if ((i70[1]* i70[4])∧(i80[1] - 2* i133[4])∧(0* i123[4]))

(1) -> (7), if ((0* i123[7])∧(i70[1]* i70[7])∧(i80[1] - 2* i132[7]))

(2) -> (3), if ((i133[2] > 1 && i123[2] + 1 > 0* TRUE)∧(i123[2]* i123[3])∧(i133[2]* i133[3])∧(i70[2]* i70[3]))

(3) -> (2), if ((i70[3]* i70[2])∧(i133[3] - 2* i133[2])∧(i123[3] + 1* i123[2]))

(3) -> (4), if ((i70[3]* i70[4])∧(i133[3] - 2* i133[4])∧(i123[3] + 1* i123[4]))

(3) -> (7), if ((i123[3] + 1* i123[7])∧(i70[3]* i70[7])∧(i133[3] - 2* i132[7]))

(4) -> (5), if ((i133[4] > 0 && i133[4] <= 1* TRUE)∧(i133[4]* i133[5])∧(i70[4]* i70[5])∧(i123[4]* i123[5]))

(5) -> (6), if ((i123[5]* i123[6])∧(i70[5]* i70[6]))

(6) -> (0), if ((i123[6] + 1* i80[0])∧(i70[6] + 1* i70[0]))

(7) -> (8), if ((i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0* TRUE)∧(i70[7]* i70[8])∧(i123[7]* i123[8])∧(i132[7]* i132[8]))

(8) -> (0), if ((i123[8] + 1* i80[0])∧(i70[8] + 1* i70[0]))

The set Q consists of the following terms:

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

### (10) 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): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])
(3): COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], i133[3] - 2, i123[3] + 1)
(4): LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(i133[4] > 0 && i133[4] <= 1, i70[4], i133[4], i123[4])
(7): LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0, i70[7], i132[7], i123[7])
(8): COND_LOAD11582(TRUE, i70[8], i132[8], i123[8]) → LOAD945(i123[8] + 1, i70[8] + 1)

(0) -> (1), if ((i80[0]* i80[1])∧(i80[0] > 1* TRUE)∧(i70[0]* i70[1]))

(1) -> (2), if ((0* i123[2])∧(i80[1] - 2* i133[2])∧(i70[1]* i70[2]))

(1) -> (4), if ((i70[1]* i70[4])∧(i80[1] - 2* i133[4])∧(0* i123[4]))

(1) -> (7), if ((0* i123[7])∧(i70[1]* i70[7])∧(i80[1] - 2* i132[7]))

(2) -> (3), if ((i133[2] > 1 && i123[2] + 1 > 0* TRUE)∧(i123[2]* i123[3])∧(i133[2]* i133[3])∧(i70[2]* i70[3]))

(3) -> (2), if ((i70[3]* i70[2])∧(i133[3] - 2* i133[2])∧(i123[3] + 1* i123[2]))

(3) -> (4), if ((i70[3]* i70[4])∧(i133[3] - 2* i133[4])∧(i123[3] + 1* i123[4]))

(3) -> (7), if ((i123[3] + 1* i123[7])∧(i70[3]* i70[7])∧(i133[3] - 2* i132[7]))

(4) -> (5), if ((i133[4] > 0 && i133[4] <= 1* TRUE)∧(i133[4]* i133[5])∧(i70[4]* i70[5])∧(i123[4]* i123[5]))

(5) -> (6), if ((i123[5]* i123[6])∧(i70[5]* i70[6]))

(6) -> (0), if ((i123[6] + 1* i80[0])∧(i70[6] + 1* i70[0]))

(7) -> (8), if ((i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0* TRUE)∧(i70[7]* i70[8])∧(i123[7]* i123[8])∧(i132[7]* i132[8]))

(8) -> (0), if ((i123[8] + 1* i80[0])∧(i70[8] + 1* i70[0]))

The set Q consists of the following terms:

### (11) 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 LOAD945(i80, i70) → COND_LOAD945(>(i80, 1), i80, i70) the following chains were created:
• We consider the chain LOAD945(i80[0], i70[0]) → COND_LOAD945(>(i80[0], 1), i80[0], i70[0]), COND_LOAD945(TRUE, i80[1], i70[1]) → LOAD1158(i70[1], -(i80[1], 2), 0) which results in the following constraint:

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

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

(3)    (i80[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD945(>(i80[0], 1), i80[0], i70[0])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [bni_35]i80[0] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(4)    (i80[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD945(>(i80[0], 1), i80[0], i70[0])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [bni_35]i80[0] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(5)    (i80[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD945(>(i80[0], 1), i80[0], i70[0])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [bni_35]i80[0] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(6)    (i80[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD945(>(i80[0], 1), i80[0], i70[0])), ≥)∧0 = 0∧[(-1)bni_35 + (-1)Bound*bni_35] + [bni_35]i80[0] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

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

(7)    (i80[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD945(>(i80[0], 1), i80[0], i70[0])), ≥)∧0 = 0∧[bni_35 + (-1)Bound*bni_35] + [bni_35]i80[0] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

For Pair COND_LOAD945(TRUE, i80, i70) → LOAD1158(i70, -(i80, 2), 0) the following chains were created:

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

(9)    (>(+(i123[6], 1), 1)=TRUE>(-(+(i123[6], 1), 2), 1)=TRUECOND_LOAD945(TRUE, +(i123[6], 1), +(i70[6], 1))≥NonInfC∧COND_LOAD945(TRUE, +(i123[6], 1), +(i70[6], 1))≥LOAD1158(+(i70[6], 1), -(+(i123[6], 1), 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(10)    (i123[6] + [-1] ≥ 0∧i123[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(11)    (i123[6] + [-1] ≥ 0∧i123[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(12)    (i123[6] + [-1] ≥ 0∧i123[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(13)    (i123[6] + [-1] ≥ 0∧i123[6] + [-3] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

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

(14)    (i123[6] ≥ 0∧[-2] + i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

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

(15)    ([2] + i123[6] ≥ 0∧i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (3)bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

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

(17)    (>(+(i123[6], 1), 1)=TRUE>(-(+(i123[6], 1), 2), 0)=TRUE<=(-(+(i123[6], 1), 2), 1)=TRUECOND_LOAD945(TRUE, +(i123[6], 1), +(i70[6], 1))≥NonInfC∧COND_LOAD945(TRUE, +(i123[6], 1), +(i70[6], 1))≥LOAD1158(+(i70[6], 1), -(+(i123[6], 1), 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(18)    (i123[6] + [-1] ≥ 0∧i123[6] + [-2] ≥ 0∧[2] + [-1]i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(19)    (i123[6] + [-1] ≥ 0∧i123[6] + [-2] ≥ 0∧[2] + [-1]i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(20)    (i123[6] + [-1] ≥ 0∧i123[6] + [-2] ≥ 0∧[2] + [-1]i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(21)    (i123[6] + [-1] ≥ 0∧i123[6] + [-2] ≥ 0∧[2] + [-1]i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

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

(22)    (i123[6] ≥ 0∧[-1] + i123[6] ≥ 0∧[1] + [-1]i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

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

(23)    ([1] + i123[6] ≥ 0∧i123[6] ≥ 0∧[-1]i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

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

(24)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (2)bni_37] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)

(25)    (i123[5]=i123[6]i70[5]=i70[6]+(i123[6], 1)=i80[0]+(i70[6], 1)=i70[0]i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[7]i70[1]=i70[7]-(i80[1], 2)=i132[7]&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]COND_LOAD945(TRUE, i80[1], i70[1])≥NonInfC∧COND_LOAD945(TRUE, i80[1], i70[1])≥LOAD1158(i70[1], -(i80[1], 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(26)    (>(+(i123[6], 1), 1)=TRUE<=(-(+(i123[6], 1), 2), 1)=TRUE>(+(+(i70[6], 1), 1), 0)=TRUECOND_LOAD945(TRUE, +(i123[6], 1), +(i70[6], 1))≥NonInfC∧COND_LOAD945(TRUE, +(i123[6], 1), +(i70[6], 1))≥LOAD1158(+(i70[6], 1), -(+(i123[6], 1), 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(27)    (i123[6] + [-1] ≥ 0∧[2] + [-1]i123[6] ≥ 0∧i70[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(28)    (i123[6] + [-1] ≥ 0∧[2] + [-1]i123[6] ≥ 0∧i70[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(29)    (i123[6] + [-1] ≥ 0∧[2] + [-1]i123[6] ≥ 0∧i70[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(30)    (i123[6] ≥ 0∧[1] + [-1]i123[6] ≥ 0∧i70[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(31)    (i123[6] ≥ 0∧[1] + [-1]i123[6] ≥ 0∧[-1]i70[6] + [1] ≥ 0∧i70[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

(32)    (i123[6] ≥ 0∧[1] + [-1]i123[6] ≥ 0∧i70[6] + [1] ≥ 0∧i70[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

(33)    (&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]+(i123[8], 1)=i80[0]+(i70[8], 1)=i70[0]i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[2]-(i80[1], 2)=i133[2]i70[1]=i70[2]&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]COND_LOAD945(TRUE, i80[1], i70[1])≥NonInfC∧COND_LOAD945(TRUE, i80[1], i70[1])≥LOAD1158(i70[1], -(i80[1], 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(34)    (>(+(i123[7], 1), 1)=TRUE>(+(i123[7], 1), 0)=TRUE>(-(+(i123[7], 1), 2), 1)=TRUE<=(i132[7], 1)=TRUE>(+(i70[7], 1), 0)=TRUECOND_LOAD945(TRUE, +(i123[7], 1), +(i70[7], 1))≥NonInfC∧COND_LOAD945(TRUE, +(i123[7], 1), +(i70[7], 1))≥LOAD1158(+(i70[7], 1), -(+(i123[7], 1), 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(35)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧i123[7] + [-3] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(36)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧i123[7] + [-3] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(37)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧i123[7] + [-3] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(38)    (i123[7] ≥ 0∧[1] + i123[7] ≥ 0∧[-2] + i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(39)    ([2] + i123[7] ≥ 0∧[3] + i123[7] ≥ 0∧i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (3)bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(40)    ([2] + i123[7] ≥ 0∧[3] + i123[7] ≥ 0∧i123[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (3)bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

(41)    (&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]+(i123[8], 1)=i80[0]+(i70[8], 1)=i70[0]i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]i70[1]=i70[4]-(i80[1], 2)=i133[4]0=i123[4]&&(>(i133[4], 0), <=(i133[4], 1))=TRUEi133[4]=i133[5]i70[4]=i70[5]i123[4]=i123[5]COND_LOAD945(TRUE, i80[1], i70[1])≥NonInfC∧COND_LOAD945(TRUE, i80[1], i70[1])≥LOAD1158(i70[1], -(i80[1], 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(42)    (>(+(i123[7], 1), 1)=TRUE>(+(i123[7], 1), 0)=TRUE>(-(+(i123[7], 1), 2), 0)=TRUE<=(-(+(i123[7], 1), 2), 1)=TRUE<=(i132[7], 1)=TRUE>(+(i70[7], 1), 0)=TRUECOND_LOAD945(TRUE, +(i123[7], 1), +(i70[7], 1))≥NonInfC∧COND_LOAD945(TRUE, +(i123[7], 1), +(i70[7], 1))≥LOAD1158(+(i70[7], 1), -(+(i123[7], 1), 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(43)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧i123[7] + [-2] ≥ 0∧[2] + [-1]i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(44)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧i123[7] + [-2] ≥ 0∧[2] + [-1]i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(45)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧i123[7] + [-2] ≥ 0∧[2] + [-1]i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(46)    (i123[7] ≥ 0∧[1] + i123[7] ≥ 0∧[-1] + i123[7] ≥ 0∧[1] + [-1]i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(47)    ([1] + i123[7] ≥ 0∧[2] + i123[7] ≥ 0∧i123[7] ≥ 0∧[-1]i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(48)    ([1] ≥ 0∧[2] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(49)    ([1] ≥ 0∧[2] ≥ 0∧0 ≥ 0∧0 ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(50)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧i70[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

(51)    (&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]+(i123[8], 1)=i80[0]+(i70[8], 1)=i70[0]i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[7]1i70[1]=i70[7]1-(i80[1], 2)=i132[7]1&&(&&(<=(i132[7]1, 1), >(+(i70[7]1, 1), 0)), >(+(i123[7]1, 1), 0))=TRUEi70[7]1=i70[8]1i123[7]1=i123[8]1i132[7]1=i132[8]1COND_LOAD945(TRUE, i80[1], i70[1])≥NonInfC∧COND_LOAD945(TRUE, i80[1], i70[1])≥LOAD1158(i70[1], -(i80[1], 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(52)    (>(+(i123[7], 1), 1)=TRUE>(+(i123[7], 1), 0)=TRUE<=(i132[7], 1)=TRUE>(+(i70[7], 1), 0)=TRUE<=(-(+(i123[7], 1), 2), 1)=TRUE>(+(+(i70[7], 1), 1), 0)=TRUECOND_LOAD945(TRUE, +(i123[7], 1), +(i70[7], 1))≥NonInfC∧COND_LOAD945(TRUE, +(i123[7], 1), +(i70[7], 1))≥LOAD1158(+(i70[7], 1), -(+(i123[7], 1), 2), 0)∧(UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥))

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

(53)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0∧[2] + [-1]i123[7] ≥ 0∧i70[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(54)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0∧[2] + [-1]i123[7] ≥ 0∧i70[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(55)    (i123[7] + [-1] ≥ 0∧i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0∧[2] + [-1]i123[7] ≥ 0∧i70[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(56)    (i123[7] ≥ 0∧[1] + i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0∧[1] + [-1]i123[7] ≥ 0∧i70[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

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

(57)    (i123[7] ≥ 0∧[1] + i123[7] ≥ 0∧i70[7] ≥ 0∧[1] + [-1]i123[7] ≥ 0∧i70[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

For Pair LOAD1158(i70, i133, i123) → COND_LOAD1158(&&(>(i133, 1), >(+(i123, 1), 0)), i70, i133, i123) the following chains were created:
• We consider the chain LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2]), COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1)) which results in the following constraint:

(58)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]LOAD1158(i70[2], i133[2], i123[2])≥NonInfC∧LOAD1158(i70[2], i133[2], i123[2])≥COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])∧(UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥))

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

(59)    (>(i133[2], 1)=TRUE>(+(i123[2], 1), 0)=TRUELOAD1158(i70[2], i133[2], i123[2])≥NonInfC∧LOAD1158(i70[2], i133[2], i123[2])≥COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])∧(UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥))

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

(60)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i123[2] + [bni_39]i133[2] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(61)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i123[2] + [bni_39]i133[2] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(62)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i123[2] + [bni_39]i133[2] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(63)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧0 = 0∧[(-1)Bound*bni_39] + [bni_39]i123[2] + [bni_39]i133[2] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)

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

(64)    (i133[2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧0 = 0∧[(-1)Bound*bni_39 + (2)bni_39] + [bni_39]i123[2] + [bni_39]i133[2] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)

For Pair COND_LOAD1158(TRUE, i70, i133, i123) → LOAD1158(i70, -(i133, 2), +(i123, 1)) the following chains were created:

(65)    (i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[2]-(i80[1], 2)=i133[2]i70[1]=i70[2]&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]i70[3]=i70[2]1-(i133[3], 2)=i133[2]1+(i123[3], 1)=i123[2]1&&(>(i133[2]1, 1), >(+(i123[2]1, 1), 0))=TRUEi123[2]1=i123[3]1i133[2]1=i133[3]1i70[2]1=i70[3]1COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥NonInfC∧COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

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

(66)    (>(i80[0], 1)=TRUE>(-(i80[0], 2), 1)=TRUE>(-(-(i80[0], 2), 2), 1)=TRUECOND_LOAD1158(TRUE, i70[0], -(i80[0], 2), 0)≥NonInfC∧COND_LOAD1158(TRUE, i70[0], -(i80[0], 2), 0)≥LOAD1158(i70[0], -(-(i80[0], 2), 2), +(0, 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

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

(67)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(68)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(69)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(70)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(71)    (i80[0] ≥ 0∧[-2] + i80[0] ≥ 0∧[-4] + i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(72)    ([2] + i80[0] ≥ 0∧i80[0] ≥ 0∧[-2] + i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(73)    ([4] + i80[0] ≥ 0∧[2] + i80[0] ≥ 0∧i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

(74)    (i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[2]-(i80[1], 2)=i133[2]i70[1]=i70[2]&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]i70[3]=i70[4]-(i133[3], 2)=i133[4]+(i123[3], 1)=i123[4]&&(>(i133[4], 0), <=(i133[4], 1))=TRUEi133[4]=i133[5]i70[4]=i70[5]i123[4]=i123[5]COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥NonInfC∧COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

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

(75)    (>(i80[0], 1)=TRUE>(-(i80[0], 2), 1)=TRUE>(-(-(i80[0], 2), 2), 0)=TRUE<=(-(-(i80[0], 2), 2), 1)=TRUECOND_LOAD1158(TRUE, i70[0], -(i80[0], 2), 0)≥NonInfC∧COND_LOAD1158(TRUE, i70[0], -(i80[0], 2), 0)≥LOAD1158(i70[0], -(-(i80[0], 2), 2), +(0, 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

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

(76)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-5] ≥ 0∧[5] + [-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(77)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-5] ≥ 0∧[5] + [-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(78)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-5] ≥ 0∧[5] + [-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(79)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧i80[0] + [-5] ≥ 0∧[5] + [-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(80)    (i80[0] ≥ 0∧[-2] + i80[0] ≥ 0∧[-3] + i80[0] ≥ 0∧[3] + [-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(81)    ([2] + i80[0] ≥ 0∧i80[0] ≥ 0∧[-1] + i80[0] ≥ 0∧[1] + [-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(82)    ([3] + i80[0] ≥ 0∧[1] + i80[0] ≥ 0∧i80[0] ≥ 0∧[-1]i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(83)    ([3] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(84)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

(85)    (i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[2]-(i80[1], 2)=i133[2]i70[1]=i70[2]&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]+(i123[3], 1)=i123[7]i70[3]=i70[7]-(i133[3], 2)=i132[7]&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥NonInfC∧COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

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

(86)    (>(i80[0], 1)=TRUE>(-(i80[0], 2), 1)=TRUE<=(-(-(i80[0], 2), 2), 1)=TRUE>(+(i70[7], 1), 0)=TRUECOND_LOAD1158(TRUE, i70[7], -(i80[0], 2), 0)≥NonInfC∧COND_LOAD1158(TRUE, i70[7], -(i80[0], 2), 0)≥LOAD1158(i70[7], -(-(i80[0], 2), 2), +(0, 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

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

(87)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧[5] + [-1]i80[0] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(88)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧[5] + [-1]i80[0] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(89)    (i80[0] + [-2] ≥ 0∧i80[0] + [-4] ≥ 0∧[5] + [-1]i80[0] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(90)    (i80[0] ≥ 0∧[-2] + i80[0] ≥ 0∧[3] + [-1]i80[0] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(91)    ([2] + i80[0] ≥ 0∧i80[0] ≥ 0∧[1] + [-1]i80[0] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)

(92)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]i70[3]=i70[2]1-(i133[3], 2)=i133[2]1+(i123[3], 1)=i123[2]1&&(>(i133[2]1, 1), >(+(i123[2]1, 1), 0))=TRUEi123[2]1=i123[3]1i133[2]1=i133[3]1i70[2]1=i70[3]1i70[3]1=i70[2]2-(i133[3]1, 2)=i133[2]2+(i123[3]1, 1)=i123[2]2&&(>(i133[2]2, 1), >(+(i123[2]2, 1), 0))=TRUEi123[2]2=i123[3]2i133[2]2=i133[3]2i70[2]2=i70[3]2COND_LOAD1158(TRUE, i70[3]1, i133[3]1, i123[3]1)≥NonInfC∧COND_LOAD1158(TRUE, i70[3]1, i133[3]1, i123[3]1)≥LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))∧(UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥))

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

(93)    (>(i133[2], 1)=TRUE>(+(i123[2], 1), 0)=TRUE>(-(i133[2], 2), 1)=TRUE>(+(+(i123[2], 1), 1), 0)=TRUE>(-(-(i133[2], 2), 2), 1)=TRUE>(+(+(+(i123[2], 1), 1), 1), 0)=TRUECOND_LOAD1158(TRUE, i70[2], -(i133[2], 2), +(i123[2], 1))≥NonInfC∧COND_LOAD1158(TRUE, i70[2], -(i133[2], 2), +(i123[2], 1))≥LOAD1158(i70[2], -(-(i133[2], 2), 2), +(+(i123[2], 1), 1))∧(UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥))

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

(94)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-6] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(95)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-6] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(96)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-6] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(97)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-6] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(98)    (i133[2] ≥ 0∧i123[2] ≥ 0∧[-2] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧[-4] + i133[2] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(99)    ([2] + i133[2] ≥ 0∧i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧[-2] + i133[2] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(100)    ([4] + i133[2] ≥ 0∧i123[2] ≥ 0∧[2] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] ≥ 0∧i123[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(4)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

We simplified constraint (100) using rule (IDP_POLY_GCD) which results in the following new constraint:

(101)    ([4] + i133[2] ≥ 0∧i123[2] ≥ 0∧[2] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(4)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

(102)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]i70[3]=i70[2]1-(i133[3], 2)=i133[2]1+(i123[3], 1)=i123[2]1&&(>(i133[2]1, 1), >(+(i123[2]1, 1), 0))=TRUEi123[2]1=i123[3]1i133[2]1=i133[3]1i70[2]1=i70[3]1i70[3]1=i70[4]-(i133[3]1, 2)=i133[4]+(i123[3]1, 1)=i123[4]&&(>(i133[4], 0), <=(i133[4], 1))=TRUEi133[4]=i133[5]i70[4]=i70[5]i123[4]=i123[5]COND_LOAD1158(TRUE, i70[3]1, i133[3]1, i123[3]1)≥NonInfC∧COND_LOAD1158(TRUE, i70[3]1, i133[3]1, i123[3]1)≥LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))∧(UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥))

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

(103)    (>(i133[2], 1)=TRUE>(+(i123[2], 1), 0)=TRUE>(-(i133[2], 2), 1)=TRUE>(+(+(i123[2], 1), 1), 0)=TRUE>(-(-(i133[2], 2), 2), 0)=TRUE<=(-(-(i133[2], 2), 2), 1)=TRUECOND_LOAD1158(TRUE, i70[2], -(i133[2], 2), +(i123[2], 1))≥NonInfC∧COND_LOAD1158(TRUE, i70[2], -(i133[2], 2), +(i123[2], 1))≥LOAD1158(i70[2], -(-(i133[2], 2), 2), +(+(i123[2], 1), 1))∧(UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥))

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

(104)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-5] ≥ 0∧[5] + [-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(105)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-5] ≥ 0∧[5] + [-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(106)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-5] ≥ 0∧[5] + [-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(107)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] + [-5] ≥ 0∧[5] + [-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(108)    (i133[2] ≥ 0∧i123[2] ≥ 0∧[-2] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧[-3] + i133[2] ≥ 0∧[3] + [-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(109)    ([2] + i133[2] ≥ 0∧i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧[-1] + i133[2] ≥ 0∧[1] + [-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(110)    ([3] + i133[2] ≥ 0∧i123[2] ≥ 0∧[1] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] ≥ 0∧[-1]i133[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(111)    ([3] ≥ 0∧i123[2] ≥ 0∧[1] ≥ 0∧i123[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

We simplified constraint (111) using rule (IDP_POLY_GCD) which results in the following new constraint:

(112)    (i123[2] ≥ 0∧[1] ≥ 0∧i123[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

(113)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]i70[3]=i70[2]1-(i133[3], 2)=i133[2]1+(i123[3], 1)=i123[2]1&&(>(i133[2]1, 1), >(+(i123[2]1, 1), 0))=TRUEi123[2]1=i123[3]1i133[2]1=i133[3]1i70[2]1=i70[3]1+(i123[3]1, 1)=i123[7]i70[3]1=i70[7]-(i133[3]1, 2)=i132[7]&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]COND_LOAD1158(TRUE, i70[3]1, i133[3]1, i123[3]1)≥NonInfC∧COND_LOAD1158(TRUE, i70[3]1, i133[3]1, i123[3]1)≥LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))∧(UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥))

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

(114)    (>(i133[2], 1)=TRUE>(+(i123[2], 1), 0)=TRUE>(-(i133[2], 2), 1)=TRUE>(+(+(i123[2], 1), 1), 0)=TRUE>(+(+(+(i123[2], 1), 1), 1), 0)=TRUE<=(-(-(i133[2], 2), 2), 1)=TRUE>(+(i70[7], 1), 0)=TRUECOND_LOAD1158(TRUE, i70[7], -(i133[2], 2), +(i123[2], 1))≥NonInfC∧COND_LOAD1158(TRUE, i70[7], -(i133[2], 2), +(i123[2], 1))≥LOAD1158(i70[7], -(-(i133[2], 2), 2), +(+(i123[2], 1), 1))∧(UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥))

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

(115)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i123[2] + [2] ≥ 0∧[5] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(116)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i123[2] + [2] ≥ 0∧[5] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(117)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i133[2] + [-4] ≥ 0∧i123[2] + [1] ≥ 0∧i123[2] + [2] ≥ 0∧[5] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(118)    (i133[2] ≥ 0∧i123[2] ≥ 0∧[-2] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧i123[2] + [2] ≥ 0∧[3] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(119)    ([2] + i133[2] ≥ 0∧i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧i123[2] + [2] ≥ 0∧[1] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

We simplified constraint (119) using rule (IDP_POLY_GCD) which results in the following new constraint:

(120)    ([2] + i133[2] ≥ 0∧i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧[1] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

For Pair LOAD1158(i70, i133, i123) → COND_LOAD11581(&&(>(i133, 0), <=(i133, 1)), i70, i133, i123) the following chains were created:
• We consider the chain LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4]), COND_LOAD11581(TRUE, i70[5], i133[5], i123[5]) → LOAD1172(i70[5], i123[5]) which results in the following constraint:

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

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

(123)    (i133[4] + [-1] ≥ 0∧[1] + [-1]i133[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[(-1)Bound*bni_43] + [bni_43]i123[4] + [bni_43]i133[4] ≥ 0∧[-1 + (-1)bso_44] + i133[4] ≥ 0)

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

(124)    (i133[4] + [-1] ≥ 0∧[1] + [-1]i133[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[(-1)Bound*bni_43] + [bni_43]i123[4] + [bni_43]i133[4] ≥ 0∧[-1 + (-1)bso_44] + i133[4] ≥ 0)

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

(125)    (i133[4] + [-1] ≥ 0∧[1] + [-1]i133[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[(-1)Bound*bni_43] + [bni_43]i123[4] + [bni_43]i133[4] ≥ 0∧[-1 + (-1)bso_44] + i133[4] ≥ 0)

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

(126)    (i133[4] + [-1] ≥ 0∧[1] + [-1]i133[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43] + [bni_43]i133[4] ≥ 0∧0 = 0∧0 = 0∧[-1 + (-1)bso_44] + i133[4] ≥ 0)

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

(127)    (i133[4] ≥ 0∧[-1]i133[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43 + bni_43] + [bni_43]i133[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_44] + i133[4] ≥ 0)

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

(128)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43 + bni_43] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)

For Pair COND_LOAD11581(TRUE, i70, i133, i123) → LOAD1172(i70, i123) the following chains were created:
• We consider the chain COND_LOAD11581(TRUE, i70[5], i133[5], i123[5]) → LOAD1172(i70[5], i123[5]), LOAD1172(i70[6], i123[6]) → LOAD945(+(i123[6], 1), +(i70[6], 1)) which results in the following constraint:

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

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

(131)    ((UIncreasing(LOAD1172(i70[5], i123[5])), ≥)∧[(-1)bso_46] ≥ 0)

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

(132)    ((UIncreasing(LOAD1172(i70[5], i123[5])), ≥)∧[(-1)bso_46] ≥ 0)

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

(133)    ((UIncreasing(LOAD1172(i70[5], i123[5])), ≥)∧[(-1)bso_46] ≥ 0)

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

(134)    ((UIncreasing(LOAD1172(i70[5], i123[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

For Pair LOAD1172(i70, i123) → LOAD945(+(i123, 1), +(i70, 1)) the following chains were created:

We solved constraint (135) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (IDP_BOOLEAN).

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

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

(138)    (i123[3] ≥ 0∧i133[3] + [-3] ≥ 0∧[3] + [-1]i133[3] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[6], 1), +(i70[6], 1))), ≥)∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i123[3] ≥ 0∧[1 + (-1)bso_48] ≥ 0)

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

(139)    (i123[3] ≥ 0∧i133[3] + [-3] ≥ 0∧[3] + [-1]i133[3] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[6], 1), +(i70[6], 1))), ≥)∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i123[3] ≥ 0∧[1 + (-1)bso_48] ≥ 0)

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

(140)    (i123[3] ≥ 0∧i133[3] + [-3] ≥ 0∧[3] + [-1]i133[3] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[6], 1), +(i70[6], 1))), ≥)∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i123[3] ≥ 0∧[1 + (-1)bso_48] ≥ 0)

We simplified constraint (140) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

(141)    (i123[3] ≥ 0∧[3] + [-1]i133[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[6], 1), +(i70[6], 1))), ≥)∧0 = 0∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i123[3] ≥ 0∧0 = 0∧[1 + (-1)bso_48] ≥ 0)

For Pair LOAD1158(i70, i132, i123) → COND_LOAD11582(&&(&&(<=(i132, 1), >(+(i70, 1), 0)), >(+(i123, 1), 0)), i70, i132, i123) the following chains were created:
• We consider the chain LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7]), COND_LOAD11582(TRUE, i70[8], i132[8], i123[8]) → LOAD945(+(i123[8], 1), +(i70[8], 1)) which results in the following constraint:

(142)    (&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]LOAD1158(i70[7], i132[7], i123[7])≥NonInfC∧LOAD1158(i70[7], i132[7], i123[7])≥COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])∧(UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥))

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

(143)    (>(+(i123[7], 1), 0)=TRUE<=(i132[7], 1)=TRUE>(+(i70[7], 1), 0)=TRUELOAD1158(i70[7], i132[7], i123[7])≥NonInfC∧LOAD1158(i70[7], i132[7], i123[7])≥COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])∧(UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥))

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

(144)    (i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(145)    (i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(146)    (i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(147)    (i123[7] ≥ 0∧[1] + i132[7] ≥ 0∧i70[7] ≥ 0∧i132[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [(-1)bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)

(148)    (i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0∧i132[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)

For Pair COND_LOAD11582(TRUE, i70, i132, i123) → LOAD945(+(i123, 1), +(i70, 1)) the following chains were created:

(149)    (i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]0=i123[7]i70[1]=i70[7]-(i80[1], 2)=i132[7]&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]+(i123[8], 1)=i80[0]1+(i70[8], 1)=i70[0]1i80[0]1=i80[1]1>(i80[0]1, 1)=TRUEi70[0]1=i70[1]1COND_LOAD11582(TRUE, i70[8], i132[8], i123[8])≥NonInfC∧COND_LOAD11582(TRUE, i70[8], i132[8], i123[8])≥LOAD945(+(i123[8], 1), +(i70[8], 1))∧(UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥))

We solved constraint (149) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN).

(150)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]+(i123[3], 1)=i123[7]i70[3]=i70[7]-(i133[3], 2)=i132[7]&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0))=TRUEi70[7]=i70[8]i123[7]=i123[8]i132[7]=i132[8]+(i123[8], 1)=i80[0]+(i70[8], 1)=i70[0]i80[0]=i80[1]>(i80[0], 1)=TRUEi70[0]=i70[1]COND_LOAD11582(TRUE, i70[8], i132[8], i123[8])≥NonInfC∧COND_LOAD11582(TRUE, i70[8], i132[8], i123[8])≥LOAD945(+(i123[8], 1), +(i70[8], 1))∧(UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥))

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

(151)    (>(+(+(i123[2], 1), 1), 1)=TRUE>(i133[2], 1)=TRUE>(+(i123[2], 1), 0)=TRUE>(+(+(i123[2], 1), 1), 0)=TRUE<=(-(i133[2], 2), 1)=TRUE>(+(i70[7], 1), 0)=TRUECOND_LOAD11582(TRUE, i70[7], -(i133[2], 2), +(i123[2], 1))≥NonInfC∧COND_LOAD11582(TRUE, i70[7], -(i133[2], 2), +(i123[2], 1))≥LOAD945(+(+(i123[2], 1), 1), +(i70[7], 1))∧(UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥))

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

(152)    (i123[2] ≥ 0∧i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i123[2] + [1] ≥ 0∧[3] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]i123[2] + [bni_51]i133[2] ≥ 0∧[-2 + (-1)bso_52] + i133[2] ≥ 0)

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

(153)    (i123[2] ≥ 0∧i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i123[2] + [1] ≥ 0∧[3] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]i123[2] + [bni_51]i133[2] ≥ 0∧[-2 + (-1)bso_52] + i133[2] ≥ 0)

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

(154)    (i123[2] ≥ 0∧i133[2] + [-2] ≥ 0∧i123[2] ≥ 0∧i123[2] + [1] ≥ 0∧[3] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]i123[2] + [bni_51]i133[2] ≥ 0∧[-2 + (-1)bso_52] + i133[2] ≥ 0)

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

(155)    (i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] ≥ 0∧i123[2] + [1] ≥ 0∧[1] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥)∧[bni_51 + (-1)Bound*bni_51] + [bni_51]i123[2] + [bni_51]i133[2] ≥ 0∧[(-1)bso_52] + i133[2] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i80[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD945(>(i80[0], 1), i80[0], i70[0])), ≥)∧0 = 0∧[bni_35 + (-1)Bound*bni_35] + [bni_35]i80[0] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

• ([2] + i123[6] ≥ 0∧i123[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (3)bni_37] + [bni_37]i123[6] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (2)bni_37] ≥ 0∧0 = 0∧[1 + (-1)bso_38] ≥ 0)
• (i123[6] ≥ 0∧[1] + [-1]i123[6] ≥ 0∧[-1]i70[6] + [1] ≥ 0∧i70[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)
• (i123[6] ≥ 0∧[1] + [-1]i123[6] ≥ 0∧i70[6] + [1] ≥ 0∧i70[6] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[6] ≥ 0∧[1 + (-1)bso_38] ≥ 0)
• ([2] + i123[7] ≥ 0∧[3] + i123[7] ≥ 0∧i123[7] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (3)bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧i70[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] ≥ 0∧[1 + (-1)bso_38] ≥ 0)
• (i123[7] ≥ 0∧[1] + i123[7] ≥ 0∧i70[7] ≥ 0∧[1] + [-1]i123[7] ≥ 0∧i70[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[1], -(i80[1], 2), 0)), ≥)∧[(-1)Bound*bni_37 + bni_37] + [bni_37]i123[7] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

• LOAD1158(i70, i133, i123) → COND_LOAD1158(&&(>(i133, 1), >(+(i123, 1), 0)), i70, i133, i123)
• (i133[2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧0 = 0∧[(-1)Bound*bni_39 + (2)bni_39] + [bni_39]i123[2] + [bni_39]i133[2] ≥ 0∧0 = 0∧[(-1)bso_40] ≥ 0)

• ([4] + i80[0] ≥ 0∧[2] + i80[0] ≥ 0∧i80[0] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• ([2] + i80[0] ≥ 0∧i80[0] ≥ 0∧[1] + [-1]i80[0] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i80[0] ≥ 0∧[(-1)bso_42] ≥ 0)
• ([4] + i133[2] ≥ 0∧i123[2] ≥ 0∧[2] + i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧i133[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(4)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• (i123[2] ≥ 0∧[1] ≥ 0∧i123[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• ([2] + i133[2] ≥ 0∧i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] + [1] ≥ 0∧[1] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3]1, -(i133[3]1, 2), +(i123[3]1, 1))), ≥)∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i123[2] + [bni_41]i133[2] ≥ 0∧[(-1)bso_42] ≥ 0)

• LOAD1158(i70, i133, i123) → COND_LOAD11581(&&(>(i133, 0), <=(i133, 1)), i70, i133, i123)
• (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD11581(&&(>(i133[4], 0), <=(i133[4], 1)), i70[4], i133[4], i123[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43 + bni_43] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)

• ((UIncreasing(LOAD1172(i70[5], i123[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

• (i123[3] ≥ 0∧[3] + [-1]i133[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[6], 1), +(i70[6], 1))), ≥)∧0 = 0∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i123[3] ≥ 0∧0 = 0∧[1 + (-1)bso_48] ≥ 0)

• LOAD1158(i70, i132, i123) → COND_LOAD11582(&&(&&(<=(i132, 1), >(+(i70, 1), 0)), >(+(i123, 1), 0)), i70, i132, i123)
• (i123[7] ≥ 0∧[1] + i132[7] ≥ 0∧i70[7] ≥ 0∧i132[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [(-1)bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)
• (i123[7] ≥ 0∧[1] + [-1]i132[7] ≥ 0∧i70[7] ≥ 0∧i132[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i123[7] + [bni_49]i132[7] ≥ 0∧[(-1)bso_50] ≥ 0)

• (i123[2] ≥ 0∧i133[2] ≥ 0∧i123[2] ≥ 0∧i123[2] + [1] ≥ 0∧[1] + [-1]i133[2] ≥ 0∧i70[7] ≥ 0 ⇒ (UIncreasing(LOAD945(+(i123[8], 1), +(i70[8], 1))), ≥)∧[bni_51 + (-1)Bound*bni_51] + [bni_51]i123[2] + [bni_51]i133[2] ≥ 0∧[(-1)bso_52] + i133[2] ≥ 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(LOAD945(x1, x2)) = [-1] + x1
POL(COND_LOAD945(x1, x2, x3)) = [-1] + x2
POL(>(x1, x2)) = [-1]
POL(1) = [1]
POL(LOAD1158(x1, x2, x3)) = x3 + x2
POL(-(x1, x2)) = x1 + [-1]x2
POL(2) = [2]
POL(0) = 0
POL(COND_LOAD1158(x1, x2, x3, x4)) = [-1] + x4 + x3 + [-1]x1
POL(&&(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(COND_LOAD11581(x1, x2, x3, x4)) = [1] + x4
POL(<=(x1, x2)) = [-1]
POL(LOAD1172(x1, x2)) = [1] + x2
POL(COND_LOAD11582(x1, x2, x3, x4)) = x4 + x3

The following pairs are in P>:

The following pairs are in Pbound:

LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])

The following pairs are in P:

LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])
LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(&&(&&(<=(i132[7], 1), >(+(i70[7], 1), 0)), >(+(i123[7], 1), 0)), i70[7], i132[7], i123[7])

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

### (13) 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): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])
(3): COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], i133[3] - 2, i123[3] + 1)
(4): LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(i133[4] > 0 && i133[4] <= 1, i70[4], i133[4], i123[4])
(7): LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0, i70[7], i132[7], i123[7])
(8): COND_LOAD11582(TRUE, i70[8], i132[8], i123[8]) → LOAD945(i123[8] + 1, i70[8] + 1)

(8) -> (0), if ((i123[8] + 1* i80[0])∧(i70[8] + 1* i70[0]))

(3) -> (2), if ((i70[3]* i70[2])∧(i133[3] - 2* i133[2])∧(i123[3] + 1* i123[2]))

(2) -> (3), if ((i133[2] > 1 && i123[2] + 1 > 0* TRUE)∧(i123[2]* i123[3])∧(i133[2]* i133[3])∧(i70[2]* i70[3]))

(3) -> (4), if ((i70[3]* i70[4])∧(i133[3] - 2* i133[4])∧(i123[3] + 1* i123[4]))

(4) -> (5), if ((i133[4] > 0 && i133[4] <= 1* TRUE)∧(i133[4]* i133[5])∧(i70[4]* i70[5])∧(i123[4]* i123[5]))

(3) -> (7), if ((i123[3] + 1* i123[7])∧(i70[3]* i70[7])∧(i133[3] - 2* i132[7]))

(7) -> (8), if ((i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0* TRUE)∧(i70[7]* i70[8])∧(i123[7]* i123[8])∧(i132[7]* i132[8]))

The set Q consists of the following terms:

### (14) IDependencyGraphProof (EQUIVALENT transformation)

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

### (15) 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:
(3): COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], i133[3] - 2, i123[3] + 1)
(2): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])

(3) -> (2), if ((i70[3]* i70[2])∧(i133[3] - 2* i133[2])∧(i123[3] + 1* i123[2]))

(2) -> (3), if ((i133[2] > 1 && i123[2] + 1 > 0* TRUE)∧(i123[2]* i123[3])∧(i133[2]* i133[3])∧(i70[2]* i70[3]))

The set Q consists of the following terms:

### (16) 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_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1)) the following chains were created:
• We consider the chain LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2]), COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1)), LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2]) which results in the following constraint:

(1)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]i70[3]=i70[2]1-(i133[3], 2)=i133[2]1+(i123[3], 1)=i123[2]1COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥NonInfC∧COND_LOAD1158(TRUE, i70[3], i133[3], i123[3])≥LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))∧(UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥))

We simplified constraint (1) using rules (III), (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)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]i133[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)

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

(4)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]i133[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)

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

(5)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]i133[2] ≥ 0∧[1 + (-1)bso_15] ≥ 0)

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

(6)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[(-1)bni_14 + (-1)Bound*bni_14] + [bni_14]i133[2] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

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

(7)    (i133[2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[bni_14 + (-1)Bound*bni_14] + [bni_14]i133[2] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

For Pair LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2]) the following chains were created:
• We consider the chain LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2]), COND_LOAD1158(TRUE, i70[3], i133[3], i123[3]) → LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1)) which results in the following constraint:

(8)    (&&(>(i133[2], 1), >(+(i123[2], 1), 0))=TRUEi123[2]=i123[3]i133[2]=i133[3]i70[2]=i70[3]LOAD1158(i70[2], i133[2], i123[2])≥NonInfC∧LOAD1158(i70[2], i133[2], i123[2])≥COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])∧(UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥))

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

(9)    (>(i133[2], 1)=TRUE>(+(i123[2], 1), 0)=TRUELOAD1158(i70[2], i133[2], i123[2])≥NonInfC∧LOAD1158(i70[2], i133[2], i123[2])≥COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])∧(UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥))

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

(10)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]i133[2] ≥ 0∧[(-1)bso_17] ≥ 0)

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

(11)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]i133[2] ≥ 0∧[(-1)bso_17] ≥ 0)

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

(12)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧[(-1)Bound*bni_16] + [bni_16]i133[2] ≥ 0∧[(-1)bso_17] ≥ 0)

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

(13)    (i133[2] + [-2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧0 = 0∧[(-1)Bound*bni_16] + [bni_16]i133[2] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)

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

(14)    (i133[2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧0 = 0∧[(-1)Bound*bni_16 + (2)bni_16] + [bni_16]i133[2] ≥ 0∧0 = 0∧[(-1)bso_17] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i133[2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(LOAD1158(i70[3], -(i133[3], 2), +(i123[3], 1))), ≥)∧0 = 0∧[bni_14 + (-1)Bound*bni_14] + [bni_14]i133[2] ≥ 0∧0 = 0∧[1 + (-1)bso_15] ≥ 0)

• LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])
• (i133[2] ≥ 0∧i123[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])), ≥)∧0 = 0∧[(-1)Bound*bni_16 + (2)bni_16] + [bni_16]i133[2] ≥ 0∧0 = 0∧[(-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) = 0
POL(FALSE) = [1]
POL(COND_LOAD1158(x1, x2, x3, x4)) = [-1] + x3 + [-1]x1
POL(-(x1, x2)) = x1 + [-1]x2
POL(2) = [2]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0

The following pairs are in P>:

The following pairs are in Pbound:

LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[2])

The following pairs are in P:

LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(&&(>(i133[2], 1), >(+(i123[2], 1), 0)), i70[2], i133[2], i123[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

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

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1158(i70[2], i133[2], i123[2]) → COND_LOAD1158(i133[2] > 1 && i123[2] + 1 > 0, i70[2], i133[2], i123[2])

The set Q consists of the following terms:

### (19) IDependencyGraphProof (EQUIVALENT transformation)

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

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

### (22) IDependencyGraphProof (EQUIVALENT transformation)

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

### (24) 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:
(4): LOAD1158(i70[4], i133[4], i123[4]) → COND_LOAD11581(i133[4] > 0 && i133[4] <= 1, i70[4], i133[4], i123[4])
(7): LOAD1158(i70[7], i132[7], i123[7]) → COND_LOAD11582(i132[7] <= 1 && i70[7] + 1 > 0 && i123[7] + 1 > 0, i70[7], i132[7], i123[7])

(4) -> (5), if ((i133[4] > 0 && i133[4] <= 1* TRUE)∧(i133[4]* i133[5])∧(i70[4]* i70[5])∧(i123[4]* i123[5]))

The set Q consists of the following terms: