(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: BubbleSort
`class BubbleSort {    public static void main(String[] args) {	sort(new int[100]);    }    public static void sort(int[] x) {	int n = x.length;	for (int pass=1; pass < n; pass++)  // count how many times	    // This next loop becomes shorter and shorter	    for (int i=0; i < n - pass; i++)		if (x[i] > x[i+1]) {		    // exchange elements		    int temp = x[i]; x[i] = x[i+1];  x[i+1] = temp;		}    }}`

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 217 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:
Load1421(java.lang.Object(ARRAY(100, a390data)), 100, i25) → Cond_Load1421(i25 > 0 && i25 < 100, java.lang.Object(ARRAY(100, a390data)), 100, i25)
Inc1614(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33) → Load1523(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33 + 1)
Load1523(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33) → Load1523ARR1(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i39, i37)
Load1523ARR1(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i39, i37) → Cond_Load1523ARR1(i37 <= i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 < 100 - i25 && i33 + 1 > 0 && i25 > 0, java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i39, i37)
Cond_Load1523ARR1(TRUE, java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i39, i37) → Load1523(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33 + 1)
Load1523(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33) → Cond_Load1523(i33 >= 100 - i25 && i25 > 0 && i25 + 1 > 0, java.lang.Object(ARRAY(100, a396data)), 100, i25, i33)
Cond_Load1523(TRUE, java.lang.Object(ARRAY(100, a396data)), 100, i25, i33) → Load1421(java.lang.Object(ARRAY(100, a396data)), 100, i25 + 1)
Load1523(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33) → Load1523ARR2(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i44, i42, i39, i37)
Load1523ARR2(java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i44, i42, i39, i37) → Cond_Load1523ARR2(i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 + 1 > 0 && i33 + 1 < 100 && i37 > i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 < 100 - i25 && i25 > 0, java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i44, i42, i39, i37)
Cond_Load1523ARR2(TRUE, java.lang.Object(ARRAY(100, a396data)), 100, i25, i33, i44, i42, i39, i37) → Inc1614(java.lang.Object(ARRAY(100, a396dataNew)), 100, i25, i33)
The set Q consists of the following terms:
Inc1614(java.lang.Object(ARRAY(100, x0)), 100, x1, x2)
Load1523ARR1(java.lang.Object(ARRAY(100, x0)), 100, x1, x2, x3, x4)
Cond_Load1523ARR1(TRUE, java.lang.Object(ARRAY(100, x0)), 100, x1, x2, x3, x4)
Cond_Load1523(TRUE, java.lang.Object(ARRAY(100, x0)), 100, x1, x2)
Load1523ARR2(java.lang.Object(ARRAY(100, x0)), 100, x1, x2, x3, x4, x5, x6)
Cond_Load1523ARR2(TRUE, java.lang.Object(ARRAY(100, x0)), 100, x1, x2, x3, x4, x5, x6)

(5) GroundTermsRemoverProof (EQUIVALENT transformation)

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

We removed arguments according to the following replacements:

Inc1614(x1, x2, x3, x4) → Inc1614(x1, x3, x4)
ARRAY(x1, x2) → ARRAY(x2)
Cond_Load1523ARR2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_Load1523ARR2(x1, x2, x4, x5, x6, x7, x8, x9)
Load1523ARR2(x1, x2, x3, x4, x5, x6, x7, x8) → Load1523ARR2(x1, x3, x4, x5, x6, x7, x8)
Cond_Load1523ARR1(x1, x2, x3, x4, x5, x6, x7) → Cond_Load1523ARR1(x1, x2, x4, x5, x6, x7)
Load1523ARR1(x1, x2, x3, x4, x5, x6) → Load1523ARR1(x1, x3, x4, x5, x6)

(6) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
Load1421(java.lang.Object(ARRAY(a390data)), i25) → Cond_Load1421(i25 > 0 && i25 < 100, java.lang.Object(ARRAY(a390data)), i25)
Inc1614(java.lang.Object(ARRAY(a396data)), i25, i33) → Load1523(java.lang.Object(ARRAY(a396data)), i25, i33 + 1)
Load1523ARR1(java.lang.Object(ARRAY(a396data)), i25, i33, i39, i37) → Cond_Load1523ARR1(i37 <= i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 < 100 - i25 && i33 + 1 > 0 && i25 > 0, java.lang.Object(ARRAY(a396data)), i25, i33, i39, i37)
Cond_Load1523ARR1(TRUE, java.lang.Object(ARRAY(a396data)), i25, i33, i39, i37) → Load1523(java.lang.Object(ARRAY(a396data)), i25, i33 + 1)
Load1523(java.lang.Object(ARRAY(a396data)), i25, i33) → Cond_Load1523(i33 >= 100 - i25 && i25 > 0 && i25 + 1 > 0, java.lang.Object(ARRAY(a396data)), i25, i33)
Load1523ARR2(java.lang.Object(ARRAY(a396data)), i25, i33, i44, i42, i39, i37) → Cond_Load1523ARR2(i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 + 1 > 0 && i33 + 1 < 100 && i37 > i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 < 100 - i25 && i25 > 0, java.lang.Object(ARRAY(a396data)), i25, i33, i44, i42, i39, i37)
Cond_Load1523ARR2(TRUE, java.lang.Object(ARRAY(a396data)), i25, i33, i44, i42, i39, i37) → Inc1614(java.lang.Object(ARRAY(a396dataNew)), i25, i33)
The set Q consists of the following terms:
Inc1614(java.lang.Object(ARRAY(x0)), x1, x2)
Cond_Load1523ARR1(TRUE, java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)
Load1523ARR2(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6)
Cond_Load1523ARR2(TRUE, java.lang.Object(ARRAY(x0)), x1, x2, x3, x4, x5, x6)

(7) ITRSFilterProcessorProof (SOUND transformation)

We filter according the heuristic IdpCand1ShapeHeuristic
We removed arguments according to the following replacements:

java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY
Inc1614(x1, x2, x3) → Inc1614(x2, x3)
Cond_Load1523ARR1(x1, x2, x3, x4, x5, x6) → Cond_Load1523ARR1(x1, x3, x4, x5, x6)
Load1523ARR2(x1, x2, x3, x4, x5, x6, x7) → Load1523ARR2(x2, x3, x6, x7)
Cond_Load1523ARR2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_Load1523ARR2(x1, x3, x4, x7, x8)

(8) Obligation:

ITRS problem:

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

The TRS R consists of the following rules:
Inc1614(i25, i33) → Load1523(i25, i33 + 1)
Load1523ARR1(i25, i33, i39, i37) → Cond_Load1523ARR1(i37 <= i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 < 100 - i25 && i33 + 1 > 0 && i25 > 0, i25, i33, i39, i37)
Load1523(i25, i33) → Cond_Load1523(i33 >= 100 - i25 && i25 > 0 && i25 + 1 > 0, i25, i33)
Load1523ARR2(i25, i33, i39, i37) → Cond_Load1523ARR2(i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 + 1 > 0 && i33 + 1 < 100 && i37 > i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 < 100 - i25 && i25 > 0, i25, i33, i39, i37)
Cond_Load1523ARR2(TRUE, i25, i33, i39, i37) → Inc1614(i25, i33)
The set Q consists of the following terms:
Inc1614(x0, x1)

(10) Obligation:

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

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Inc1614(i25, i33) → Load1523(i25, i33 + 1)
Load1523ARR1(i25, i33, i39, i37) → Cond_Load1523ARR1(i37 <= i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 < 100 - i25 && i33 + 1 > 0 && i25 > 0, i25, i33, i39, i37)
Load1523(i25, i33) → Cond_Load1523(i33 >= 100 - i25 && i25 > 0 && i25 + 1 > 0, i25, i33)
Load1523ARR2(i25, i33, i39, i37) → Cond_Load1523ARR2(i33 + 1 > 0 && i33 + 1 < 100 && i33 >= 0 && i33 < 100 && i33 + 1 > 0 && i33 + 1 < 100 && i37 > i39 && i33 + 1 > 0 && i33 + 1 < 100 && i33 < 100 - i25 && i25 > 0, i25, i33, i39, i37)
Cond_Load1523ARR2(TRUE, i25, i33, i39, i37) → Inc1614(i25, i33)

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(4): LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0, i25[4], i33[4], i39[4], i37[4])
(6): LOAD1523(i25[6], i33[6]) → COND_LOAD1523(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0, i25[6], i33[6])
(9): LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0, i25[9], i33[9], i39[9], i37[9])
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])

(0) -> (1), if ((i25[0]* i25[1])∧(i25[0] > 0 && i25[0] < 100* TRUE))

(1) -> (3), if ((i25[1]* i25[3])∧(0* i33[3]))

(1) -> (6), if ((0* i33[6])∧(i25[1]* i25[6]))

(1) -> (8), if ((i25[1]* i25[8])∧(0* i33[8]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(2) -> (6), if ((i33[2] + 1* i33[6])∧(i25[2]* i25[6]))

(2) -> (8), if ((i33[2] + 1* i33[8])∧(i25[2]* i25[8]))

(3) -> (4), if ((i33[3]* i33[4])∧(i39[3]* i39[4])∧(i25[3]* i25[4])∧(i37[3]* i37[4]))

(4) -> (5), if ((i37[4]* i37[5])∧(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0* TRUE)∧(i25[4]* i25[5])∧(i39[4]* i39[5])∧(i33[4]* i33[5]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(5) -> (6), if ((i25[5]* i25[6])∧(i33[5] + 1* i33[6]))

(5) -> (8), if ((i33[5] + 1* i33[8])∧(i25[5]* i25[8]))

(6) -> (7), if ((i25[6]* i25[7])∧(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0* TRUE)∧(i33[6]* i33[7]))

(7) -> (0), if ((i25[7] + 1* i25[0]))

(8) -> (9), if ((i33[8]* i33[9])∧(i39[8]* i39[9])∧(i25[8]* i25[9])∧(i37[8]* i37[9]))

(9) -> (10), if ((i39[9]* i39[10])∧(i25[9]* i25[10])∧(i37[9]* i37[10])∧(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0* TRUE)∧(i33[9]* i33[10]))

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

The set Q consists of the following terms:
Inc1614(x0, x1)

(11) UsableRulesProof (EQUIVALENT transformation)

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

(12) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(4): LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0, i25[4], i33[4], i39[4], i37[4])
(6): LOAD1523(i25[6], i33[6]) → COND_LOAD1523(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0, i25[6], i33[6])
(9): LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0, i25[9], i33[9], i39[9], i37[9])
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])

(0) -> (1), if ((i25[0]* i25[1])∧(i25[0] > 0 && i25[0] < 100* TRUE))

(1) -> (3), if ((i25[1]* i25[3])∧(0* i33[3]))

(1) -> (6), if ((0* i33[6])∧(i25[1]* i25[6]))

(1) -> (8), if ((i25[1]* i25[8])∧(0* i33[8]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(2) -> (6), if ((i33[2] + 1* i33[6])∧(i25[2]* i25[6]))

(2) -> (8), if ((i33[2] + 1* i33[8])∧(i25[2]* i25[8]))

(3) -> (4), if ((i33[3]* i33[4])∧(i39[3]* i39[4])∧(i25[3]* i25[4])∧(i37[3]* i37[4]))

(4) -> (5), if ((i37[4]* i37[5])∧(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0* TRUE)∧(i25[4]* i25[5])∧(i39[4]* i39[5])∧(i33[4]* i33[5]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(5) -> (6), if ((i25[5]* i25[6])∧(i33[5] + 1* i33[6]))

(5) -> (8), if ((i33[5] + 1* i33[8])∧(i25[5]* i25[8]))

(6) -> (7), if ((i25[6]* i25[7])∧(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0* TRUE)∧(i33[6]* i33[7]))

(7) -> (0), if ((i25[7] + 1* i25[0]))

(8) -> (9), if ((i33[8]* i33[9])∧(i39[8]* i39[9])∧(i25[8]* i25[9])∧(i37[8]* i37[9]))

(9) -> (10), if ((i39[9]* i39[10])∧(i25[9]* i25[10])∧(i37[9]* i37[10])∧(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0* TRUE)∧(i33[9]* i33[10]))

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

The set Q consists of the following terms:
Inc1614(x0, x1)

(13) IDPNonInfProof (SOUND transformation)

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

For Pair LOAD1421(i25) → COND_LOAD1421(&&(>(i25, 0), <(i25, 100)), i25) the following chains were created:
• We consider the chain LOAD1421(i25[0]) → COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0]), COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0) 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)    (i25[0] + [-1] ≥ 0∧[99] + [-1]i25[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]i25[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

(4)    (i25[0] + [-1] ≥ 0∧[99] + [-1]i25[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]i25[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

(5)    (i25[0] + [-1] ≥ 0∧[99] + [-1]i25[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥)∧[(-1)Bound*bni_26] + [(-1)bni_26]i25[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

(6)    (i25[0] ≥ 0∧[98] + [-1]i25[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥)∧[(-1)Bound*bni_26 + (-1)bni_26] + [(-1)bni_26]i25[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

For Pair COND_LOAD1421(TRUE, i25) → LOAD1523(i25, 0) the following chains were created:
• We consider the chain COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0) which results in the following constraint:

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

(8)    ((UIncreasing(LOAD1523(i25[1], 0)), ≥)∧[(-1)bso_29] ≥ 0)

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

(9)    ((UIncreasing(LOAD1523(i25[1], 0)), ≥)∧[(-1)bso_29] ≥ 0)

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

(10)    ((UIncreasing(LOAD1523(i25[1], 0)), ≥)∧[(-1)bso_29] ≥ 0)

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

(11)    ((UIncreasing(LOAD1523(i25[1], 0)), ≥)∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair INC1614(i25, i33) → LOAD1523(i25, +(i33, 1)) the following chains were created:
• We consider the chain INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1)) which results in the following constraint:

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

(13)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧[(-1)bso_31] ≥ 0)

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

(14)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧[(-1)bso_31] ≥ 0)

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

(15)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧[(-1)bso_31] ≥ 0)

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

(16)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

For Pair LOAD1523(i25, i33) → LOAD1523ARR1(i25, i33, i39, i37) the following chains were created:
• We consider the chain LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3]) which results in the following constraint:

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

(18)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧[(-1)bso_33] ≥ 0)

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

(19)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧[(-1)bso_33] ≥ 0)

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

(20)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧[(-1)bso_33] ≥ 0)

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

(21)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair LOAD1523ARR1(i25, i33, i39, i37) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37, i39), >(+(i33, 1), 0)), <(+(i33, 1), 100)), >=(i33, 0)), <(i33, 100)), <(i33, -(100, i25))), >(+(i33, 1), 0)), >(i25, 0)), i25, i33, i39, i37) the following chains were created:
• We consider the chain LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4]), COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1)) which results in the following constraint:

(22)    (i37[4]=i37[5]&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0))=TRUEi25[4]=i25[5]i39[4]=i39[5]i33[4]=i33[5]LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥NonInfC∧LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])∧(UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥))

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

(23)    (>(i25[4], 0)=TRUE>(+(i33[4], 1), 0)=TRUE<(i33[4], -(100, i25[4]))=TRUE<(i33[4], 100)=TRUE>=(i33[4], 0)=TRUE<(+(i33[4], 1), 100)=TRUE<=(i37[4], i39[4])=TRUELOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥NonInfC∧LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])∧(UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥))

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

(24)    (i25[4] + [-1] ≥ 0∧i33[4] ≥ 0∧[99] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

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

(25)    (i25[4] + [-1] ≥ 0∧i33[4] ≥ 0∧[99] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

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

(26)    (i25[4] + [-1] ≥ 0∧i33[4] ≥ 0∧[99] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

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

(27)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

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

(28)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

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

(29)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

(30)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

For Pair COND_LOAD1523ARR1(TRUE, i25, i33, i39, i37) → LOAD1523(i25, +(i33, 1)) the following chains were created:
• We consider the chain COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1)) which results in the following constraint:

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

(32)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧[(-1)bso_37] ≥ 0)

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

(33)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧[(-1)bso_37] ≥ 0)

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

(34)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧[(-1)bso_37] ≥ 0)

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

(35)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

For Pair LOAD1523(i25, i33) → COND_LOAD1523(&&(&&(>=(i33, -(100, i25)), >(i25, 0)), >(+(i25, 1), 0)), i25, i33) the following chains were created:
• We consider the chain LOAD1523(i25[6], i33[6]) → COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6]), COND_LOAD1523(TRUE, i25[7], i33[7]) → LOAD1421(+(i25[7], 1)) which results in the following constraint:

(36)    (i25[6]=i25[7]&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0))=TRUEi33[6]=i33[7]LOAD1523(i25[6], i33[6])≥NonInfC∧LOAD1523(i25[6], i33[6])≥COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])∧(UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥))

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

(37)    (>(+(i25[6], 1), 0)=TRUE>=(i33[6], -(100, i25[6]))=TRUE>(i25[6], 0)=TRUELOAD1523(i25[6], i33[6])≥NonInfC∧LOAD1523(i25[6], i33[6])≥COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])∧(UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥))

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

(38)    (i25[6] ≥ 0∧i33[6] + [-100] + i25[6] ≥ 0∧i25[6] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

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

(39)    (i25[6] ≥ 0∧i33[6] + [-100] + i25[6] ≥ 0∧i25[6] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

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

(40)    (i25[6] ≥ 0∧i33[6] + [-100] + i25[6] ≥ 0∧i25[6] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-1)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

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

(41)    ([-1]i33[6] + [100] + i25[6] ≥ 0∧i25[6] ≥ 0∧[-1]i33[6] + [99] + i25[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-101)bni_38 + (-1)Bound*bni_38] + [bni_38]i33[6] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

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

(42)    (i33[6] + [100] + i25[6] ≥ 0∧i25[6] ≥ 0∧i33[6] + [99] + i25[6] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-101)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]i33[6] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

(43)    ([-1]i33[6] + [100] + i25[6] ≥ 0∧i25[6] ≥ 0∧[-1]i33[6] + [99] + i25[6] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-101)bni_38 + (-1)Bound*bni_38] + [bni_38]i33[6] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

For Pair COND_LOAD1523(TRUE, i25, i33) → LOAD1421(+(i25, 1)) the following chains were created:
• We consider the chain COND_LOAD1523(TRUE, i25[7], i33[7]) → LOAD1421(+(i25[7], 1)) which results in the following constraint:

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

(45)    ((UIncreasing(LOAD1421(+(i25[7], 1))), ≥)∧[(-1)bso_41] ≥ 0)

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

(46)    ((UIncreasing(LOAD1421(+(i25[7], 1))), ≥)∧[(-1)bso_41] ≥ 0)

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

(47)    ((UIncreasing(LOAD1421(+(i25[7], 1))), ≥)∧[(-1)bso_41] ≥ 0)

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

(48)    ((UIncreasing(LOAD1421(+(i25[7], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

For Pair LOAD1523(i25, i33) → LOAD1523ARR2(i25, i33, i39, i37) the following chains were created:
• We consider the chain LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8]) which results in the following constraint:

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

(50)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧[(-1)bso_43] ≥ 0)

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

(51)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧[(-1)bso_43] ≥ 0)

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

(52)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧[(-1)bso_43] ≥ 0)

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

(53)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

For Pair LOAD1523ARR2(i25, i33, i39, i37) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33, 1), 0), <(+(i33, 1), 100)), >=(i33, 0)), <(i33, 100)), >(+(i33, 1), 0)), <(+(i33, 1), 100)), >(i37, i39)), >(+(i33, 1), 0)), <(+(i33, 1), 100)), <(i33, -(100, i25))), >(i25, 0)), i25, i33, i39, i37) the following chains were created:
• We consider the chain LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9]), COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10]) which results in the following constraint:

(54)    (i39[9]=i39[10]i25[9]=i25[10]i37[9]=i37[10]&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0))=TRUEi33[9]=i33[10]LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥NonInfC∧LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])∧(UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥))

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

(55)    (>(i25[9], 0)=TRUE<(i33[9], -(100, i25[9]))=TRUE<(+(i33[9], 1), 100)=TRUE>(+(i33[9], 1), 0)=TRUE>(i37[9], i39[9])=TRUE<(i33[9], 100)=TRUE>=(i33[9], 0)=TRUELOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥NonInfC∧LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])∧(UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥))

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

(56)    (i25[9] + [-1] ≥ 0∧[99] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(57)    (i25[9] + [-1] ≥ 0∧[99] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(58)    (i25[9] + [-1] ≥ 0∧[99] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(59)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-2)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(60)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-2)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

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

(61)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-2)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

(62)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-2)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

For Pair COND_LOAD1523ARR2(TRUE, i25, i33, i39, i37) → INC1614(i25, i33) the following chains were created:
• We consider the chain COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10]), INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1)) which results in the following constraint:

(63)    (i33[10]=i33[2]i25[10]=i25[2]COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥NonInfC∧COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥INC1614(i25[10], i33[10])∧(UIncreasing(INC1614(i25[10], i33[10])), ≥))

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

(64)    (COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥NonInfC∧COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥INC1614(i25[10], i33[10])∧(UIncreasing(INC1614(i25[10], i33[10])), ≥))

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

(65)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧[(-1)bso_47] ≥ 0)

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

(66)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧[(-1)bso_47] ≥ 0)

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

(67)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧[(-1)bso_47] ≥ 0)

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

(68)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i25[0] ≥ 0∧[98] + [-1]i25[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥)∧[(-1)Bound*bni_26 + (-1)bni_26] + [(-1)bni_26]i25[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

• ((UIncreasing(LOAD1523(i25[1], 0)), ≥)∧0 = 0∧[(-1)bso_29] ≥ 0)

• INC1614(i25, i33) → LOAD1523(i25, +(i33, 1))
• ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

• ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

• LOAD1523ARR1(i25, i33, i39, i37) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37, i39), >(+(i33, 1), 0)), <(+(i33, 1), 100)), >=(i33, 0)), <(i33, 100)), <(i33, -(100, i25))), >(+(i33, 1), 0)), >(i25, 0)), i25, i33, i39, i37)
• (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)
• (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i25[4] ≥ 0∧[(-1)bso_35] ≥ 0)

• ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

• LOAD1523(i25, i33) → COND_LOAD1523(&&(&&(>=(i33, -(100, i25)), >(i25, 0)), >(+(i25, 1), 0)), i25, i33)
• (i33[6] + [100] + i25[6] ≥ 0∧i25[6] ≥ 0∧i33[6] + [99] + i25[6] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-101)bni_38 + (-1)Bound*bni_38] + [(-1)bni_38]i33[6] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)
• ([-1]i33[6] + [100] + i25[6] ≥ 0∧i25[6] ≥ 0∧[-1]i33[6] + [99] + i25[6] ≥ 0∧i33[6] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])), ≥)∧[(-101)bni_38 + (-1)Bound*bni_38] + [bni_38]i33[6] + [(-1)bni_38]i25[6] ≥ 0∧[(-1)bso_39] ≥ 0)

• ((UIncreasing(LOAD1421(+(i25[7], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

• ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

• LOAD1523ARR2(i25, i33, i39, i37) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33, 1), 0), <(+(i33, 1), 100)), >=(i33, 0)), <(i33, 100)), >(+(i33, 1), 0)), <(+(i33, 1), 100)), >(i37, i39)), >(+(i33, 1), 0)), <(+(i33, 1), 100)), <(i33, -(100, i25))), >(i25, 0)), i25, i33, i39, i37)
• (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-2)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)
• (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-2)bni_44 + (-1)Bound*bni_44] + [(-1)bni_44]i25[9] ≥ 0∧[(-1)bso_45] ≥ 0)

• COND_LOAD1523ARR2(TRUE, i25, i33, i39, i37) → INC1614(i25, i33)
• ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 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_LOAD1421(x1, x2)) = [-1] + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<(x1, x2)) = [-1]
POL(100) = [100]
POL(LOAD1523(x1, x2)) = [-1] + [-1]x1
POL(INC1614(x1, x2)) = [-1] + [-1]x1
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(LOAD1523ARR1(x1, x2, x3, x4)) = [-1] + [-1]x1
POL(COND_LOAD1523ARR1(x1, x2, x3, x4, x5)) = [-1] + [-1]x2
POL(<=(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(-(x1, x2)) = x1 + [-1]x2
POL(COND_LOAD1523(x1, x2, x3)) = [-1] + [-1]x2
POL(LOAD1523ARR2(x1, x2, x3, x4)) = [-1] + [-1]x1
POL(COND_LOAD1523ARR2(x1, x2, x3, x4, x5)) = [-1] + [-1]x2

The following pairs are in P>:

The following pairs are in Pbound:

LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])
LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])

The following pairs are in P:

INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1))
LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])
LOAD1523(i25[6], i33[6]) → COND_LOAD1523(&&(&&(>=(i33[6], -(100, i25[6])), >(i25[6], 0)), >(+(i25[6], 1), 0)), i25[6], i33[6])
LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])
COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])

There are no usable rules.

(15) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(4): LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0, i25[4], i33[4], i39[4], i37[4])
(6): LOAD1523(i25[6], i33[6]) → COND_LOAD1523(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0, i25[6], i33[6])
(9): LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0, i25[9], i33[9], i39[9], i37[9])
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

(1) -> (3), if ((i25[1]* i25[3])∧(0* i33[3]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(3) -> (4), if ((i33[3]* i33[4])∧(i39[3]* i39[4])∧(i25[3]* i25[4])∧(i37[3]* i37[4]))

(4) -> (5), if ((i37[4]* i37[5])∧(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0* TRUE)∧(i25[4]* i25[5])∧(i39[4]* i39[5])∧(i33[4]* i33[5]))

(1) -> (6), if ((0* i33[6])∧(i25[1]* i25[6]))

(2) -> (6), if ((i33[2] + 1* i33[6])∧(i25[2]* i25[6]))

(5) -> (6), if ((i25[5]* i25[6])∧(i33[5] + 1* i33[6]))

(6) -> (7), if ((i25[6]* i25[7])∧(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0* TRUE)∧(i33[6]* i33[7]))

(1) -> (8), if ((i25[1]* i25[8])∧(0* i33[8]))

(2) -> (8), if ((i33[2] + 1* i33[8])∧(i25[2]* i25[8]))

(5) -> (8), if ((i33[5] + 1* i33[8])∧(i25[5]* i25[8]))

(8) -> (9), if ((i33[8]* i33[9])∧(i39[8]* i39[9])∧(i25[8]* i25[9])∧(i37[8]* i37[9]))

(9) -> (10), if ((i39[9]* i39[10])∧(i25[9]* i25[10])∧(i37[9]* i37[10])∧(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0* TRUE)∧(i33[9]* i33[10]))

The set Q consists of the following terms:
Inc1614(x0, x1)

(16) IDependencyGraphProof (EQUIVALENT transformation)

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

(17) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])
(9): LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0, i25[9], i33[9], i39[9], i37[9])
(4): LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0, i25[4], i33[4], i39[4], i37[4])

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(3) -> (4), if ((i33[3]* i33[4])∧(i39[3]* i39[4])∧(i25[3]* i25[4])∧(i37[3]* i37[4]))

(4) -> (5), if ((i37[4]* i37[5])∧(i37[4] <= i39[4] && i33[4] + 1 > 0 && i33[4] + 1 < 100 && i33[4] >= 0 && i33[4] < 100 && i33[4] < 100 - i25[4] && i33[4] + 1 > 0 && i25[4] > 0* TRUE)∧(i25[4]* i25[5])∧(i39[4]* i39[5])∧(i33[4]* i33[5]))

(2) -> (8), if ((i33[2] + 1* i33[8])∧(i25[2]* i25[8]))

(5) -> (8), if ((i33[5] + 1* i33[8])∧(i25[5]* i25[8]))

(8) -> (9), if ((i33[8]* i33[9])∧(i39[8]* i39[9])∧(i25[8]* i25[9])∧(i37[8]* i37[9]))

(9) -> (10), if ((i39[9]* i39[10])∧(i25[9]* i25[10])∧(i37[9]* i37[10])∧(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0* TRUE)∧(i33[9]* i33[10]))

The set Q consists of the following terms:
Inc1614(x0, x1)

(18) IDPNonInfProof (SOUND transformation)

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

For Pair INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1)) the following chains were created:
• We consider the chain INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1)) which results in the following constraint:

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

(2)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧[(-1)bso_16] ≥ 0)

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

(3)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧[(-1)bso_16] ≥ 0)

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

(4)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧[(-1)bso_16] ≥ 0)

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

(5)    ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

For Pair COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10]) the following chains were created:
• We consider the chain COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10]), INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1)) which results in the following constraint:

(6)    (i33[10]=i33[2]i25[10]=i25[2]COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥NonInfC∧COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥INC1614(i25[10], i33[10])∧(UIncreasing(INC1614(i25[10], i33[10])), ≥))

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

(7)    (COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥NonInfC∧COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10])≥INC1614(i25[10], i33[10])∧(UIncreasing(INC1614(i25[10], i33[10])), ≥))

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

(8)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧[(-1)bso_18] ≥ 0)

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

(9)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧[(-1)bso_18] ≥ 0)

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

(10)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧[(-1)bso_18] ≥ 0)

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

(11)    ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_18] ≥ 0)

For Pair LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9]) the following chains were created:
• We consider the chain LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9]), COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10]) which results in the following constraint:

(12)    (i39[9]=i39[10]i25[9]=i25[10]i37[9]=i37[10]&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0))=TRUEi33[9]=i33[10]LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥NonInfC∧LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])∧(UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥))

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

(13)    (>(i25[9], 0)=TRUE<(i33[9], -(100, i25[9]))=TRUE<(+(i33[9], 1), 100)=TRUE>(+(i33[9], 1), 0)=TRUE>(i37[9], i39[9])=TRUE<(i33[9], 100)=TRUE>=(i33[9], 0)=TRUELOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥NonInfC∧LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9])≥COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])∧(UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥))

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

(14)    (i25[9] + [-1] ≥ 0∧[99] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(15)    (i25[9] + [-1] ≥ 0∧[99] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(16)    (i25[9] + [-1] ≥ 0∧[99] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(17)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] + [-1] + [-1]i39[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(18)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(19)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

(20)    (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

For Pair LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8]) the following chains were created:
• We consider the chain LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8]) which results in the following constraint:

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

(22)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧[1 + (-1)bso_22] ≥ 0)

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

(23)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧[1 + (-1)bso_22] ≥ 0)

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

(24)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧[1 + (-1)bso_22] ≥ 0)

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

(25)    ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

For Pair COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1)) the following chains were created:
• We consider the chain COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1)) which results in the following constraint:

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

(27)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧[(-1)bso_24] ≥ 0)

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

(28)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧[(-1)bso_24] ≥ 0)

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

(29)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧[(-1)bso_24] ≥ 0)

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

(30)    ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_24] ≥ 0)

For Pair LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4]) the following chains were created:
• We consider the chain LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4]), COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1)) which results in the following constraint:

(31)    (i37[4]=i37[5]&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0))=TRUEi25[4]=i25[5]i39[4]=i39[5]i33[4]=i33[5]LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥NonInfC∧LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])∧(UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥))

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

(32)    (>(i25[4], 0)=TRUE>(+(i33[4], 1), 0)=TRUE<(i33[4], -(100, i25[4]))=TRUE<(i33[4], 100)=TRUE>=(i33[4], 0)=TRUE<(+(i33[4], 1), 100)=TRUE<=(i37[4], i39[4])=TRUELOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥NonInfC∧LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4])≥COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])∧(UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥))

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

(33)    (i25[4] + [-1] ≥ 0∧i33[4] ≥ 0∧[99] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

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

(34)    (i25[4] + [-1] ≥ 0∧i33[4] ≥ 0∧[99] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

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

(35)    (i25[4] + [-1] ≥ 0∧i33[4] ≥ 0∧[99] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

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

(36)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] + [-1]i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

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

(37)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

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

(38)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

(39)    (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

For Pair LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3]) the following chains were created:
• We consider the chain LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3]) which results in the following constraint:

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

(41)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧[(-1)bso_28] ≥ 0)

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

(42)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧[(-1)bso_28] ≥ 0)

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

(43)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧[(-1)bso_28] ≥ 0)

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

(44)    ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1))
• ((UIncreasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

• COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])
• ((UIncreasing(INC1614(i25[10], i33[10])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_18] ≥ 0)

• LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])
• (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)
• (i25[9] ≥ 0∧[98] + [-1]i25[9] + [-1]i33[9] ≥ 0∧[98] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i37[9] ≥ 0∧[99] + [-1]i33[9] ≥ 0∧i33[9] ≥ 0∧i39[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])), ≥)∧[(-1)bni_19 + (-1)Bound*bni_19] + [(-1)bni_19]i33[9] ≥ 0∧[(-1)bso_20] ≥ 0)

• ((UIncreasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

• ((UIncreasing(LOAD1523(i25[5], +(i33[5], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_24] ≥ 0)

• LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])
• (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)
• (i25[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i25[4] + [-1]i33[4] ≥ 0∧[99] + [-1]i33[4] ≥ 0∧i33[4] ≥ 0∧[98] + [-1]i33[4] ≥ 0∧i39[4] ≥ 0∧i37[4] ≥ 0 ⇒ (UIncreasing(COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])), ≥)∧[(-1)Bound*bni_25] + [(-1)bni_25]i33[4] ≥ 0∧[1 + (-1)bso_26] ≥ 0)

• ((UIncreasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_28] ≥ 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(INC1614(x1, x2)) = [-1] + [-1]x2
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(COND_LOAD1523ARR2(x1, x2, x3, x4, x5)) = [-1] + [-1]x3
POL(LOAD1523ARR2(x1, x2, x3, x4)) = [-1] + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<(x1, x2)) = [-1]
POL(100) = [100]
POL(>=(x1, x2)) = [-1]
POL(-(x1, x2)) = x1 + [-1]x2
POL(COND_LOAD1523ARR1(x1, x2, x3, x4, x5)) = [-1] + [-1]x3
POL(LOAD1523ARR1(x1, x2, x3, x4)) = [-1]x2
POL(<=(x1, x2)) = [-1]

The following pairs are in P>:

LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])

The following pairs are in Pbound:

LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])
LOAD1523ARR1(i25[4], i33[4], i39[4], i37[4]) → COND_LOAD1523ARR1(&&(&&(&&(&&(&&(&&(&&(<=(i37[4], i39[4]), >(+(i33[4], 1), 0)), <(+(i33[4], 1), 100)), >=(i33[4], 0)), <(i33[4], 100)), <(i33[4], -(100, i25[4]))), >(+(i33[4], 1), 0)), >(i25[4], 0)), i25[4], i33[4], i39[4], i37[4])

The following pairs are in P:

INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1))
COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])
LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i33[9], 1), 0), <(+(i33[9], 1), 100)), >=(i33[9], 0)), <(i33[9], 100)), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), >(i37[9], i39[9])), >(+(i33[9], 1), 0)), <(+(i33[9], 1), 100)), <(i33[9], -(100, i25[9]))), >(i25[9], 0)), i25[9], i33[9], i39[9], i37[9])

There are no usable rules.

(20) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])
(9): LOAD1523ARR2(i25[9], i33[9], i39[9], i37[9]) → COND_LOAD1523ARR2(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0, i25[9], i33[9], i39[9], i37[9])

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(9) -> (10), if ((i39[9]* i39[10])∧(i25[9]* i25[10])∧(i37[9]* i37[10])∧(i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] >= 0 && i33[9] < 100 && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i37[9] > i39[9] && i33[9] + 1 > 0 && i33[9] + 1 < 100 && i33[9] < 100 - i25[9] && i25[9] > 0* TRUE)∧(i33[9]* i33[10]))

The set Q consists of the following terms:
Inc1614(x0, x1)

(21) IDependencyGraphProof (EQUIVALENT transformation)

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

(23) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(2) -> (8), if ((i33[2] + 1* i33[8])∧(i25[2]* i25[8]))

(5) -> (8), if ((i33[5] + 1* i33[8])∧(i25[5]* i25[8]))

The set Q consists of the following terms:
Inc1614(x0, x1)

(24) IDependencyGraphProof (EQUIVALENT transformation)

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

(26) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(6): LOAD1523(i25[6], i33[6]) → COND_LOAD1523(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0, i25[6], i33[6])
(10): COND_LOAD1523ARR2(TRUE, i25[10], i33[10], i39[10], i37[10]) → INC1614(i25[10], i33[10])

(10) -> (2), if ((i33[10]* i33[2])∧(i25[10]* i25[2]))

(1) -> (3), if ((i25[1]* i25[3])∧(0* i33[3]))

(2) -> (3), if ((i33[2] + 1* i33[3])∧(i25[2]* i25[3]))

(5) -> (3), if ((i25[5]* i25[3])∧(i33[5] + 1* i33[3]))

(1) -> (6), if ((0* i33[6])∧(i25[1]* i25[6]))

(2) -> (6), if ((i33[2] + 1* i33[6])∧(i25[2]* i25[6]))

(5) -> (6), if ((i25[5]* i25[6])∧(i33[5] + 1* i33[6]))

(6) -> (7), if ((i25[6]* i25[7])∧(i33[6] >= 100 - i25[6] && i25[6] > 0 && i25[6] + 1 > 0* TRUE)∧(i33[6]* i33[7]))

(1) -> (8), if ((i25[1]* i25[8])∧(0* i33[8]))

(2) -> (8), if ((i33[2] + 1* i33[8])∧(i25[2]* i25[8]))

(5) -> (8), if ((i33[5] + 1* i33[8])∧(i25[5]* i25[8]))

The set Q consists of the following terms: