### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Log
`public class Log{  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);      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 157 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:
Load1049(1, i53, i91, i84) → Cond_Load1049(i91 > 1 && i84 + 1 > 0, 1, i53, i91, i84)
Cond_Load1049(TRUE, 1, i53, i91, i84) → Load1049(1, i53, i91 - 2, i84 + 1)
Load1049(1, i53, i91, i84) → Cond_Load10491(i91 > 0 && i91 <= 1, 1, i53, i91, i84)
Load1049(1, i53, i90, i84) → Cond_Load10492(i90 <= 1 && i53 + 1 > 0, 1, i53, i90, i84)
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:
Load1049(i53, i91, i84) → Cond_Load1049(i91 > 1 && i84 + 1 > 0, i53, i91, i84)
Cond_Load1049(TRUE, i53, i91, i84) → Load1049(i53, i91 - 2, i84 + 1)
Load1049(i53, i91, i84) → Cond_Load10491(i91 > 0 && i91 <= 1, i53, i91, i84)
Load1049(i53, i90, i84) → Cond_Load10492(i90 <= 1 && i53 + 1 > 0, i53, i90, i84)
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:
Load1049(i53, i91, i84) → Cond_Load1049(i91 > 1 && i84 + 1 > 0, i53, i91, i84)
Cond_Load1049(TRUE, i53, i91, i84) → Load1049(i53, i91 - 2, i84 + 1)
Load1049(i53, i91, i84) → Cond_Load10491(i91 > 0 && i91 <= 1, i53, i91, i84)
Load1049(i53, i90, i84) → Cond_Load10492(i90 <= 1 && i53 + 1 > 0, i53, i90, i84)

The integer pair graph contains the following rules and edges:
(2): LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(i91[2] > 1 && i84[2] + 1 > 0, i53[2], i91[2], i84[2])
(3): COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], i91[3] - 2, i84[3] + 1)
(4): LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(i91[4] > 0 && i91[4] <= 1, i53[4], i91[4], i84[4])
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])

(0) -> (1), if ((i63[0]* i63[1])∧(i63[0] > 1* TRUE)∧(i53[0]* i53[1]))

(1) -> (2), if ((i53[1]* i53[2])∧(0* i84[2])∧(i63[1]* i91[2]))

(1) -> (4), if ((i53[1]* i53[4])∧(0* i84[4])∧(i63[1]* i91[4]))

(1) -> (7), if ((i53[1]* i53[7])∧(i63[1]* i90[7])∧(0* i84[7]))

(2) -> (3), if ((i84[2]* i84[3])∧(i91[2]* i91[3])∧(i53[2]* i53[3])∧(i91[2] > 1 && i84[2] + 1 > 0* TRUE))

(3) -> (2), if ((i91[3] - 2* i91[2])∧(i84[3] + 1* i84[2])∧(i53[3]* i53[2]))

(3) -> (4), if ((i84[3] + 1* i84[4])∧(i91[3] - 2* i91[4])∧(i53[3]* i53[4]))

(3) -> (7), if ((i84[3] + 1* i84[7])∧(i53[3]* i53[7])∧(i91[3] - 2* i90[7]))

(4) -> (5), if ((i84[4]* i84[5])∧(i91[4] > 0 && i91[4] <= 1* TRUE)∧(i91[4]* i91[5])∧(i53[4]* i53[5]))

(5) -> (6), if ((i53[5]* i53[6])∧(i84[5]* i84[6]))

(6) -> (0), if ((i53[6] + 1* i53[0])∧(i84[6]* i63[0]))

(7) -> (8), if ((i90[7]* i90[8])∧(i90[7] <= 1 && i53[7] + 1 > 0* TRUE)∧(i84[7]* i84[8])∧(i53[7]* i53[8]))

(8) -> (0), if ((i53[8] + 1* i53[0])∧(i84[8]* i63[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): LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(i91[2] > 1 && i84[2] + 1 > 0, i53[2], i91[2], i84[2])
(3): COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], i91[3] - 2, i84[3] + 1)
(4): LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(i91[4] > 0 && i91[4] <= 1, i53[4], i91[4], i84[4])
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])

(0) -> (1), if ((i63[0]* i63[1])∧(i63[0] > 1* TRUE)∧(i53[0]* i53[1]))

(1) -> (2), if ((i53[1]* i53[2])∧(0* i84[2])∧(i63[1]* i91[2]))

(1) -> (4), if ((i53[1]* i53[4])∧(0* i84[4])∧(i63[1]* i91[4]))

(1) -> (7), if ((i53[1]* i53[7])∧(i63[1]* i90[7])∧(0* i84[7]))

(2) -> (3), if ((i84[2]* i84[3])∧(i91[2]* i91[3])∧(i53[2]* i53[3])∧(i91[2] > 1 && i84[2] + 1 > 0* TRUE))

(3) -> (2), if ((i91[3] - 2* i91[2])∧(i84[3] + 1* i84[2])∧(i53[3]* i53[2]))

(3) -> (4), if ((i84[3] + 1* i84[4])∧(i91[3] - 2* i91[4])∧(i53[3]* i53[4]))

(3) -> (7), if ((i84[3] + 1* i84[7])∧(i53[3]* i53[7])∧(i91[3] - 2* i90[7]))

(4) -> (5), if ((i84[4]* i84[5])∧(i91[4] > 0 && i91[4] <= 1* TRUE)∧(i91[4]* i91[5])∧(i53[4]* i53[5]))

(5) -> (6), if ((i53[5]* i53[6])∧(i84[5]* i84[6]))

(6) -> (0), if ((i53[6] + 1* i53[0])∧(i84[6]* i63[0]))

(7) -> (8), if ((i90[7]* i90[8])∧(i90[7] <= 1 && i53[7] + 1 > 0* TRUE)∧(i84[7]* i84[8])∧(i53[7]* i53[8]))

(8) -> (0), if ((i53[8] + 1* i53[0])∧(i84[8]* i63[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 LOAD872(i63, i53) → COND_LOAD872(>(i63, 1), i63, i53) the following chains were created:
• We consider the chain LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[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)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧[(-1)Bound*bni_35] + [bni_35]i63[0] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(4)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧[(-1)Bound*bni_35] + [bni_35]i63[0] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(5)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧[(-1)Bound*bni_35] + [bni_35]i63[0] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(6)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧0 = 0∧[(-1)Bound*bni_35] + [bni_35]i63[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)    (i63[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧0 = 0∧[(-1)Bound*bni_35 + (2)bni_35] + [bni_35]i63[0] ≥ 0∧0 = 0∧[(-1)bso_36] ≥ 0)

For Pair COND_LOAD872(TRUE, i63, i53) → LOAD1049(i53, i63, 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)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(11)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(12)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(13)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)

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

(14)    (i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i63[0] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 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)    (i63[0] + [-2] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(18)    (i63[0] + [-2] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(19)    (i63[0] + [-2] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(20)    (i63[0] + [-2] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 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)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(24)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(25)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[6] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

We solved constraint (25) using rule (IDP_SMT_SPLIT).
• We consider the chain LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)), LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)) which results in the following constraint:

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)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(29)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(30)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(31)    (i63[0] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(32)    (i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 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)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(36)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(37)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i63[0] + [-1] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

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

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

(40)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(41)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

(42)    (i63[0] + [-2] ≥ 0∧[1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[7] + [1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

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

For Pair LOAD1049(i53, i91, i84) → COND_LOAD1049(&&(>(i91, 1), >(+(i84, 1), 0)), i53, i91, i84) the following chains were created:
• We consider the chain LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)) which results in the following constraint:

(43)    (i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUELOAD1049(i53[2], i91[2], i84[2])≥NonInfC∧LOAD1049(i53[2], i91[2], i84[2])≥COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])∧(UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥))

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

(44)    (>(i91[2], 1)=TRUE>(+(i84[2], 1), 0)=TRUELOAD1049(i53[2], i91[2], i84[2])≥NonInfC∧LOAD1049(i53[2], i91[2], i84[2])≥COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])∧(UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥))

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

(45)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i84[2] + [bni_39]i91[2] ≥ 0∧[1 + (-1)bso_40] ≥ 0)

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

(46)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i84[2] + [bni_39]i91[2] ≥ 0∧[1 + (-1)bso_40] ≥ 0)

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

(47)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i84[2] + [bni_39]i91[2] ≥ 0∧[1 + (-1)bso_40] ≥ 0)

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

(48)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥)∧0 = 0∧[(-1)Bound*bni_39] + [bni_39]i84[2] + [bni_39]i91[2] ≥ 0∧0 = 0∧[1 + (-1)bso_40] ≥ 0)

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

(49)    (i91[2] ≥ 0∧i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥)∧0 = 0∧[(-1)Bound*bni_39 + (2)bni_39] + [bni_39]i84[2] + [bni_39]i91[2] ≥ 0∧0 = 0∧[1 + (-1)bso_40] ≥ 0)

For Pair COND_LOAD1049(TRUE, i53, i91, i84) → LOAD1049(i53, -(i91, 2), +(i84, 1)) the following chains were created:
• We consider the chain LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)) which results in the following constraint:

(50)    (i63[0]=i63[1]>(i63[0], 1)=TRUEi53[0]=i53[1]i53[1]=i53[2]0=i84[2]i63[1]=i91[2]i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE-(i91[3], 2)=i91[2]1+(i84[3], 1)=i84[2]1i53[3]=i53[2]1i84[2]1=i84[3]1i91[2]1=i91[3]1i53[2]1=i53[3]1&&(>(i91[2]1, 1), >(+(i84[2]1, 1), 0))=TRUECOND_LOAD1049(TRUE, i53[3], i91[3], i84[3])≥NonInfC∧COND_LOAD1049(TRUE, i53[3], i91[3], i84[3])≥LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))∧(UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[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:

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

(52)    (i63[0] + [-2] ≥ 0∧i63[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(53)    (i63[0] + [-2] ≥ 0∧i63[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(54)    (i63[0] + [-2] ≥ 0∧i63[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(55)    (i63[0] + [-2] ≥ 0∧i63[0] + [-4] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(56)    (i63[0] ≥ 0∧[-2] + i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(57)    ([2] + i63[0] ≥ 0∧i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

(58)    (i63[0]=i63[1]>(i63[0], 1)=TRUEi53[0]=i53[1]i53[1]=i53[2]0=i84[2]i63[1]=i91[2]i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE+(i84[3], 1)=i84[4]-(i91[3], 2)=i91[4]i53[3]=i53[4]i84[4]=i84[5]&&(>(i91[4], 0), <=(i91[4], 1))=TRUEi91[4]=i91[5]i53[4]=i53[5]COND_LOAD1049(TRUE, i53[3], i91[3], i84[3])≥NonInfC∧COND_LOAD1049(TRUE, i53[3], i91[3], i84[3])≥LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))∧(UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[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:

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

(60)    (i63[0] + [-2] ≥ 0∧i63[0] + [-3] ≥ 0∧[3] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(61)    (i63[0] + [-2] ≥ 0∧i63[0] + [-3] ≥ 0∧[3] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(62)    (i63[0] + [-2] ≥ 0∧i63[0] + [-3] ≥ 0∧[3] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(63)    (i63[0] + [-2] ≥ 0∧i63[0] + [-3] ≥ 0∧[3] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(64)    (i63[0] ≥ 0∧[-1] + i63[0] ≥ 0∧[1] + [-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(65)    ([1] + i63[0] ≥ 0∧i63[0] ≥ 0∧[-1]i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 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(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

• We consider the chain LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)) which results in the following constraint:

(67)    (i63[0]=i63[1]>(i63[0], 1)=TRUEi53[0]=i53[1]i53[1]=i53[2]0=i84[2]i63[1]=i91[2]i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE+(i84[3], 1)=i84[7]i53[3]=i53[7]-(i91[3], 2)=i90[7]i90[7]=i90[8]&&(<=(i90[7], 1), >(+(i53[7], 1), 0))=TRUEi84[7]=i84[8]i53[7]=i53[8]COND_LOAD1049(TRUE, i53[3], i91[3], i84[3])≥NonInfC∧COND_LOAD1049(TRUE, i53[3], i91[3], i84[3])≥LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))∧(UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[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:

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

(69)    (i63[0] + [-2] ≥ 0∧[3] + [-1]i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(70)    (i63[0] + [-2] ≥ 0∧[3] + [-1]i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(71)    (i63[0] + [-2] ≥ 0∧[3] + [-1]i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[(-1)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(72)    (i63[0] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)

• We consider the chain LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)) which results in the following constraint:

(73)    (i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE-(i91[3], 2)=i91[2]1+(i84[3], 1)=i84[2]1i53[3]=i53[2]1i84[2]1=i84[3]1i91[2]1=i91[3]1i53[2]1=i53[3]1&&(>(i91[2]1, 1), >(+(i84[2]1, 1), 0))=TRUE-(i91[3]1, 2)=i91[2]2+(i84[3]1, 1)=i84[2]2i53[3]1=i53[2]2i84[2]2=i84[3]2i91[2]2=i91[3]2i53[2]2=i53[3]2&&(>(i91[2]2, 1), >(+(i84[2]2, 1), 0))=TRUECOND_LOAD1049(TRUE, i53[3]1, i91[3]1, i84[3]1)≥NonInfC∧COND_LOAD1049(TRUE, i53[3]1, i91[3]1, i84[3]1)≥LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))∧(UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥))

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

(74)    (>(i91[2], 1)=TRUE>(+(i84[2], 1), 0)=TRUE>(-(i91[2], 2), 1)=TRUE>(+(+(i84[2], 1), 1), 0)=TRUE>(-(-(i91[2], 2), 2), 1)=TRUE>(+(+(+(i84[2], 1), 1), 1), 0)=TRUECOND_LOAD1049(TRUE, i53[2], -(i91[2], 2), +(i84[2], 1))≥NonInfC∧COND_LOAD1049(TRUE, i53[2], -(i91[2], 2), +(i84[2], 1))≥LOAD1049(i53[2], -(-(i91[2], 2), 2), +(+(i84[2], 1), 1))∧(UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥))

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

(75)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-6] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(76)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-6] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(77)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-6] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(78)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-6] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(79)    (i91[2] ≥ 0∧i84[2] ≥ 0∧[-2] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[-4] + i91[2] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(80)    ([2] + i91[2] ≥ 0∧i84[2] ≥ 0∧i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[-2] + i91[2] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(81)    ([4] + i91[2] ≥ 0∧i84[2] ≥ 0∧[2] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] ≥ 0∧i84[2] + [2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(4)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(82)    ([4] + i91[2] ≥ 0∧i84[2] ≥ 0∧[2] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(4)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

• We consider the chain LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4]), COND_LOAD10491(TRUE, i53[5], i91[5], i84[5]) → LOAD1065(i53[5], i84[5]) which results in the following constraint:

(83)    (i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE-(i91[3], 2)=i91[2]1+(i84[3], 1)=i84[2]1i53[3]=i53[2]1i84[2]1=i84[3]1i91[2]1=i91[3]1i53[2]1=i53[3]1&&(>(i91[2]1, 1), >(+(i84[2]1, 1), 0))=TRUE+(i84[3]1, 1)=i84[4]-(i91[3]1, 2)=i91[4]i53[3]1=i53[4]i84[4]=i84[5]&&(>(i91[4], 0), <=(i91[4], 1))=TRUEi91[4]=i91[5]i53[4]=i53[5]COND_LOAD1049(TRUE, i53[3]1, i91[3]1, i84[3]1)≥NonInfC∧COND_LOAD1049(TRUE, i53[3]1, i91[3]1, i84[3]1)≥LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))∧(UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥))

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

(84)    (>(i91[2], 1)=TRUE>(+(i84[2], 1), 0)=TRUE>(-(i91[2], 2), 1)=TRUE>(+(+(i84[2], 1), 1), 0)=TRUE>(-(-(i91[2], 2), 2), 0)=TRUE<=(-(-(i91[2], 2), 2), 1)=TRUECOND_LOAD1049(TRUE, i53[2], -(i91[2], 2), +(i84[2], 1))≥NonInfC∧COND_LOAD1049(TRUE, i53[2], -(i91[2], 2), +(i84[2], 1))≥LOAD1049(i53[2], -(-(i91[2], 2), 2), +(+(i84[2], 1), 1))∧(UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥))

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

(85)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-5] ≥ 0∧[5] + [-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(86)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-5] ≥ 0∧[5] + [-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(87)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-5] ≥ 0∧[5] + [-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(88)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] + [-5] ≥ 0∧[5] + [-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(89)    (i91[2] ≥ 0∧i84[2] ≥ 0∧[-2] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[-3] + i91[2] ≥ 0∧[3] + [-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(90)    ([2] + i91[2] ≥ 0∧i84[2] ≥ 0∧i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[-1] + i91[2] ≥ 0∧[1] + [-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(91)    ([3] + i91[2] ≥ 0∧i84[2] ≥ 0∧[1] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] ≥ 0∧[-1]i91[2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(92)    ([3] ≥ 0∧i84[2] ≥ 0∧[1] ≥ 0∧i84[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

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

(93)    (i84[2] ≥ 0∧[1] ≥ 0∧i84[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)

• We consider the chain LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)) which results in the following constraint:

(94)    (i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE-(i91[3], 2)=i91[2]1+(i84[3], 1)=i84[2]1i53[3]=i53[2]1i84[2]1=i84[3]1i91[2]1=i91[3]1i53[2]1=i53[3]1&&(>(i91[2]1, 1), >(+(i84[2]1, 1), 0))=TRUE+(i84[3]1, 1)=i84[7]i53[3]1=i53[7]-(i91[3]1, 2)=i90[7]i90[7]=i90[8]&&(<=(i90[7], 1), >(+(i53[7], 1), 0))=TRUEi84[7]=i84[8]i53[7]=i53[8]COND_LOAD1049(TRUE, i53[3]1, i91[3]1, i84[3]1)≥NonInfC∧COND_LOAD1049(TRUE, i53[3]1, i91[3]1, i84[3]1)≥LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))∧(UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥))

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

(95)    (>(i91[2], 1)=TRUE>(+(i84[2], 1), 0)=TRUE>(-(i91[2], 2), 1)=TRUE>(+(+(i84[2], 1), 1), 0)=TRUE<=(-(-(i91[2], 2), 2), 1)=TRUE>(+(i53[7], 1), 0)=TRUECOND_LOAD1049(TRUE, i53[7], -(i91[2], 2), +(i84[2], 1))≥NonInfC∧COND_LOAD1049(TRUE, i53[7], -(i91[2], 2), +(i84[2], 1))≥LOAD1049(i53[7], -(-(i91[2], 2), 2), +(+(i84[2], 1), 1))∧(UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥))

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

(96)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧[5] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(97)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧[5] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(98)    (i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧i91[2] + [-4] ≥ 0∧i84[2] + [1] ≥ 0∧[5] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(99)    (i91[2] ≥ 0∧i84[2] ≥ 0∧[-2] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[3] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

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

(100)    ([2] + i91[2] ≥ 0∧i84[2] ≥ 0∧i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[1] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

For Pair LOAD1049(i53, i91, i84) → COND_LOAD10491(&&(>(i91, 0), <=(i91, 1)), i53, i91, i84) the following chains were created:
• We consider the chain LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4]), COND_LOAD10491(TRUE, i53[5], i91[5], i84[5]) → LOAD1065(i53[5], i84[5]) which results in the following constraint:

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

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

(103)    (i91[4] + [-1] ≥ 0∧[1] + [-1]i91[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[(-1)Bound*bni_43] + [bni_43]i84[4] + [bni_43]i91[4] ≥ 0∧[-1 + (-1)bso_44] + i91[4] ≥ 0)

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

(104)    (i91[4] + [-1] ≥ 0∧[1] + [-1]i91[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[(-1)Bound*bni_43] + [bni_43]i84[4] + [bni_43]i91[4] ≥ 0∧[-1 + (-1)bso_44] + i91[4] ≥ 0)

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

(105)    (i91[4] + [-1] ≥ 0∧[1] + [-1]i91[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[(-1)Bound*bni_43] + [bni_43]i84[4] + [bni_43]i91[4] ≥ 0∧[-1 + (-1)bso_44] + i91[4] ≥ 0)

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

(106)    (i91[4] + [-1] ≥ 0∧[1] + [-1]i91[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43] + [bni_43]i91[4] ≥ 0∧0 = 0∧0 = 0∧[-1 + (-1)bso_44] + i91[4] ≥ 0)

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

(107)    (i91[4] ≥ 0∧[-1]i91[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43 + bni_43] + [bni_43]i91[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_44] + i91[4] ≥ 0)

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

(108)    (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43 + bni_43] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)

For Pair COND_LOAD10491(TRUE, i53, i91, i84) → LOAD1065(i53, i84) the following chains were created:
• We consider the chain COND_LOAD10491(TRUE, i53[5], i91[5], i84[5]) → LOAD1065(i53[5], i84[5]), LOAD1065(i53[6], i84[6]) → LOAD872(i84[6], +(i53[6], 1)) which results in the following constraint:

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

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

(111)    ((UIncreasing(LOAD1065(i53[5], i84[5])), ≥)∧[(-1)bso_46] ≥ 0)

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

(112)    ((UIncreasing(LOAD1065(i53[5], i84[5])), ≥)∧[(-1)bso_46] ≥ 0)

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

(113)    ((UIncreasing(LOAD1065(i53[5], i84[5])), ≥)∧[(-1)bso_46] ≥ 0)

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

(114)    ((UIncreasing(LOAD1065(i53[5], i84[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

For Pair LOAD1065(i53, i84) → LOAD872(i84, +(i53, 1)) the following chains were created:

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

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

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

(118)    (i84[3] + [-1] ≥ 0∧i91[3] + [-3] ≥ 0∧[3] + [-1]i91[3] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧[1 + (-1)bso_48] ≥ 0)

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

(119)    (i84[3] + [-1] ≥ 0∧i91[3] + [-3] ≥ 0∧[3] + [-1]i91[3] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧[1 + (-1)bso_48] ≥ 0)

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

(120)    (i84[3] + [-1] ≥ 0∧i91[3] + [-3] ≥ 0∧[3] + [-1]i91[3] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧[1 + (-1)bso_48] ≥ 0)

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

(121)    (i84[3] + [-1] ≥ 0∧i91[3] + [-3] ≥ 0∧[3] + [-1]i91[3] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧0 = 0∧[(2)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧0 = 0∧[1 + (-1)bso_48] ≥ 0)

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

(122)    (i84[3] ≥ 0∧i91[3] + [-3] ≥ 0∧[3] + [-1]i91[3] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧0 = 0∧[(3)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧0 = 0∧[1 + (-1)bso_48] ≥ 0)

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

(123)    (i84[3] ≥ 0∧[3] + [-1]i91[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧0 = 0∧[(3)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧0 = 0∧[1 + (-1)bso_48] ≥ 0)

For Pair LOAD1049(i53, i90, i84) → COND_LOAD10492(&&(<=(i90, 1), >(+(i53, 1), 0)), i53, i90, i84) the following chains were created:
• We consider the chain LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)) which results in the following constraint:

(124)    (i90[7]=i90[8]&&(<=(i90[7], 1), >(+(i53[7], 1), 0))=TRUEi84[7]=i84[8]i53[7]=i53[8]LOAD1049(i53[7], i90[7], i84[7])≥NonInfC∧LOAD1049(i53[7], i90[7], i84[7])≥COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])∧(UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥))

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

(125)    (<=(i90[7], 1)=TRUE>(+(i53[7], 1), 0)=TRUELOAD1049(i53[7], i90[7], i84[7])≥NonInfC∧LOAD1049(i53[7], i90[7], i84[7])≥COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])∧(UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥))

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

(126)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i84[7] + [bni_49]i90[7] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(127)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i84[7] + [bni_49]i90[7] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(128)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[(-1)Bound*bni_49] + [bni_49]i84[7] + [bni_49]i90[7] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(129)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_49] = 0∧[(-1)Bound*bni_49] + [bni_49]i90[7] ≥ 0∧0 = 0∧[(-1)bso_50] ≥ 0)

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

(130)    ([1] + i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_49] = 0∧[(-1)Bound*bni_49] + [(-1)bni_49]i90[7] ≥ 0∧0 = 0∧[(-1)bso_50] ≥ 0)

(131)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_49] = 0∧[(-1)Bound*bni_49] + [bni_49]i90[7] ≥ 0∧0 = 0∧[(-1)bso_50] ≥ 0)

For Pair COND_LOAD10492(TRUE, i53, i90, i84) → LOAD872(i84, +(i53, 1)) the following chains were created:

We solved constraint (132) using rules (I), (II), (III), (IV), (IDP_CONSTANT_FOLD), (IDP_BOOLEAN).
• We consider the chain LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2]), COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1)), LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)), LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0) which results in the following constraint:

(133)    (i84[2]=i84[3]i91[2]=i91[3]i53[2]=i53[3]&&(>(i91[2], 1), >(+(i84[2], 1), 0))=TRUE+(i84[3], 1)=i84[7]i53[3]=i53[7]-(i91[3], 2)=i90[7]i90[7]=i90[8]&&(<=(i90[7], 1), >(+(i53[7], 1), 0))=TRUEi84[7]=i84[8]i53[7]=i53[8]+(i53[8], 1)=i53[0]i84[8]=i63[0]i63[0]=i63[1]>(i63[0], 1)=TRUEi53[0]=i53[1]COND_LOAD10492(TRUE, i53[8], i90[8], i84[8])≥NonInfC∧COND_LOAD10492(TRUE, i53[8], i90[8], i84[8])≥LOAD872(i84[8], +(i53[8], 1))∧(UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥))

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

(134)    (>(+(i84[2], 1), 1)=TRUE>(i91[2], 1)=TRUE>(+(i84[2], 1), 0)=TRUE<=(-(i91[2], 2), 1)=TRUE>(+(i53[7], 1), 0)=TRUECOND_LOAD10492(TRUE, i53[7], -(i91[2], 2), +(i84[2], 1))≥NonInfC∧COND_LOAD10492(TRUE, i53[7], -(i91[2], 2), +(i84[2], 1))≥LOAD872(+(i84[2], 1), +(i53[7], 1))∧(UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥))

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

(135)    (i84[2] + [-1] ≥ 0∧i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧[3] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]i84[2] + [bni_51]i91[2] ≥ 0∧[-2 + (-1)bso_52] + i91[2] ≥ 0)

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

(136)    (i84[2] + [-1] ≥ 0∧i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧[3] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]i84[2] + [bni_51]i91[2] ≥ 0∧[-2 + (-1)bso_52] + i91[2] ≥ 0)

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

(137)    (i84[2] + [-1] ≥ 0∧i91[2] + [-2] ≥ 0∧i84[2] ≥ 0∧[3] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [bni_51]i84[2] + [bni_51]i91[2] ≥ 0∧[-2 + (-1)bso_52] + i91[2] ≥ 0)

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

(138)    (i84[2] ≥ 0∧i91[2] + [-2] ≥ 0∧[1] + i84[2] ≥ 0∧[3] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)Bound*bni_51] + [bni_51]i84[2] + [bni_51]i91[2] ≥ 0∧[-2 + (-1)bso_52] + i91[2] ≥ 0)

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

(139)    (i84[2] ≥ 0∧i91[2] ≥ 0∧[1] + i84[2] ≥ 0∧[1] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)Bound*bni_51 + (2)bni_51] + [bni_51]i84[2] + [bni_51]i91[2] ≥ 0∧[(-1)bso_52] + i91[2] ≥ 0)

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

• (i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i63[0] ≥ 0∧0 = 0∧[(-1)bso_38] ≥ 0)
• (i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(-1)Bound*bni_37 + (2)bni_37] + [bni_37]i63[0] ≥ 0∧[(-1)bso_38] ≥ 0)

• LOAD1049(i53, i91, i84) → COND_LOAD1049(&&(>(i91, 1), >(+(i84, 1), 0)), i53, i91, i84)
• (i91[2] ≥ 0∧i84[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])), ≥)∧0 = 0∧[(-1)Bound*bni_39 + (2)bni_39] + [bni_39]i84[2] + [bni_39]i91[2] ≥ 0∧0 = 0∧[1 + (-1)bso_40] ≥ 0)

• ([2] + i63[0] ≥ 0∧i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• ([1] ≥ 0∧0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧0 = 0∧[(2)bni_41 + (-1)Bound*bni_41] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• (i63[0] ≥ 0∧[1] + [-1]i63[0] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3], -(i91[3], 2), +(i84[3], 1))), ≥)∧[bni_41 + (-1)Bound*bni_41] + [bni_41]i63[0] ≥ 0∧[(-1)bso_42] ≥ 0)
• ([4] + i91[2] ≥ 0∧i84[2] ≥ 0∧[2] + i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧i91[2] ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(4)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• (i84[2] ≥ 0∧[1] ≥ 0∧i84[2] + [1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧0 = 0∧[(3)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] ≥ 0∧0 = 0∧[(-1)bso_42] ≥ 0)
• ([2] + i91[2] ≥ 0∧i84[2] ≥ 0∧i91[2] ≥ 0∧i84[2] + [1] ≥ 0∧[1] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[3]1, -(i91[3]1, 2), +(i84[3]1, 1))), ≥)∧[(2)bni_41 + (-1)Bound*bni_41] + [bni_41]i84[2] + [bni_41]i91[2] ≥ 0∧[(-1)bso_42] ≥ 0)

• LOAD1049(i53, i91, i84) → COND_LOAD10491(&&(>(i91, 0), <=(i91, 1)), i53, i91, i84)
• (0 ≥ 0∧0 ≥ 0 ⇒ (UIncreasing(COND_LOAD10491(&&(>(i91[4], 0), <=(i91[4], 1)), i53[4], i91[4], i84[4])), ≥)∧[bni_43] = 0∧0 = 0∧[(-1)Bound*bni_43 + bni_43] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_44] ≥ 0)

• ((UIncreasing(LOAD1065(i53[5], i84[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_46] ≥ 0)

• (i84[3] ≥ 0∧[3] + [-1]i91[3] ≥ 0∧[-1] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[6], +(i53[6], 1))), ≥)∧0 = 0∧[(3)bni_47 + (-1)Bound*bni_47] + [bni_47]i84[3] ≥ 0∧0 = 0∧[1 + (-1)bso_48] ≥ 0)

• LOAD1049(i53, i90, i84) → COND_LOAD10492(&&(<=(i90, 1), >(+(i53, 1), 0)), i53, i90, i84)
• ([1] + i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_49] = 0∧[(-1)Bound*bni_49] + [(-1)bni_49]i90[7] ≥ 0∧0 = 0∧[(-1)bso_50] ≥ 0)
• ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_49] = 0∧[(-1)Bound*bni_49] + [bni_49]i90[7] ≥ 0∧0 = 0∧[(-1)bso_50] ≥ 0)

• (i84[2] ≥ 0∧i91[2] ≥ 0∧[1] + i84[2] ≥ 0∧[1] + [-1]i91[2] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)Bound*bni_51 + (2)bni_51] + [bni_51]i84[2] + [bni_51]i91[2] ≥ 0∧[(-1)bso_52] + i91[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(>(x1, x2)) = [-1]
POL(1) = [1]
POL(LOAD1049(x1, x2, x3)) = x3 + x2
POL(0) = 0
POL(COND_LOAD1049(x1, x2, x3, x4)) = [-1] + x4 + x3
POL(&&(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(-(x1, x2)) = x1 + [-1]x2
POL(2) = [2]
POL(COND_LOAD10491(x1, x2, x3, x4)) = [1] + x4
POL(<=(x1, x2)) = [-1]
POL(LOAD1065(x1, x2)) = [1] + x2
POL(COND_LOAD10492(x1, x2, x3, x4)) = x4 + x3

The following pairs are in P>:

LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])

The following pairs are in Pbound:

LOAD1049(i53[2], i91[2], i84[2]) → COND_LOAD1049(&&(>(i91[2], 1), >(+(i84[2], 1), 0)), i53[2], i91[2], i84[2])

The following pairs are in P:

LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[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:
(3): COND_LOAD1049(TRUE, i53[3], i91[3], i84[3]) → LOAD1049(i53[3], i91[3] - 2, i84[3] + 1)
(4): LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(i91[4] > 0 && i91[4] <= 1, i53[4], i91[4], i84[4])
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])

(8) -> (0), if ((i53[8] + 1* i53[0])∧(i84[8]* i63[0]))

(0) -> (1), if ((i63[0]* i63[1])∧(i63[0] > 1* TRUE)∧(i53[0]* i53[1]))

(1) -> (4), if ((i53[1]* i53[4])∧(0* i84[4])∧(i63[1]* i91[4]))

(3) -> (4), if ((i84[3] + 1* i84[4])∧(i91[3] - 2* i91[4])∧(i53[3]* i53[4]))

(4) -> (5), if ((i84[4]* i84[5])∧(i91[4] > 0 && i91[4] <= 1* TRUE)∧(i91[4]* i91[5])∧(i53[4]* i53[5]))

(1) -> (7), if ((i53[1]* i53[7])∧(i63[1]* i90[7])∧(0* i84[7]))

(3) -> (7), if ((i84[3] + 1* i84[7])∧(i53[3]* i53[7])∧(i91[3] - 2* i90[7]))

(7) -> (8), if ((i90[7]* i90[8])∧(i90[7] <= 1 && i53[7] + 1 > 0* TRUE)∧(i84[7]* i84[8])∧(i53[7]* i53[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 3 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:
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])

(8) -> (0), if ((i53[8] + 1* i53[0])∧(i84[8]* i63[0]))

(0) -> (1), if ((i63[0]* i63[1])∧(i63[0] > 1* TRUE)∧(i53[0]* i53[1]))

(1) -> (7), if ((i53[1]* i53[7])∧(i63[1]* i90[7])∧(0* i84[7]))

(7) -> (8), if ((i90[7]* i90[8])∧(i90[7] <= 1 && i53[7] + 1 > 0* TRUE)∧(i84[7]* i84[8])∧(i53[7]* i53[8]))

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_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)) the following chains were created:
• We consider the chain LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)), LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[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]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]i84[7] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(4)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]i84[7] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(5)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [bni_22]i84[7] ≥ 0∧[(-1)bso_23] ≥ 0)

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

(6)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

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

(7)    ([1] + i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

(8)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

For Pair LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]) the following chains were created:
• We consider the chain LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7]), COND_LOAD10492(TRUE, i53[8], i90[8], i84[8]) → LOAD872(i84[8], +(i53[8], 1)) which results in the following constraint:

(9)    (i90[7]=i90[8]&&(<=(i90[7], 1), >(+(i53[7], 1), 0))=TRUEi84[7]=i84[8]i53[7]=i53[8]LOAD1049(i53[7], i90[7], i84[7])≥NonInfC∧LOAD1049(i53[7], i90[7], i84[7])≥COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])∧(UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥))

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

(10)    (<=(i90[7], 1)=TRUE>(+(i53[7], 1), 0)=TRUELOAD1049(i53[7], i90[7], i84[7])≥NonInfC∧LOAD1049(i53[7], i90[7], i84[7])≥COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])∧(UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥))

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

(11)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i84[7] + [(-1)bni_24]i90[7] ≥ 0∧[3 + (-1)bso_25] + [-1]i90[7] ≥ 0)

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

(12)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i84[7] + [(-1)bni_24]i90[7] ≥ 0∧[3 + (-1)bso_25] + [-1]i90[7] ≥ 0)

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

(13)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i84[7] + [(-1)bni_24]i90[7] ≥ 0∧[3 + (-1)bso_25] + [-1]i90[7] ≥ 0)

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

(14)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_24] = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i90[7] ≥ 0∧0 = 0∧[3 + (-1)bso_25] + [-1]i90[7] ≥ 0)

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

(15)    ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_24] = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i90[7] ≥ 0∧0 = 0∧[3 + (-1)bso_25] + [-1]i90[7] ≥ 0)

(16)    ([1] + i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_24] = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i90[7] ≥ 0∧0 = 0∧[3 + (-1)bso_25] + i90[7] ≥ 0)

For Pair COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0) the following chains were created:
• We consider the chain LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[1], 0), LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[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)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i63[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(20)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i63[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(21)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i63[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(22)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(2)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]i63[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

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

(23)    (i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_26] + [(-1)bni_26]i63[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]) the following chains were created:
• We consider the chain LOAD872(i63[0], i53[0]) → COND_LOAD872(>(i63[0], 1), i63[0], i53[0]), COND_LOAD872(TRUE, i63[1], i53[1]) → LOAD1049(i53[1], i63[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)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i63[0] ≥ 0∧[-3 + (-1)bso_29] + [2]i63[0] ≥ 0)

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

(27)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i63[0] ≥ 0∧[-3 + (-1)bso_29] + [2]i63[0] ≥ 0)

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

(28)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i63[0] ≥ 0∧[-3 + (-1)bso_29] + [2]i63[0] ≥ 0)

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

(29)    (i63[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧0 = 0∧[(-1)bni_28 + (-1)Bound*bni_28] + [bni_28]i63[0] ≥ 0∧0 = 0∧[-3 + (-1)bso_29] + [2]i63[0] ≥ 0)

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

(30)    (i63[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧0 = 0∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i63[0] ≥ 0∧0 = 0∧[1 + (-1)bso_29] + [2]i63[0] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• ([1] + i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)
• ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(LOAD872(i84[8], +(i53[8], 1))), ≥)∧[bni_22] = 0∧[(-1)bni_22 + (-1)Bound*bni_22] ≥ 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])
• ([1] + [-1]i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_24] = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]i90[7] ≥ 0∧0 = 0∧[3 + (-1)bso_25] + [-1]i90[7] ≥ 0)
• ([1] + i90[7] ≥ 0∧i53[7] ≥ 0∧i90[7] ≥ 0 ⇒ (UIncreasing(COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])), ≥)∧[bni_24] = 0∧[(2)bni_24 + (-1)Bound*bni_24] + [bni_24]i90[7] ≥ 0∧0 = 0∧[3 + (-1)bso_25] + i90[7] ≥ 0)

• (i63[0] ≥ 0 ⇒ (UIncreasing(LOAD1049(i53[1], i63[1], 0)), ≥)∧0 = 0∧[(-1)Bound*bni_26] + [(-1)bni_26]i63[0] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

• (i63[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD872(>(i63[0], 1), i63[0], i53[0])), ≥)∧0 = 0∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i63[0] ≥ 0∧0 = 0∧[1 + (-1)bso_29] + [2]i63[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_LOAD10492(x1, x2, x3, x4)) = [-1] + x4 + [-1]x1
POL(LOAD872(x1, x2)) = [-1] + x1
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(LOAD1049(x1, x2, x3)) = [2] + x3 + [-1]x2
POL(&&(x1, x2)) = 0
POL(<=(x1, x2)) = [-1]
POL(>(x1, x2)) = [2]
POL(0) = 0
POL(COND_LOAD872(x1, x2, x3)) = [2] + [-1]x2

The following pairs are in P>:

LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(&&(<=(i90[7], 1), >(+(i53[7], 1), 0)), i53[7], i90[7], i84[7])

The following pairs are in Pbound:

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

### (18) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

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 2 less nodes.

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

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])

(1) -> (7), if ((i53[1]* i53[7])∧(i63[1]* i90[7])∧(0* i84[7]))

(7) -> (8), if ((i90[7]* i90[8])∧(i90[7] <= 1 && i53[7] + 1 > 0* TRUE)∧(i84[7]* i84[8])∧(i53[7]* i53[8]))

The set Q consists of the following terms:

### (22) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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): LOAD1049(i53[4], i91[4], i84[4]) → COND_LOAD10491(i91[4] > 0 && i91[4] <= 1, i53[4], i91[4], i84[4])
(7): LOAD1049(i53[7], i90[7], i84[7]) → COND_LOAD10492(i90[7] <= 1 && i53[7] + 1 > 0, i53[7], i90[7], i84[7])

(4) -> (5), if ((i84[4]* i84[5])∧(i91[4] > 0 && i91[4] <= 1* TRUE)∧(i91[4]* i91[5])∧(i53[4]* i53[5]))

The set Q consists of the following terms: