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

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 354 nodes with 3 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:
The set Q consists of the following terms:

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

Integer

The ITRS R consists of the following rules:

The integer pair graph contains the following rules and edges:

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

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

The set Q consists of the following terms:

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

Integer

R is empty.

The integer pair graph contains the following rules and edges:

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

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

The set Q consists of the following terms:

### (10) 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 LOAD2356(i717) → COND_LOAD2356(>(i717, 0), i717) the following chains were created:

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

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

(3)    (i717[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)

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

(4)    (i717[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)

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

(5)    (i717[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)

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

(6)    (i717[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_LOAD2356(TRUE, i717) → LOAD2356(+(i717, -1)) the following chains were created:
• We consider the chain COND_LOAD2356(TRUE, i717[1]) → LOAD2356(+(i717[1], -1)) which results in the following constraint:

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

(8)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

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

(9)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

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

(10)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

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

(11)    ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• (i717[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2356(>(i717[0], 0), i717[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]i717[0] ≥ 0∧[(-1)bso_9] ≥ 0)

• ((UIncreasing(LOAD2356(+(i717[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]

The following pairs are in P>:

The following pairs are in Pbound:

The following pairs are in P:

There are no usable rules.

### (12) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:

### (13) IDependencyGraphProof (EQUIVALENT transformation)

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

### (15) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:

The set Q consists of the following terms:

### (16) IDependencyGraphProof (EQUIVALENT transformation)

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

### (18) 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:
Load2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → Cond_Load2110(i637 > 1, java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676)))
Cond_Load2110(TRUE, java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → JMP2394(java.lang.Object(IntList(o2075, i676)), i637 + -1, o2075)
JMP2394(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Cond_Load21101(i637 > 1, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
Cond_Load21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637 + -1, o2070)
The set Q consists of the following terms:
Cond_Load2110(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x0, x1)))
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

### (19) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

### (20) 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:
Load2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → Cond_Load2110(i637 > 1, i637, java.lang.Object(IntList(o2075, i676)))
Cond_Load2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394(java.lang.Object(IntList(o2075, i676)), i637 + -1, o2075)
JMP2394(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Cond_Load21101(i637 > 1, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
Cond_Load21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637 + -1, o2070)
The set Q consists of the following terms:
JMP2394(java.lang.Object(IntList(x0, x1)), x2, x3)
Cond_Load21101(TRUE, java.lang.Object(IntList(x0, x1)), x2, java.lang.Object(IntList(x3, x4)))

### (22) 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

The ITRS R consists of the following rules:
Load2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → Cond_Load2110(i637 > 1, i637, java.lang.Object(IntList(o2075, i676)))
Cond_Load2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394(java.lang.Object(IntList(o2075, i676)), i637 + -1, o2075)
JMP2394(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Cond_Load21101(i637 > 1, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
Cond_Load21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → Load2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637 + -1, o2070)

The integer pair graph contains the following rules and edges:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(3): LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(i637[3] > 1, java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(0) -> (1), if ((java.lang.Object(IntList(o2075[0], i676[0])) →* java.lang.Object(IntList(o2075[1], i676[1])))∧(i637[0]* i637[1])∧(i637[0] > 1* TRUE))

(1) -> (2), if ((i637[1] + -1* i650[2])∧(o2075[1]* o2070[2])∧(java.lang.Object(IntList(o2075[1], i676[1])) →* java.lang.Object(IntList(o1946Field0[2], o1946Field1[2]))))

(2) -> (0), if ((o2070[2]* java.lang.Object(IntList(o2075[0], i676[0])))∧(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i650[2]* i637[0]))

(2) -> (3), if ((java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(o2070[2]* java.lang.Object(IntList(o2070[3], i675[3])))∧(i650[2]* i637[3]))

(3) -> (4), if ((java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])) →* java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])))∧(i637[3] > 1* TRUE)∧(java.lang.Object(IntList(o2070[3], i675[3])) →* java.lang.Object(IntList(o2070[4], i675[4])))∧(i637[3]* i637[4]))

(4) -> (0), if ((java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(o2070[4]* java.lang.Object(IntList(o2075[0], i676[0])))∧(i637[4] + -1* i637[0]))

(4) -> (3), if ((o2070[4]* java.lang.Object(IntList(o2070[3], i675[3])))∧(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(i637[4] + -1* i637[3]))

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

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

### (24) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(3): LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(i637[3] > 1, java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(0) -> (1), if ((java.lang.Object(IntList(o2075[0], i676[0])) →* java.lang.Object(IntList(o2075[1], i676[1])))∧(i637[0]* i637[1])∧(i637[0] > 1* TRUE))

(1) -> (2), if ((i637[1] + -1* i650[2])∧(o2075[1]* o2070[2])∧(java.lang.Object(IntList(o2075[1], i676[1])) →* java.lang.Object(IntList(o1946Field0[2], o1946Field1[2]))))

(2) -> (0), if ((o2070[2]* java.lang.Object(IntList(o2075[0], i676[0])))∧(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(i650[2]* i637[0]))

(2) -> (3), if ((java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(o2070[2]* java.lang.Object(IntList(o2070[3], i675[3])))∧(i650[2]* i637[3]))

(3) -> (4), if ((java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])) →* java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])))∧(i637[3] > 1* TRUE)∧(java.lang.Object(IntList(o2070[3], i675[3])) →* java.lang.Object(IntList(o2070[4], i675[4])))∧(i637[3]* i637[4]))

(4) -> (0), if ((java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o2075[0], i676[0])))∧(o2070[4]* java.lang.Object(IntList(o2075[0], i676[0])))∧(i637[4] + -1* i637[0]))

(4) -> (3), if ((o2070[4]* java.lang.Object(IntList(o2070[3], i675[3])))∧(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])) →* java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])))∧(i637[4] + -1* i637[3]))

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

### (25) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (26) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(3): LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(i637[3] > 1, java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(0) -> (1), if (((o2075[0]* o2075[1])∧(i676[0]* i676[1]))∧(i637[0]* i637[1])∧(i637[0] > 1* TRUE))

(1) -> (2), if ((i637[1] + -1* i650[2])∧(o2075[1]* o2070[2])∧((o2075[1]* o1946Field0[2])∧(i676[1]* o1946Field1[2])))

(2) -> (0), if ((o2070[2]* java.lang.Object(IntList(o2075[0], i676[0])))∧((o1946Field0[2]* o2075[0])∧(o1946Field1[2]* i676[0]))∧(i650[2]* i637[0]))

(2) -> (3), if (((o1946Field0[2]* o1946Field0[3])∧(o1946Field1[2]* o1946Field1[3]))∧(o2070[2]* java.lang.Object(IntList(o2070[3], i675[3])))∧(i650[2]* i637[3]))

(3) -> (4), if (((o1946Field0[3]* o1946Field0[4])∧(o1946Field1[3]* o1946Field1[4]))∧(i637[3] > 1* TRUE)∧((o2070[3]* o2070[4])∧(i675[3]* i675[4]))∧(i637[3]* i637[4]))

(4) -> (0), if (((o1946Field0[4]* o2075[0])∧(o1946Field1[4]* i676[0]))∧(o2070[4]* java.lang.Object(IntList(o2075[0], i676[0])))∧(i637[4] + -1* i637[0]))

(4) -> (3), if ((o2070[4]* java.lang.Object(IntList(o2070[3], i675[3])))∧((o1946Field0[4]* o1946Field0[3])∧(o1946Field1[4]* o1946Field1[3]))∧(i637[4] + -1* i637[3]))

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

### (27) 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 LOAD2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → COND_LOAD2110(>(i637, 1), i637, java.lang.Object(IntList(o2075, i676))) the following chains were created:
• We consider the chain LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))), COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1]) which results in the following constraint:

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

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

(3)    (i637[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)

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

(4)    (i637[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)

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

(5)    (i637[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)

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

(6)    (i637[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[(5)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)

For Pair COND_LOAD2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394'(java.lang.Object(IntList(o2075, i676)), +(i637, -1), o2075) the following chains were created:
• We consider the chain COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1]) which results in the following constraint:

(7)    (COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1])))≥NonInfC∧COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1])))≥JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])∧(UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥))

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

(8)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧[1 + (-1)bso_17] ≥ 0)

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

(9)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧[1 + (-1)bso_17] ≥ 0)

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

(10)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧[1 + (-1)bso_17] ≥ 0)

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

(11)    ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧0 = 0∧[1 + (-1)bso_17] ≥ 0)

For Pair JMP2394'(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) the following chains were created:
• We consider the chain JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]), LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) which results in the following constraint:

(12)    (o2070[2]=java.lang.Object(IntList(o2075[0], i676[0]))∧o1946Field0[2]=o2075[0]o1946Field1[2]=i676[0]i650[2]=i637[0]JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))

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

(13)    (JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])))≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])))≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])))∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))

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

(14)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(15)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(16)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(17)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

• We consider the chain JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]), LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) which results in the following constraint:

(18)    (o1946Field0[2]=o1946Field0[3]o1946Field1[2]=o1946Field1[3]o2070[2]=java.lang.Object(IntList(o2070[3], i675[3]))∧i650[2]=i637[3]JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))

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

(19)    (JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o2070[3], i675[3])))≥NonInfC∧JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o2070[3], i675[3])))≥LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], java.lang.Object(IntList(o2070[3], i675[3])))∧(UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥))

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

(20)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(21)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(22)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(23)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → COND_LOAD21101(>(i637, 1), java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) the following chains were created:
• We consider the chain LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))), COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4]) which results in the following constraint:

(24)    (o1946Field0[3]=o1946Field0[4]o1946Field1[3]=o1946Field1[4]>(i637[3], 1)=TRUEo2070[3]=o2070[4]i675[3]=i675[4]i637[3]=i637[4]LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥NonInfC∧LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))∧(UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥))

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

(25)    (>(i637[3], 1)=TRUELOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥NonInfC∧LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))≥COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))∧(UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥))

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

(26)    (i637[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)

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

(27)    (i637[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)

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

(28)    (i637[3] + [-2] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)

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

(29)    (i637[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[(5)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)

For Pair COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), +(i637, -1), o2070) the following chains were created:
• We consider the chain COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4]) which results in the following constraint:

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

(31)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧[1 + (-1)bso_23] ≥ 0)

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

(32)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧[1 + (-1)bso_23] ≥ 0)

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

(33)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧[1 + (-1)bso_23] ≥ 0)

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

(34)    ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD2110(java.lang.Object(IntList(o2075, i676)), i637, java.lang.Object(IntList(o2075, i676))) → COND_LOAD2110(>(i637, 1), i637, java.lang.Object(IntList(o2075, i676)))
• (i637[0] ≥ 0 ⇒ (UIncreasing(COND_LOAD2110(>(i637[0], 1), i637[0], java.lang.Object(IntList(o2075[0], i676[0])))), ≥)∧[(5)bni_14 + (-1)Bound*bni_14] + [(2)bni_14]i637[0] ≥ 0∧[(-1)bso_15] ≥ 0)

• COND_LOAD2110(TRUE, i637, java.lang.Object(IntList(o2075, i676))) → JMP2394'(java.lang.Object(IntList(o2075, i676)), +(i637, -1), o2075)
• ((UIncreasing(JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])), ≥)∧0 = 0∧[1 + (-1)bso_17] ≥ 0)

• JMP2394'(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i650, o2070)
• ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)
• ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])), ≥)∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

• LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → COND_LOAD21101(>(i637, 1), java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675)))
• (i637[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))), ≥)∧[(5)bni_20 + (-1)Bound*bni_20] + [(2)bni_20]i637[3] ≥ 0∧[1 + (-1)bso_21] ≥ 0)

• COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0, o1946Field1)), i637, java.lang.Object(IntList(o2070, i675))) → LOAD2110(java.lang.Object(IntList(o1946Field0, o1946Field1)), +(i637, -1), o2070)
• ((UIncreasing(LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])), ≥)∧0 = 0∧[1 + (-1)bso_23] ≥ 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(LOAD2110(x1, x2, x3)) = [1] + [2]x2
POL(java.lang.Object(x1)) = [-1]
POL(IntList(x1, x2)) = [-1]
POL(COND_LOAD2110(x1, x2, x3)) = [1] + [2]x2
POL(>(x1, x2)) = [-1]
POL(1) = [1]
POL(JMP2394'(x1, x2, x3)) = [2] + [2]x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_LOAD21101(x1, x2, x3, x4)) = [2]x3

The following pairs are in P>:

COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), +(i637[1], -1), o2075[1])
JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))
COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), +(i637[4], -1), o2070[4])

The following pairs are in Pbound:

LOAD2110(java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3]))) → COND_LOAD21101(>(i637[3], 1), java.lang.Object(IntList(o1946Field0[3], o1946Field1[3])), i637[3], java.lang.Object(IntList(o2070[3], i675[3])))

The following pairs are in P:

There are no usable rules.

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

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2110(java.lang.Object(IntList(o2075[0], i676[0])), i637[0], java.lang.Object(IntList(o2075[0], i676[0]))) → COND_LOAD2110(i637[0] > 1, i637[0], java.lang.Object(IntList(o2075[0], i676[0])))

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

### (30) IDependencyGraphProof (EQUIVALENT transformation)

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

### (32) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_LOAD2110(TRUE, i637[1], java.lang.Object(IntList(o2075[1], i676[1]))) → JMP2394'(java.lang.Object(IntList(o2075[1], i676[1])), i637[1] + -1, o2075[1])
(2): JMP2394'(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2]) → LOAD2110(java.lang.Object(IntList(o1946Field0[2], o1946Field1[2])), i650[2], o2070[2])
(4): COND_LOAD21101(TRUE, java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4], java.lang.Object(IntList(o2070[4], i675[4]))) → LOAD2110(java.lang.Object(IntList(o1946Field0[4], o1946Field1[4])), i637[4] + -1, o2070[4])

(1) -> (2), if ((i637[1] + -1* i650[2])∧(o2075[1]* o2070[2])∧((o2075[1]* o1946Field0[2])∧(i676[1]* o1946Field1[2])))

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

### (33) IDependencyGraphProof (EQUIVALENT transformation)

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

### (35) 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:
Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Cond_Load1206ARR1(i116 > 0 && i116 < i3 && i121 > 0 && i116 + 1 > 0, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116 + 1, i121 + -1)
The set Q consists of the following terms:
Load1206ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (37) Obligation:

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

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Load1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Cond_Load1206ARR1(i116 > 0 && i116 < i3 && i121 > 0 && i116 + 1 > 0, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
Cond_Load1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → Load1206(java.lang.Object(ARRAY(i3, a1405data)), i116 + 1, i121 + -1)

The integer pair graph contains the following rules and edges:
(0): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(0) -> (1), if ((java.lang.Object(ARRAY(i3[0], a1405data[0])) →* java.lang.Object(ARRAY(i3[1], a1405data[1])))∧(i116[0]* i116[1])∧(java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])) →* java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(i121[0]* i121[1]))

(1) -> (2), if ((i121[1]* i121[2])∧(java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])) →* java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))∧(java.lang.Object(ARRAY(i3[1], a1405data[1])) →* java.lang.Object(ARRAY(i3[2], a1405data[2])))∧(i116[1]* i116[2])∧(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0* TRUE))

(2) -> (0), if ((i116[2] + 1* i116[0])∧(i121[2] + -1* i121[0])∧(java.lang.Object(ARRAY(i3[2], a1405data[2])) →* java.lang.Object(ARRAY(i3[0], a1405data[0]))))

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

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

### (39) 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): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(0) -> (1), if ((java.lang.Object(ARRAY(i3[0], a1405data[0])) →* java.lang.Object(ARRAY(i3[1], a1405data[1])))∧(i116[0]* i116[1])∧(java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])) →* java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(i121[0]* i121[1]))

(1) -> (2), if ((i121[1]* i121[2])∧(java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])) →* java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))∧(java.lang.Object(ARRAY(i3[1], a1405data[1])) →* java.lang.Object(ARRAY(i3[2], a1405data[2])))∧(i116[1]* i116[2])∧(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0* TRUE))

(2) -> (0), if ((i116[2] + 1* i116[0])∧(i121[2] + -1* i121[0])∧(java.lang.Object(ARRAY(i3[2], a1405data[2])) →* java.lang.Object(ARRAY(i3[0], a1405data[0]))))

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

### (40) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (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): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(0) -> (1), if (((i3[0]* i3[1])∧(a1405data[0]* a1405data[1]))∧(i116[0]* i116[1])∧((i212[0]* i212[1])∧(i211[0]* i211[1])∧(i213[0]* i213[1])∧(a1774[0]* a1774[1]))∧(i121[0]* i121[1]))

(1) -> (2), if ((i121[1]* i121[2])∧((i212[1]* i212[2])∧(i211[1]* i211[2])∧(i213[1]* i213[2])∧(a1774[1]* a1774[2]))∧((i3[1]* i3[2])∧(a1405data[1]* a1405data[2]))∧(i116[1]* i116[2])∧(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0* TRUE))

(2) -> (0), if ((i116[2] + 1* i116[0])∧(i121[2] + -1* i121[0])∧((i3[2]* i3[0])∧(a1405data[2]* a1405data[0])))

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

### (42) 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 LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) the following chains were created:
• We consider the chain LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0]))) which results in the following constraint:

(1)    (LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0])≥NonInfC∧LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0])≥LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))∧(UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥))

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

(2)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(3)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(4)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(5)    ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116, 0), <(i116, i3)), >(i121, 0)), >(+(i116, 1), 0)), java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) the following chains were created:
• We consider the chain LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))), COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1)) which results in the following constraint:

(6)    (i121[1]=i121[2]i212[1]=i212[2]i211[1]=i211[2]i213[1]=i213[2]a1774[1]=a1774[2]i3[1]=i3[2]a1405data[1]=a1405data[2]i116[1]=i116[2]&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0))=TRUELOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥NonInfC∧LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥))

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

(7)    (>(+(i116[1], 1), 0)=TRUE>(i121[1], 0)=TRUE>(i116[1], 0)=TRUE<(i116[1], i3[1])=TRUELOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥NonInfC∧LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))≥COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))∧(UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥))

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

(8)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[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)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[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)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[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)    (i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] + [-1] ≥ 0∧i3[1] + [-1] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[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] + i116[1] ≥ 0∧i121[1] + [-1] ≥ 0∧i116[1] ≥ 0∧i3[1] + [-2] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[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] + i116[1] ≥ 0∧i121[1] ≥ 0∧i116[1] ≥ 0∧i3[1] + [-2] + [-1]i116[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [(-1)bni_18]i116[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] + i116[1] ≥ 0∧i121[1] ≥ 0∧i116[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

For Pair COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), +(i116, 1), +(i121, -1)) the following chains were created:
• We consider the chain COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1)) which results in the following constraint:

(15)    (COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))≥NonInfC∧COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2])))≥LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))∧(UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))), ≥))

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

(16)    ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[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(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[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(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[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(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[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.
• LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), i116, i121) → LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
• ((UIncreasing(LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

• LOAD1206ARR1(java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116, 0), <(i116, i3)), >(i121, 0)), >(+(i116, 1), 0)), java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774)))
• ([1] + i116[1] ≥ 0∧i121[1] ≥ 0∧i116[1] ≥ 0∧i3[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))), ≥)∧0 = 0∧[(4)bni_18 + (-1)Bound*bni_18] + [bni_18]i121[1] + [bni_18]i3[1] ≥ 0∧0 = 0∧[(-1)bso_19] ≥ 0)

• COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3, a1405data)), i116, i121, java.lang.Object(java.lang.String(i212, i211, i213, a1774))) → LOAD1206(java.lang.Object(ARRAY(i3, a1405data)), +(i116, 1), +(i121, -1))
• ((UIncreasing(LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[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(LOAD1206(x1, x2, x3)) = [1] + x3 + [-1]x2 + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1] + [-1]x1
POL(LOAD1206ARR1(x1, x2, x3, x4)) = [1] + x3 + [-1]x2 + [-1]x1
POL(java.lang.String(x1, x2, x3, x4)) = [-1]
POL(COND_LOAD1206ARR1(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_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), +(i116[2], 1), +(i121[2], -1))

The following pairs are in Pbound:

LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))

The following pairs are in P:

LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(&&(&&(&&(>(i116[1], 0), <(i116[1], i3[1])), >(i121[1], 0)), >(+(i116[1], 1), 0)), java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))

There are no usable rules.

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

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(1): LOAD1206ARR1(java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1]))) → COND_LOAD1206ARR1(i116[1] > 0 && i116[1] < i3[1] && i121[1] > 0 && i116[1] + 1 > 0, java.lang.Object(ARRAY(i3[1], a1405data[1])), i116[1], i121[1], java.lang.Object(java.lang.String(i212[1], i211[1], i213[1], a1774[1])))

(0) -> (1), if (((i3[0]* i3[1])∧(a1405data[0]* a1405data[1]))∧(i116[0]* i116[1])∧((i212[0]* i212[1])∧(i211[0]* i211[1])∧(i213[0]* i213[1])∧(a1774[0]* a1774[1]))∧(i121[0]* i121[1]))

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

### (45) IDependencyGraphProof (EQUIVALENT transformation)

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

### (47) 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): LOAD1206(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0]) → LOAD1206ARR1(java.lang.Object(ARRAY(i3[0], a1405data[0])), i116[0], i121[0], java.lang.Object(java.lang.String(i212[0], i211[0], i213[0], a1774[0])))
(2): COND_LOAD1206ARR1(TRUE, java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2], i121[2], java.lang.Object(java.lang.String(i212[2], i211[2], i213[2], a1774[2]))) → LOAD1206(java.lang.Object(ARRAY(i3[2], a1405data[2])), i116[2] + 1, i121[2] + -1)

(2) -> (0), if ((i116[2] + 1* i116[0])∧(i121[2] + -1* i121[0])∧((i3[2]* i3[0])∧(a1405data[2]* a1405data[0])))

The set Q consists of the following terms: