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

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 496 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:
Load3023(o1761, o1759) → NULL3243(o1761, o1759, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253)), java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253)), java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)
The set Q consists of the following terms:
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)), java.lang.Object(Tree(NULL, x1, x2)))

### (6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

NULL3243(x1, x2, x3) → NULL3243(x1, x3)

### (7) 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:
Load3023(o1761, o1759) → NULL3243(o1761, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)
The set Q consists of the following terms:
JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

### (8) ITRStoQTRSProof (EQUIVALENT transformation)

Represented integers and predefined function symbols by Terms

### (9) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)

The set Q consists of the following terms:

JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

### (10) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP6184(x1, x2)) = 1 + x1 + x2
POL(JMP8999(x1, x2)) = x1 + x2
POL(Load3023(x1, x2)) = x1 + x2
POL(NULL) = 0
POL(NULL3243(x1, x2)) = x1 + x2
POL(Tree(x1, x2, x3)) = x1 + x2 + x3
POL(java.lang.Object(x1)) = 2 + x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

JMP6184(o1883, o2252) → Load3023(o1883, o2252)
NULL3243(o1883, java.lang.Object(Tree(NULL, o2252, o2253))) → Load3023(o1883, o2252)
NULL3243(java.lang.Object(Tree(NULL, o2258, o2259)), java.lang.Object(Tree(NULL, o2258, o2259))) → JMP6184(java.lang.Object(Tree(NULL, o2258, o2259)), o2258)

### (11) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

The set Q consists of the following terms:

JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

### (12) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP8999(x1, x2)) = 2·x1 + x2
POL(Load3023(x1, x2)) = 2·x1 + x2
POL(NULL) = 0
POL(NULL3243(x1, x2)) = 2·x1 + x2
POL(Tree(x1, x2, x3)) = 1 + 2·x1 + x2 + 2·x3
POL(java.lang.Object(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

NULL3243(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259))) → JMP8999(java.lang.Object(Tree(java.lang.Object(Tree(o3001, o3002, o3003)), o2258, o2259)), java.lang.Object(Tree(o3001, java.lang.Object(Tree(o3002, o2258, NULL)), NULL)))
NULL3243(o1883, java.lang.Object(Tree(java.lang.Object(Tree(o2987, o2988, o2989)), o2252, o2253))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

### (13) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

The set Q consists of the following terms:

JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

### (14) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(JMP8999(x1, x2)) = 2 + x1 + x2
POL(Load3023(x1, x2)) = 1 + x1 + x2
POL(NULL) = 0
POL(NULL3243(x1, x2)) = x1 + x2
POL(Tree(x1, x2, x3)) = x1 + x2 + x3
POL(java.lang.Object(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

Load3023(o1761, o1759) → NULL3243(o1761, o1759)
JMP8999(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL))) → Load3023(o1883, java.lang.Object(Tree(o2987, java.lang.Object(Tree(o2988, o2252, NULL)), NULL)))

### (15) Obligation:

Q restricted rewrite system:
R is empty.
The set Q consists of the following terms:

JMP8999(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3, NULL)), NULL)))
NULL3243(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
JMP6184(x0, x1)
NULL3243(x0, java.lang.Object(Tree(NULL, x1, x2)))

### (16) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

### (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:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC)))) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)))
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814))) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807))) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807))) → Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR4(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC)))) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)))
JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814))) → Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR6(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC)))) → Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR7(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC)))) → Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR8(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))))
The set Q consists of the following terms:
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)))
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)))
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Inc13311(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, NULL, x7)))
Load9325ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
JMP13263(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, x6, x7)))
Load9325ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load9325ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Load9325ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

### (19) DuplicateArgsRemoverProof (EQUIVALENT transformation)

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

JMP13263(x1, x2, x3, x4, x5) → JMP13263(x1, x2, x3, x5)
Cond_Load9325ARR8(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR8(x1, x2, x3, x4, x6, x7)
Load9325ARR8(x1, x2, x3, x4, x5, x6) → Load9325ARR8(x1, x2, x3, x5, x6)
JMP13217(x1, x2, x3, x4, x5) → JMP13217(x1, x2, x3, x5)
Cond_Load9325ARR7(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR7(x1, x2, x3, x4, x6, x7)
Load9325ARR7(x1, x2, x3, x4, x5, x6) → Load9325ARR7(x1, x2, x3, x5, x6)
Inc13311(x1, x2, x3, x4, x5) → Inc13311(x1, x2, x3, x5)
Cond_Load9325ARR5(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR5(x1, x2, x3, x4, x6, x7)
Load9325ARR5(x1, x2, x3, x4, x5, x6) → Load9325ARR5(x1, x2, x3, x5, x6)
Cond_Load9325ARR1(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR1(x1, x2, x3, x4, x6, x7)
Load9325ARR1(x1, x2, x3, x4, x5, x6) → Load9325ARR1(x1, x2, x3, x5, x6)

### (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:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC)))) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)), java.lang.Object(EOC))), java.lang.Object(Tree(o6850Field0, o6850Field1, o6850Field2)))
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814))) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6947Field0, o6947Field1, o6947Field2)))
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807))) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6928Field0, o6928Field1, o6928Field2)))
Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807))) → Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, NULL, o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR4(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6805, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6807)), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC)))) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)), o6454, java.lang.Object(EOC))), java.lang.Object(Tree(o6896Field0, o6896Field1, o6896Field2)))
JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC)))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814))) → Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR6(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6813, o6814)), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, o6454, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC)))) → Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, NULL, java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → Cond_Load9325ARR7(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, i862, i864, a4416))) → JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(o6453, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC)))) → Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(NULL, o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR8(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))), java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), o6454, java.lang.Object(EOC))))
The set Q consists of the following terms:
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(x5, x6, x7)), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x8, x9, x10)))
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)))
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), java.lang.Object(java.lang.String(x11, x12, x13, x14)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, x7, x8)))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)))
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(x7, x8, x9)), x10)), java.lang.Object(java.lang.String(0, x11, x12, x13)))
Inc13311(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
JMP13217(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, NULL, x7)))
Load9325ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(x6, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x7)), java.lang.Object(java.lang.String(0, x8, x9, x10)))
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(x4, x5, x6)), x7, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
JMP13263(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))))
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(NULL, x6, x7)))
Load9325ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, x5, java.lang.Object(EOC))), java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x6, x7)), java.lang.Object(java.lang.String(x8, x9, x10, x11)))
Load9325ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(x4, java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), java.lang.Object(EOC))), java.lang.Object(java.lang.String(0, x5, x6, x7)))
Load9325ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(Tree(java.lang.Object(Tree(NULL, NULL, java.lang.Object(EOC))), x4, java.lang.Object(EOC))), java.lang.Object(java.lang.String(x5, x6, x7, x8)))

### (21) ITRSFilterProcessorProof (SOUND transformation)

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

Load9325(x1, x2, x3, x4, x5) → Load9325(x1, x2, x3)
Tree(x1, x2, x3) → Tree
Load9325ARR1(x1, x2, x3, x4, x5) → Load9325ARR1(x1, x2, x3)
Cond_Load9325ARR1(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR1(x1, x2, x3, x4)
Inc11229(x1, x2, x3, x4, x5) → Inc11229(x1, x2, x3)
JMP11303(x1, x2, x3, x4, x5) → JMP11303(x1, x2, x3)
Load9325ARR2(x1, x2, x3, x4, x5, x6) → Load9325ARR2(x1, x2, x3, x6)
Cond_Load9325ARR2(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR2(x1, x2, x3, x4, x7)
Load9325ARR3(x1, x2, x3, x4, x5, x6) → Load9325ARR3(x1, x2, x3)
Cond_Load9325ARR3(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR3(x1, x2, x3, x4)
Inc13311(x1, x2, x3, x4) → Inc13311(x1, x2, x3)
JMP13217(x1, x2, x3, x4) → JMP13217(x1, x2, x3)
Load9325ARR4(x1, x2, x3, x4, x5, x6) → Load9325ARR4(x1, x2, x3)
Cond_Load9325ARR4(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR4(x1, x2, x3, x4)
Load9325ARR5(x1, x2, x3, x4, x5) → Load9325ARR5(x1, x2, x3, x5)
Cond_Load9325ARR5(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR5(x1, x2, x3, x4, x6)
JMP13263(x1, x2, x3, x4) → JMP13263(x1, x2, x3)
Load9325ARR6(x1, x2, x3, x4, x5, x6) → Load9325ARR6(x1, x2, x3, x6)
Cond_Load9325ARR6(x1, x2, x3, x4, x5, x6, x7) → Cond_Load9325ARR6(x1, x2, x3, x4, x7)
Load9325ARR7(x1, x2, x3, x4, x5) → Load9325ARR7(x1, x2, x3)
Cond_Load9325ARR7(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR7(x1, x2, x3, x4)
Load9325ARR8(x1, x2, x3, x4, x5) → Load9325ARR8(x1, x2, x3, x5)
Cond_Load9325ARR8(x1, x2, x3, x4, x5, x6) → Cond_Load9325ARR8(x1, x2, x3, x4, x6)

### (22) 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:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR4(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR4(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR6(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR6(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc13311(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR7(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR7(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → JMP13217(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR8(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR8(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP13263(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Inc13311(java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP13217(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR4(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR4(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
JMP13263(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR6(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR6(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Load9325ARR7(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR7(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR8(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR8(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (23) ITRSFSMergerProof (SOUND transformation)

The following function symbols have been merged:

### (24) 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:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

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

Boolean, Integer

The ITRS R consists of the following rules:
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR1(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR2(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)
Inc11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i843, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Load9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Cond_Load9325ARR3(i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826 + -1)
Load9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Load9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → Cond_Load9325ARR5(i901 > 0 && i824 > 0 && i824 < i2 && i826 > 0 && i824 + 1 > 0, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303(java.lang.Object(ARRAY(i2, a4262data)), i824 + 1, i826)

The integer pair graph contains the following rules and edges:
(0): LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
(1): LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(5): LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
(6): COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6] + 1, i826[6])
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(8): LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
(9): LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(12): LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))
(13): COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13] + 1, i826[13])

(0) -> (1), if ((i824[0]* i824[1])∧(java.lang.Object(ARRAY(i2[0], a4262data[0])) →* java.lang.Object(ARRAY(i2[1], a4262data[1])))∧(i826[0]* i826[1]))

(1) -> (2), if ((i826[1]* i826[2])∧(i824[1]* i824[2])∧(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0* TRUE)∧(java.lang.Object(ARRAY(i2[1], a4262data[1])) →* java.lang.Object(ARRAY(i2[2], a4262data[2]))))

(2) -> (7), if ((java.lang.Object(ARRAY(i2[2], a4262data[2])) →* java.lang.Object(ARRAY(i2[7], a4262data[7])))∧(i824[2] + 1* i843[7])∧(i826[2]* i826[7]))

(3) -> (7), if ((i843[3]* i843[7])∧(java.lang.Object(ARRAY(i2[3], a4262data[3])) →* java.lang.Object(ARRAY(i2[7], a4262data[7])))∧(i826[3]* i826[7]))

(4) -> (5), if ((java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])) →* java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))∧(i824[4]* i824[5])∧(java.lang.Object(ARRAY(i2[4], a4262data[4])) →* java.lang.Object(ARRAY(i2[5], a4262data[5])))∧(i826[4]* i826[5]))

(5) -> (6), if ((i826[5]* i826[6])∧(java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])) →* java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6])))∧(i824[5]* i824[6])∧(java.lang.Object(ARRAY(i2[5], a4262data[5])) →* java.lang.Object(ARRAY(i2[6], a4262data[6])))∧(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0* TRUE))

(6) -> (7), if ((i826[6]* i826[7])∧(i824[6] + 1* i843[7])∧(java.lang.Object(ARRAY(i2[6], a4262data[6])) →* java.lang.Object(ARRAY(i2[7], a4262data[7]))))

(7) -> (0), if ((i826[7] + -1* i826[0])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[0], a4262data[0])))∧(i843[7]* i824[0]))

(7) -> (4), if ((i843[7]* i824[4])∧(i826[7] + -1* i826[4])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[4], a4262data[4]))))

(7) -> (8), if ((i826[7] + -1* i826[8])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[8], a4262data[8])))∧(i843[7]* i824[8]))

(7) -> (11), if ((i843[7]* i824[11])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[11], a4262data[11])))∧(i826[7] + -1* i826[11]))

(8) -> (9), if ((java.lang.Object(ARRAY(i2[8], a4262data[8])) →* java.lang.Object(ARRAY(i2[9], a4262data[9])))∧(i826[8]* i826[9])∧(i824[8]* i824[9]))

(9) -> (10), if ((i826[9]* i826[10])∧(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0* TRUE)∧(i824[9]* i824[10])∧(java.lang.Object(ARRAY(i2[9], a4262data[9])) →* java.lang.Object(ARRAY(i2[10], a4262data[10]))))

(10) -> (0), if ((java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[0], a4262data[0])))∧(i824[10] + 1* i824[0])∧(i826[10] + -1* i826[0]))

(10) -> (4), if ((i824[10] + 1* i824[4])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[4], a4262data[4])))∧(i826[10] + -1* i826[4]))

(10) -> (8), if ((i824[10] + 1* i824[8])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[8], a4262data[8])))∧(i826[10] + -1* i826[8]))

(10) -> (11), if ((i826[10] + -1* i826[11])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[11], a4262data[11])))∧(i824[10] + 1* i824[11]))

(11) -> (12), if ((i824[11]* i824[12])∧(java.lang.Object(ARRAY(i2[11], a4262data[11])) →* java.lang.Object(ARRAY(i2[12], a4262data[12])))∧(i826[11]* i826[12])∧(java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])) →* java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))))

(12) -> (13), if ((i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0* TRUE)∧(java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])) →* java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13])))∧(i824[12]* i824[13])∧(java.lang.Object(ARRAY(i2[12], a4262data[12])) →* java.lang.Object(ARRAY(i2[13], a4262data[13])))∧(i826[12]* i826[13]))

(13) -> (3), if ((java.lang.Object(ARRAY(i2[13], a4262data[13])) →* java.lang.Object(ARRAY(i2[3], a4262data[3])))∧(i824[13] + 1* i843[3])∧(i826[13]* i826[3]))

The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

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

### (28) 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): LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
(1): LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(5): LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
(6): COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6] + 1, i826[6])
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(8): LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
(9): LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(12): LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))
(13): COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13] + 1, i826[13])

(0) -> (1), if ((i824[0]* i824[1])∧(java.lang.Object(ARRAY(i2[0], a4262data[0])) →* java.lang.Object(ARRAY(i2[1], a4262data[1])))∧(i826[0]* i826[1]))

(1) -> (2), if ((i826[1]* i826[2])∧(i824[1]* i824[2])∧(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0* TRUE)∧(java.lang.Object(ARRAY(i2[1], a4262data[1])) →* java.lang.Object(ARRAY(i2[2], a4262data[2]))))

(2) -> (7), if ((java.lang.Object(ARRAY(i2[2], a4262data[2])) →* java.lang.Object(ARRAY(i2[7], a4262data[7])))∧(i824[2] + 1* i843[7])∧(i826[2]* i826[7]))

(3) -> (7), if ((i843[3]* i843[7])∧(java.lang.Object(ARRAY(i2[3], a4262data[3])) →* java.lang.Object(ARRAY(i2[7], a4262data[7])))∧(i826[3]* i826[7]))

(4) -> (5), if ((java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])) →* java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))∧(i824[4]* i824[5])∧(java.lang.Object(ARRAY(i2[4], a4262data[4])) →* java.lang.Object(ARRAY(i2[5], a4262data[5])))∧(i826[4]* i826[5]))

(5) -> (6), if ((i826[5]* i826[6])∧(java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])) →* java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6])))∧(i824[5]* i824[6])∧(java.lang.Object(ARRAY(i2[5], a4262data[5])) →* java.lang.Object(ARRAY(i2[6], a4262data[6])))∧(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0* TRUE))

(6) -> (7), if ((i826[6]* i826[7])∧(i824[6] + 1* i843[7])∧(java.lang.Object(ARRAY(i2[6], a4262data[6])) →* java.lang.Object(ARRAY(i2[7], a4262data[7]))))

(7) -> (0), if ((i826[7] + -1* i826[0])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[0], a4262data[0])))∧(i843[7]* i824[0]))

(7) -> (4), if ((i843[7]* i824[4])∧(i826[7] + -1* i826[4])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[4], a4262data[4]))))

(7) -> (8), if ((i826[7] + -1* i826[8])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[8], a4262data[8])))∧(i843[7]* i824[8]))

(7) -> (11), if ((i843[7]* i824[11])∧(java.lang.Object(ARRAY(i2[7], a4262data[7])) →* java.lang.Object(ARRAY(i2[11], a4262data[11])))∧(i826[7] + -1* i826[11]))

(8) -> (9), if ((java.lang.Object(ARRAY(i2[8], a4262data[8])) →* java.lang.Object(ARRAY(i2[9], a4262data[9])))∧(i826[8]* i826[9])∧(i824[8]* i824[9]))

(9) -> (10), if ((i826[9]* i826[10])∧(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0* TRUE)∧(i824[9]* i824[10])∧(java.lang.Object(ARRAY(i2[9], a4262data[9])) →* java.lang.Object(ARRAY(i2[10], a4262data[10]))))

(10) -> (0), if ((java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[0], a4262data[0])))∧(i824[10] + 1* i824[0])∧(i826[10] + -1* i826[0]))

(10) -> (4), if ((i824[10] + 1* i824[4])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[4], a4262data[4])))∧(i826[10] + -1* i826[4]))

(10) -> (8), if ((i824[10] + 1* i824[8])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[8], a4262data[8])))∧(i826[10] + -1* i826[8]))

(10) -> (11), if ((i826[10] + -1* i826[11])∧(java.lang.Object(ARRAY(i2[10], a4262data[10])) →* java.lang.Object(ARRAY(i2[11], a4262data[11])))∧(i824[10] + 1* i824[11]))

(11) -> (12), if ((i824[11]* i824[12])∧(java.lang.Object(ARRAY(i2[11], a4262data[11])) →* java.lang.Object(ARRAY(i2[12], a4262data[12])))∧(i826[11]* i826[12])∧(java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])) →* java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))))

(12) -> (13), if ((i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0* TRUE)∧(java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])) →* java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13])))∧(i824[12]* i824[13])∧(java.lang.Object(ARRAY(i2[12], a4262data[12])) →* java.lang.Object(ARRAY(i2[13], a4262data[13])))∧(i826[12]* i826[13]))

(13) -> (3), if ((java.lang.Object(ARRAY(i2[13], a4262data[13])) →* java.lang.Object(ARRAY(i2[3], a4262data[3])))∧(i824[13] + 1* i843[3])∧(i826[13]* i826[3]))

The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (29) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (30) Obligation:

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

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
(1): LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(5): LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
(6): COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6] + 1, i826[6])
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(8): LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
(9): LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(12): LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))
(13): COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13] + 1, i826[13])

(0) -> (1), if ((i824[0]* i824[1])∧((i2[0]* i2[1])∧(a4262data[0]* a4262data[1]))∧(i826[0]* i826[1]))

(1) -> (2), if ((i826[1]* i826[2])∧(i824[1]* i824[2])∧(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0* TRUE)∧((i2[1]* i2[2])∧(a4262data[1]* a4262data[2])))

(2) -> (7), if (((i2[2]* i2[7])∧(a4262data[2]* a4262data[7]))∧(i824[2] + 1* i843[7])∧(i826[2]* i826[7]))

(3) -> (7), if ((i843[3]* i843[7])∧((i2[3]* i2[7])∧(a4262data[3]* a4262data[7]))∧(i826[3]* i826[7]))

(4) -> (5), if (((i901[4]* i901[5])∧(i862[4]* i862[5])∧(i864[4]* i864[5])∧(a4416[4]* a4416[5]))∧(i824[4]* i824[5])∧((i2[4]* i2[5])∧(a4262data[4]* a4262data[5]))∧(i826[4]* i826[5]))

(5) -> (6), if ((i826[5]* i826[6])∧((i901[5]* i901[6])∧(i862[5]* i862[6])∧(i864[5]* i864[6])∧(a4416[5]* a4416[6]))∧(i824[5]* i824[6])∧((i2[5]* i2[6])∧(a4262data[5]* a4262data[6]))∧(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0* TRUE))

(6) -> (7), if ((i826[6]* i826[7])∧(i824[6] + 1* i843[7])∧((i2[6]* i2[7])∧(a4262data[6]* a4262data[7])))

(7) -> (0), if ((i826[7] + -1* i826[0])∧((i2[7]* i2[0])∧(a4262data[7]* a4262data[0]))∧(i843[7]* i824[0]))

(7) -> (4), if ((i843[7]* i824[4])∧(i826[7] + -1* i826[4])∧((i2[7]* i2[4])∧(a4262data[7]* a4262data[4])))

(7) -> (8), if ((i826[7] + -1* i826[8])∧((i2[7]* i2[8])∧(a4262data[7]* a4262data[8]))∧(i843[7]* i824[8]))

(7) -> (11), if ((i843[7]* i824[11])∧((i2[7]* i2[11])∧(a4262data[7]* a4262data[11]))∧(i826[7] + -1* i826[11]))

(8) -> (9), if (((i2[8]* i2[9])∧(a4262data[8]* a4262data[9]))∧(i826[8]* i826[9])∧(i824[8]* i824[9]))

(9) -> (10), if ((i826[9]* i826[10])∧(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0* TRUE)∧(i824[9]* i824[10])∧((i2[9]* i2[10])∧(a4262data[9]* a4262data[10])))

(10) -> (0), if (((i2[10]* i2[0])∧(a4262data[10]* a4262data[0]))∧(i824[10] + 1* i824[0])∧(i826[10] + -1* i826[0]))

(10) -> (4), if ((i824[10] + 1* i824[4])∧((i2[10]* i2[4])∧(a4262data[10]* a4262data[4]))∧(i826[10] + -1* i826[4]))

(10) -> (8), if ((i824[10] + 1* i824[8])∧((i2[10]* i2[8])∧(a4262data[10]* a4262data[8]))∧(i826[10] + -1* i826[8]))

(10) -> (11), if ((i826[10] + -1* i826[11])∧((i2[10]* i2[11])∧(a4262data[10]* a4262data[11]))∧(i824[10] + 1* i824[11]))

(11) -> (12), if ((i824[11]* i824[12])∧((i2[11]* i2[12])∧(a4262data[11]* a4262data[12]))∧(i826[11]* i826[12])∧((i901[11]* i901[12])∧(i862[11]* i862[12])∧(i864[11]* i864[12])∧(a4416[11]* a4416[12])))

(12) -> (13), if ((i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0* TRUE)∧((i901[12]* i901[13])∧(i862[12]* i862[13])∧(i864[12]* i864[13])∧(a4416[12]* a4416[13]))∧(i824[12]* i824[13])∧((i2[12]* i2[13])∧(a4262data[12]* a4262data[13]))∧(i826[12]* i826[13]))

(13) -> (3), if (((i2[13]* i2[3])∧(a4262data[13]* a4262data[3]))∧(i824[13] + 1* i843[3])∧(i826[13]* i826[3]))

The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (31) 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 LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) the following chains were created:
• We consider the chain LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]), LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) which results in the following constraint:

(1)    (i824[0]=i824[1]i2[0]=i2[1]a4262data[0]=a4262data[1]i826[0]=i826[1]LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])≥NonInfC∧LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])≥LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])∧(UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥))

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

(2)    (LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])≥NonInfC∧LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])≥LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])∧(UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥))

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

(3)    ((UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥)∧[1 + (-1)bso_31] ≥ 0)

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

(4)    ((UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥)∧[1 + (-1)bso_31] ≥ 0)

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

(5)    ((UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥)∧[1 + (-1)bso_31] ≥ 0)

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

(6)    ((UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

For Pair LOAD9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → COND_LOAD9325ARR1(&&(&&(&&(>(i824, 0), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826) the following chains were created:
• We consider the chain LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]), COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2]) which results in the following constraint:

(7)    (i826[1]=i826[2]i824[1]=i824[2]&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0))=TRUEi2[1]=i2[2]a4262data[1]=a4262data[2]LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])≥NonInfC∧LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])≥COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])∧(UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥))

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

(8)    (>(+(i824[1], 1), 0)=TRUE>(i826[1], 0)=TRUE>(i824[1], 0)=TRUE<(i824[1], i2[1])=TRUELOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])≥NonInfC∧LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])≥COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])∧(UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥))

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

(9)    (i824[1] ≥ 0∧i826[1] + [-1] ≥ 0∧i824[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i824[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧[(-1)Bound*bni_32] + [bni_32]i2[1] + [(-1)bni_32]i824[1] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(10)    (i824[1] ≥ 0∧i826[1] + [-1] ≥ 0∧i824[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i824[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧[(-1)Bound*bni_32] + [bni_32]i2[1] + [(-1)bni_32]i824[1] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(11)    (i824[1] ≥ 0∧i826[1] + [-1] ≥ 0∧i824[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i824[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧[(-1)Bound*bni_32] + [bni_32]i2[1] + [(-1)bni_32]i824[1] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(12)    (i824[1] ≥ 0∧i826[1] + [-1] ≥ 0∧i824[1] + [-1] ≥ 0∧i2[1] + [-1] + [-1]i824[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧0 = 0∧[(-1)Bound*bni_32] + [bni_32]i2[1] + [(-1)bni_32]i824[1] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

(13)    ([1] + i824[1] ≥ 0∧i826[1] + [-1] ≥ 0∧i824[1] ≥ 0∧i2[1] + [-2] + [-1]i824[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + (-1)bni_32] + [bni_32]i2[1] + [(-1)bni_32]i824[1] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

(14)    ([1] + i824[1] ≥ 0∧i826[1] ≥ 0∧i824[1] ≥ 0∧i2[1] + [-2] + [-1]i824[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + (-1)bni_32] + [bni_32]i2[1] + [(-1)bni_32]i824[1] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

(15)    ([1] + i824[1] ≥ 0∧i826[1] ≥ 0∧i824[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + bni_32] + [bni_32]i2[1] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → INC11229(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), i826) the following chains were created:
• We consider the chain COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2]) which results in the following constraint:

(16)    (COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2])≥NonInfC∧COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2])≥INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])∧(UIncreasing(INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])), ≥))

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

(17)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])), ≥)∧[(-1)bso_35] ≥ 0)

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

(18)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])), ≥)∧[(-1)bso_35] ≥ 0)

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

(19)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])), ≥)∧[(-1)bso_35] ≥ 0)

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

(20)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

For Pair JMP11303'(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → INC11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) the following chains were created:
• We consider the chain JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]), INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1)) which results in the following constraint:

(21)    (i843[3]=i843[7]i2[3]=i2[7]a4262data[3]=a4262data[7]i826[3]=i826[7]JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])≥NonInfC∧JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])≥INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])∧(UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥))

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

(22)    (JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])≥NonInfC∧JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])≥INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])∧(UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥))

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

(23)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥)∧[(-1)bso_37] ≥ 0)

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

(24)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥)∧[(-1)bso_37] ≥ 0)

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

(25)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥)∧[(-1)bso_37] ≥ 0)

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

(26)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

For Pair LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) the following chains were created:
• We consider the chain LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4]))) which results in the following constraint:

(27)    (LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4])≥NonInfC∧LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4])≥LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))∧(UIncreasing(LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))), ≥))

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

(28)    ((UIncreasing(LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))), ≥)∧[(-1)bso_39] ≥ 0)

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

(29)    ((UIncreasing(LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))), ≥)∧[(-1)bso_39] ≥ 0)

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

(30)    ((UIncreasing(LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))), ≥)∧[(-1)bso_39] ≥ 0)

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

(31)    ((UIncreasing(LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)

For Pair LOAD9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901, 0), >(i824, 0)), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) the following chains were created:
• We consider the chain LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))), COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6]) which results in the following constraint:

(32)    (i826[5]=i826[6]i901[5]=i901[6]i862[5]=i862[6]i864[5]=i864[6]a4416[5]=a4416[6]i824[5]=i824[6]i2[5]=i2[6]a4262data[5]=a4262data[6]&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0))=TRUELOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))≥NonInfC∧LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))≥COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))∧(UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥))

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

(33)    (>(+(i824[5], 1), 0)=TRUE>(i826[5], 0)=TRUE<(i824[5], i2[5])=TRUE>(i901[5], 0)=TRUE>(i824[5], 0)=TRUELOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))≥NonInfC∧LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))≥COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))∧(UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥))

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

(34)    (i824[5] ≥ 0∧i826[5] + [-1] ≥ 0∧i2[5] + [-1] + [-1]i824[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] + [(-1)bni_40]i824[5] ≥ 0∧[(-1)bso_41] ≥ 0)

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

(35)    (i824[5] ≥ 0∧i826[5] + [-1] ≥ 0∧i2[5] + [-1] + [-1]i824[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] + [(-1)bni_40]i824[5] ≥ 0∧[(-1)bso_41] ≥ 0)

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

(36)    (i824[5] ≥ 0∧i826[5] + [-1] ≥ 0∧i2[5] + [-1] + [-1]i824[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] + [(-1)bni_40]i824[5] ≥ 0∧[(-1)bso_41] ≥ 0)

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

(37)    (i824[5] ≥ 0∧i826[5] + [-1] ≥ 0∧i2[5] + [-1] + [-1]i824[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] + [(-1)bni_40]i824[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

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

(38)    ([1] + i824[5] ≥ 0∧i826[5] + [-1] ≥ 0∧i2[5] + [-2] + [-1]i824[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]i2[5] + [(-1)bni_40]i824[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

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

(39)    ([1] + i824[5] ≥ 0∧i826[5] ≥ 0∧i2[5] + [-2] + [-1]i824[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_40] + [bni_40]i2[5] + [(-1)bni_40]i824[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

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

(40)    ([1] + i824[5] ≥ 0∧i826[5] ≥ 0∧i2[5] ≥ 0∧i901[5] + [-1] ≥ 0∧i824[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

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

(41)    ([1] + i824[5] ≥ 0∧i826[5] ≥ 0∧i2[5] ≥ 0∧i901[5] ≥ 0∧i824[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

For Pair COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → INC11229(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), i826) the following chains were created:
• We consider the chain COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6]) which results in the following constraint:

(42)    (COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6])))≥NonInfC∧COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6])))≥INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])∧(UIncreasing(INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])), ≥))

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

(43)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])), ≥)∧[1 + (-1)bso_43] ≥ 0)

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

(44)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])), ≥)∧[1 + (-1)bso_43] ≥ 0)

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

(45)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])), ≥)∧[1 + (-1)bso_43] ≥ 0)

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

(46)    ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

For Pair INC11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i843, +(i826, -1)) the following chains were created:
• We consider the chain INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1)) which results in the following constraint:

(47)    (INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7])≥NonInfC∧INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7])≥LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))∧(UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))), ≥))

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

(48)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))), ≥)∧[(-1)bso_45] ≥ 0)

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

(49)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))), ≥)∧[(-1)bso_45] ≥ 0)

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

(50)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))), ≥)∧[(-1)bso_45] ≥ 0)

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

(51)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

For Pair LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) the following chains were created:
• We consider the chain LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]), LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) which results in the following constraint:

(52)    (i2[8]=i2[9]a4262data[8]=a4262data[9]i826[8]=i826[9]i824[8]=i824[9]LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])≥NonInfC∧LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])≥LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])∧(UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥))

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

(53)    (LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])≥NonInfC∧LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])≥LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])∧(UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥))

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

(54)    ((UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥)∧[1 + (-1)bso_47] ≥ 0)

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

(55)    ((UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥)∧[1 + (-1)bso_47] ≥ 0)

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

(56)    ((UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥)∧[1 + (-1)bso_47] ≥ 0)

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

(57)    ((UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

For Pair LOAD9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → COND_LOAD9325ARR3(&&(&&(&&(>(i824, 0), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826) the following chains were created:
• We consider the chain LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]), COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1)) which results in the following constraint:

(58)    (i826[9]=i826[10]&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0))=TRUEi824[9]=i824[10]i2[9]=i2[10]a4262data[9]=a4262data[10]LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])≥NonInfC∧LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])≥COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])∧(UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥))

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

(59)    (>(+(i824[9], 1), 0)=TRUE>(i826[9], 0)=TRUE>(i824[9], 0)=TRUE<(i824[9], i2[9])=TRUELOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])≥NonInfC∧LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])≥COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])∧(UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥))

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

(60)    (i824[9] ≥ 0∧i826[9] + [-1] ≥ 0∧i824[9] + [-1] ≥ 0∧i2[9] + [-1] + [-1]i824[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧[(-1)Bound*bni_48] + [(-1)bni_48]i824[9] + [bni_48]i2[9] ≥ 0∧[(-1)bso_49] ≥ 0)

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

(61)    (i824[9] ≥ 0∧i826[9] + [-1] ≥ 0∧i824[9] + [-1] ≥ 0∧i2[9] + [-1] + [-1]i824[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧[(-1)Bound*bni_48] + [(-1)bni_48]i824[9] + [bni_48]i2[9] ≥ 0∧[(-1)bso_49] ≥ 0)

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

(62)    (i824[9] ≥ 0∧i826[9] + [-1] ≥ 0∧i824[9] + [-1] ≥ 0∧i2[9] + [-1] + [-1]i824[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧[(-1)Bound*bni_48] + [(-1)bni_48]i824[9] + [bni_48]i2[9] ≥ 0∧[(-1)bso_49] ≥ 0)

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

(63)    (i824[9] ≥ 0∧i826[9] + [-1] ≥ 0∧i824[9] + [-1] ≥ 0∧i2[9] + [-1] + [-1]i824[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧0 = 0∧[(-1)Bound*bni_48] + [(-1)bni_48]i824[9] + [bni_48]i2[9] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)

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

(64)    ([1] + i824[9] ≥ 0∧i826[9] + [-1] ≥ 0∧i824[9] ≥ 0∧i2[9] + [-2] + [-1]i824[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧0 = 0∧[(-1)Bound*bni_48 + (-1)bni_48] + [(-1)bni_48]i824[9] + [bni_48]i2[9] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)

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

(65)    ([1] + i824[9] ≥ 0∧i826[9] ≥ 0∧i824[9] ≥ 0∧i2[9] + [-2] + [-1]i824[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧0 = 0∧[(-1)Bound*bni_48 + (-1)bni_48] + [(-1)bni_48]i824[9] + [bni_48]i2[9] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)

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

(66)    ([1] + i824[9] ≥ 0∧i826[9] ≥ 0∧i824[9] ≥ 0∧i2[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧0 = 0∧[(-1)Bound*bni_48 + bni_48] + [bni_48]i2[9] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)

For Pair COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), +(i826, -1)) the following chains were created:
• We consider the chain COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1)) which results in the following constraint:

(67)    (COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10])≥NonInfC∧COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10])≥LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))∧(UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))), ≥))

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

(68)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))), ≥)∧[(-1)bso_51] ≥ 0)

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

(69)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))), ≥)∧[(-1)bso_51] ≥ 0)

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

(70)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))), ≥)∧[(-1)bso_51] ≥ 0)

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

(71)    ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

For Pair LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) the following chains were created:
• We consider the chain LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11]))) which results in the following constraint:

(72)    (LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11])≥NonInfC∧LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11])≥LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))∧(UIncreasing(LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))), ≥))

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

(73)    ((UIncreasing(LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))), ≥)∧[(-1)bso_53] ≥ 0)

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

(74)    ((UIncreasing(LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))), ≥)∧[(-1)bso_53] ≥ 0)

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

(75)    ((UIncreasing(LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))), ≥)∧[(-1)bso_53] ≥ 0)

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

(76)    ((UIncreasing(LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

For Pair LOAD9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901, 0), >(i824, 0)), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) the following chains were created:
• We consider the chain LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))), COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13]) which results in the following constraint:

(77)    (&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0))=TRUEi901[12]=i901[13]i862[12]=i862[13]i864[12]=i864[13]a4416[12]=a4416[13]i824[12]=i824[13]i2[12]=i2[13]a4262data[12]=a4262data[13]i826[12]=i826[13]LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))≥NonInfC∧LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))≥COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))∧(UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥))

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

(78)    (>(+(i824[12], 1), 0)=TRUE>(i826[12], 0)=TRUE<(i824[12], i2[12])=TRUE>(i901[12], 0)=TRUE>(i824[12], 0)=TRUELOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))≥NonInfC∧LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))≥COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))∧(UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥))

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

(79)    (i824[12] ≥ 0∧i826[12] + [-1] ≥ 0∧i2[12] + [-1] + [-1]i824[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧[bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i824[12] + [bni_54]i2[12] ≥ 0∧[(-1)bso_55] ≥ 0)

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

(80)    (i824[12] ≥ 0∧i826[12] + [-1] ≥ 0∧i2[12] + [-1] + [-1]i824[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧[bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i824[12] + [bni_54]i2[12] ≥ 0∧[(-1)bso_55] ≥ 0)

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

(81)    (i824[12] ≥ 0∧i826[12] + [-1] ≥ 0∧i2[12] + [-1] + [-1]i824[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧[bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i824[12] + [bni_54]i2[12] ≥ 0∧[(-1)bso_55] ≥ 0)

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

(82)    (i824[12] ≥ 0∧i826[12] + [-1] ≥ 0∧i2[12] + [-1] + [-1]i824[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[bni_54 + (-1)Bound*bni_54] + [(-1)bni_54]i824[12] + [bni_54]i2[12] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

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

(83)    ([1] + i824[12] ≥ 0∧i826[12] + [-1] ≥ 0∧i2[12] + [-2] + [-1]i824[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_54] + [(-1)bni_54]i824[12] + [bni_54]i2[12] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

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

(84)    ([1] + i824[12] ≥ 0∧i826[12] ≥ 0∧i2[12] + [-2] + [-1]i824[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_54] + [(-1)bni_54]i824[12] + [bni_54]i2[12] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

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

(85)    ([1] + i824[12] ≥ 0∧i826[12] ≥ 0∧i2[12] ≥ 0∧i901[12] + [-1] ≥ 0∧i824[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_54 + (2)bni_54] + [bni_54]i2[12] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

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

(86)    ([1] + i824[12] ≥ 0∧i826[12] ≥ 0∧i2[12] ≥ 0∧i901[12] ≥ 0∧i824[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_54 + (2)bni_54] + [bni_54]i2[12] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

For Pair COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303'(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), i826) the following chains were created:
• We consider the chain COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13]) which results in the following constraint:

(87)    (COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13])))≥NonInfC∧COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13])))≥JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])∧(UIncreasing(JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])), ≥))

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

(88)    ((UIncreasing(JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])), ≥)∧[1 + (-1)bso_57] ≥ 0)

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

(89)    ((UIncreasing(JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])), ≥)∧[1 + (-1)bso_57] ≥ 0)

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

(90)    ((UIncreasing(JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])), ≥)∧[1 + (-1)bso_57] ≥ 0)

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

(91)    ((UIncreasing(JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_57] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
• ((UIncreasing(LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_31] ≥ 0)

• LOAD9325ARR1(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → COND_LOAD9325ARR1(&&(&&(&&(>(i824, 0), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
• ([1] + i824[1] ≥ 0∧i826[1] ≥ 0∧i824[1] ≥ 0∧i2[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])), ≥)∧0 = 0∧[(-1)Bound*bni_32 + bni_32] + [bni_32]i2[1] ≥ 0∧0 = 0∧[(-1)bso_33] ≥ 0)

• COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → INC11229(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), i826)
• ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

• JMP11303'(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → INC11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826)
• ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

• LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
• ((UIncreasing(LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)

• LOAD9325ARR2(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901, 0), >(i824, 0)), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
• ([1] + i824[5] ≥ 0∧i826[5] ≥ 0∧i2[5] ≥ 0∧i901[5] ≥ 0∧i824[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_40 + (-1)Bound*bni_40] + [bni_40]i2[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

• COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → INC11229(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), i826)
• ((UIncreasing(INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_43] ≥ 0)

• INC11229(java.lang.Object(ARRAY(i2, a4262data)), i843, i826) → LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i843, +(i826, -1))
• ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

• LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
• ((UIncreasing(LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_47] ≥ 0)

• LOAD9325ARR3(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → COND_LOAD9325ARR3(&&(&&(&&(>(i824, 0), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826)
• ([1] + i824[9] ≥ 0∧i826[9] ≥ 0∧i824[9] ≥ 0∧i2[9] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])), ≥)∧0 = 0∧[(-1)Bound*bni_48 + bni_48] + [bni_48]i2[9] ≥ 0∧0 = 0∧[(-1)bso_49] ≥ 0)

• COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), +(i826, -1))
• ((UIncreasing(LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

• LOAD9325(java.lang.Object(ARRAY(i2, a4262data)), i824, i826) → LOAD9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
• ((UIncreasing(LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_53] ≥ 0)

• LOAD9325ARR5(java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901, 0), >(i824, 0)), <(i824, i2)), >(i826, 0)), >(+(i824, 1), 0)), java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416)))
• ([1] + i824[12] ≥ 0∧i826[12] ≥ 0∧i2[12] ≥ 0∧i901[12] ≥ 0∧i824[12] ≥ 0 ⇒ (UIncreasing(COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)Bound*bni_54 + (2)bni_54] + [bni_54]i2[12] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_55] ≥ 0)

• COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2, a4262data)), i824, i826, java.lang.Object(java.lang.String(i901, i862, i864, a4416))) → JMP11303'(java.lang.Object(ARRAY(i2, a4262data)), +(i824, 1), i826)
• ((UIncreasing(JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_57] ≥ 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(LOAD9325(x1, x2, x3)) = [-1]x1 + [-1]x2
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1] + [-1]x1
POL(LOAD9325ARR1(x1, x2, x3)) = [-1] + [-1]x1 + [-1]x2
POL(COND_LOAD9325ARR1(x1, x2, x3, x4)) = [-1] + [-1]x2 + [-1]x3
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(INC11229(x1, x2, x3)) = [-1]x2 + [-1]x1
POL(JMP11303'(x1, x2, x3)) = [-1]x2 + [-1]x1
POL(LOAD9325ARR2(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x1 + [-1]x2
POL(java.lang.String(x1, x2, x3, x4)) = [-1]
POL(COND_LOAD9325ARR2(x1, x2, x3, x4, x5)) = [-1] + [-1]x5 + [-1]x2 + [-1]x3
POL(-1) = [-1]
POL(LOAD9325ARR3(x1, x2, x3)) = [-1] + [-1]x2 + [-1]x1
POL(COND_LOAD9325ARR3(x1, x2, x3, x4)) = [-1] + [-1]x3 + [-1]x2
POL(LOAD9325ARR5(x1, x2, x3, x4)) = [-1] + [-1]x4 + [-1]x2 + [-1]x1
POL(COND_LOAD9325ARR5(x1, x2, x3, x4, x5)) = [-1] + [-1]x5 + [-1]x3 + [-1]x2

The following pairs are in P>:

LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), +(i824[6], 1), i826[6])
LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), +(i824[13], 1), i826[13])

The following pairs are in Pbound:

LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))

The following pairs are in P:

LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(&&(&&(&&(>(i824[1], 0), <(i824[1], i2[1])), >(i826[1], 0)), >(+(i824[1], 1), 0)), java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), +(i824[2], 1), i826[2])
JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(&&(&&(&&(&&(>(i901[5], 0), >(i824[5], 0)), <(i824[5], i2[5])), >(i826[5], 0)), >(+(i824[5], 1), 0)), java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], +(i826[7], -1))
LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(&&(&&(&&(>(i824[9], 0), <(i824[9], i2[9])), >(i826[9], 0)), >(+(i824[9], 1), 0)), java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), +(i824[10], 1), +(i826[10], -1))
LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(&&(&&(&&(&&(>(i901[12], 0), >(i824[12], 0)), <(i824[12], i2[12])), >(i826[12], 0)), >(+(i824[12], 1), 0)), java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))

There are no usable rules.

### (33) 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:
(1): LOAD9325ARR1(java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1]) → COND_LOAD9325ARR1(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0, java.lang.Object(ARRAY(i2[1], a4262data[1])), i824[1], i826[1])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(5): LOAD9325ARR2(java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5]))) → COND_LOAD9325ARR2(i901[5] > 0 && i824[5] > 0 && i824[5] < i2[5] && i826[5] > 0 && i824[5] + 1 > 0, java.lang.Object(ARRAY(i2[5], a4262data[5])), i824[5], i826[5], java.lang.Object(java.lang.String(i901[5], i862[5], i864[5], a4416[5])))
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(9): LOAD9325ARR3(java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9]) → COND_LOAD9325ARR3(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0, java.lang.Object(ARRAY(i2[9], a4262data[9])), i824[9], i826[9])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(12): LOAD9325ARR5(java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12]))) → COND_LOAD9325ARR5(i901[12] > 0 && i824[12] > 0 && i824[12] < i2[12] && i826[12] > 0 && i824[12] + 1 > 0, java.lang.Object(ARRAY(i2[12], a4262data[12])), i824[12], i826[12], java.lang.Object(java.lang.String(i901[12], i862[12], i864[12], a4416[12])))

(1) -> (2), if ((i826[1]* i826[2])∧(i824[1]* i824[2])∧(i824[1] > 0 && i824[1] < i2[1] && i826[1] > 0 && i824[1] + 1 > 0* TRUE)∧((i2[1]* i2[2])∧(a4262data[1]* a4262data[2])))

(7) -> (4), if ((i843[7]* i824[4])∧(i826[7] + -1* i826[4])∧((i2[7]* i2[4])∧(a4262data[7]* a4262data[4])))

(10) -> (4), if ((i824[10] + 1* i824[4])∧((i2[10]* i2[4])∧(a4262data[10]* a4262data[4]))∧(i826[10] + -1* i826[4]))

(4) -> (5), if (((i901[4]* i901[5])∧(i862[4]* i862[5])∧(i864[4]* i864[5])∧(a4416[4]* a4416[5]))∧(i824[4]* i824[5])∧((i2[4]* i2[5])∧(a4262data[4]* a4262data[5]))∧(i826[4]* i826[5]))

(2) -> (7), if (((i2[2]* i2[7])∧(a4262data[2]* a4262data[7]))∧(i824[2] + 1* i843[7])∧(i826[2]* i826[7]))

(3) -> (7), if ((i843[3]* i843[7])∧((i2[3]* i2[7])∧(a4262data[3]* a4262data[7]))∧(i826[3]* i826[7]))

(9) -> (10), if ((i826[9]* i826[10])∧(i824[9] > 0 && i824[9] < i2[9] && i826[9] > 0 && i824[9] + 1 > 0* TRUE)∧(i824[9]* i824[10])∧((i2[9]* i2[10])∧(a4262data[9]* a4262data[10])))

(7) -> (11), if ((i843[7]* i824[11])∧((i2[7]* i2[11])∧(a4262data[7]* a4262data[11]))∧(i826[7] + -1* i826[11]))

(10) -> (11), if ((i826[10] + -1* i826[11])∧((i2[10]* i2[11])∧(a4262data[10]* a4262data[11]))∧(i824[10] + 1* i824[11]))

(11) -> (12), if ((i824[11]* i824[12])∧((i2[11]* i2[12])∧(a4262data[11]* a4262data[12]))∧(i826[11]* i826[12])∧((i901[11]* i901[12])∧(i862[11]* i862[12])∧(i864[11]* i864[12])∧(a4416[11]* a4416[12])))

The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (34) IDependencyGraphProof (EQUIVALENT transformation)

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

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

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD9325(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0]) → LOAD9325ARR1(java.lang.Object(ARRAY(i2[0], a4262data[0])), i824[0], i826[0])
(2): COND_LOAD9325ARR1(TRUE, java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2], i826[2]) → INC11229(java.lang.Object(ARRAY(i2[2], a4262data[2])), i824[2] + 1, i826[2])
(3): JMP11303'(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3]) → INC11229(java.lang.Object(ARRAY(i2[3], a4262data[3])), i843[3], i826[3])
(4): LOAD9325(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4]) → LOAD9325ARR2(java.lang.Object(ARRAY(i2[4], a4262data[4])), i824[4], i826[4], java.lang.Object(java.lang.String(i901[4], i862[4], i864[4], a4416[4])))
(6): COND_LOAD9325ARR2(TRUE, java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6], i826[6], java.lang.Object(java.lang.String(i901[6], i862[6], i864[6], a4416[6]))) → INC11229(java.lang.Object(ARRAY(i2[6], a4262data[6])), i824[6] + 1, i826[6])
(7): INC11229(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7]) → LOAD9325(java.lang.Object(ARRAY(i2[7], a4262data[7])), i843[7], i826[7] + -1)
(8): LOAD9325(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8]) → LOAD9325ARR3(java.lang.Object(ARRAY(i2[8], a4262data[8])), i824[8], i826[8])
(10): COND_LOAD9325ARR3(TRUE, java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10], i826[10]) → LOAD9325(java.lang.Object(ARRAY(i2[10], a4262data[10])), i824[10] + 1, i826[10] + -1)
(11): LOAD9325(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11]) → LOAD9325ARR5(java.lang.Object(ARRAY(i2[11], a4262data[11])), i824[11], i826[11], java.lang.Object(java.lang.String(i901[11], i862[11], i864[11], a4416[11])))
(13): COND_LOAD9325ARR5(TRUE, java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13], i826[13], java.lang.Object(java.lang.String(i901[13], i862[13], i864[13], a4416[13]))) → JMP11303'(java.lang.Object(ARRAY(i2[13], a4262data[13])), i824[13] + 1, i826[13])

(7) -> (0), if ((i826[7] + -1* i826[0])∧((i2[7]* i2[0])∧(a4262data[7]* a4262data[0]))∧(i843[7]* i824[0]))

(10) -> (0), if (((i2[10]* i2[0])∧(a4262data[10]* a4262data[0]))∧(i824[10] + 1* i824[0])∧(i826[10] + -1* i826[0]))

(13) -> (3), if (((i2[13]* i2[3])∧(a4262data[13]* a4262data[3]))∧(i824[13] + 1* i843[3])∧(i826[13]* i826[3]))

(7) -> (4), if ((i843[7]* i824[4])∧(i826[7] + -1* i826[4])∧((i2[7]* i2[4])∧(a4262data[7]* a4262data[4])))

(10) -> (4), if ((i824[10] + 1* i824[4])∧((i2[10]* i2[4])∧(a4262data[10]* a4262data[4]))∧(i826[10] + -1* i826[4]))

(2) -> (7), if (((i2[2]* i2[7])∧(a4262data[2]* a4262data[7]))∧(i824[2] + 1* i843[7])∧(i826[2]* i826[7]))

(3) -> (7), if ((i843[3]* i843[7])∧((i2[3]* i2[7])∧(a4262data[3]* a4262data[7]))∧(i826[3]* i826[7]))

(6) -> (7), if ((i826[6]* i826[7])∧(i824[6] + 1* i843[7])∧((i2[6]* i2[7])∧(a4262data[6]* a4262data[7])))

(7) -> (8), if ((i826[7] + -1* i826[8])∧((i2[7]* i2[8])∧(a4262data[7]* a4262data[8]))∧(i843[7]* i824[8]))

(10) -> (8), if ((i824[10] + 1* i824[8])∧((i2[10]* i2[8])∧(a4262data[10]* a4262data[8]))∧(i826[10] + -1* i826[8]))

(7) -> (11), if ((i843[7]* i824[11])∧((i2[7]* i2[11])∧(a4262data[7]* a4262data[11]))∧(i826[7] + -1* i826[11]))

(10) -> (11), if ((i826[10] + -1* i826[11])∧((i2[10]* i2[11])∧(a4262data[10]* a4262data[11]))∧(i824[10] + 1* i824[11]))

The set Q consists of the following terms:
Load9325(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
JMP11303(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR2(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Inc11229(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR3(java.lang.Object(ARRAY(x0, x1)), x2, x3)
Cond_Load9325ARR3(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3)
Load9325ARR5(java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))
Cond_Load9325ARR5(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, java.lang.Object(java.lang.String(x4, x5, x6, x7)))

### (37) IDependencyGraphProof (EQUIVALENT transformation)

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