### (0) Obligation:

JBC Problem based on JBC Program:

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Log

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 134 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:
Load475(1, i29, i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, 1, i29, i25, i29, i41, i38)
Cond_Load475(TRUE, 1, i29, i25, i29, i41, i38) → Load475(1, i29, i25, i29, i41 - 2, i38 + 1)
Load475(1, i29, i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, 1, i29, i25, i29, i41, i38)
Cond_Load4751(TRUE, 1, i29, i25, i29, i41, i38) → Load487(1, i29, i25, i29, i38)
Load475(1, i29, i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, 1, i29, i25, i29, i40, i38)
Cond_Load4752(TRUE, 1, i29, i25, i29, i40, i38) → Load344(1, i38, i25 + 1)
The set Q consists of the following terms:
Load475(1, x0, x1, x0, x2, x3)
Cond_Load475(TRUE, 1, x0, x1, x0, x2, x3)
Cond_Load4751(TRUE, 1, x0, x1, x0, x2, x3)
Cond_Load4752(TRUE, 1, x0, x1, x0, x2, x3)

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

Cond_Load4752(x1, x2, x3, x4, x5, x6, x7) → Cond_Load4752(x1, x3, x4, x5, x6, x7)
Load475(x1, x2, x3, x4, x5, x6) → Load475(x2, x3, x4, x5, x6)
Cond_Load4751(x1, x2, x3, x4, x5, x6, x7) → Cond_Load4751(x1, x3, x4, x5, x6, x7)
Cond_Load475(x1, x2, x3, x4, x5, x6, x7) → Cond_Load475(x1, x3, x4, x5, x6, x7)

### (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:
Load475(i29, i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, i29, i25, i29, i41, i38)
Cond_Load475(TRUE, i29, i25, i29, i41, i38) → Load475(i29, i25, i29, i41 - 2, i38 + 1)
Load475(i29, i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, i29, i25, i29, i41, i38)
Load475(i29, i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, i29, i25, i29, i40, i38)
The set Q consists of the following terms:
Cond_Load475(TRUE, x0, x1, x0, x2, x3)
Cond_Load4751(TRUE, x0, x1, x0, x2, x3)
Cond_Load4752(TRUE, x0, x1, x0, x2, x3)

### (7) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Cond_Load4752(x1, x2, x3, x4, x5, x6) → Cond_Load4752(x1, x3, x4, x5, x6)
Cond_Load4751(x1, x2, x3, x4, x5, x6) → Cond_Load4751(x1, x3, x4, x5, x6)
Cond_Load475(x1, x2, x3, x4, x5, x6) → Cond_Load475(x1, x3, x4, x5, x6)

### (8) 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:
Load475(i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, i25, i29, i41, i38)
Cond_Load475(TRUE, i25, i29, i41, i38) → Load475(i25, i29, i41 - 2, i38 + 1)
Load475(i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, i25, i29, i41, i38)
Load475(i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, i25, i29, i40, i38)
The set Q consists of the following terms:

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

The ITRS R consists of the following rules:
Load475(i25, i29, i41, i38) → Cond_Load475(i41 > 1 && i38 + 1 > 0, i25, i29, i41, i38)
Cond_Load475(TRUE, i25, i29, i41, i38) → Load475(i25, i29, i41 - 2, i38 + 1)
Load475(i25, i29, i41, i38) → Cond_Load4751(i41 > 0 && i41 <= 1, i25, i29, i41, i38)
Load475(i25, i29, i40, i38) → Cond_Load4752(i40 <= 1 && i25 + 1 > 0, i25, i29, i40, i38)

The integer pair graph contains the following rules and edges:
(2): LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(i41[2] > 1 && i38[2] + 1 > 0, i25[2], i29[2], i41[2], i38[2])
(3): COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], i41[3] - 2, i38[3] + 1)
(4): LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(i41[4] > 0 && i41[4] <= 1, i25[4], i29[4], i41[4], i38[4])
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])

(0) -> (1), if ((i29[0] > 1* TRUE)∧(i29[0]* i29[1])∧(i25[0]* i25[1]))

(1) -> (2), if ((i25[1]* i25[2])∧(0* i38[2])∧(i29[1]* i29[2])∧(i29[1]* i41[2]))

(1) -> (4), if ((i29[1]* i29[4])∧(0* i38[4])∧(i29[1]* i41[4])∧(i25[1]* i25[4]))

(1) -> (7), if ((i25[1]* i25[7])∧(i29[1]* i40[7])∧(i29[1]* i29[7])∧(0* i38[7]))

(2) -> (3), if ((i41[2]* i41[3])∧(i38[2]* i38[3])∧(i29[2]* i29[3])∧(i25[2]* i25[3])∧(i41[2] > 1 && i38[2] + 1 > 0* TRUE))

(3) -> (2), if ((i29[3]* i29[2])∧(i41[3] - 2* i41[2])∧(i25[3]* i25[2])∧(i38[3] + 1* i38[2]))

(3) -> (4), if ((i25[3]* i25[4])∧(i38[3] + 1* i38[4])∧(i29[3]* i29[4])∧(i41[3] - 2* i41[4]))

(3) -> (7), if ((i41[3] - 2* i40[7])∧(i25[3]* i25[7])∧(i38[3] + 1* i38[7])∧(i29[3]* i29[7]))

(4) -> (5), if ((i38[4]* i38[5])∧(i41[4]* i41[5])∧(i41[4] > 0 && i41[4] <= 1* TRUE)∧(i29[4]* i29[5])∧(i25[4]* i25[5]))

(5) -> (6), if ((i25[5]* i25[6])∧(i38[5]* i38[6])∧(i29[5]* i29[6]))

(6) -> (0), if ((i38[6]* i29[0])∧(i25[6] + 1* i25[0]))

(7) -> (8), if ((i38[7]* i38[8])∧(i40[7]* i40[8])∧(i25[7]* i25[8])∧(i29[7]* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0* TRUE))

(8) -> (0), if ((i25[8] + 1* i25[0])∧(i38[8]* i29[0]))

The set Q consists of the following terms:

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

### (12) 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): LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(i41[2] > 1 && i38[2] + 1 > 0, i25[2], i29[2], i41[2], i38[2])
(3): COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], i41[3] - 2, i38[3] + 1)
(4): LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(i41[4] > 0 && i41[4] <= 1, i25[4], i29[4], i41[4], i38[4])
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])

(0) -> (1), if ((i29[0] > 1* TRUE)∧(i29[0]* i29[1])∧(i25[0]* i25[1]))

(1) -> (2), if ((i25[1]* i25[2])∧(0* i38[2])∧(i29[1]* i29[2])∧(i29[1]* i41[2]))

(1) -> (4), if ((i29[1]* i29[4])∧(0* i38[4])∧(i29[1]* i41[4])∧(i25[1]* i25[4]))

(1) -> (7), if ((i25[1]* i25[7])∧(i29[1]* i40[7])∧(i29[1]* i29[7])∧(0* i38[7]))

(2) -> (3), if ((i41[2]* i41[3])∧(i38[2]* i38[3])∧(i29[2]* i29[3])∧(i25[2]* i25[3])∧(i41[2] > 1 && i38[2] + 1 > 0* TRUE))

(3) -> (2), if ((i29[3]* i29[2])∧(i41[3] - 2* i41[2])∧(i25[3]* i25[2])∧(i38[3] + 1* i38[2]))

(3) -> (4), if ((i25[3]* i25[4])∧(i38[3] + 1* i38[4])∧(i29[3]* i29[4])∧(i41[3] - 2* i41[4]))

(3) -> (7), if ((i41[3] - 2* i40[7])∧(i25[3]* i25[7])∧(i38[3] + 1* i38[7])∧(i29[3]* i29[7]))

(4) -> (5), if ((i38[4]* i38[5])∧(i41[4]* i41[5])∧(i41[4] > 0 && i41[4] <= 1* TRUE)∧(i29[4]* i29[5])∧(i25[4]* i25[5]))

(5) -> (6), if ((i25[5]* i25[6])∧(i38[5]* i38[6])∧(i29[5]* i29[6]))

(6) -> (0), if ((i38[6]* i29[0])∧(i25[6] + 1* i25[0]))

(7) -> (8), if ((i38[7]* i38[8])∧(i40[7]* i40[8])∧(i25[7]* i25[8])∧(i29[7]* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0* TRUE))

(8) -> (0), if ((i25[8] + 1* i25[0])∧(i38[8]* i29[0]))

The set Q consists of the following terms:

### (13) 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 LOAD344(i29, i25) → COND_LOAD344(>(i29, 1), i29, i25) the following chains were created:
• We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 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)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧[(-1)bso_41] ≥ 0)

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

(4)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧[(-1)bso_41] ≥ 0)

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

(5)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧[(-1)bso_41] ≥ 0)

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

(6)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

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

(7)    (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

For Pair COND_LOAD344(TRUE, i29, i25) → LOAD475(i25, i29, i29, 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:

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

(10)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(11)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(12)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(13)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)

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

(14)    (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)

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

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

(17)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(18)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(19)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(20)    (i29[0] + [-2] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)

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

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

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

(23)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(24)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(25)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(26)    (i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE+(i25[8], 1)=i25[0]i38[8]=i29[0]>(i29[0], 1)=TRUEi29[0]=i29[1]i25[0]=i25[1]i25[1]=i25[2]0=i38[2]i29[1]=i29[2]i29[1]=i41[2]i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUECOND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))

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

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

(28)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(29)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(30)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(31)    (i29[0] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(32)    (i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

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

(35)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(36)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(37)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i29[0] + [-1] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(38)    (i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE+(i25[8], 1)=i25[0]i38[8]=i29[0]>(i29[0], 1)=TRUEi29[0]=i29[1]i25[0]=i25[1]i25[1]=i25[7]1i29[1]=i40[7]1i29[1]=i29[7]10=i38[7]1i38[7]1=i38[8]1i40[7]1=i40[8]1i25[7]1=i25[8]1i29[7]1=i29[8]1&&(<=(i40[7]1, 1), >(+(i25[7]1, 1), 0))=TRUECOND_LOAD344(TRUE, i29[1], i25[1])≥NonInfC∧COND_LOAD344(TRUE, i29[1], i25[1])≥LOAD475(i25[1], i29[1], i29[1], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))

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

(39)    (>(i29[0], 1)=TRUE<=(i40[7], 1)=TRUE>(+(i25[7], 1), 0)=TRUE<=(i29[0], 1)=TRUE>(+(+(i25[7], 1), 1), 0)=TRUECOND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥NonInfC∧COND_LOAD344(TRUE, i29[0], +(i25[7], 1))≥LOAD475(+(i25[7], 1), i29[0], i29[0], 0)∧(UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥))

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

(40)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(41)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

(42)    (i29[0] + [-2] ≥ 0∧[1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[(-1)bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

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

For Pair LOAD475(i25, i29, i41, i38) → COND_LOAD475(&&(>(i41, 1), >(+(i38, 1), 0)), i25, i29, i41, i38) the following chains were created:
• We consider the chain LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2]), COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1)) which results in the following constraint:

(43)    (i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUELOAD475(i25[2], i29[2], i41[2], i38[2])≥NonInfC∧LOAD475(i25[2], i29[2], i41[2], i38[2])≥COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])∧(UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥))

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

(44)    (>(i41[2], 1)=TRUE>(+(i38[2], 1), 0)=TRUELOAD475(i25[2], i29[2], i41[2], i38[2])≥NonInfC∧LOAD475(i25[2], i29[2], i41[2], i38[2])≥COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])∧(UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥))

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

(45)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(46)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(47)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(48)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

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

(49)    (i41[2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧0 = 0∧0 = 0∧[bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

For Pair COND_LOAD475(TRUE, i25, i29, i41, i38) → LOAD475(i25, i29, -(i41, 2), +(i38, 1)) the following chains were created:

(50)    (>(i29[0], 1)=TRUEi29[0]=i29[1]i25[0]=i25[1]i25[1]=i25[2]0=i38[2]i29[1]=i29[2]i29[1]=i41[2]i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUEi29[3]=i29[2]1-(i41[3], 2)=i41[2]1i25[3]=i25[2]1+(i38[3], 1)=i38[2]1i41[2]1=i41[3]1i38[2]1=i38[3]1i29[2]1=i29[3]1i25[2]1=i25[3]1&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUECOND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥NonInfC∧COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))

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

(51)    (>(i29[0], 1)=TRUE>(-(i29[0], 2), 1)=TRUECOND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥NonInfC∧COND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥LOAD475(i25[0], i29[0], -(i29[0], 2), +(0, 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))

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

(52)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(53)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(54)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(55)    (i29[0] + [-2] ≥ 0∧i29[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(56)    (i29[0] ≥ 0∧[-2] + i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(57)    ([2] + i29[0] ≥ 0∧i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

(58)    (>(i29[0], 1)=TRUEi29[0]=i29[1]i25[0]=i25[1]i25[1]=i25[2]0=i38[2]i29[1]=i29[2]i29[1]=i41[2]i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUEi25[3]=i25[4]+(i38[3], 1)=i38[4]i29[3]=i29[4]-(i41[3], 2)=i41[4]i38[4]=i38[5]i41[4]=i41[5]&&(>(i41[4], 0), <=(i41[4], 1))=TRUEi29[4]=i29[5]i25[4]=i25[5]COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥NonInfC∧COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))

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

(59)    (>(i29[0], 1)=TRUE>(-(i29[0], 2), 0)=TRUE<=(-(i29[0], 2), 1)=TRUECOND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥NonInfC∧COND_LOAD475(TRUE, i25[0], i29[0], i29[0], 0)≥LOAD475(i25[0], i29[0], -(i29[0], 2), +(0, 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))

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

(60)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(61)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(62)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(63)    (i29[0] + [-2] ≥ 0∧i29[0] + [-3] ≥ 0∧[3] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(64)    (i29[0] ≥ 0∧[-1] + i29[0] ≥ 0∧[1] + [-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(65)    ([1] + i29[0] ≥ 0∧i29[0] ≥ 0∧[-1]i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(66)    ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

(67)    (>(i29[0], 1)=TRUEi29[0]=i29[1]i25[0]=i25[1]i25[1]=i25[2]0=i38[2]i29[1]=i29[2]i29[1]=i41[2]i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE-(i41[3], 2)=i40[7]i25[3]=i25[7]+(i38[3], 1)=i38[7]i29[3]=i29[7]i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUECOND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥NonInfC∧COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3])≥LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))

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

(68)    (>(i29[0], 1)=TRUE<=(-(i29[0], 2), 1)=TRUE>(+(i25[7], 1), 0)=TRUECOND_LOAD475(TRUE, i25[7], i29[0], i29[0], 0)≥NonInfC∧COND_LOAD475(TRUE, i25[7], i29[0], i29[0], 0)≥LOAD475(i25[7], i29[0], -(i29[0], 2), +(0, 1))∧(UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥))

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

(69)    (i29[0] + [-2] ≥ 0∧[3] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(70)    (i29[0] + [-2] ≥ 0∧[3] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(71)    (i29[0] + [-2] ≥ 0∧[3] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[(-1)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(72)    (i29[0] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

(73)    (i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUEi29[3]=i29[2]1-(i41[3], 2)=i41[2]1i25[3]=i25[2]1+(i38[3], 1)=i38[2]1i41[2]1=i41[3]1i38[2]1=i38[3]1i29[2]1=i29[3]1i25[2]1=i25[3]1&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUEi29[3]1=i29[2]2-(i41[3]1, 2)=i41[2]2i25[3]1=i25[2]2+(i38[3]1, 1)=i38[2]2i41[2]2=i41[3]2i38[2]2=i38[3]2i29[2]2=i29[3]2i25[2]2=i25[3]2&&(>(i41[2]2, 1), >(+(i38[2]2, 1), 0))=TRUECOND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥NonInfC∧COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))

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

(74)    (>(i41[2], 1)=TRUE>(+(i38[2], 1), 0)=TRUE>(-(i41[2], 2), 1)=TRUE>(+(+(i38[2], 1), 1), 0)=TRUE>(-(-(i41[2], 2), 2), 1)=TRUE>(+(+(+(i38[2], 1), 1), 1), 0)=TRUECOND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD475(i25[2], i29[2], -(-(i41[2], 2), 2), +(+(i38[2], 1), 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))

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

(75)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(76)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(77)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(78)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-6] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(79)    (i41[2] ≥ 0∧i38[2] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-4] + i41[2] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(80)    ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(81)    ([4] + i41[2] ≥ 0∧i38[2] ≥ 0∧[2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧i38[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(82)    ([4] + i41[2] ≥ 0∧i38[2] ≥ 0∧[2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

(83)    (i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUEi29[3]=i29[2]1-(i41[3], 2)=i41[2]1i25[3]=i25[2]1+(i38[3], 1)=i38[2]1i41[2]1=i41[3]1i38[2]1=i38[3]1i29[2]1=i29[3]1i25[2]1=i25[3]1&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUEi25[3]1=i25[4]+(i38[3]1, 1)=i38[4]i29[3]1=i29[4]-(i41[3]1, 2)=i41[4]i38[4]=i38[5]i41[4]=i41[5]&&(>(i41[4], 0), <=(i41[4], 1))=TRUEi29[4]=i29[5]i25[4]=i25[5]COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥NonInfC∧COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))

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

(84)    (>(i41[2], 1)=TRUE>(+(i38[2], 1), 0)=TRUE>(-(i41[2], 2), 1)=TRUE>(+(+(i38[2], 1), 1), 0)=TRUE>(-(-(i41[2], 2), 2), 0)=TRUE<=(-(-(i41[2], 2), 2), 1)=TRUECOND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD475(TRUE, i25[2], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD475(i25[2], i29[2], -(-(i41[2], 2), 2), +(+(i38[2], 1), 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))

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

(85)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(86)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(87)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(88)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] + [-5] ≥ 0∧[5] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(89)    (i41[2] ≥ 0∧i38[2] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-3] + i41[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(90)    ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[-1] + i41[2] ≥ 0∧[1] + [-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(91)    ([3] + i41[2] ≥ 0∧i38[2] ≥ 0∧[1] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧[-1]i41[2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(92)    ([3] ≥ 0∧i38[2] ≥ 0∧[1] ≥ 0∧i38[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(93)    (i38[2] ≥ 0∧[1] ≥ 0∧i38[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

(94)    (i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUEi29[3]=i29[2]1-(i41[3], 2)=i41[2]1i25[3]=i25[2]1+(i38[3], 1)=i38[2]1i41[2]1=i41[3]1i38[2]1=i38[3]1i29[2]1=i29[3]1i25[2]1=i25[3]1&&(>(i41[2]1, 1), >(+(i38[2]1, 1), 0))=TRUE-(i41[3]1, 2)=i40[7]i25[3]1=i25[7]+(i38[3]1, 1)=i38[7]i29[3]1=i29[7]i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUECOND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥NonInfC∧COND_LOAD475(TRUE, i25[3]1, i29[3]1, i41[3]1, i38[3]1)≥LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))

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

(95)    (>(i41[2], 1)=TRUE>(+(i38[2], 1), 0)=TRUE>(-(i41[2], 2), 1)=TRUE>(+(+(i38[2], 1), 1), 0)=TRUE<=(-(-(i41[2], 2), 2), 1)=TRUE>(+(i25[7], 1), 0)=TRUECOND_LOAD475(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD475(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD475(i25[7], i29[2], -(-(i41[2], 2), 2), +(+(i38[2], 1), 1))∧(UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥))

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

(96)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(97)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(98)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧[1 + (-1)bso_47] ≥ 0)

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

(99)    (i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧i41[2] + [-4] ≥ 0∧i38[2] + [1] ≥ 0∧[5] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(100)    (i41[2] ≥ 0∧i38[2] ≥ 0∧[-2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

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

(101)    ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

For Pair LOAD475(i25, i29, i41, i38) → COND_LOAD4751(&&(>(i41, 0), <=(i41, 1)), i25, i29, i41, i38) the following chains were created:
• We consider the chain LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4]), COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]) which results in the following constraint:

(102)    (i38[4]=i38[5]i41[4]=i41[5]&&(>(i41[4], 0), <=(i41[4], 1))=TRUEi29[4]=i29[5]i25[4]=i25[5]LOAD475(i25[4], i29[4], i41[4], i38[4])≥NonInfC∧LOAD475(i25[4], i29[4], i41[4], i38[4])≥COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])∧(UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥))

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

(103)    (>(i41[4], 0)=TRUE<=(i41[4], 1)=TRUELOAD475(i25[4], i29[4], i41[4], i38[4])≥NonInfC∧LOAD475(i25[4], i29[4], i41[4], i38[4])≥COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])∧(UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥))

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

(104)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i38[4] + [bni_48]i41[4] ≥ 0∧[(-1)bso_49] + i41[4] ≥ 0)

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

(105)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i38[4] + [bni_48]i41[4] ≥ 0∧[(-1)bso_49] + i41[4] ≥ 0)

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

(106)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i38[4] + [bni_48]i41[4] ≥ 0∧[(-1)bso_49] + i41[4] ≥ 0)

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

(107)    (i41[4] + [-1] ≥ 0∧[1] + [-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)bni_48 + (-1)Bound*bni_48] + [bni_48]i41[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_49] + i41[4] ≥ 0)

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

(108)    (i41[4] ≥ 0∧[-1]i41[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] + [bni_48]i41[4] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] + i41[4] ≥ 0)

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

(109)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] ≥ 0)

For Pair COND_LOAD4751(TRUE, i25, i29, i41, i38) → LOAD487(i25, i29, i38) the following chains were created:
• We consider the chain COND_LOAD4751(TRUE, i25[5], i29[5], i41[5], i38[5]) → LOAD487(i25[5], i29[5], i38[5]), LOAD487(i25[6], i29[6], i38[6]) → LOAD344(i38[6], +(i25[6], 1)) which results in the following constraint:

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

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

(112)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧[(-1)bso_51] ≥ 0)

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

(113)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧[(-1)bso_51] ≥ 0)

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

(114)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧[(-1)bso_51] ≥ 0)

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

(115)    ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

For Pair LOAD487(i25, i29, i38) → LOAD344(i38, +(i25, 1)) the following chains were created:

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

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

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

(119)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧[(-1)bso_53] ≥ 0)

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

(120)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧[(-1)bso_53] ≥ 0)

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

(121)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧[(-1)bso_53] ≥ 0)

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

(122)    (i38[3] + [-1] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

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

(123)    (i38[3] ≥ 0∧i41[3] + [-3] ≥ 0∧[3] + [-1]i41[3] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52 + bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

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

(124)    (i38[3] ≥ 0∧[3] + [-1]i41[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52 + bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

For Pair LOAD475(i25, i29, i40, i38) → COND_LOAD4752(&&(<=(i40, 1), >(+(i25, 1), 0)), i25, i29, i40, i38) the following chains were created:
• We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

(125)    (i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUELOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))

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

(126)    (<=(i40[7], 1)=TRUE>(+(i25[7], 1), 0)=TRUELOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))

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

(127)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i38[7] + [bni_54]i40[7] ≥ 0∧[(-1)bso_55] ≥ 0)

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

(128)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i38[7] + [bni_54]i40[7] ≥ 0∧[(-1)bso_55] ≥ 0)

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

(129)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i38[7] + [bni_54]i40[7] ≥ 0∧[(-1)bso_55] ≥ 0)

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

(130)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

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

(131)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

(132)    ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

For Pair COND_LOAD4752(TRUE, i25, i29, i40, i38) → LOAD344(i38, +(i25, 1)) the following chains were created:

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

(134)    (i41[2]=i41[3]i38[2]=i38[3]i29[2]=i29[3]i25[2]=i25[3]&&(>(i41[2], 1), >(+(i38[2], 1), 0))=TRUE-(i41[3], 2)=i40[7]i25[3]=i25[7]+(i38[3], 1)=i38[7]i29[3]=i29[7]i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUE+(i25[8], 1)=i25[0]i38[8]=i29[0]>(i29[0], 1)=TRUEi29[0]=i29[1]i25[0]=i25[1]COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥NonInfC∧COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8])≥LOAD344(i38[8], +(i25[8], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))

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

(135)    (>(+(i38[2], 1), 1)=TRUE>(i41[2], 1)=TRUE>(+(i38[2], 1), 0)=TRUE<=(-(i41[2], 2), 1)=TRUE>(+(i25[7], 1), 0)=TRUECOND_LOAD4752(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥NonInfC∧COND_LOAD4752(TRUE, i25[7], i29[2], -(i41[2], 2), +(i38[2], 1))≥LOAD344(+(i38[2], 1), +(i25[7], 1))∧(UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥))

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

(136)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)

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

(137)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)

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

(138)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)

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

(139)    (i38[2] + [-1] ≥ 0∧i41[2] + [-2] ≥ 0∧i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[(-2)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)

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

(140)    (i38[2] ≥ 0∧i41[2] + [-2] ≥ 0∧[1] + i38[2] ≥ 0∧[3] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[(-1)bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[-2 + (-1)bso_57] + i41[2] ≥ 0)

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

(141)    (i38[2] ≥ 0∧i41[2] ≥ 0∧[1] + i38[2] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[(-1)bso_57] + i41[2] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i29[0] ≥ 0∧0 = 0∧[(-1)bso_41] ≥ 0)

• (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧0 = 0∧[(-1)bso_43] ≥ 0)
• (i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_42 + (-1)Bound*bni_42] + [bni_42]i29[0] ≥ 0∧[(-1)bso_43] ≥ 0)

• LOAD475(i25, i29, i41, i38) → COND_LOAD475(&&(>(i41, 1), >(+(i38, 1), 0)), i25, i29, i41, i38)
• (i41[2] ≥ 0∧i38[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])), ≥)∧0 = 0∧0 = 0∧[bni_44 + (-1)Bound*bni_44] + [bni_44]i38[2] + [bni_44]i41[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

• COND_LOAD475(TRUE, i25, i29, i41, i38) → LOAD475(i25, i29, -(i41, 2), +(i38, 1))
• ([2] + i29[0] ≥ 0∧i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
• (i29[0] ≥ 0∧[1] + [-1]i29[0] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))), ≥)∧[bni_46 + (-1)Bound*bni_46] + [bni_46]i29[0] ≥ 0∧[1 + (-1)bso_47] ≥ 0)
• ([4] + i41[2] ≥ 0∧i38[2] ≥ 0∧[2] + i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧i41[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(4)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
• (i38[2] ≥ 0∧[1] ≥ 0∧i38[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧0 = 0∧[(3)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)
• ([2] + i41[2] ≥ 0∧i38[2] ≥ 0∧i41[2] ≥ 0∧i38[2] + [1] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[3]1, i29[3]1, -(i41[3]1, 2), +(i38[3]1, 1))), ≥)∧0 = 0∧[(2)bni_46 + (-1)Bound*bni_46] + [bni_46]i38[2] + [bni_46]i41[2] ≥ 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

• LOAD475(i25, i29, i41, i38) → COND_LOAD4751(&&(>(i41, 0), <=(i41, 1)), i25, i29, i41, i38)
• (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])), ≥)∧[bni_48] = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_48] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] ≥ 0)

• ((UIncreasing(LOAD487(i25[5], i29[5], i38[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

• (i38[3] ≥ 0∧[3] + [-1]i41[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[6], +(i25[6], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_52 + bni_52] + [bni_52]i38[3] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

• LOAD475(i25, i29, i40, i38) → COND_LOAD4752(&&(<=(i40, 1), >(+(i25, 1), 0)), i25, i29, i40, i38)
• ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)
• ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_54] = 0∧0 = 0∧[(-1)bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i40[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

• (i38[2] ≥ 0∧i41[2] ≥ 0∧[1] + i38[2] ≥ 0∧[1] + [-1]i41[2] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧[bni_56 + (-1)Bound*bni_56] + [bni_56]i38[2] + [bni_56]i41[2] ≥ 0∧0 = 0∧[(-1)bso_57] + i41[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(LOAD344(x1, x2)) = [-1] + x1
POL(COND_LOAD344(x1, x2, x3)) = [-1] + x2
POL(>(x1, x2)) = [-1]
POL(1) = [1]
POL(LOAD475(x1, x2, x3, x4)) = [-1] + x4 + x3
POL(0) = 0
POL(COND_LOAD475(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + [-1]x1
POL(&&(x1, x2)) = 0
POL(+(x1, x2)) = x1 + x2
POL(-(x1, x2)) = x1 + [-1]x2
POL(2) = [2]
POL(COND_LOAD4751(x1, x2, x3, x4, x5)) = [-1] + x5 + [-1]x1
POL(<=(x1, x2)) = [-1]
POL(LOAD487(x1, x2, x3)) = [-1] + x3
POL(COND_LOAD4752(x1, x2, x3, x4, x5)) = [-1] + x5 + x4 + [-1]x1

The following pairs are in P>:

COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))
LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(&&(>(i41[4], 0), <=(i41[4], 1)), i25[4], i29[4], i41[4], i38[4])

The following pairs are in Pbound:

LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])
COND_LOAD475(TRUE, i25[3], i29[3], i41[3], i38[3]) → LOAD475(i25[3], i29[3], -(i41[3], 2), +(i38[3], 1))

The following pairs are in P:

LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(&&(>(i41[2], 1), >(+(i38[2], 1), 0)), i25[2], i29[2], i41[2], i38[2])
LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])

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

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

### (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:
(2): LOAD475(i25[2], i29[2], i41[2], i38[2]) → COND_LOAD475(i41[2] > 1 && i38[2] + 1 > 0, i25[2], i29[2], i41[2], i38[2])
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])

(8) -> (0), if ((i25[8] + 1* i25[0])∧(i38[8]* i29[0]))

(0) -> (1), if ((i29[0] > 1* TRUE)∧(i29[0]* i29[1])∧(i25[0]* i25[1]))

(1) -> (2), if ((i25[1]* i25[2])∧(0* i38[2])∧(i29[1]* i29[2])∧(i29[1]* i41[2]))

(1) -> (7), if ((i25[1]* i25[7])∧(i29[1]* i40[7])∧(i29[1]* i29[7])∧(0* i38[7]))

(7) -> (8), if ((i38[7]* i38[8])∧(i40[7]* i40[8])∧(i25[7]* i25[8])∧(i29[7]* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0* TRUE))

The set Q consists of the following terms:

### (16) IDependencyGraphProof (EQUIVALENT transformation)

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

### (17) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])

(8) -> (0), if ((i25[8] + 1* i25[0])∧(i38[8]* i29[0]))

(0) -> (1), if ((i29[0] > 1* TRUE)∧(i29[0]* i29[1])∧(i25[0]* i25[1]))

(1) -> (7), if ((i25[1]* i25[7])∧(i29[1]* i40[7])∧(i29[1]* i29[7])∧(0* i38[7]))

(7) -> (8), if ((i38[7]* i38[8])∧(i40[7]* i40[8])∧(i25[7]* i25[8])∧(i29[7]* i29[8])∧(i40[7] <= 1 && i25[7] + 1 > 0* TRUE))

The set Q consists of the following terms:

### (18) 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_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) the following chains were created:
• We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)), LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]) which results in the following constraint:

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)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(4)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(5)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(6)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

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

(7)    ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

(8)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]) the following chains were created:
• We consider the chain LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]), COND_LOAD4752(TRUE, i25[8], i29[8], i40[8], i38[8]) → LOAD344(i38[8], +(i25[8], 1)) which results in the following constraint:

(9)    (i38[7]=i38[8]i40[7]=i40[8]i25[7]=i25[8]i29[7]=i29[8]&&(<=(i40[7], 1), >(+(i25[7], 1), 0))=TRUELOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))

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

(10)    (<=(i40[7], 1)=TRUE>(+(i25[7], 1), 0)=TRUELOAD475(i25[7], i29[7], i40[7], i38[7])≥NonInfC∧LOAD475(i25[7], i29[7], i40[7], i38[7])≥COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])∧(UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥))

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

(11)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

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

(12)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

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

(13)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

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

(14)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

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

(15)    ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + i40[7] ≥ 0)

(16)    ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

For Pair COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) the following chains were created:
• We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0), LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7]) which results in the following constraint:

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

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

(19)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(20)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(21)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(22)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

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

(23)    (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]) the following chains were created:
• We consider the chain LOAD344(i29[0], i25[0]) → COND_LOAD344(>(i29[0], 1), i29[0], i25[0]), COND_LOAD344(TRUE, i29[1], i25[1]) → LOAD475(i25[1], i29[1], i29[1], 0) which results in the following constraint:

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

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

(26)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)

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

(27)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)

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

(28)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)

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

(29)    (i29[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 = 0∧[-2 + (-1)bso_31] + i29[0] ≥ 0)

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

(30)    (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 = 0∧[(-1)bso_31] + i29[0] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
• ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(LOAD344(i38[8], +(i25[8], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

• LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])
• ([1] + i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + i40[7] ≥ 0)
• ([1] + [-1]i40[7] ≥ 0∧i25[7] ≥ 0∧i40[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i40[7] ≥ 0∧0 = 0∧0 = 0∧[2 + (-1)bso_27] + [-1]i40[7] ≥ 0)

• (i29[0] ≥ 0 ⇒ (UIncreasing(LOAD475(i25[1], i29[1], i29[1], 0)), ≥)∧0 = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i29[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

• (i29[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD344(>(i29[0], 1), i29[0], i25[0])), ≥)∧0 = 0∧[(-1)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 = 0∧[(-1)bso_31] + i29[0] ≥ 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_LOAD4752(x1, x2, x3, x4, x5)) = [-1] + [-1]x1
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(LOAD475(x1, x2, x3, x4)) = [1] + [-1]x3
POL(&&(x1, x2)) = 0
POL(<=(x1, x2)) = [-1]
POL(>(x1, x2)) = 0
POL(0) = 0
POL(COND_LOAD344(x1, x2, x3)) = [1] + [-1]x2

The following pairs are in P>:

LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])

The following pairs are in Pbound:

LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(&&(<=(i40[7], 1), >(+(i25[7], 1), 0)), i25[7], i29[7], i40[7], i38[7])

The following pairs are in P:

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

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

### (20) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

(8) -> (0), if ((i25[8] + 1* i25[0])∧(i38[8]* i29[0]))

(0) -> (1), if ((i29[0] > 1* TRUE)∧(i29[0]* i29[1])∧(i25[0]* i25[1]))

The set Q consists of the following terms:

### (21) IDependencyGraphProof (EQUIVALENT transformation)

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

### (23) 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 contains the following rules and edges:

The set Q consists of the following terms:

### (24) IDependencyGraphProof (EQUIVALENT transformation)

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

### (26) 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): LOAD475(i25[4], i29[4], i41[4], i38[4]) → COND_LOAD4751(i41[4] > 0 && i41[4] <= 1, i25[4], i29[4], i41[4], i38[4])
(7): LOAD475(i25[7], i29[7], i40[7], i38[7]) → COND_LOAD4752(i40[7] <= 1 && i25[7] + 1 > 0, i25[7], i29[7], i40[7], i38[7])

(4) -> (5), if ((i38[4]* i38[5])∧(i41[4]* i41[5])∧(i41[4] > 0 && i41[4] <= 1* TRUE)∧(i29[4]* i29[5])∧(i25[4]* i25[5]))

The set Q consists of the following terms: