### (0) Obligation:

JBC Problem based on JBC Program:
`No human-readable program information known.`

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

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 283 nodes with 2 SCCs.

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

### (5) 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:
Load1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → Cond_Load1852(i453 > 0 && i451 + 1 > 0, java.lang.Object(IntList(o1725, i453)), i183, i451)
Cond_Load1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → Load1852(java.lang.Object(IntList(o1725, i453 - 1)), i183, i451 + 1)
Load1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Cond_Load18521(i454 <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Load1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, i451 * i183)
Load1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → Cond_Load18522(i454 <= 0, java.lang.Object(IntList(NULL, i454)), i183, i451)
The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (7) 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:
Load1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → Cond_Load1852(i453 > 0 && i451 + 1 > 0, java.lang.Object(IntList(o1725, i453)), i183, i451)
Cond_Load1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → Load1852(java.lang.Object(IntList(o1725, i453 - 1)), i183, i451 + 1)
Load1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Cond_Load18521(i454 <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451)
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → Load1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, i451 * i183)
Load1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → Cond_Load18522(i454 <= 0, java.lang.Object(IntList(NULL, i454)), i183, i451)

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])
(4): LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(i454[4] <= 0, java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])

(0) -> (1), if ((java.lang.Object(IntList(o1725[0], i453[0])) →* java.lang.Object(IntList(o1725[1], i453[1])))∧(i451[0]* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0* TRUE)∧(i183[0]* i183[1]))

(1) -> (0), if ((i183[1]* i183[0])∧(i451[1] + 1* i451[0])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(o1725[0], i453[0]))))

(1) -> (2), if ((i183[1]* i183[2])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[1] + 1* i451[2]))

(1) -> (4), if ((java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[1]* i183[4])∧(i451[1] + 1* i451[4]))

(2) -> (3), if ((i183[2]* i183[3])∧(i454[2] <= 0* TRUE)∧(i451[2]* i451[3])∧(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3]))))

(3) -> (0), if ((java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(o1725[0], i453[0])))∧(i451[3] * i183[3]* i451[0])∧(i183[3]* i183[0]))

(3) -> (2), if ((i183[3]* i183[2])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[3] * i183[3]* i451[2]))

(3) -> (4), if ((i451[3] * i183[3]* i451[4])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[3]* i183[4]))

(4) -> (5), if ((i451[4]* i451[5])∧(i183[4]* i183[5])∧(java.lang.Object(IntList(NULL, i454[4])) →* java.lang.Object(IntList(NULL, i454[5])))∧(i454[4] <= 0* TRUE))

(5) -> (0), if ((i451[5]* i451[0])∧(NULL* java.lang.Object(IntList(o1725[0], i453[0])))∧(i183[5]* i183[0]))

(5) -> (2), if ((NULL* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i183[5]* i183[2])∧(i451[5]* i451[2]))

(5) -> (4), if ((i183[5]* i183[4])∧(i451[5]* i451[4])∧(NULL* java.lang.Object(IntList(NULL, i454[4]))))

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

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

### (9) 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): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])
(4): LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(i454[4] <= 0, java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])

(0) -> (1), if ((java.lang.Object(IntList(o1725[0], i453[0])) →* java.lang.Object(IntList(o1725[1], i453[1])))∧(i451[0]* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0* TRUE)∧(i183[0]* i183[1]))

(1) -> (0), if ((i183[1]* i183[0])∧(i451[1] + 1* i451[0])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(o1725[0], i453[0]))))

(1) -> (2), if ((i183[1]* i183[2])∧(java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[1] + 1* i451[2]))

(1) -> (4), if ((java.lang.Object(IntList(o1725[1], i453[1] - 1)) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[1]* i183[4])∧(i451[1] + 1* i451[4]))

(2) -> (3), if ((i183[2]* i183[3])∧(i454[2] <= 0* TRUE)∧(i451[2]* i451[3])∧(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3]))))

(3) -> (0), if ((java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(o1725[0], i453[0])))∧(i451[3] * i183[3]* i451[0])∧(i183[3]* i183[0]))

(3) -> (2), if ((i183[3]* i183[2])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i451[3] * i183[3]* i451[2]))

(3) -> (4), if ((i451[3] * i183[3]* i451[4])∧(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])) →* java.lang.Object(IntList(NULL, i454[4])))∧(i183[3]* i183[4]))

(4) -> (5), if ((i451[4]* i451[5])∧(i183[4]* i183[5])∧(java.lang.Object(IntList(NULL, i454[4])) →* java.lang.Object(IntList(NULL, i454[5])))∧(i454[4] <= 0* TRUE))

(5) -> (0), if ((i451[5]* i451[0])∧(NULL* java.lang.Object(IntList(o1725[0], i453[0])))∧(i183[5]* i183[0]))

(5) -> (2), if ((NULL* java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])))∧(i183[5]* i183[2])∧(i451[5]* i451[2]))

(5) -> (4), if ((i183[5]* i183[4])∧(i451[5]* i451[4])∧(NULL* java.lang.Object(IntList(NULL, i454[4]))))

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (10) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (11) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])
(4): LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(i454[4] <= 0, java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])

(0) -> (1), if (((o1725[0]* o1725[1])∧(i453[0]* i453[1]))∧(i451[0]* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0* TRUE)∧(i183[0]* i183[1]))

(1) -> (0), if ((i183[1]* i183[0])∧(i451[1] + 1* i451[0])∧((o1725[1]* o1725[0])∧(i453[1] - 1* i453[0])))

(1) -> (2), if ((i183[1]* i183[2])∧((o1725[1]* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(i453[1] - 1* i454[2]))∧(i451[1] + 1* i451[2]))

(1) -> (4), if (((o1725[1]* NULL)∧(i453[1] - 1* i454[4]))∧(i183[1]* i183[4])∧(i451[1] + 1* i451[4]))

(2) -> (3), if ((i183[2]* i183[3])∧(i454[2] <= 0* TRUE)∧(i451[2]* i451[3])∧((o1731Field0[2]* o1731Field0[3])∧(o1731Field1[2]* o1731Field1[3])∧(i454[2]* i454[3])))

(3) -> (0), if (((o1731Field0[3]* o1725[0])∧(o1731Field1[3]* i453[0]))∧(i451[3] * i183[3]* i451[0])∧(i183[3]* i183[0]))

(3) -> (2), if ((i183[3]* i183[2])∧((o1731Field0[3]* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(o1731Field1[3]* i454[2]))∧(i451[3] * i183[3]* i451[2]))

(3) -> (4), if ((i451[3] * i183[3]* i451[4])∧((o1731Field0[3]* NULL)∧(o1731Field1[3]* i454[4]))∧(i183[3]* i183[4]))

(4) -> (5), if ((i451[4]* i451[5])∧(i183[4]* i183[5])∧((i454[4]* i454[5]))∧(i454[4] <= 0* TRUE))

(5) -> (0), if ((i451[5]* i451[0])∧false∧(i183[5]* i183[0]))

(5) -> (2), if (false∧(i183[5]* i183[2])∧(i451[5]* i451[2]))

(5) -> (4), if ((i183[5]* i183[4])∧(i451[5]* i451[4])∧false)

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (12) 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 LOAD1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → COND_LOAD1852(&&(>(i453, 0), >(+(i451, 1), 0)), java.lang.Object(IntList(o1725, i453)), i183, i451) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) which results in the following constraint:

(1)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))

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

(2)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUELOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))

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

(3)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(16)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[0] + [bni_26]i183[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(4)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(16)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[0] + [bni_26]i183[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(5)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(16)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[0] + [bni_26]i183[0] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(6)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[bni_26] ≥ 0∧[bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)

For Pair COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1725, -(i453, 1))), i183, +(i451, 1)) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

(7)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]i183[1]=i183[0]1+(i451[1], 1)=i451[0]1o1725[1]=o1725[0]1-(i453[1], 1)=i453[0]1COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(8)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUECOND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(o1725[0], -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(9)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(10)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(11)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(12)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

(13)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]i183[1]=i183[2]o1725[1]=java.lang.Object(IntList(o1731Field0[2], o1731Field1[2]))∧-(i453[1], 1)=i454[2]+(i451[1], 1)=i451[2]COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(14)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUECOND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(15)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(16)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(17)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(18)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) which results in the following constraint:

(19)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]o1725[1]=NULL-(i453[1], 1)=i454[4]i183[1]=i183[4]+(i451[1], 1)=i451[4]COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(20)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUECOND_LOAD1852(TRUE, java.lang.Object(IntList(NULL, i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(NULL, i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(NULL, -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(21)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(22)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(23)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(16)bni_28 + (-1)Bound*bni_28] + [bni_28]i451[0] + [bni_28]i183[0] ≥ 0∧[(-1)bso_29] + i451[0] ≥ 0)

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

(24)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)

For Pair LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → COND_LOAD18521(<=(i454, 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])) which results in the following constraint:

(25)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))

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

(26)    (<=(i454[2], 0)=TRUELOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))

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

(27)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(16)bni_30 + (-1)Bound*bni_30] + [bni_30]i451[2] + [bni_30]i183[2] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(28)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(16)bni_30 + (-1)Bound*bni_30] + [bni_30]i451[2] + [bni_30]i183[2] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(29)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(16)bni_30 + (-1)Bound*bni_30] + [bni_30]i451[2] + [bni_30]i183[2] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(30)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[bni_30] ≥ 0∧[bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_31] ≥ 0)

For Pair COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, *(i451, i183)) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

(31)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]o1731Field0[3]=o1725[0]o1731Field1[3]=i453[0]*(i451[3], i183[3])=i451[0]i183[3]=i183[0]COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

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

(33)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(34)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(35)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(36)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

(37)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]i183[3]=i183[2]1o1731Field0[3]=java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1))∧o1731Field1[3]=i454[2]1*(i451[3], i183[3])=i451[2]1COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

(38)    (<=(i454[2], 0)=TRUECOND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

(39)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(40)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(41)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(42)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) which results in the following constraint:

(43)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]*(i451[3], i183[3])=i451[4]o1731Field0[3]=NULLo1731Field1[3]=i454[4]i183[3]=i183[4]COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

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

(45)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(46)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(47)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(16)bni_32 + (-1)Bound*bni_32] + [bni_32]i451[2] + [bni_32]i183[2] ≥ 0∧[(-1)bso_33] + i451[2] ≥ 0)

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

(48)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)

For Pair LOAD1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → COND_LOAD18522(<=(i454, 0), java.lang.Object(IntList(NULL, i454)), i183, i451) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]) which results in the following constraint:

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

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

(51)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[(16)bni_34 + (-1)Bound*bni_34] + [bni_34]i451[4] + [bni_34]i183[4] ≥ 0∧[15 + (-1)bso_35] ≥ 0)

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

(52)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[(16)bni_34 + (-1)Bound*bni_34] + [bni_34]i451[4] + [bni_34]i183[4] ≥ 0∧[15 + (-1)bso_35] ≥ 0)

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

(53)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[(16)bni_34 + (-1)Bound*bni_34] + [bni_34]i451[4] + [bni_34]i183[4] ≥ 0∧[15 + (-1)bso_35] ≥ 0)

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

(54)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[bni_34] ≥ 0∧[bni_34] ≥ 0∧0 ≥ 0∧[(16)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[15 + (-1)bso_35] ≥ 0)

For Pair COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454)), i183, i451) → LOAD1852(NULL, i183, i451) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

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

(56)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(57)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(58)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(59)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

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

(61)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(62)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(63)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(64)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]), COND_LOAD18522(TRUE, java.lang.Object(IntList(NULL, i454[5])), i183[5], i451[5]) → LOAD1852(NULL, i183[5], i451[5]), LOAD1852(java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) → COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4]) which results in the following constraint:

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

(66)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(67)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(68)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧[1 + (-1)bso_37] ≥ 0)

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

(69)    ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1852(java.lang.Object(IntList(o1725, i453)), i183, i451) → COND_LOAD1852(&&(>(i453, 0), >(+(i451, 1), 0)), java.lang.Object(IntList(o1725, i453)), i183, i451)
• (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[bni_26] ≥ 0∧[bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_27] ≥ 0)

• COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725, i453)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1725, -(i453, 1))), i183, +(i451, 1))
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_28] ≥ 0∧[bni_28] ≥ 0∧0 ≥ 0∧[(16)bni_28 + (-1)Bound*bni_28] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_29] ≥ 0)

• LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → COND_LOAD18521(<=(i454, 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451)
• (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[bni_30] ≥ 0∧[bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_30 + (-1)Bound*bni_30] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_31] ≥ 0)

• COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0, o1731Field1)), i454)), i183, i451) → LOAD1852(java.lang.Object(IntList(o1731Field0, o1731Field1)), i183, *(i451, i183))
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_32] ≥ 0∧[bni_32] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(16)bni_32 + (-1)Bound*bni_32] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_33] ≥ 0)

• LOAD1852(java.lang.Object(IntList(NULL, i454)), i183, i451) → COND_LOAD18522(<=(i454, 0), java.lang.Object(IntList(NULL, i454)), i183, i451)
• (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18522(<=(i454[4], 0), java.lang.Object(IntList(NULL, i454[4])), i183[4], i451[4])), ≥)∧[bni_34] ≥ 0∧[bni_34] ≥ 0∧0 ≥ 0∧[(16)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[15 + (-1)bso_35] ≥ 0)

• ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)
• ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)
• ((UIncreasing(LOAD1852(NULL, i183[5], i451[5])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_37] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD1852(x1, x2, x3)) = x3 + x2 + [2]x1
POL(java.lang.Object(x1)) = [2] + [2]x1
POL(IntList(x1, x2)) = [3]
POL(COND_LOAD1852(x1, x2, x3, x4)) = x4 + x3 + [2]x2 + [3]x1
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = 0
POL(0) = 0
POL(+(x1, x2)) = 0
POL(1) = 0
POL(-(x1, x2)) = 0
POL(COND_LOAD18521(x1, x2, x3, x4)) = x4 + x3 + [2]x2
POL(<=(x1, x2)) = 0
POL(*(x1, x2)) = 0
POL(NULL) = 0
POL(COND_LOAD18522(x1, x2, x3, x4)) = [1] + x4 + x3

The following pairs are in P>:

The following pairs are in Pbound:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

The following pairs are in P:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

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

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

### (14) 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): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)
(2): LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(i454[2] <= 0, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
(3): COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], i451[3] * i183[3])

(1) -> (0), if ((i183[1]* i183[0])∧(i451[1] + 1* i451[0])∧((o1725[1]* o1725[0])∧(i453[1] - 1* i453[0])))

(3) -> (0), if (((o1731Field0[3]* o1725[0])∧(o1731Field1[3]* i453[0]))∧(i451[3] * i183[3]* i451[0])∧(i183[3]* i183[0]))

(0) -> (1), if (((o1725[0]* o1725[1])∧(i453[0]* i453[1]))∧(i451[0]* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0* TRUE)∧(i183[0]* i183[1]))

(1) -> (2), if ((i183[1]* i183[2])∧((o1725[1]* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(i453[1] - 1* i454[2]))∧(i451[1] + 1* i451[2]))

(3) -> (2), if ((i183[3]* i183[2])∧((o1731Field0[3]* java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])))∧(o1731Field1[3]* i454[2]))∧(i451[3] * i183[3]* i451[2]))

(2) -> (3), if ((i183[2]* i183[3])∧(i454[2] <= 0* TRUE)∧(i451[2]* i451[3])∧((o1731Field0[2]* o1731Field0[3])∧(o1731Field1[2]* o1731Field1[3])∧(i454[2]* i454[3])))

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (15) 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 LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) which results in the following constraint:

(1)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))

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

(2)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUELOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))

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

(3)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i451[0] + [(2)bni_20]i183[0] + [(4)bni_20]o1725[0] ≥ 0∧[(-1)bso_21] + i451[0] ≥ 0)

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

(4)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i451[0] + [(2)bni_20]i183[0] + [(4)bni_20]o1725[0] ≥ 0∧[(-1)bso_21] + i451[0] ≥ 0)

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

(5)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i451[0] + [(2)bni_20]i183[0] + [(4)bni_20]o1725[0] ≥ 0∧[(-1)bso_21] + i451[0] ≥ 0)

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

(6)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20] ≥ 0∧[(2)bni_20] ≥ 0∧0 ≥ 0∧[(4)bni_20] ≥ 0∧[(2)bni_20 + (-1)Bound*bni_20] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_21] ≥ 0)

For Pair COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

(7)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]i183[1]=i183[0]1+(i451[1], 1)=i451[0]1o1725[1]=o1725[0]1-(i453[1], 1)=i453[0]1COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(8)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUECOND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(o1725[0], -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(9)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(4)bni_22]o1725[0] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)

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

(10)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(4)bni_22]o1725[0] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)

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

(11)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(4)bni_22]o1725[0] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)

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

(12)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧[(4)bni_22] ≥ 0∧[(2)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

(13)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]i183[1]=i183[2]o1725[1]=java.lang.Object(IntList(o1731Field0[2], o1731Field1[2]))∧-(i453[1], 1)=i454[2]+(i451[1], 1)=i451[2]COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(14)    (&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUECOND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(15)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(6)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(8)bni_22]o1731Field0[2] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)

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

(16)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(6)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(8)bni_22]o1731Field0[2] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)

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

(17)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(6)bni_22 + (-1)Bound*bni_22] + [bni_22]i451[0] + [(2)bni_22]i183[0] + [(8)bni_22]o1731Field0[2] ≥ 0∧[(-1)bso_23] + i451[0] ≥ 0)

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

(18)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_22] ≥ 0∧[(6)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)

For Pair LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])) which results in the following constraint:

(19)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))

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

(20)    (<=(i454[2], 0)=TRUELOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])≥COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])∧(UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥))

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

(21)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(6)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i451[2] + [(2)bni_24]i183[2] + [(8)bni_24]o1731Field0[2] ≥ 0∧[3 + (-1)bso_25] + i451[2] + [4]o1731Field0[2] ≥ 0)

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

(22)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(6)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i451[2] + [(2)bni_24]i183[2] + [(8)bni_24]o1731Field0[2] ≥ 0∧[3 + (-1)bso_25] + i451[2] + [4]o1731Field0[2] ≥ 0)

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

(23)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(6)bni_24 + (-1)Bound*bni_24] + [(2)bni_24]i451[2] + [(2)bni_24]i183[2] + [(8)bni_24]o1731Field0[2] ≥ 0∧[3 + (-1)bso_25] + i451[2] + [4]o1731Field0[2] ≥ 0)

We simplified constraint (23) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

(24)    (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(2)bni_24] ≥ 0∧[(2)bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_24] ≥ 0∧[(6)bni_24 + (-1)Bound*bni_24] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_25] ≥ 0∧[1] ≥ 0)

For Pair COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

(25)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]o1731Field0[3]=o1725[0]o1731Field1[3]=i453[0]*(i451[3], i183[3])=i451[0]i183[3]=i183[0]COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

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

(27)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(4)bni_26]o1731Field0[2] ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)

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

(28)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(4)bni_26]o1731Field0[2] ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)

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

(29)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(3)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(4)bni_26]o1731Field0[2] ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)

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

(30)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(4)bni_26] ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)

• We consider the chain LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]), COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3])), LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) which results in the following constraint:

(31)    (i183[2]=i183[3]<=(i454[2], 0)=TRUEi451[2]=i451[3]o1731Field0[2]=o1731Field0[3]o1731Field1[2]=o1731Field1[3]i454[2]=i454[3]i183[3]=i183[2]1o1731Field0[3]=java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1))∧o1731Field1[3]=i454[2]1*(i451[3], i183[3])=i451[2]1COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3])≥LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

(32)    (<=(i454[2], 0)=TRUECOND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥NonInfC∧COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i454[2])), i183[2], i451[2])≥LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2]1, o1731Field1[2]1)), o1731Field1[2])), i183[2], *(i451[2], i183[2]))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥))

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

(33)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(7)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(8)bni_26]o1731Field0[2]1 ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)

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

(34)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(7)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(8)bni_26]o1731Field0[2]1 ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)

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

(35)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[(7)bni_26 + (-1)Bound*bni_26] + [bni_26]i451[2] + [(2)bni_26]i183[2] + [(8)bni_26]o1731Field0[2]1 ≥ 0∧[1 + (-1)bso_27] + i451[2] ≥ 0)

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

(36)    (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_26] ≥ 0∧[(7)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
• (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(2)bni_20] ≥ 0∧[(2)bni_20] ≥ 0∧0 ≥ 0∧[(4)bni_20] ≥ 0∧[(2)bni_20 + (-1)Bound*bni_20] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_21] ≥ 0)

• COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧[(4)bni_22] ≥ 0∧[(2)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[bni_22] ≥ 0∧[(2)bni_22] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_22] ≥ 0∧[(6)bni_22 + (-1)Bound*bni_22] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_23] ≥ 0)

• LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
• (0 ≥ 0 ⇒ (UIncreasing(COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])), ≥)∧[(2)bni_24] ≥ 0∧[(2)bni_24] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_24] ≥ 0∧[(6)bni_24 + (-1)Bound*bni_24] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[3 + (-1)bso_25] ≥ 0∧[1] ≥ 0)

• COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(4)bni_26] ≥ 0∧[(3)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))), ≥)∧[bni_26] ≥ 0∧[(2)bni_26] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(8)bni_26] ≥ 0∧[(7)bni_26 + (-1)Bound*bni_26] ≥ 0∧[1] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD1852(x1, x2, x3)) = [2]x3 + [2]x2 + [2]x1
POL(java.lang.Object(x1)) = x1
POL(IntList(x1, x2)) = [1] + [2]x1
POL(COND_LOAD1852(x1, x2, x3, x4)) = x4 + [2]x3 + [2]x2 + [3]x1
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = 0
POL(0) = 0
POL(+(x1, x2)) = 0
POL(1) = 0
POL(-(x1, x2)) = 0
POL(COND_LOAD18521(x1, x2, x3, x4)) = x4 + [2]x3 + x2
POL(<=(x1, x2)) = 0
POL(*(x1, x2)) = 0

The following pairs are in P>:

LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

The following pairs are in Pbound:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
LOAD1852(java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2]) → COND_LOAD18521(<=(i454[2], 0), java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[2], o1731Field1[2])), i454[2])), i183[2], i451[2])
COND_LOAD18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i454[3])), i183[3], i451[3]) → LOAD1852(java.lang.Object(IntList(o1731Field0[3], o1731Field1[3])), i183[3], *(i451[3], i183[3]))

The following pairs are in P:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))

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

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

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

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
(1): COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], i453[1] - 1)), i183[1], i451[1] + 1)

(1) -> (0), if ((i183[1]* i183[0])∧(i451[1] + 1* i451[0])∧((o1725[1]* o1725[0])∧(i453[1] - 1* i453[0])))

(0) -> (1), if (((o1725[0]* o1725[1])∧(i453[0]* i453[1]))∧(i451[0]* i451[1])∧(i453[0] > 0 && i451[0] + 1 > 0* TRUE)∧(i183[0]* i183[1]))

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (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 LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) which results in the following constraint:

(1)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))

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

(2)    (>(i453[0], 0)=TRUE>(+(i451[0], 1), 0)=TRUELOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])∧(UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥))

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

(3)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(4)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(5)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧[(-1)bso_20] ≥ 0)

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

(6)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19] + [bni_19]i453[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)

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

(7)    (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19 + bni_19] + [bni_19]i453[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)

For Pair COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)) the following chains were created:
• We consider the chain LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]), COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1)), LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) which results in the following constraint:

(8)    (o1725[0]=o1725[1]i453[0]=i453[1]i451[0]=i451[1]&&(>(i453[0], 0), >(+(i451[0], 1), 0))=TRUEi183[0]=i183[1]i183[1]=i183[0]1+(i451[1], 1)=i451[0]1o1725[1]=o1725[0]1-(i453[1], 1)=i453[0]1COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1])≥LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(9)    (>(i453[0], 0)=TRUE>(+(i451[0], 1), 0)=TRUECOND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥NonInfC∧COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])≥LOAD1852(java.lang.Object(IntList(o1725[0], -(i453[0], 1))), i183[0], +(i451[0], 1))∧(UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥))

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

(10)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)

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

(11)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)

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

(12)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧[1 + (-1)bso_22] ≥ 0)

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

(13)    (i453[0] + [-1] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21] + [bni_21]i453[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

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

(14)    (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + bni_21] + [bni_21]i453[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
• (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_19 + bni_19] + [bni_19]i453[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_20] ≥ 0)

• COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))
• (i453[0] ≥ 0∧i451[0] ≥ 0 ⇒ (UIncreasing(LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_21 + bni_21] + [bni_21]i453[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = [1]
POL(LOAD1852(x1, x2, x3)) = [-1] + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(IntList(x1, x2)) = [-1] + [-1]x2
POL(COND_LOAD1852(x1, x2, x3, x4)) = [-1] + [-1]x2 + [-1]x1
POL(&&(x1, x2)) = 0
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(-(x1, x2)) = x1 + [-1]x2

The following pairs are in P>:

COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))

The following pairs are in Pbound:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])
COND_LOAD1852(TRUE, java.lang.Object(IntList(o1725[1], i453[1])), i183[1], i451[1]) → LOAD1852(java.lang.Object(IntList(o1725[1], -(i453[1], 1))), i183[1], +(i451[1], 1))

The following pairs are in P:

LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(&&(>(i453[0], 0), >(+(i451[0], 1), 0)), java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])

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

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

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

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1852(java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0]) → COND_LOAD1852(i453[0] > 0 && i451[0] + 1 > 0, java.lang.Object(IntList(o1725[0], i453[0])), i183[0], i451[0])

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (21) IDependencyGraphProof (EQUIVALENT transformation)

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

### (23) Obligation:

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

The following domains are used:
none

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (24) IDependencyGraphProof (EQUIVALENT transformation)

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

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

R is empty.

The integer pair graph is empty.

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (27) IDependencyGraphProof (EQUIVALENT transformation)

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

### (29) Obligation:

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

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:
Cond_Load18521(TRUE, java.lang.Object(IntList(java.lang.Object(IntList(x0, x1)), x2)), x3, x4)

### (30) IDependencyGraphProof (EQUIVALENT transformation)

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

### (32) 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:
Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Cond_Load1102ARR1(i96 > 0 && i96 < i3 && i98 > 0 && i96 + 1 > 0, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96 + 1, i98 + -1)
The set Q consists of the following terms:
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (34) 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:
Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Load1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Cond_Load1102ARR1(i96 > 0 && i96 < i3 && i98 > 0 && i96 + 1 > 0, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → Load1102(java.lang.Object(ARRAY(i3, a1201data)), i96 + 1, i98 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(0) -> (1), if ((i98[0]* i98[1])∧(java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])) →* java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(java.lang.Object(ARRAY(i3[0], a1201data[0])) →* java.lang.Object(ARRAY(i3[1], a1201data[1])))∧(i96[0]* i96[1]))

(1) -> (2), if ((i96[1]* i96[2])∧(java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])) →* java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))∧(i98[1]* i98[2])∧(java.lang.Object(ARRAY(i3[1], a1201data[1])) →* java.lang.Object(ARRAY(i3[2], a1201data[2])))∧(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0* TRUE))

(2) -> (0), if ((i98[2] + -1* i98[0])∧(java.lang.Object(ARRAY(i3[2], a1201data[2])) →* java.lang.Object(ARRAY(i3[0], a1201data[0])))∧(i96[2] + 1* i96[0]))

The set Q consists of the following terms:
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

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

### (36) 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): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(0) -> (1), if ((i98[0]* i98[1])∧(java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])) →* java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(java.lang.Object(ARRAY(i3[0], a1201data[0])) →* java.lang.Object(ARRAY(i3[1], a1201data[1])))∧(i96[0]* i96[1]))

(1) -> (2), if ((i96[1]* i96[2])∧(java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])) →* java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))∧(i98[1]* i98[2])∧(java.lang.Object(ARRAY(i3[1], a1201data[1])) →* java.lang.Object(ARRAY(i3[2], a1201data[2])))∧(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0* TRUE))

(2) -> (0), if ((i98[2] + -1* i98[0])∧(java.lang.Object(ARRAY(i3[2], a1201data[2])) →* java.lang.Object(ARRAY(i3[0], a1201data[0])))∧(i96[2] + 1* i96[0]))

The set Q consists of the following terms:
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (37) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (38) 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): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(0) -> (1), if ((i98[0]* i98[1])∧((i175[0]* i175[1])∧(i174[0]* i174[1])∧(i176[0]* i176[1])∧(a1572[0]* a1572[1]))∧((i3[0]* i3[1])∧(a1201data[0]* a1201data[1]))∧(i96[0]* i96[1]))

(1) -> (2), if ((i96[1]* i96[2])∧((i175[1]* i175[2])∧(i174[1]* i174[2])∧(i176[1]* i176[2])∧(a1572[1]* a1572[2]))∧(i98[1]* i98[2])∧((i3[1]* i3[2])∧(a1201data[1]* a1201data[2]))∧(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0* TRUE))

(2) -> (0), if ((i98[2] + -1* i98[0])∧((i3[2]* i3[0])∧(a1201data[2]* a1201data[0]))∧(i96[2] + 1* i96[0]))

The set Q consists of the following terms:
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (39) 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 LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) the following chains were created:
• We consider the chain LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0]))) which results in the following constraint:

(1)    (LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0])≥NonInfC∧LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0])≥LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))∧(UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥))

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

(2)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(3)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(4)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(5)    ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96, 0), <(i96, i3)), >(i98, 0)), >(+(i96, 1), 0)), java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) the following chains were created:
• We consider the chain LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))), COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1)) which results in the following constraint:

(6)    (i96[1]=i96[2]i175[1]=i175[2]i174[1]=i174[2]i176[1]=i176[2]a1572[1]=a1572[2]i98[1]=i98[2]i3[1]=i3[2]a1201data[1]=a1201data[2]&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0))=TRUELOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥NonInfC∧LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥))

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

(7)    (>(+(i96[1], 1), 0)=TRUE>(i98[1], 0)=TRUE>(i96[1], 0)=TRUE<(i96[1], i3[1])=TRUELOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥NonInfC∧LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))≥COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))∧(UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥))

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

(8)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)

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

(9)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)

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

(10)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧[(-1)bso_19] ≥ 0)

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

(11)    (i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

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

(12)    ([1] + i96[1] ≥ 0∧i98[1] + [-1] ≥ 0∧i96[1] ≥ 0∧i3[1] + [-2] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

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

(13)    ([1] + i96[1] ≥ 0∧i98[1] ≥ 0∧i96[1] ≥ 0∧i3[1] + [-2] + [-1]i96[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [(-1)bni_18]i96[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

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

(14)    ([1] + i96[1] ≥ 0∧i98[1] ≥ 0∧i96[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

For Pair COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), +(i96, 1), +(i98, -1)) the following chains were created:
• We consider the chain COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1)) which results in the following constraint:

(15)    (COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))≥NonInfC∧COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2])))≥LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))∧(UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥))

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

(16)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)

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

(17)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)

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

(18)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧[2 + (-1)bso_21] ≥ 0)

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

(19)    ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), i96, i98) → LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
• ((UIncreasing(LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

• LOAD1102ARR1(java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96, 0), <(i96, i3)), >(i98, 0)), >(+(i96, 1), 0)), java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572)))
• ([1] + i96[1] ≥ 0∧i98[1] ≥ 0∧i96[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i98[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

• COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3, a1201data)), i96, i98, java.lang.Object(java.lang.String(i175, i174, i176, a1572))) → LOAD1102(java.lang.Object(ARRAY(i3, a1201data)), +(i96, 1), +(i98, -1))
• ((UIncreasing(LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[2 + (-1)bso_21] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD1102(x1, x2, x3)) = [1] + x3 + [-1]x2 + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1] + [-1]x1
POL(LOAD1102ARR1(x1, x2, x3, x4)) = [1] + x3 + [-1]x2 + [-1]x1
POL(java.lang.String(x1, x2, x3, x4)) = [-1]
POL(COND_LOAD1102ARR1(x1, x2, x3, x4, x5)) = [1] + x4 + [-1]x3 + [-1]x2
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(-1) = [-1]

The following pairs are in P>:

COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), +(i96[2], 1), +(i98[2], -1))

The following pairs are in Pbound:

LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))

The following pairs are in P:

LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(&&(&&(&&(>(i96[1], 0), <(i96[1], i3[1])), >(i98[1], 0)), >(+(i96[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))

There are no usable rules.

### (41) 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): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(1): LOAD1102ARR1(java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1]))) → COND_LOAD1102ARR1(i96[1] > 0 && i96[1] < i3[1] && i98[1] > 0 && i96[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1201data[1])), i96[1], i98[1], java.lang.Object(java.lang.String(i175[1], i174[1], i176[1], a1572[1])))

(0) -> (1), if ((i98[0]* i98[1])∧((i175[0]* i175[1])∧(i174[0]* i174[1])∧(i176[0]* i176[1])∧(a1572[0]* a1572[1]))∧((i3[0]* i3[1])∧(a1201data[0]* a1201data[1]))∧(i96[0]* i96[1]))

The set Q consists of the following terms:
Load1102ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1102ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (42) IDependencyGraphProof (EQUIVALENT transformation)

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

### (44) 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:
(0): LOAD1102(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0]) → LOAD1102ARR1(java.lang.Object(ARRAY(i3[0], a1201data[0])), i96[0], i98[0], java.lang.Object(java.lang.String(i175[0], i174[0], i176[0], a1572[0])))
(2): COND_LOAD1102ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2], i98[2], java.lang.Object(java.lang.String(i175[2], i174[2], i176[2], a1572[2]))) → LOAD1102(java.lang.Object(ARRAY(i3[2], a1201data[2])), i96[2] + 1, i98[2] + -1)

(2) -> (0), if ((i98[2] + -1* i98[0])∧((i3[2]* i3[0])∧(a1201data[2]* a1201data[0]))∧(i96[2] + 1* i96[0]))

The set Q consists of the following terms: