Termination of the given JBC could be proven:

(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)
Cond_Load1421(TRUE, java.lang.Object(ARRAY(100, a390data)), 100, i25) → Load1523(java.lang.Object(ARRAY(100, a390data)), 100, i25, 0)
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:
Load1421(java.lang.Object(ARRAY(100, x0)), 100, x1)
Cond_Load1421(TRUE, java.lang.Object(ARRAY(100, x0)), 100, x1)
Inc1614(java.lang.Object(ARRAY(100, x0)), 100, x1, x2)
Load1523(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)
Load1421(x1, x2, x3) → Load1421(x1, x3)
Cond_Load1523(x1, x2, x3, x4, x5) → Cond_Load1523(x1, x2, x4, x5)
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)
Load1523(x1, x2, x3, x4) → Load1523(x1, x3, x4)
Cond_Load1421(x1, x2, x3, x4) → Cond_Load1421(x1, x2, x4)

(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)
Cond_Load1421(TRUE, java.lang.Object(ARRAY(a390data)), i25) → Load1523(java.lang.Object(ARRAY(a390data)), i25, 0)
Inc1614(java.lang.Object(ARRAY(a396data)), i25, i33) → Load1523(java.lang.Object(ARRAY(a396data)), i25, i33 + 1)
Load1523(java.lang.Object(ARRAY(a396data)), i25, i33) → Load1523ARR1(java.lang.Object(ARRAY(a396data)), i25, i33, i39, i37)
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)
Cond_Load1523(TRUE, java.lang.Object(ARRAY(a396data)), i25, i33) → Load1421(java.lang.Object(ARRAY(a396data)), i25 + 1)
Load1523(java.lang.Object(ARRAY(a396data)), i25, i33) → Load1523ARR2(java.lang.Object(ARRAY(a396data)), i25, i33, i44, i42, i39, i37)
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:
Load1421(java.lang.Object(ARRAY(x0)), x1)
Cond_Load1421(TRUE, java.lang.Object(ARRAY(x0)), x1)
Inc1614(java.lang.Object(ARRAY(x0)), x1, x2)
Load1523(java.lang.Object(ARRAY(x0)), x1, x2)
Load1523ARR1(java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)
Cond_Load1523ARR1(TRUE, java.lang.Object(ARRAY(x0)), x1, x2, x3, x4)
Cond_Load1523(TRUE, java.lang.Object(ARRAY(x0)), x1, x2)
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:

Load1421(x1, x2) → Load1421(x2)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY
Cond_Load1421(x1, x2, x3) → Cond_Load1421(x1, x3)
Load1523(x1, x2, x3) → Load1523(x2, x3)
Inc1614(x1, x2, x3) → Inc1614(x2, x3)
Load1523ARR1(x1, x2, x3, x4, x5) → Load1523ARR1(x2, x3, x4, x5)
Cond_Load1523ARR1(x1, x2, x3, x4, x5, x6) → Cond_Load1523ARR1(x1, x3, x4, x5, x6)
Cond_Load1523(x1, x2, x3, x4) → Cond_Load1523(x1, x3, x4)
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:
Load1421(i25) → Cond_Load1421(i25 > 0 && i25 < 100, i25)
Cond_Load1421(TRUE, i25) → Load1523(i25, 0)
Inc1614(i25, i33) → Load1523(i25, i33 + 1)
Load1523(i25, i33) → Load1523ARR1(i25, i33, i39, i37)
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)
Cond_Load1523ARR1(TRUE, i25, i33, i39, i37) → Load1523(i25, i33 + 1)
Load1523(i25, i33) → Cond_Load1523(i33 >= 100 - i25 && i25 > 0 && i25 + 1 > 0, i25, i33)
Cond_Load1523(TRUE, i25, i33) → Load1421(i25 + 1)
Load1523(i25, i33) → Load1523ARR2(i25, i33, i39, i37)
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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

(9) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(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:
Load1421(i25) → Cond_Load1421(i25 > 0 && i25 < 100, i25)
Cond_Load1421(TRUE, i25) → Load1523(i25, 0)
Inc1614(i25, i33) → Load1523(i25, i33 + 1)
Load1523(i25, i33) → Load1523ARR1(i25, i33, i39, i37)
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)
Cond_Load1523ARR1(TRUE, i25, i33, i39, i37) → Load1523(i25, i33 + 1)
Load1523(i25, i33) → Cond_Load1523(i33 >= 100 - i25 && i25 > 0 && i25 + 1 > 0, i25, i33)
Cond_Load1523(TRUE, i25, i33) → Load1421(i25 + 1)
Load1523(i25, i33) → Load1523ARR2(i25, i33, i39, i37)
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:
(0): LOAD1421(i25[0]) → COND_LOAD1421(i25[0] > 0 && i25[0] < 100, i25[0])
(1): COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0)
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])
(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])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 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])
(7): COND_LOAD1523(TRUE, i25[7], i33[7]) → LOAD1421(i25[7] + 1)
(8): LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

(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:
(0): LOAD1421(i25[0]) → COND_LOAD1421(i25[0] > 0 && i25[0] < 100, i25[0])
(1): COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0)
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])
(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])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 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])
(7): COND_LOAD1523(TRUE, i25[7], i33[7]) → LOAD1421(i25[7] + 1)
(8): LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

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

  (1)    (i25[0]=i25[1]∧&&(>(i25[0], 0), <(i25[0], 100))=TRUE ⇒ LOAD1421(i25[0])≥NonInfC∧LOAD1421(i25[0])≥COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])∧(U^Increasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥))

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

  (2)    (>(i25[0], 0)=TRUE∧<(i25[0], 100)=TRUE ⇒ LOAD1421(i25[0])≥NonInfC∧LOAD1421(i25[0])≥COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])∧(U^Increasing(COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])), ≥))

  
  
  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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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:
  

  (7)    (COND_LOAD1421(TRUE, i25[1])≥NonInfC∧COND_LOAD1421(TRUE, i25[1])≥LOAD1523(i25[1], 0)∧(U^Increasing(LOAD1523(i25[1], 0)), ≥))

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

  (8)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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:
  

  (12)    (INC1614(i25[2], i33[2])≥NonInfC∧INC1614(i25[2], i33[2])≥LOAD1523(i25[2], +(i33[2], 1))∧(U^Increasing(LOAD1523(i25[2], +(i33[2], 1))), ≥))

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

  (13)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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:
  

  (17)    (LOAD1523(i25[3], i33[3])≥NonInfC∧LOAD1523(i25[3], i33[3])≥LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])∧(U^Increasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥))

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

  (18)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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))=TRUE∧i25[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])∧(U^Increasing(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])=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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:
  

  (31)    (COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5])≥NonInfC∧COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5])≥LOAD1523(i25[5], +(i33[5], 1))∧(U^Increasing(LOAD1523(i25[5], +(i33[5], 1))), ≥))

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

  (32)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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))=TRUE∧i33[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])∧(U^Increasing(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)=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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:
  

  (44)    (COND_LOAD1523(TRUE, i25[7], i33[7])≥NonInfC∧COND_LOAD1523(TRUE, i25[7], i33[7])≥LOAD1421(+(i25[7], 1))∧(U^Increasing(LOAD1421(+(i25[7], 1))), ≥))

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

  (45)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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:
  

  (49)    (LOAD1523(i25[8], i33[8])≥NonInfC∧LOAD1523(i25[8], i33[8])≥LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])∧(U^Increasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥))

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

  (50)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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))=TRUE∧i33[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])∧(U^Increasing(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)=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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])∧(U^Increasing(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])∧(U^Increasing(INC1614(i25[10], i33[10])), ≥))

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

  (65)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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.

• LOAD1421(i25) → COND_LOAD1421(&&(>(i25, 0), <(i25, 100)), i25)
  
  • (i25[0] ≥ 0∧[98] + [-1]i25[0] ≥ 0 ⇒ (U^Increasing(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)
    
  
  
• COND_LOAD1421(TRUE, i25) → LOAD1523(i25, 0)
  
  • ((U^Increasing(LOAD1523(i25[1], 0)), ≥)∧0 = 0∧[(-1)bso_29] ≥ 0)
    
  
  
• INC1614(i25, i33) → LOAD1523(i25, +(i33, 1))
  
  • ((U^Increasing(LOAD1523(i25[2], +(i33[2], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
    
  
  
• LOAD1523(i25, i33) → LOAD1523ARR1(i25, i33, i39, i37)
  
  • ((U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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)
    
  
  
• COND_LOAD1523ARR1(TRUE, i25, i33, i39, i37) → LOAD1523(i25, +(i33, 1))
  
  • ((U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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)
    
  
  
• COND_LOAD1523(TRUE, i25, i33) → LOAD1421(+(i25, 1))
  
  • ((U^Increasing(LOAD1421(+(i25[7], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
    
  
  
• LOAD1523(i25, i33) → LOAD1523ARR2(i25, i33, i39, i37)
  
  • ((U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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)
  
  • ((U^Increasing(INC1614(i25[10], i33[10])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
    
  
  

The constraints for P_> respective P_bound 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 P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(LOAD1421(x₁)) = [-1]x₁   
POL(COND_LOAD1421(x₁, x₂)) = [-1] + [-1]x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(0) = 0   
POL(<(x₁, x₂)) = [-1]   
POL(100) = [100]   
POL(LOAD1523(x₁, x₂)) = [-1] + [-1]x₁   
POL(INC1614(x₁, x₂)) = [-1] + [-1]x₁   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(LOAD1523ARR1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₁   
POL(COND_LOAD1523ARR1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₂   
POL(<=(x₁, x₂)) = [-1]   
POL(>=(x₁, x₂)) = [-1]   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(COND_LOAD1523(x₁, x₂, x₃)) = [-1] + [-1]x₂   
POL(LOAD1523ARR2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₁   
POL(COND_LOAD1523ARR2(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₂   

The following pairs are in P_>:

LOAD1421(i25[0]) → COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[0])

The following pairs are in P_bound:

LOAD1421(i25[0]) → COND_LOAD1421(&&(>(i25[0], 0), <(i25[0], 100)), i25[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])
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_≥:

COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0)
INC1614(i25[2], i33[2]) → LOAD1523(i25[2], +(i33[2], 1))
LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])
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))
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))
LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
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.

(14) Complex Obligation (AND)

(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:
(1): COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0)
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])
(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])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 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])
(7): COND_LOAD1523(TRUE, i25[7], i33[7]) → LOAD1421(i25[7] + 1)
(8): LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

(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])
(8): LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 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])
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])

(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

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

  (1)    (INC1614(i25[2], i33[2])≥NonInfC∧INC1614(i25[2], i33[2])≥LOAD1523(i25[2], +(i33[2], 1))∧(U^Increasing(LOAD1523(i25[2], +(i33[2], 1))), ≥))

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

  (2)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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])∧(U^Increasing(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])∧(U^Increasing(INC1614(i25[10], i33[10])), ≥))

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

  (8)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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))=TRUE∧i33[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])∧(U^Increasing(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)=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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:
  

  (21)    (LOAD1523(i25[8], i33[8])≥NonInfC∧LOAD1523(i25[8], i33[8])≥LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])∧(U^Increasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥))

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

  (22)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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:
  

  (26)    (COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5])≥NonInfC∧COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5])≥LOAD1523(i25[5], +(i33[5], 1))∧(U^Increasing(LOAD1523(i25[5], +(i33[5], 1))), ≥))

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

  (27)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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))=TRUE∧i25[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])∧(U^Increasing(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])=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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:
  

  (40)    (LOAD1523(i25[3], i33[3])≥NonInfC∧LOAD1523(i25[3], i33[3])≥LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])∧(U^Increasing(LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])), ≥))

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

  (41)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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))
  
  • ((U^Increasing(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])
  
  • ((U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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)
    
  
  
• LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
  
  • ((U^Increasing(LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
    
  
  
• COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1))
  
  • ((U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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)
    
  
  
• LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])
  
  • ((U^Increasing(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 P_bound 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 P_bound.
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(x₁, x₂)) = [-1] + [-1]x₂   
POL(LOAD1523(x₁, x₂)) = [-1]x₂   
POL(+(x₁, x₂)) = x₁ + x₂   
POL(1) = [1]   
POL(COND_LOAD1523ARR2(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₃   
POL(LOAD1523ARR2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₂   
POL(&&(x₁, x₂)) = [-1]   
POL(>(x₁, x₂)) = [-1]   
POL(0) = 0   
POL(<(x₁, x₂)) = [-1]   
POL(100) = [100]   
POL(>=(x₁, x₂)) = [-1]   
POL(-(x₁, x₂)) = x₁ + [-1]x₂   
POL(COND_LOAD1523ARR1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₃   
POL(LOAD1523ARR1(x₁, x₂, x₃, x₄)) = [-1]x₂   
POL(<=(x₁, x₂)) = [-1]   

The following pairs are in P_>:

LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
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_bound:

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])
COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], +(i33[5], 1))
LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])

There are no usable rules.

(19) Complex Obligation (AND)

(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])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 1)
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])

(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

(21) IDependencyGraphProof (EQUIVALENT transformation)

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

(22) TRUE

(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])
(8): LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 1)
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])

(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

(24) IDependencyGraphProof (EQUIVALENT transformation)

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

(25) TRUE

(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:
(1): COND_LOAD1421(TRUE, i25[1]) → LOAD1523(i25[1], 0)
(2): INC1614(i25[2], i33[2]) → LOAD1523(i25[2], i33[2] + 1)
(3): LOAD1523(i25[3], i33[3]) → LOAD1523ARR1(i25[3], i33[3], i39[3], i37[3])
(5): COND_LOAD1523ARR1(TRUE, i25[5], i33[5], i39[5], i37[5]) → LOAD1523(i25[5], i33[5] + 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])
(7): COND_LOAD1523(TRUE, i25[7], i33[7]) → LOAD1421(i25[7] + 1)
(8): LOAD1523(i25[8], i33[8]) → LOAD1523ARR2(i25[8], i33[8], i39[8], i37[8])
(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:
Load1421(x0)
Cond_Load1421(TRUE, x0)
Inc1614(x0, x1)
Load1523(x0, x1)
Load1523ARR1(x0, x1, x2, x3)
Cond_Load1523ARR1(TRUE, x0, x1, x2, x3)
Cond_Load1523(TRUE, x0, x1)
Load1523ARR2(x0, x1, x2, x3)
Cond_Load1523ARR2(TRUE, x0, x1, x2, x3)

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(28) TRUE