### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaB13
`/** * Example taken from "A Term Rewriting Approach to the Automated Termination * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf) * and converted to Java. */public class PastaB13 {    public static void main(String[] args) {        Random.args = args;        int x = Random.random();        int y = Random.random();        int z = Random.random();        while (x > z || y > z) {            if (x > z) {                x--;            } else if (y > z) {                y--;            } else {                continue;            }        }    }}public class Random {  static String[] args;  static int index = 0;  public static int random() {    String string = args[index];    index++;    return string.length();  }}`

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

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

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

### (4) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
Load1328(i14, i29, i59) → Cond_Load1328(i29 > i59 && i14 <= i59, i14, i29, i59)
Load1411(i14, i29, i59) → Cond_Load1411(i29 <= i59 && i14 <= i59, i14, i29, i59)
Load1328(i14, i29, i59) → Cond_Load13281(i29 <= i59 && i14 <= i59 && i14 > i59, i14, i29, i59)
Load1411(i14, i29, i59) → Cond_Load14111(i29 > i59 && i14 <= i59, i14, i29, i59)
Load1328(i14, i29, i59) → Cond_Load13282(i29 > i59 && i14 <= i59 && i14 > i59, i14, i29, i59)
The set Q consists of the following terms:

### (6) Obligation:

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

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load1328(i14, i29, i59) → Cond_Load1328(i29 > i59 && i14 <= i59, i14, i29, i59)
Load1411(i14, i29, i59) → Cond_Load1411(i29 <= i59 && i14 <= i59, i14, i29, i59)
Load1328(i14, i29, i59) → Cond_Load13281(i29 <= i59 && i14 <= i59 && i14 > i59, i14, i29, i59)
Load1411(i14, i29, i59) → Cond_Load14111(i29 > i59 && i14 <= i59, i14, i29, i59)
Load1328(i14, i29, i59) → Cond_Load13282(i29 > i59 && i14 <= i59 && i14 > i59, i14, i29, i59)

The integer pair graph contains the following rules and edges:
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(4): LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(i29[4] <= i59[4] && i14[4] <= i59[4] && i14[4] > i59[4], i14[4], i29[4], i59[4])
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])
(8): LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(i29[8] > i59[8] && i14[8] <= i59[8] && i14[8] > i59[8], i14[8], i29[8], i59[8])

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

(1) -> (10), if ((i29[1]* i29[10])∧(i14[1]* i14[10])∧(i59[1]* i59[10]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(3) -> (4), if ((i14[3]* i14[4])∧(i29[3]* i29[4])∧(i59[3]* i59[4]))

(3) -> (8), if ((i14[3]* i14[8])∧(i29[3]* i29[8])∧(i59[3]* i59[8]))

(3) -> (12), if ((i29[3]* i29[12])∧(i14[3]* i14[12])∧(i59[3]* i59[12]))

(4) -> (5), if ((i29[4]* i29[5])∧(i29[4] <= i59[4] && i14[4] <= i59[4] && i14[4] > i59[4]* TRUE)∧(i59[4]* i59[5])∧(i14[4]* i14[5]))

(5) -> (0), if ((i59[5]* i59[0])∧(i14[5]* i14[0])∧(i29[5]* i29[0]))

(5) -> (4), if ((i29[5]* i29[4])∧(i14[5]* i14[4])∧(i59[5]* i59[4]))

(5) -> (8), if ((i14[5]* i14[8])∧(i29[5]* i29[8])∧(i59[5]* i59[8]))

(5) -> (12), if ((i29[5]* i29[12])∧(i59[5]* i59[12])∧(i14[5]* i14[12]))

(6) -> (7), if ((i59[6]* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6]* TRUE)∧(i29[6]* i29[7])∧(i14[6]* i14[7]))

(7) -> (0), if ((i59[7]* i59[0])∧(i29[7] + -1* i29[0])∧(i14[7]* i14[0]))

(7) -> (4), if ((i59[7]* i59[4])∧(i29[7] + -1* i29[4])∧(i14[7]* i14[4]))

(7) -> (8), if ((i14[7]* i14[8])∧(i59[7]* i59[8])∧(i29[7] + -1* i29[8]))

(7) -> (12), if ((i29[7] + -1* i29[12])∧(i14[7]* i14[12])∧(i59[7]* i59[12]))

(8) -> (9), if ((i29[8]* i29[9])∧(i14[8]* i14[9])∧(i29[8] > i59[8] && i14[8] <= i59[8] && i14[8] > i59[8]* TRUE)∧(i59[8]* i59[9]))

(9) -> (0), if ((i59[9]* i59[0])∧(i29[9] + -1* i29[0])∧(i14[9]* i14[0]))

(9) -> (4), if ((i14[9]* i14[4])∧(i29[9] + -1* i29[4])∧(i59[9]* i59[4]))

(9) -> (8), if ((i29[9] + -1* i29[8])∧(i14[9]* i14[8])∧(i59[9]* i59[8]))

(9) -> (12), if ((i59[9]* i59[12])∧(i14[9]* i14[12])∧(i29[9] + -1* i29[12]))

(10) -> (11), if ((i14[10]* i14[11])∧(i14[10] > i59[10]* TRUE)∧(i59[10]* i59[11])∧(i29[10]* i29[11]))

(11) -> (0), if ((i29[11]* i29[0])∧(i14[11] + -1* i14[0])∧(i59[11]* i59[0]))

(11) -> (4), if ((i59[11]* i59[4])∧(i29[11]* i29[4])∧(i14[11] + -1* i14[4]))

(11) -> (8), if ((i29[11]* i29[8])∧(i14[11] + -1* i14[8])∧(i59[11]* i59[8]))

(11) -> (12), if ((i59[11]* i59[12])∧(i14[11] + -1* i14[12])∧(i29[11]* i29[12]))

(12) -> (13), if ((i14[12] > i59[12]* TRUE)∧(i59[12]* i59[13])∧(i29[12]* i29[13])∧(i14[12]* i14[13]))

(13) -> (0), if ((i59[13]* i59[0])∧(i29[13]* i29[0])∧(i14[13] + -1* i14[0]))

(13) -> (4), if ((i29[13]* i29[4])∧(i59[13]* i59[4])∧(i14[13] + -1* i14[4]))

(13) -> (8), if ((i14[13] + -1* i14[8])∧(i29[13]* i29[8])∧(i59[13]* i59[8]))

(13) -> (12), if ((i59[13]* i59[12])∧(i14[13] + -1* i14[12])∧(i29[13]* i29[12]))

The set Q consists of the following terms:

### (7) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

### (8) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(4): LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(i29[4] <= i59[4] && i14[4] <= i59[4] && i14[4] > i59[4], i14[4], i29[4], i59[4])
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])
(8): LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(i29[8] > i59[8] && i14[8] <= i59[8] && i14[8] > i59[8], i14[8], i29[8], i59[8])

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

(1) -> (10), if ((i29[1]* i29[10])∧(i14[1]* i14[10])∧(i59[1]* i59[10]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(3) -> (4), if ((i14[3]* i14[4])∧(i29[3]* i29[4])∧(i59[3]* i59[4]))

(3) -> (8), if ((i14[3]* i14[8])∧(i29[3]* i29[8])∧(i59[3]* i59[8]))

(3) -> (12), if ((i29[3]* i29[12])∧(i14[3]* i14[12])∧(i59[3]* i59[12]))

(4) -> (5), if ((i29[4]* i29[5])∧(i29[4] <= i59[4] && i14[4] <= i59[4] && i14[4] > i59[4]* TRUE)∧(i59[4]* i59[5])∧(i14[4]* i14[5]))

(5) -> (0), if ((i59[5]* i59[0])∧(i14[5]* i14[0])∧(i29[5]* i29[0]))

(5) -> (4), if ((i29[5]* i29[4])∧(i14[5]* i14[4])∧(i59[5]* i59[4]))

(5) -> (8), if ((i14[5]* i14[8])∧(i29[5]* i29[8])∧(i59[5]* i59[8]))

(5) -> (12), if ((i29[5]* i29[12])∧(i59[5]* i59[12])∧(i14[5]* i14[12]))

(6) -> (7), if ((i59[6]* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6]* TRUE)∧(i29[6]* i29[7])∧(i14[6]* i14[7]))

(7) -> (0), if ((i59[7]* i59[0])∧(i29[7] + -1* i29[0])∧(i14[7]* i14[0]))

(7) -> (4), if ((i59[7]* i59[4])∧(i29[7] + -1* i29[4])∧(i14[7]* i14[4]))

(7) -> (8), if ((i14[7]* i14[8])∧(i59[7]* i59[8])∧(i29[7] + -1* i29[8]))

(7) -> (12), if ((i29[7] + -1* i29[12])∧(i14[7]* i14[12])∧(i59[7]* i59[12]))

(8) -> (9), if ((i29[8]* i29[9])∧(i14[8]* i14[9])∧(i29[8] > i59[8] && i14[8] <= i59[8] && i14[8] > i59[8]* TRUE)∧(i59[8]* i59[9]))

(9) -> (0), if ((i59[9]* i59[0])∧(i29[9] + -1* i29[0])∧(i14[9]* i14[0]))

(9) -> (4), if ((i14[9]* i14[4])∧(i29[9] + -1* i29[4])∧(i59[9]* i59[4]))

(9) -> (8), if ((i29[9] + -1* i29[8])∧(i14[9]* i14[8])∧(i59[9]* i59[8]))

(9) -> (12), if ((i59[9]* i59[12])∧(i14[9]* i14[12])∧(i29[9] + -1* i29[12]))

(10) -> (11), if ((i14[10]* i14[11])∧(i14[10] > i59[10]* TRUE)∧(i59[10]* i59[11])∧(i29[10]* i29[11]))

(11) -> (0), if ((i29[11]* i29[0])∧(i14[11] + -1* i14[0])∧(i59[11]* i59[0]))

(11) -> (4), if ((i59[11]* i59[4])∧(i29[11]* i29[4])∧(i14[11] + -1* i14[4]))

(11) -> (8), if ((i29[11]* i29[8])∧(i14[11] + -1* i14[8])∧(i59[11]* i59[8]))

(11) -> (12), if ((i59[11]* i59[12])∧(i14[11] + -1* i14[12])∧(i29[11]* i29[12]))

(12) -> (13), if ((i14[12] > i59[12]* TRUE)∧(i59[12]* i59[13])∧(i29[12]* i29[13])∧(i14[12]* i14[13]))

(13) -> (0), if ((i59[13]* i59[0])∧(i29[13]* i29[0])∧(i14[13] + -1* i14[0]))

(13) -> (4), if ((i29[13]* i29[4])∧(i59[13]* i59[4])∧(i14[13] + -1* i14[4]))

(13) -> (8), if ((i14[13] + -1* i14[8])∧(i29[13]* i29[8])∧(i59[13]* i59[8]))

(13) -> (12), if ((i59[13]* i59[12])∧(i14[13] + -1* i14[12])∧(i29[13]* i29[12]))

The set Q consists of the following terms:

### (9) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LOAD1328(i14, i29, i59) → COND_LOAD1328(&&(>(i29, i59), <=(i14, i59)), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) which results in the following constraint:

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

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

(3)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(4)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(5)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(6)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] + [bni_49]i14[0] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(7)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)

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

(8)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)

(9)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)

For Pair COND_LOAD1328(TRUE, i14, i29, i59) → LOAD1411(i14, i29, i59) the following chains were created:
• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) which results in the following constraint:

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

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

(12)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(13)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(14)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(15)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]) which results in the following constraint:

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

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

(18)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(19)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(20)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(21)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[10], i29[10], i59[10]) → COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10]) which results in the following constraint:

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

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

(24)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(25)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(26)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_52] ≥ 0)

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

(27)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

For Pair LOAD1411(i14, i29, i59) → COND_LOAD1411(&&(<=(i29, i59), <=(i14, i59)), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) which results in the following constraint:

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

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

(30)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(31)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(32)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(33)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i29[2] + [(-1)bni_53]i59[2] + [bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(34)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

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

(35)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

(36)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

For Pair COND_LOAD1411(TRUE, i14, i29, i59) → LOAD1328(i14, i29, i59) the following chains were created:
• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) which results in the following constraint:

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

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

(39)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(40)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(41)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(42)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4]) which results in the following constraint:

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

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

(45)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(46)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(47)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(48)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8]) which results in the following constraint:

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

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

(51)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(52)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(53)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(54)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[12], i29[12], i59[12]) → COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12]) which results in the following constraint:

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

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

(57)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(58)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(59)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_56] ≥ 0)

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

(60)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

For Pair LOAD1328(i14, i29, i59) → COND_LOAD13281(&&(&&(<=(i29, i59), <=(i14, i59)), >(i14, i59)), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4]), COND_LOAD13281(TRUE, i14[5], i29[5], i59[5]) → LOAD1328(i14[5], i29[5], i59[5]) which results in the following constraint:

(61)    (i29[4]=i29[5]&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4]))=TRUEi59[4]=i59[5]i14[4]=i14[5]LOAD1328(i14[4], i29[4], i59[4])≥NonInfC∧LOAD1328(i14[4], i29[4], i59[4])≥COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])∧(UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥))

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

(62)    (>(i14[4], i59[4])=TRUE<=(i29[4], i59[4])=TRUE<=(i14[4], i59[4])=TRUELOAD1328(i14[4], i29[4], i59[4])≥NonInfC∧LOAD1328(i14[4], i29[4], i59[4])≥COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])∧(UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥))

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

(63)    (i14[4] + [-1] + [-1]i59[4] ≥ 0∧i59[4] + [-1]i29[4] ≥ 0∧i59[4] + [-1]i14[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]i59[4] + [bni_57]i14[4] ≥ 0∧[-3 + (-1)bso_58] ≥ 0)

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

(64)    (i14[4] + [-1] + [-1]i59[4] ≥ 0∧i59[4] + [-1]i29[4] ≥ 0∧i59[4] + [-1]i14[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]i59[4] + [bni_57]i14[4] ≥ 0∧[-3 + (-1)bso_58] ≥ 0)

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

(65)    (i14[4] + [-1] + [-1]i59[4] ≥ 0∧i59[4] + [-1]i29[4] ≥ 0∧i59[4] + [-1]i14[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])), ≥)∧[(-1)bni_57 + (-1)Bound*bni_57] + [(-1)bni_57]i59[4] + [bni_57]i14[4] ≥ 0∧[-3 + (-1)bso_58] ≥ 0)

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

For Pair COND_LOAD13281(TRUE, i14, i29, i59) → LOAD1328(i14, i29, i59) the following chains were created:
• We consider the chain COND_LOAD13281(TRUE, i14[5], i29[5], i59[5]) → LOAD1328(i14[5], i29[5], i59[5]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) which results in the following constraint:

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

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

(68)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(69)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(70)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(71)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)

• We consider the chain COND_LOAD13281(TRUE, i14[5], i29[5], i59[5]) → LOAD1328(i14[5], i29[5], i59[5]), LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4]) which results in the following constraint:

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

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

(74)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(75)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(76)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(77)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)

• We consider the chain COND_LOAD13281(TRUE, i14[5], i29[5], i59[5]) → LOAD1328(i14[5], i29[5], i59[5]), LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8]) which results in the following constraint:

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

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

(80)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(81)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(82)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(83)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)

• We consider the chain COND_LOAD13281(TRUE, i14[5], i29[5], i59[5]) → LOAD1328(i14[5], i29[5], i59[5]), LOAD1328(i14[12], i29[12], i59[12]) → COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12]) which results in the following constraint:

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

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

(86)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(87)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(88)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧[2 + (-1)bso_60] ≥ 0)

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

(89)    ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)

For Pair LOAD1411(i14, i29, i59) → COND_LOAD14111(&&(>(i29, i59), <=(i14, i59)), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]), COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]) which results in the following constraint:

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

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

(92)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)

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

(93)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)

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

(94)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)

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

(95)    (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] + [bni_61]i14[6] ≥ 0∧[(-1)bso_62] ≥ 0)

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

(96)    (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)

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

(97)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)

(98)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)

For Pair COND_LOAD14111(TRUE, i14, i29, i59) → LOAD1328(i14, +(i29, -1), i59) the following chains were created:
• We consider the chain LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]), COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]) which results in the following constraint:

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

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

(101)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)

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

(102)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)

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

(103)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)

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

(104)    (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] + [bni_63]i14[6] ≥ 0∧[(-1)bso_64] ≥ 0)

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

(105)    (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)

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

(106)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)

(107)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)

For Pair LOAD1328(i14, i29, i59) → COND_LOAD13282(&&(&&(>(i29, i59), <=(i14, i59)), >(i14, i59)), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8]), COND_LOAD13282(TRUE, i14[9], i29[9], i59[9]) → LOAD1328(i14[9], +(i29[9], -1), i59[9]) which results in the following constraint:

(108)    (i29[8]=i29[9]i14[8]=i14[9]&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8]))=TRUEi59[8]=i59[9]LOAD1328(i14[8], i29[8], i59[8])≥NonInfC∧LOAD1328(i14[8], i29[8], i59[8])≥COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])∧(UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥))

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

(109)    (>(i14[8], i59[8])=TRUE>(i29[8], i59[8])=TRUE<=(i14[8], i59[8])=TRUELOAD1328(i14[8], i29[8], i59[8])≥NonInfC∧LOAD1328(i14[8], i29[8], i59[8])≥COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])∧(UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥))

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

(110)    (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]i59[8] + [bni_65]i14[8] ≥ 0∧[-1 + (-1)bso_66] + i29[8] + [2]i14[8] ≥ 0)

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

(111)    (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]i59[8] + [bni_65]i14[8] ≥ 0∧[-1 + (-1)bso_66] + i29[8] + [2]i14[8] ≥ 0)

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

(112)    (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])), ≥)∧[(-1)bni_65 + (-1)Bound*bni_65] + [(-1)bni_65]i59[8] + [bni_65]i14[8] ≥ 0∧[-1 + (-1)bso_66] + i29[8] + [2]i14[8] ≥ 0)

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

For Pair COND_LOAD13282(TRUE, i14, i29, i59) → LOAD1328(i14, +(i29, -1), i59) the following chains were created:
• We consider the chain LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8]), COND_LOAD13282(TRUE, i14[9], i29[9], i59[9]) → LOAD1328(i14[9], +(i29[9], -1), i59[9]) which results in the following constraint:

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

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

(115)    (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]i59[8] + [(-1)bni_67]i29[8] + [(-1)bni_67]i14[8] ≥ 0∧[(-1)bso_68] + [-1]i29[8] + [-2]i14[8] ≥ 0)

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

(116)    (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]i59[8] + [(-1)bni_67]i29[8] + [(-1)bni_67]i14[8] ≥ 0∧[(-1)bso_68] + [-1]i29[8] + [-2]i14[8] ≥ 0)

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

(117)    (i14[8] + [-1] + [-1]i59[8] ≥ 0∧i29[8] + [-1] + [-1]i59[8] ≥ 0∧i59[8] + [-1]i14[8] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[9], +(i29[9], -1), i59[9])), ≥)∧[(-1)bni_67 + (-1)Bound*bni_67] + [(-1)bni_67]i59[8] + [(-1)bni_67]i29[8] + [(-1)bni_67]i14[8] ≥ 0∧[(-1)bso_68] + [-1]i29[8] + [-2]i14[8] ≥ 0)

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

For Pair LOAD1411(i14, i29, i59) → COND_LOAD14112(>(i14, i59), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1411(i14[10], i29[10], i59[10]) → COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10]), COND_LOAD14112(TRUE, i14[11], i29[11], i59[11]) → LOAD1328(+(i14[11], -1), i29[11], i59[11]) which results in the following constraint:

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

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

(120)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧[(-1)bso_70] ≥ 0)

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

(121)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧[(-1)bso_70] ≥ 0)

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

(122)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧[(-1)bso_70] ≥ 0)

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

(123)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)bni_69 + (-1)Bound*bni_69] + [(-1)bni_69]i59[10] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)

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

(124)    (i14[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)

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

(125)    (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)

(126)    (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)

For Pair COND_LOAD14112(TRUE, i14, i29, i59) → LOAD1328(+(i14, -1), i29, i59) the following chains were created:
• We consider the chain LOAD1411(i14[10], i29[10], i59[10]) → COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10]), COND_LOAD14112(TRUE, i14[11], i29[11], i59[11]) → LOAD1328(+(i14[11], -1), i29[11], i59[11]) which results in the following constraint:

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

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

(129)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

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

(130)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

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

(131)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧[1 + (-1)bso_72] ≥ 0)

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

(132)    (i14[10] + [-1] + [-1]i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)bni_71 + (-1)Bound*bni_71] + [(-1)bni_71]i59[10] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)

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

(133)    (i14[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)

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

(134)    (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)

(135)    (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)

For Pair LOAD1328(i14, i29, i59) → COND_LOAD13283(>(i14, i59), i14, i29, i59) the following chains were created:
• We consider the chain LOAD1328(i14[12], i29[12], i59[12]) → COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12]), COND_LOAD13283(TRUE, i14[13], i29[13], i59[13]) → LOAD1328(+(i14[13], -1), i29[13], i59[13]) which results in the following constraint:

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

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

(138)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧[(-1)bso_74] ≥ 0)

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

(139)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧[(-1)bso_74] ≥ 0)

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

(140)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧[(-1)bso_74] ≥ 0)

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

(141)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)bni_73 + (-1)Bound*bni_73] + [(-1)bni_73]i59[12] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)

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

(142)    (i14[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)

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

(143)    (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)

(144)    (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)

For Pair COND_LOAD13283(TRUE, i14, i29, i59) → LOAD1328(+(i14, -1), i29, i59) the following chains were created:
• We consider the chain LOAD1328(i14[12], i29[12], i59[12]) → COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12]), COND_LOAD13283(TRUE, i14[13], i29[13], i59[13]) → LOAD1328(+(i14[13], -1), i29[13], i59[13]) which results in the following constraint:

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

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

(147)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

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

(148)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

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

(149)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧[1 + (-1)bso_76] ≥ 0)

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

(150)    (i14[12] + [-1] + [-1]i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)bni_75 + (-1)Bound*bni_75] + [(-1)bni_75]i59[12] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)

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

(151)    (i14[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)

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

(152)    (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)

(153)    (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1328(i14, i29, i59) → COND_LOAD1328(&&(>(i29, i59), <=(i14, i59)), i14, i29, i59)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_49 + (-1)Bound*bni_49] + [(-1)bni_49]i59[0] ≥ 0∧[(-1)bso_50] ≥ 0)

• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

• LOAD1411(i14, i29, i59) → COND_LOAD1411(&&(<=(i29, i59), <=(i14, i59)), i14, i29, i59)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_53 + (-1)Bound*bni_53] + [(-1)bni_53]i14[2] ≥ 0∧[(-1)bso_54] ≥ 0)

• ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
• ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
• ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)
• ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_56] ≥ 0)

• LOAD1328(i14, i29, i59) → COND_LOAD13281(&&(&&(<=(i29, i59), <=(i14, i59)), >(i14, i59)), i14, i29, i59)

• ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
• ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
• ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)
• ((UIncreasing(LOAD1328(i14[5], i29[5], i59[5])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_60] ≥ 0)

• LOAD1411(i14, i29, i59) → COND_LOAD14111(&&(>(i29, i59), <=(i14, i59)), i14, i29, i59)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_61 + (-1)Bound*bni_61] + [(-1)bni_61]i59[6] ≥ 0∧[(-1)bso_62] ≥ 0)

• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_63 + (-1)Bound*bni_63] + [(-1)bni_63]i59[6] ≥ 0∧[(-1)bso_64] ≥ 0)

• LOAD1328(i14, i29, i59) → COND_LOAD13282(&&(&&(>(i29, i59), <=(i14, i59)), >(i14, i59)), i14, i29, i59)

• (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)
• (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(COND_LOAD14112(>(i14[10], i59[10]), i14[10], i29[10], i59[10])), ≥)∧0 = 0∧[(-1)Bound*bni_69] + [bni_69]i14[10] ≥ 0∧0 = 0∧[(-1)bso_70] ≥ 0)

• (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)
• (i14[10] ≥ 0∧i59[10] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[11], -1), i29[11], i59[11])), ≥)∧0 = 0∧[(-1)Bound*bni_71] + [bni_71]i14[10] ≥ 0∧0 = 0∧[1 + (-1)bso_72] ≥ 0)

• (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)
• (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD13283(>(i14[12], i59[12]), i14[12], i29[12], i59[12])), ≥)∧0 = 0∧[(-1)Bound*bni_73] + [bni_73]i14[12] ≥ 0∧0 = 0∧[(-1)bso_74] ≥ 0)

• (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 0)
• (i14[12] ≥ 0∧i59[12] ≥ 0 ⇒ (UIncreasing(LOAD1328(+(i14[13], -1), i29[13], i59[13])), ≥)∧0 = 0∧[(-1)Bound*bni_75] + [bni_75]i14[12] ≥ 0∧0 = 0∧[1 + (-1)bso_76] ≥ 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) = [3]
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(LOAD1411(x1, x2, x3)) = [-1] + [-1]x3 + x1
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(COND_LOAD13281(x1, x2, x3, x4)) = [1] + [-1]x4 + x2 + [-1]x1
POL(COND_LOAD14111(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_LOAD13282(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x3 + [-1]x2 + [-1]x1
POL(COND_LOAD14112(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2
POL(COND_LOAD13283(x1, x2, x3, x4)) = [-1] + [-1]x4 + x2

The following pairs are in P>:

LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])
LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])

The following pairs are in Pbound:

LOAD1328(i14[4], i29[4], i59[4]) → COND_LOAD13281(&&(&&(<=(i29[4], i59[4]), <=(i14[4], i59[4])), >(i14[4], i59[4])), i14[4], i29[4], i59[4])
LOAD1328(i14[8], i29[8], i59[8]) → COND_LOAD13282(&&(&&(>(i29[8], i59[8]), <=(i14[8], i59[8])), >(i14[8], i59[8])), i14[8], i29[8], i59[8])

The following pairs are in P:

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

### (11) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(7) -> (0), if ((i59[7]* i59[0])∧(i29[7] + -1* i29[0])∧(i14[7]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

(6) -> (7), if ((i59[6]* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6]* TRUE)∧(i29[6]* i29[7])∧(i14[6]* i14[7]))

(1) -> (10), if ((i29[1]* i29[10])∧(i14[1]* i14[10])∧(i59[1]* i59[10]))

(3) -> (12), if ((i29[3]* i29[12])∧(i14[3]* i14[12])∧(i59[3]* i59[12]))

(7) -> (12), if ((i29[7] + -1* i29[12])∧(i14[7]* i14[12])∧(i59[7]* i59[12]))

The set Q consists of the following terms:

### (12) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(7) -> (0), if ((i59[7]* i59[0])∧(i29[7] + -1* i29[0])∧(i14[7]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

(6) -> (7), if ((i59[6]* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6]* TRUE)∧(i29[6]* i29[7])∧(i14[6]* i14[7]))

The set Q consists of the following terms:

### (14) 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_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]) the following chains were created:
• We consider the chain LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]), COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[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)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(4)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(5)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(6)    (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(7)    (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(8)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

(9)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

For Pair LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]) the following chains were created:
• We consider the chain LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]), COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]) which results in the following constraint:

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

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

(12)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(13)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(14)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(15)    (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(16)    (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(17)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

(18)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

For Pair COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) the following chains were created:
• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) which results in the following constraint:

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

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

(21)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)

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

(22)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)

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

(23)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)

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

(24)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

For Pair LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) the following chains were created:
• We consider the chain LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) which results in the following constraint:

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

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

(27)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(28)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(29)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(30)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(31)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(32)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

(33)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

For Pair COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) the following chains were created:
• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) which results in the following constraint:

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

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

(36)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(37)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(38)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(39)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]) which results in the following constraint:

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

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

(42)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(43)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(44)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(45)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

For Pair LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) the following chains were created:
• We consider the chain LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) which results in the following constraint:

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

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

(48)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(49)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(50)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(51)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(52)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(53)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

(54)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

• LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

• ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

• LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

• LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

The constraints for P> respective Pbound are constructed from P where we just replace every occurence of "t ≥ s" in P by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = [1]
POL(COND_LOAD14111(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(LOAD1411(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3

The following pairs are in P>:

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:

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

### (16) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

The set Q consists of the following terms:

### (17) IDependencyGraphProof (EQUIVALENT transformation)

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

### (18) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

The set Q consists of the following terms:

### (19) 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 LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) the following chains were created:
• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) 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)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)

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

(4)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)

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

(5)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)

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

(6)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i29[2] + [(2)bni_24]i59[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

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

(7)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

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

(8)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

(9)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

For Pair COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) the following chains were created:
• We consider the chain LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) which results in the following constraint:

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

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

(12)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

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

(13)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

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

(14)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(2)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

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

(15)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

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

(16)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

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

(17)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

(18)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

For Pair LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) the following chains were created:
• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) which results in the following constraint:

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

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

(21)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-3 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)

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

(22)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-3 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)

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

(23)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-3 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)

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

(24)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)

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

(25)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)

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

(26)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)

(27)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)

For Pair COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) the following chains were created:
• We consider the chain LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) which results in the following constraint:

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

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

(30)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)

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

(31)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)

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

(32)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)

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

(33)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

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

(34)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

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

(35)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

(36)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[2 + (-1)bso_27] ≥ 0)

• LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[(-1)bso_29] + [3]i29[0] ≥ 0)

• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[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) = [1]
POL(LOAD1411(x1, x2, x3)) = [2]x3 + [-1]x2 + [-1]x1
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + x3 + [-1]x2 + [-1]x1
POL(&&(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1328(x1, x2, x3, x4)) = [2] + [2]x4 + [-1]x3 + [-1]x2
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + [-1]x1
POL(>(x1, x2)) = [-1]

The following pairs are in P>:

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:

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

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

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

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:
none

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:

### (25) IDependencyGraphProof (EQUIVALENT transformation)

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

### (27) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

The set Q consists of the following terms:

### (28) IDependencyGraphProof (EQUIVALENT transformation)

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

### (30) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(5) -> (0), if ((i59[5]* i59[0])∧(i14[5]* i14[0])∧(i29[5]* i29[0]))

(7) -> (0), if ((i59[7]* i59[0])∧(i29[7] + -1* i29[0])∧(i14[7]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

(6) -> (7), if ((i59[6]* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6]* TRUE)∧(i29[6]* i29[7])∧(i14[6]* i14[7]))

The set Q consists of the following terms:

### (31) IDependencyGraphProof (EQUIVALENT transformation)

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

### (32) 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:
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(7) -> (0), if ((i59[7]* i59[0])∧(i29[7] + -1* i29[0])∧(i14[7]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

(6) -> (7), if ((i59[6]* i59[7])∧(i29[6] > i59[6] && i14[6] <= i59[6]* TRUE)∧(i29[6]* i29[7])∧(i14[6]* i14[7]))

The set Q consists of the following terms:

### (33) 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_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]) the following chains were created:
• We consider the chain LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]), COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[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)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(4)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(5)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)bni_29 + (-1)Bound*bni_29] + [(-1)bni_29]i59[6] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(6)    (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(7)    (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

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

(8)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

(9)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

For Pair LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]) the following chains were created:
• We consider the chain LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]), COND_LOAD14111(TRUE, i14[7], i29[7], i59[7]) → LOAD1328(i14[7], +(i29[7], -1), i59[7]) which results in the following constraint:

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

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

(12)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(13)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(14)    (i29[6] + [-1] + [-1]i59[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)bni_31 + (-1)Bound*bni_31] + [(-1)bni_31]i59[6] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(15)    (i29[6] ≥ 0∧i59[6] + [-1]i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(16)    (i29[6] ≥ 0∧i59[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

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

(17)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

(18)    (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

For Pair COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) the following chains were created:
• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) which results in the following constraint:

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

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

(21)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)

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

(22)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)

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

(23)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bso_34] ≥ 0)

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

(24)    ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

For Pair LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) the following chains were created:
• We consider the chain LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) which results in the following constraint:

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

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

(27)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(28)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(29)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] + [bni_35]i29[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(30)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(31)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(32)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

(33)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

For Pair COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) the following chains were created:
• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) which results in the following constraint:

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

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

(36)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(37)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(38)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(39)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6]) which results in the following constraint:

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

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

(42)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(43)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(44)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bso_38] ≥ 0)

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

(45)    ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

For Pair LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) the following chains were created:
• We consider the chain LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) which results in the following constraint:

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

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

(48)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(49)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(50)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_39 + (-1)Bound*bni_39] + [(-1)bni_39]i59[0] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(51)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(52)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

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

(53)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

(54)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[7], +(i29[7], -1), i59[7])), ≥)∧[(-1)Bound*bni_29] + [bni_29]i29[6] ≥ 0∧[1 + (-1)bso_30] ≥ 0)

• LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)
• (i29[6] ≥ 0∧i59[6] ≥ 0∧i14[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD14111(&&(>(i29[6], i59[6]), <=(i14[6], i59[6])), i14[6], i29[6], i59[6])), ≥)∧[(-1)Bound*bni_31] + [bni_31]i29[6] ≥ 0∧[(-1)bso_32] ≥ 0)

• ((UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_34] ≥ 0)

• LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_35 + (-1)Bound*bni_35] + [(-1)bni_35]i59[2] ≥ 0∧[(-1)bso_36] ≥ 0)

• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)
• ((UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_38] ≥ 0)

• LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)Bound*bni_39] + [bni_39]i29[0] ≥ 0∧[(-1)bso_40] ≥ 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_LOAD14111(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(LOAD1411(x1, x2, x3)) = [-1] + [-1]x3 + x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3

The following pairs are in P>:

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:

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

### (35) 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:
(6): LOAD1411(i14[6], i29[6], i59[6]) → COND_LOAD14111(i29[6] > i59[6] && i14[6] <= i59[6], i14[6], i29[6], i59[6])
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

(1) -> (6), if ((i14[1]* i14[6])∧(i59[1]* i59[6])∧(i29[1]* i29[6]))

The set Q consists of the following terms:

### (36) IDependencyGraphProof (EQUIVALENT transformation)

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

### (37) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])
(0): LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(i29[0] > i59[0] && i14[0] <= i59[0], i14[0], i29[0], i59[0])

(3) -> (0), if ((i59[3]* i59[0])∧(i29[3]* i29[0])∧(i14[3]* i14[0]))

(0) -> (1), if ((i29[0]* i29[1])∧(i29[0] > i59[0] && i14[0] <= i59[0]* TRUE)∧(i59[0]* i59[1])∧(i14[0]* i14[1]))

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

The set Q consists of the following terms:

### (38) 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 LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) the following chains were created:
• We consider the chain COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) 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)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)

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

(4)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)

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

(5)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i59[2] + [(-1)bni_24]i29[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] + [-2]i29[2] ≥ 0)

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

(6)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i29[2] + [(2)bni_24]i59[2] + [(-1)bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

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

(7)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

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

(8)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

(9)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

For Pair COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) the following chains were created:
• We consider the chain LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]), LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]) which results in the following constraint:

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

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

(12)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(13)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(14)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(2)bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(15)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] + [(-1)bni_26]i14[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(16)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(17)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)

(18)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)

For Pair LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) the following chains were created:
• We consider the chain COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]), COND_LOAD1328(TRUE, i14[1], i29[1], i59[1]) → LOAD1411(i14[1], i29[1], i59[1]) which results in the following constraint:

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

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

(21)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-1 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)

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

(22)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-1 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)

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

(23)    (i29[0] + [-1] + [-1]i59[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[(-1)bni_28 + (-1)Bound*bni_28] + [(-1)bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[-1 + (-1)bso_29] + [-3]i59[0] + [3]i29[0] ≥ 0)

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

(24)    (i29[0] ≥ 0∧i59[0] + [-1]i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] + [(-1)bni_28]i14[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)

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

(25)    (i29[0] ≥ 0∧i59[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)

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

(26)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)

(27)    (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)

For Pair COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]) the following chains were created:
• We consider the chain LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2]), COND_LOAD1411(TRUE, i14[3], i29[3], i59[3]) → LOAD1328(i14[3], i29[3], i59[3]), LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0]) which results in the following constraint:

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

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

(30)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)

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

(31)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)

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

(32)    (i59[2] + [-1]i29[2] ≥ 0∧i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] + [-1]i29[2] ≥ 0)

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

(33)    (i59[2] ≥ 0∧i29[2] + i59[2] + [-1]i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [bni_30]i29[2] + [(-1)bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

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

(34)    (i59[2] ≥ 0∧i14[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

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

(35)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

(36)    (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(COND_LOAD1411(&&(<=(i29[2], i59[2]), <=(i14[2], i59[2])), i14[2], i29[2], i59[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [bni_24]i59[2] + [bni_24]i14[2] ≥ 0∧[(-1)bso_25] + [2]i59[2] ≥ 0)

• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(LOAD1411(i14[1], i29[1], i59[1])), ≥)∧[(-2)bni_26 + (-1)Bound*bni_26] + [bni_26]i59[0] + [(-1)bni_26]i29[0] ≥ 0∧[(-1)bso_27] ≥ 0)

• LOAD1328(i14[0], i29[0], i59[0]) → COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)
• (i29[0] ≥ 0∧i59[0] ≥ 0∧i14[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1328(&&(>(i29[0], i59[0]), <=(i14[0], i59[0])), i14[0], i29[0], i59[0])), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]i59[0] + [(2)bni_28]i29[0] ≥ 0∧[2 + (-1)bso_29] + [3]i29[0] ≥ 0)

• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[2] ≥ 0)
• (i59[2] ≥ 0∧i14[2] ≥ 0∧i29[2] ≥ 0 ⇒ (UIncreasing(LOAD1328(i14[3], i29[3], i59[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]i59[2] + [bni_30]i14[2] ≥ 0∧[(-1)bso_31] + i59[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(LOAD1411(x1, x2, x3)) = [-1] + [2]x3 + [-1]x2 + [-1]x1
POL(COND_LOAD1411(x1, x2, x3, x4)) = [-1] + x3 + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(<=(x1, x2)) = [-1]
POL(COND_LOAD1328(x1, x2, x3, x4)) = [-1] + [2]x4 + [-1]x3 + [-1]x2 + [-1]x1
POL(LOAD1328(x1, x2, x3)) = [-1] + [-1]x3 + [2]x2 + [-1]x1
POL(>(x1, x2)) = [-1]

The following pairs are in P>:

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:

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

### (40) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

The set Q consists of the following terms:

### (41) IDependencyGraphProof (EQUIVALENT transformation)

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

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

### (44) IDependencyGraphProof (EQUIVALENT transformation)

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

### (46) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): LOAD1411(i14[2], i29[2], i59[2]) → COND_LOAD1411(i29[2] <= i59[2] && i14[2] <= i59[2], i14[2], i29[2], i59[2])

(1) -> (2), if ((i59[1]* i59[2])∧(i14[1]* i14[2])∧(i29[1]* i29[2]))

(2) -> (3), if ((i14[2]* i14[3])∧(i59[2]* i59[3])∧(i29[2] <= i59[2] && i14[2] <= i59[2]* TRUE)∧(i29[2]* i29[3]))

The set Q consists of the following terms: