### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: CountMetaList
`public class CountMetaList {	public static void main(String[] args) {		Random.args = args;		List l = createMetaList();		int count = countMetaList(l);	}	public static int countMetaList(List cur) {		int res = 0;		while (cur != null) {			if (cur.value instanceof List) {				List inner = (List) cur.value;				cur.value = inner.next;				cur = new List(inner.value, cur);			}			cur = cur.next;			res++;		}		return res;	}	public static List createMetaList() {		int count = Random.random();		List cur = null;		for (int i = 0; i < count; i++) {			int innerCount = Random.random();			List innerList = null;			for (int j = innerCount; j > 0; j--) {				innerList = new List(null, innerList);			}			cur = new List(innerList, cur);		}		return cur;	}}class List {	Object value;	List next;	public List(Object v, List n) {		this.value = v;		this.next = n;	}}public class Random {  static String[] args;  static int index = 0;  public static int random() {    String string = args[index];    index++;    return string.length();  }}`

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
Graph of 355 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:
Load2486(o2217, java.lang.Object(List(java.lang.Object(List(o4531, o4532)), o2493)), i128) → Inc4194(o2217new, java.lang.Object(List(o4532, o2493)), i128)
Load2486(o2217, java.lang.Object(List(java.lang.Object(o2641Sub1234), o2493)), i128) → Inc4194(o2217, o2493, i128)
Load2486(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), i128) → Inc4194(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), o2498, i128)
Load2486(java.lang.Object(List(NULL, o2498)), java.lang.Object(List(NULL, o2498)), i128) → Inc4194(java.lang.Object(List(NULL, o2498)), o2498, i128)
Inc4194(o2217, o2493, i128) → Load2486(o2217, o2493, i128 + 1)
Load2486(java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), i128) → Load2486(java.lang.Object(List(o4550, o2498)), java.lang.Object(List(o4550, o2498)), i128 + 1)
The set Q consists of the following terms:
Inc4194(x0, x1, x2)

### (7) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
Load2486(o2217, java.lang.Object(List(java.lang.Object(List(o4531, o4532)), o2493)), i128) → Inc4194(o2217new, java.lang.Object(List(o4532, o2493)), i128)
Load2486(o2217, java.lang.Object(List(java.lang.Object(o2641Sub1234), o2493)), i128) → Inc4194(o2217, o2493, i128)
Load2486(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), i128) → Inc4194(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), o2498, i128)
Load2486(java.lang.Object(List(NULL, o2498)), java.lang.Object(List(NULL, o2498)), i128) → Inc4194(java.lang.Object(List(NULL, o2498)), o2498, i128)
Inc4194(o2217, o2493, i128) → Load2486(o2217, o2493, i128 + 1)
Load2486(java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), i128) → Load2486(java.lang.Object(List(o4550, o2498)), java.lang.Object(List(o4550, o2498)), i128 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
(1): LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
(2): LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
(3): LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
(4): INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], i128[4] + 1)
(6): LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), i128[6] + 1)

(0) -> (4), if ((java.lang.Object(List(o4532[0], o2493[0])) →* o2493[4])∧(i128[0]* i128[4])∧(o2217new[0]* o2217[4]))

(1) -> (4), if ((o2493[1]* o2493[4])∧(i128[1]* i128[4])∧(o2217[1]* o2217[4]))

(2) -> (4), if ((java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])) →* o2217[4])∧(i128[2]* i128[4])∧(o2498[2]* o2493[4]))

(3) -> (4), if ((o2498[3]* o2493[4])∧(i128[3]* i128[4])∧(java.lang.Object(List(NULL, o2498[3])) →* o2217[4]))

(4) -> (0), if ((i128[4] + 1* i128[0])∧(o2493[4]* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[4]* o2217[0]))

(4) -> (1), if ((o2217[4]* o2217[1])∧(i128[4] + 1* i128[1])∧(o2493[4]* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1]))))

(4) -> (2), if ((o2493[4]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[4] + 1* i128[2])∧(o2217[4]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))))

(4) -> (3), if ((i128[4] + 1* i128[3])∧(o2217[4]* java.lang.Object(List(NULL, o2498[3])))∧(o2493[4]* java.lang.Object(List(NULL, o2498[3]))))

(4) -> (5), if ((o2493[4]* java.lang.Object(List(NULL, o2493[5])))∧(i128[4] + 1* i128[5])∧(o2217[4]* o2217[5]))

(4) -> (6), if ((i128[4] + 1* i128[6])∧(o2493[4]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(o2217[4]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(5) -> (0), if ((o2493[5]* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[5]* o2217[0])∧(i128[5] + 1* i128[0]))

(5) -> (1), if ((o2493[5]* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(o2217[5]* o2217[1])∧(i128[5] + 1* i128[1]))

(5) -> (2), if ((o2493[5]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(o2217[5]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[5] + 1* i128[2]))

(5) -> (3), if ((o2493[5]* java.lang.Object(List(NULL, o2498[3])))∧(o2217[5]* java.lang.Object(List(NULL, o2498[3])))∧(i128[5] + 1* i128[3]))

(5) -> (5), if ((i128[5] + 1* i128[5]')∧(o2493[5]* java.lang.Object(List(NULL, o2493[5]')))∧(o2217[5]* o2217[5]'))

(5) -> (6), if ((o2217[5]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(i128[5] + 1* i128[6])∧(o2493[5]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(6) -> (0), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(i128[6] + 1* i128[0])∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[0]))

(6) -> (1), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(i128[6] + 1* i128[1])∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[1]))

(6) -> (2), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[6] + 1* i128[2]))

(6) -> (3), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(NULL, o2498[3])))∧(i128[6] + 1* i128[3]))

(6) -> (5), if ((i128[6] + 1* i128[5])∧(java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(NULL, o2493[5])))∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[5]))

(6) -> (6), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(List(o4549[6]', o4550[6]')), o2498[6]')))∧(i128[6] + 1* i128[6]'))

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

### (8) UsableRulesProof (EQUIVALENT transformation)

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

### (9) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
(1): LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
(2): LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
(3): LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
(4): INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], i128[4] + 1)
(6): LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), i128[6] + 1)

(0) -> (4), if ((java.lang.Object(List(o4532[0], o2493[0])) →* o2493[4])∧(i128[0]* i128[4])∧(o2217new[0]* o2217[4]))

(1) -> (4), if ((o2493[1]* o2493[4])∧(i128[1]* i128[4])∧(o2217[1]* o2217[4]))

(2) -> (4), if ((java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])) →* o2217[4])∧(i128[2]* i128[4])∧(o2498[2]* o2493[4]))

(3) -> (4), if ((o2498[3]* o2493[4])∧(i128[3]* i128[4])∧(java.lang.Object(List(NULL, o2498[3])) →* o2217[4]))

(4) -> (0), if ((i128[4] + 1* i128[0])∧(o2493[4]* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[4]* o2217[0]))

(4) -> (1), if ((o2217[4]* o2217[1])∧(i128[4] + 1* i128[1])∧(o2493[4]* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1]))))

(4) -> (2), if ((o2493[4]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[4] + 1* i128[2])∧(o2217[4]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))))

(4) -> (3), if ((i128[4] + 1* i128[3])∧(o2217[4]* java.lang.Object(List(NULL, o2498[3])))∧(o2493[4]* java.lang.Object(List(NULL, o2498[3]))))

(4) -> (5), if ((o2493[4]* java.lang.Object(List(NULL, o2493[5])))∧(i128[4] + 1* i128[5])∧(o2217[4]* o2217[5]))

(4) -> (6), if ((i128[4] + 1* i128[6])∧(o2493[4]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(o2217[4]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(5) -> (0), if ((o2493[5]* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[5]* o2217[0])∧(i128[5] + 1* i128[0]))

(5) -> (1), if ((o2493[5]* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(o2217[5]* o2217[1])∧(i128[5] + 1* i128[1]))

(5) -> (2), if ((o2493[5]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(o2217[5]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[5] + 1* i128[2]))

(5) -> (3), if ((o2493[5]* java.lang.Object(List(NULL, o2498[3])))∧(o2217[5]* java.lang.Object(List(NULL, o2498[3])))∧(i128[5] + 1* i128[3]))

(5) -> (5), if ((i128[5] + 1* i128[5]')∧(o2493[5]* java.lang.Object(List(NULL, o2493[5]')))∧(o2217[5]* o2217[5]'))

(5) -> (6), if ((o2217[5]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(i128[5] + 1* i128[6])∧(o2493[5]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(6) -> (0), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(i128[6] + 1* i128[0])∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[0]))

(6) -> (1), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(i128[6] + 1* i128[1])∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[1]))

(6) -> (2), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[6] + 1* i128[2]))

(6) -> (3), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(NULL, o2498[3])))∧(i128[6] + 1* i128[3]))

(6) -> (5), if ((i128[6] + 1* i128[5])∧(java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(NULL, o2493[5])))∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[5]))

(6) -> (6), if ((java.lang.Object(List(o4550[6], o2498[6])) →* java.lang.Object(List(java.lang.Object(List(o4549[6]', o4550[6]')), o2498[6]')))∧(i128[6] + 1* i128[6]'))

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

### (10) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (11) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
(1): LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
(2): LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
(3): LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
(4): INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], i128[4] + 1)
(6): LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), i128[6] + 1)

(0) -> (4), if ((java.lang.Object(List(o4532[0], o2493[0])) →* o2493[4])∧(i128[0]* i128[4])∧(o2217new[0]* o2217[4]))

(1) -> (4), if ((o2493[1]* o2493[4])∧(i128[1]* i128[4])∧(o2217[1]* o2217[4]))

(2) -> (4), if ((java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])) →* o2217[4])∧(i128[2]* i128[4])∧(o2498[2]* o2493[4]))

(3) -> (4), if ((o2498[3]* o2493[4])∧(i128[3]* i128[4])∧(java.lang.Object(List(NULL, o2498[3])) →* o2217[4]))

(4) -> (0), if ((i128[4] + 1* i128[0])∧(o2493[4]* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[4]* o2217[0]))

(4) -> (1), if ((o2217[4]* o2217[1])∧(i128[4] + 1* i128[1])∧(o2493[4]* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1]))))

(4) -> (2), if ((o2493[4]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[4] + 1* i128[2])∧(o2217[4]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))))

(4) -> (3), if ((i128[4] + 1* i128[3])∧(o2217[4]* java.lang.Object(List(NULL, o2498[3])))∧(o2493[4]* java.lang.Object(List(NULL, o2498[3]))))

(4) -> (5), if ((o2493[4]* java.lang.Object(List(NULL, o2493[5])))∧(i128[4] + 1* i128[5])∧(o2217[4]* o2217[5]))

(4) -> (6), if ((i128[4] + 1* i128[6])∧(o2493[4]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(o2217[4]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(5) -> (0), if ((o2493[5]* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[5]* o2217[0])∧(i128[5] + 1* i128[0]))

(5) -> (1), if ((o2493[5]* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(o2217[5]* o2217[1])∧(i128[5] + 1* i128[1]))

(5) -> (2), if ((o2493[5]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(o2217[5]* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[5] + 1* i128[2]))

(5) -> (3), if ((o2493[5]* java.lang.Object(List(NULL, o2498[3])))∧(o2217[5]* java.lang.Object(List(NULL, o2498[3])))∧(i128[5] + 1* i128[3]))

(5) -> (5), if ((i128[5] + 1* i128[5]')∧(o2493[5]* java.lang.Object(List(NULL, o2493[5]')))∧(o2217[5]* o2217[5]'))

(5) -> (6), if ((o2217[5]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(i128[5] + 1* i128[6])∧(o2493[5]* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(6) -> (0), if (((o4550[6]* java.lang.Object(List(o4531[0], o4532[0])))∧(o2498[6]* o2493[0]))∧(i128[6] + 1* i128[0])∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[0]))

(6) -> (1), if (((o4550[6]* java.lang.Object(o2641Sub1234[1]))∧(o2498[6]* o2493[1]))∧(i128[6] + 1* i128[1])∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[1]))

(6) -> (2), if (((o4550[6]* java.lang.Object(o2824Sub1234[2]))∧(o2498[6]* o2498[2]))∧(i128[6] + 1* i128[2]))

(6) -> (3), if (((o4550[6]* NULL)∧(o2498[6]* o2498[3]))∧(i128[6] + 1* i128[3]))

(6) -> (5), if ((i128[6] + 1* i128[5])∧((o4550[6]* NULL)∧(o2498[6]* o2493[5]))∧(java.lang.Object(List(o4550[6], o2498[6])) →* o2217[5]))

(6) -> (6), if (((o4550[6]* java.lang.Object(List(o4549[6]', o4550[6]')))∧(o2498[6]* o2498[6]'))∧(i128[6] + 1* i128[6]'))

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

### (12) IDPNonInfProof (SOUND transformation)

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

For Pair LOAD2486(o2217, java.lang.Object(List(java.lang.Object(List(o4531, o4532)), o2493)), i128) → INC4194(o2217new, java.lang.Object(List(o4532, o2493)), i128) the following chains were created:
• We consider the chain INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)), LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(1)    (+(i128[4], 1)=i128[0]o2493[4]=java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0]))∧o2217[4]=o2217[0]java.lang.Object(List(o4532[0], o2493[0]))=o2493[4]1i128[0]=i128[4]1o2217new[0]=o2217[4]1LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0])≥INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])∧(UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥))

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

(2)    (LOAD2486(o2217[4], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), +(i128[4], 1))≥INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), +(i128[4], 1))∧(UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥))

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

(3)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(4)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(5)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(6)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[324 + (-1)bso_15] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)), LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(7)    (o2493[5]=java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0]))∧o2217[5]=o2217[0]+(i128[5], 1)=i128[0]java.lang.Object(List(o4532[0], o2493[0]))=o2493[4]i128[0]=i128[4]o2217new[0]=o2217[4]LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0])≥INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])∧(UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥))

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

(8)    (LOAD2486(o2217[5], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), +(i128[5], 1))≥INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), +(i128[5], 1))∧(UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥))

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

(9)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(10)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(11)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(12)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[324 + (-1)bso_15] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)), LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(13)    (o4550[6]=java.lang.Object(List(o4531[0], o4532[0]))∧o2498[6]=o2493[0]+(i128[6], 1)=i128[0]java.lang.Object(List(o4550[6], o2498[6]))=o2217[0]java.lang.Object(List(o4532[0], o2493[0]))=o2493[4]i128[0]=i128[4]o2217new[0]=o2217[4]LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0])≥INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])∧(UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥))

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

(14)    (LOAD2486(java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2498[6])), +(i128[6], 1))≥INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2498[6])), +(i128[6], 1))∧(UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥))

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

(15)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(16)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(17)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧[324 + (-1)bso_15] + [216]o4532[0] + [243]o4531[0] ≥ 0)

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

(18)    ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧[324 + (-1)bso_15] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

For Pair LOAD2486(o2217, java.lang.Object(List(java.lang.Object(o2641Sub1234), o2493)), i128) → INC4194(o2217, o2493, i128) the following chains were created:
• We consider the chain INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)), LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(19)    (o2217[4]=o2217[1]+(i128[4], 1)=i128[1]o2493[4]=java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1]))∧o2493[1]=o2493[4]1i128[1]=i128[4]1o2217[1]=o2217[4]1LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1])≥INC4194(o2217[1], o2493[1], i128[1])∧(UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥))

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

(20)    (LOAD2486(o2217[4], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), +(i128[4], 1))≥INC4194(o2217[4], o2493[1], +(i128[4], 1))∧(UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥))

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

(21)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2493[1] + [81]o2641Sub1234[1] ≥ 0)

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

(22)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2493[1] + [81]o2641Sub1234[1] ≥ 0)

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

(23)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2493[1] + [81]o2641Sub1234[1] ≥ 0)

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

(24)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧0 ≥ 0∧[117 + (-1)bso_16] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)), LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(25)    (o2493[5]=java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1]))∧o2217[5]=o2217[1]+(i128[5], 1)=i128[1]o2493[1]=o2493[4]i128[1]=i128[4]o2217[1]=o2217[4]LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1])≥INC4194(o2217[1], o2493[1], i128[1])∧(UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥))

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

(26)    (LOAD2486(o2217[5], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), +(i128[5], 1))≥INC4194(o2217[5], o2493[1], +(i128[5], 1))∧(UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥))

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

(27)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2493[1] + [81]o2641Sub1234[1] ≥ 0)

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

(28)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2493[1] + [81]o2641Sub1234[1] ≥ 0)

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

(29)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2493[1] + [81]o2641Sub1234[1] ≥ 0)

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

(30)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧0 ≥ 0∧[117 + (-1)bso_16] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)), LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(31)    (o4550[6]=java.lang.Object(o2641Sub1234[1])∧o2498[6]=o2493[1]+(i128[6], 1)=i128[1]java.lang.Object(List(o4550[6], o2498[6]))=o2217[1]o2493[1]=o2493[4]i128[1]=i128[4]o2217[1]=o2217[4]LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1])≥INC4194(o2217[1], o2493[1], i128[1])∧(UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥))

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

(32)    (LOAD2486(java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2498[6])), java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2498[6])), +(i128[6], 1))≥INC4194(java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2498[6])), o2498[6], +(i128[6], 1))∧(UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥))

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

(33)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2498[6] + [81]o2641Sub1234[1] ≥ 0)

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

(34)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2498[6] + [81]o2641Sub1234[1] ≥ 0)

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

(35)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] + [24]o2498[6] + [81]o2641Sub1234[1] ≥ 0)

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

(36)    ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

For Pair LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), i128) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), o2498, i128) the following chains were created:
• We consider the chain INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)), LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(37)    (o2493[4]=java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))∧+(i128[4], 1)=i128[2]o2217[4]=java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))∧java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))=o2217[4]1i128[2]=i128[4]1o2498[2]=o2493[4]1LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2])≥INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])∧(UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥))

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

(38)    (LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), +(i128[4], 1))≥INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], +(i128[4], 1))∧(UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥))

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

(39)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[2] + [81]o2824Sub1234[2] ≥ 0)

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

(40)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[2] + [81]o2824Sub1234[2] ≥ 0)

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

(41)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[2] + [81]o2824Sub1234[2] ≥ 0)

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

(42)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)), LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(43)    (o2493[5]=java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))∧o2217[5]=java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))∧+(i128[5], 1)=i128[2]java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))=o2217[4]i128[2]=i128[4]o2498[2]=o2493[4]LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2])≥INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])∧(UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥))

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

(44)    (LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), +(i128[5], 1))≥INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], +(i128[5], 1))∧(UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥))

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

(45)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[2] + [81]o2824Sub1234[2] ≥ 0)

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

(46)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[2] + [81]o2824Sub1234[2] ≥ 0)

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

(47)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[2] + [81]o2824Sub1234[2] ≥ 0)

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

(48)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)), LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(49)    (o4550[6]=java.lang.Object(o2824Sub1234[2])∧o2498[6]=o2498[2]+(i128[6], 1)=i128[2]java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))=o2217[4]i128[2]=i128[4]o2498[2]=o2493[4]LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2])≥INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])∧(UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥))

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

(50)    (LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[6])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[6])), +(i128[6], 1))≥INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[6])), o2498[6], +(i128[6], 1))∧(UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥))

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

(51)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[6] + [81]o2824Sub1234[2] ≥ 0)

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

(52)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[6] + [81]o2824Sub1234[2] ≥ 0)

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

(53)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] + [24]o2498[6] + [81]o2824Sub1234[2] ≥ 0)

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

(54)    ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

For Pair LOAD2486(java.lang.Object(List(NULL, o2498)), java.lang.Object(List(NULL, o2498)), i128) → INC4194(java.lang.Object(List(NULL, o2498)), o2498, i128) the following chains were created:
• We consider the chain INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)), LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(55)    (+(i128[4], 1)=i128[3]o2217[4]=java.lang.Object(List(NULL, o2498[3]))∧o2493[4]=java.lang.Object(List(NULL, o2498[3]))∧o2498[3]=o2493[4]1i128[3]=i128[4]1java.lang.Object(List(NULL, o2498[3]))=o2217[4]1LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3])≥INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])∧(UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥))

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

(56)    (LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), +(i128[4], 1))≥INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], +(i128[4], 1))∧(UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥))

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

(57)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[3] ≥ 0)

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

(58)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[3] ≥ 0)

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

(59)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[3] ≥ 0)

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

(60)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)), LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(61)    (o2493[5]=java.lang.Object(List(NULL, o2498[3]))∧o2217[5]=java.lang.Object(List(NULL, o2498[3]))∧+(i128[5], 1)=i128[3]o2498[3]=o2493[4]i128[3]=i128[4]java.lang.Object(List(NULL, o2498[3]))=o2217[4]LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3])≥INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])∧(UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥))

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

(62)    (LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), +(i128[5], 1))≥INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], +(i128[5], 1))∧(UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥))

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

(63)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[3] ≥ 0)

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

(64)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[3] ≥ 0)

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

(65)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[3] ≥ 0)

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

(66)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)), LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(67)    (o4550[6]=NULLo2498[6]=o2498[3]+(i128[6], 1)=i128[3]o2498[3]=o2493[4]i128[3]=i128[4]java.lang.Object(List(NULL, o2498[3]))=o2217[4]LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3])≥INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])∧(UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥))

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

(68)    (LOAD2486(java.lang.Object(List(NULL, o2498[6])), java.lang.Object(List(NULL, o2498[6])), +(i128[6], 1))≥INC4194(java.lang.Object(List(NULL, o2498[6])), o2498[6], +(i128[6], 1))∧(UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥))

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

(69)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[6] ≥ 0)

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

(70)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[6] ≥ 0)

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

(71)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] + [24]o2498[6] ≥ 0)

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

(72)    ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] ≥ 0∧[1] ≥ 0)

For Pair INC4194(o2217, o2493, i128) → LOAD2486(o2217, o2493, +(i128, 1)) the following chains were created:
• We consider the chain LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(73)    (java.lang.Object(List(o4532[0], o2493[0]))=o2493[4]i128[0]=i128[4]o2217new[0]=o2217[4]INC4194(o2217[4], o2493[4], i128[4])≥LOAD2486(o2217[4], o2493[4], +(i128[4], 1))∧(UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥))

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

(74)    (INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])≥LOAD2486(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), +(i128[0], 1))∧(UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥))

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

(75)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(76)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(77)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(78)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)

• We consider the chain LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

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

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

(81)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(82)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(83)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(84)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(85)    (java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))=o2217[4]i128[2]=i128[4]o2498[2]=o2493[4]INC4194(o2217[4], o2493[4], i128[4])≥LOAD2486(o2217[4], o2493[4], +(i128[4], 1))∧(UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥))

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

(86)    (INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])≥LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], +(i128[2], 1))∧(UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥))

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

(87)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(88)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(89)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(90)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3]), INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)) which results in the following constraint:

(91)    (o2498[3]=o2493[4]i128[3]=i128[4]java.lang.Object(List(NULL, o2498[3]))=o2217[4]INC4194(o2217[4], o2493[4], i128[4])≥LOAD2486(o2217[4], o2493[4], +(i128[4], 1))∧(UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥))

We simplified constraint (91) using rule (III) which results in the following new constraint:

(92)    (INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])≥LOAD2486(java.lang.Object(List(NULL, o2498[3])), o2498[3], +(i128[3], 1))∧(UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥))

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

(93)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(94)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(95)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧[(-1)bso_19] ≥ 0)

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

(96)    ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)

For Pair LOAD2486(o2217, java.lang.Object(List(NULL, o2493)), i128) → LOAD2486(o2217, o2493, +(i128, 1)) the following chains were created:
• We consider the chain INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)), LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)) which results in the following constraint:

We simplified constraint (97) using rule (III) which results in the following new constraint:

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

(99)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] + [24]o2493[5] ≥ 0)

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

(100)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] + [24]o2493[5] ≥ 0)

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

(101)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] + [24]o2493[5] ≥ 0)

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

(102)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧0 ≥ 0∧[36 + (-1)bso_20] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)), LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)) which results in the following constraint:

We simplified constraint (103) using rule (III) which results in the following new constraint:

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

(105)    ((UIncreasing(LOAD2486(o2217[5]1, o2493[5]1, +(i128[5]1, 1))), ≥)∧[36 + (-1)bso_20] + [24]o2493[5]1 ≥ 0)

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

(106)    ((UIncreasing(LOAD2486(o2217[5]1, o2493[5]1, +(i128[5]1, 1))), ≥)∧[36 + (-1)bso_20] + [24]o2493[5]1 ≥ 0)

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

(107)    ((UIncreasing(LOAD2486(o2217[5]1, o2493[5]1, +(i128[5]1, 1))), ≥)∧[36 + (-1)bso_20] + [24]o2493[5]1 ≥ 0)

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

(108)    ((UIncreasing(LOAD2486(o2217[5]1, o2493[5]1, +(i128[5]1, 1))), ≥)∧0 ≥ 0∧[36 + (-1)bso_20] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)), LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)) which results in the following constraint:

We simplified constraint (109) using rule (III) which results in the following new constraint:

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

(111)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] + [24]o2498[6] ≥ 0)

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

(112)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] + [24]o2498[6] ≥ 0)

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

(113)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] + [24]o2498[6] ≥ 0)

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

(114)    ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] ≥ 0∧[1] ≥ 0)

For Pair LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), i128) → LOAD2486(java.lang.Object(List(o4550, o2498)), java.lang.Object(List(o4550, o2498)), +(i128, 1)) the following chains were created:
• We consider the chain INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1)), LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)) which results in the following constraint:

(115)    (+(i128[4], 1)=i128[6]o2493[4]=java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))∧o2217[4]=java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])) ⇒ LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6])≥LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))∧(UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥))

We simplified constraint (115) using rule (III) which results in the following new constraint:

(116)    (LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), +(i128[4], 1))≥LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(+(i128[4], 1), 1))∧(UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥))

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

(117)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6] + [243]o4549[6] ≥ 0)

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

(118)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6] + [243]o4549[6] ≥ 0)

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

(119)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6] + [243]o4549[6] ≥ 0)

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

(120)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧0 ≥ 0∧[324 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], +(i128[5], 1)), LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)) which results in the following constraint:

(121)    (o2217[5]=java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))∧+(i128[5], 1)=i128[6]o2493[5]=java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])) ⇒ LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6])≥LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))∧(UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥))

We simplified constraint (121) using rule (III) which results in the following new constraint:

(122)    (LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), +(i128[5], 1))≥LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(+(i128[5], 1), 1))∧(UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥))

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

(123)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6] + [243]o4549[6] ≥ 0)

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

(124)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6] + [243]o4549[6] ≥ 0)

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

(125)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6] + [243]o4549[6] ≥ 0)

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

(126)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧0 ≥ 0∧[324 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• We consider the chain LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)), LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1)) which results in the following constraint:

(127)    (o4550[6]=java.lang.Object(List(o4549[6]1, o4550[6]1))∧o2498[6]=o2498[6]1+(i128[6], 1)=i128[6]1LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6]1, o4550[6]1)), o2498[6]1)), java.lang.Object(List(java.lang.Object(List(o4549[6]1, o4550[6]1)), o2498[6]1)), i128[6]1)≥LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))∧(UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥))

We simplified constraint (127) using rule (III) which results in the following new constraint:

(128)    (LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6]1, o4550[6]1)), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6]1, o4550[6]1)), o2498[6])), +(i128[6], 1))≥LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6])), java.lang.Object(List(o4550[6]1, o2498[6])), +(+(i128[6], 1), 1))∧(UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥))

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

(129)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6]1 + [243]o4549[6]1 ≥ 0)

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

(130)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6]1 + [243]o4549[6]1 ≥ 0)

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

(131)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥)∧[324 + (-1)bso_21] + [216]o4550[6]1 + [243]o4549[6]1 ≥ 0)

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

(132)    ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥)∧0 ≥ 0∧[324 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD2486(o2217, java.lang.Object(List(java.lang.Object(List(o4531, o4532)), o2493)), i128) → INC4194(o2217new, java.lang.Object(List(o4532, o2493)), i128)
• ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[324 + (-1)bso_15] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[324 + (-1)bso_15] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])), ≥)∧0 ≥ 0∧0 ≥ 0∧[324 + (-1)bso_15] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• LOAD2486(o2217, java.lang.Object(List(java.lang.Object(o2641Sub1234), o2493)), i128) → INC4194(o2217, o2493, i128)
• ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧0 ≥ 0∧[117 + (-1)bso_16] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧0 ≥ 0∧[117 + (-1)bso_16] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(o2217[1], o2493[1], i128[1])), ≥)∧[117 + (-1)bso_16] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), i128) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), o2498, i128)
• ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])), ≥)∧[117 + (-1)bso_17] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

• LOAD2486(java.lang.Object(List(NULL, o2498)), java.lang.Object(List(NULL, o2498)), i128) → INC4194(java.lang.Object(List(NULL, o2498)), o2498, i128)
• ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])), ≥)∧[36 + (-1)bso_18] ≥ 0∧[1] ≥ 0)

• INC4194(o2217, o2493, i128) → LOAD2486(o2217, o2493, +(i128, 1))
• ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)
• ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)
• ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)
• ((UIncreasing(LOAD2486(o2217[4], o2493[4], +(i128[4], 1))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_19] ≥ 0)

• ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧0 ≥ 0∧[36 + (-1)bso_20] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(LOAD2486(o2217[5]1, o2493[5]1, +(i128[5]1, 1))), ≥)∧0 ≥ 0∧[36 + (-1)bso_20] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(LOAD2486(o2217[5], o2493[5], +(i128[5], 1))), ≥)∧[36 + (-1)bso_20] ≥ 0∧[1] ≥ 0)

• LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), i128) → LOAD2486(java.lang.Object(List(o4550, o2498)), java.lang.Object(List(o4550, o2498)), +(i128, 1))
• ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧0 ≥ 0∧[324 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))), ≥)∧0 ≥ 0∧[324 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(LOAD2486(java.lang.Object(List(o4550[6]1, o2498[6]1)), java.lang.Object(List(o4550[6]1, o2498[6]1)), +(i128[6]1, 1))), ≥)∧0 ≥ 0∧[324 + (-1)bso_21] ≥ 0∧[1] ≥ 0∧[1] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD2486(x1, x2, x3)) = [1] + [3]x2
POL(java.lang.Object(x1)) = [3] + [3]x1
POL(List(x1, x2)) = [3] + [3]x2 + [3]x1
POL(INC4194(x1, x2, x3)) = [1] + [3]x2
POL(NULL) = 0
POL(+(x1, x2)) = 0
POL(1) = 0

The following pairs are in P>:

LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))

The following pairs are in Pbound:

LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1))
LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), +(i128[6], 1))

The following pairs are in P:

INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], +(i128[4], 1))

There are no usable rules.

### (14) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(4): INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], i128[4] + 1)

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

### (15) IDependencyGraphProof (EQUIVALENT transformation)

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

### (17) Obligation:

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

The following domains are used:
none

R is empty.

The integer pair graph is empty.

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

### (18) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
Load1729(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → Load1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65, java.lang.Object(java.lang.String(i89)))
Load1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65, java.lang.Object(java.lang.String(i89))) → Cond_Load1729ARR1(i63 > 0 && i63 < i4 && i65 >= 0 && i65 < i64 && i63 + 1 > 0, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65, java.lang.Object(java.lang.String(i89)))
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65, java.lang.Object(java.lang.String(i89))) → Load4728(java.lang.Object(ARRAY(i4, a1662data)), i63 + 1, i64, i65, i89)
Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → Cond_Load4728(i222 > 0, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222 + -1)
Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → Cond_Load47281(i223 <= 0 && i65 + 1 > 0, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → Load1729(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65 + 1)
The set Q consists of the following terms:
Load1729ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)))
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)))
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (21) ITRSFilterProcessorProof (SOUND transformation)

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

java.lang.String(x1) → java.lang.String
Cond_Load1729ARR1(x1, x2, x3, x4, x5, x6) → Cond_Load1729ARR1(x1, x2, x3, x4, x5)

### (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:
Load1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → Cond_Load1729ARR1(i63 > 0 && i63 < i4 && i65 >= 0 && i65 < i64 && i63 + 1 > 0, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65)
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → Load4728(java.lang.Object(ARRAY(i4, a1662data)), i63 + 1, i64, i65, i89)
Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → Cond_Load4728(i222 > 0, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222 + -1)
Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → Cond_Load47281(i223 <= 0 && i65 + 1 > 0, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → Load1729(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65 + 1)
The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (24) Obligation:

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

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → Cond_Load1729ARR1(i63 > 0 && i63 < i4 && i65 >= 0 && i65 < i64 && i63 + 1 > 0, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65)
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → Load4728(java.lang.Object(ARRAY(i4, a1662data)), i63 + 1, i64, i65, i89)
Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → Cond_Load4728(i222 > 0, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222 + -1)
Load4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → Cond_Load47281(i223 <= 0 && i65 + 1 > 0, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → Load1729(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD1729(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]) → LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])
(1): LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0, java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])
(2): COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2] + 1, i64[2], i65[2], i89[2])
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(5): LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(i223[5] <= 0 && i65[5] + 1 > 0, java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])
(6): COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6] + 1)

(0) -> (1), if ((java.lang.Object(ARRAY(i4[0], a1662data[0])) →* java.lang.Object(ARRAY(i4[1], a1662data[1])))∧(i64[0]* i64[1])∧(i63[0]* i63[1])∧(i65[0]* i65[1]))

(1) -> (2), if ((java.lang.Object(ARRAY(i4[1], a1662data[1])) →* java.lang.Object(ARRAY(i4[2], a1662data[2])))∧(i63[1]* i63[2])∧(i65[1]* i65[2])∧(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0* TRUE)∧(i64[1]* i64[2]))

(2) -> (3), if ((i89[2]* i222[3])∧(i63[2] + 1* i66[3])∧(i64[2]* i64[3])∧(java.lang.Object(ARRAY(i4[2], a1662data[2])) →* java.lang.Object(ARRAY(i4[3], a5089data[3])))∧(i65[2]* i65[3]))

(2) -> (5), if ((i65[2]* i65[5])∧(java.lang.Object(ARRAY(i4[2], a1662data[2])) →* java.lang.Object(ARRAY(i4[5], a5089data[5])))∧(i89[2]* i223[5])∧(i63[2] + 1* i66[5])∧(i64[2]* i64[5]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧(java.lang.Object(ARRAY(i4[3], a5089data[3])) →* java.lang.Object(ARRAY(i4[4], a5089data[4])))∧(i222[3] > 0* TRUE))

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧(java.lang.Object(ARRAY(i4[4], a5089data[4])) →* java.lang.Object(ARRAY(i4[3], a5089data[3])))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(4) -> (5), if ((i222[4] + -1* i223[5])∧(i64[4]* i64[5])∧(i66[4]* i66[5])∧(i65[4]* i65[5])∧(java.lang.Object(ARRAY(i4[4], a5089data[4])) →* java.lang.Object(ARRAY(i4[5], a5089data[5]))))

(5) -> (6), if ((i66[5]* i66[6])∧(i223[5] <= 0 && i65[5] + 1 > 0* TRUE)∧(i64[5]* i64[6])∧(java.lang.Object(ARRAY(i4[5], a5089data[5])) →* java.lang.Object(ARRAY(i4[6], a5089data[6])))∧(i65[5]* i65[6])∧(i223[5]* i223[6]))

(6) -> (0), if ((i65[6] + 1* i65[0])∧(java.lang.Object(ARRAY(i4[6], a5089data[6])) →* java.lang.Object(ARRAY(i4[0], a1662data[0])))∧(i66[6]* i63[0])∧(i64[6]* i64[0]))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

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

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

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1729(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]) → LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])
(1): LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0, java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])
(2): COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2] + 1, i64[2], i65[2], i89[2])
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(5): LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(i223[5] <= 0 && i65[5] + 1 > 0, java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])
(6): COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6] + 1)

(0) -> (1), if ((java.lang.Object(ARRAY(i4[0], a1662data[0])) →* java.lang.Object(ARRAY(i4[1], a1662data[1])))∧(i64[0]* i64[1])∧(i63[0]* i63[1])∧(i65[0]* i65[1]))

(1) -> (2), if ((java.lang.Object(ARRAY(i4[1], a1662data[1])) →* java.lang.Object(ARRAY(i4[2], a1662data[2])))∧(i63[1]* i63[2])∧(i65[1]* i65[2])∧(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0* TRUE)∧(i64[1]* i64[2]))

(2) -> (3), if ((i89[2]* i222[3])∧(i63[2] + 1* i66[3])∧(i64[2]* i64[3])∧(java.lang.Object(ARRAY(i4[2], a1662data[2])) →* java.lang.Object(ARRAY(i4[3], a5089data[3])))∧(i65[2]* i65[3]))

(2) -> (5), if ((i65[2]* i65[5])∧(java.lang.Object(ARRAY(i4[2], a1662data[2])) →* java.lang.Object(ARRAY(i4[5], a5089data[5])))∧(i89[2]* i223[5])∧(i63[2] + 1* i66[5])∧(i64[2]* i64[5]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧(java.lang.Object(ARRAY(i4[3], a5089data[3])) →* java.lang.Object(ARRAY(i4[4], a5089data[4])))∧(i222[3] > 0* TRUE))

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧(java.lang.Object(ARRAY(i4[4], a5089data[4])) →* java.lang.Object(ARRAY(i4[3], a5089data[3])))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(4) -> (5), if ((i222[4] + -1* i223[5])∧(i64[4]* i64[5])∧(i66[4]* i66[5])∧(i65[4]* i65[5])∧(java.lang.Object(ARRAY(i4[4], a5089data[4])) →* java.lang.Object(ARRAY(i4[5], a5089data[5]))))

(5) -> (6), if ((i66[5]* i66[6])∧(i223[5] <= 0 && i65[5] + 1 > 0* TRUE)∧(i64[5]* i64[6])∧(java.lang.Object(ARRAY(i4[5], a5089data[5])) →* java.lang.Object(ARRAY(i4[6], a5089data[6])))∧(i65[5]* i65[6])∧(i223[5]* i223[6]))

(6) -> (0), if ((i65[6] + 1* i65[0])∧(java.lang.Object(ARRAY(i4[6], a5089data[6])) →* java.lang.Object(ARRAY(i4[0], a1662data[0])))∧(i66[6]* i63[0])∧(i64[6]* i64[0]))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (27) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

### (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): LOAD1729(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]) → LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])
(1): LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0, java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])
(2): COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2] + 1, i64[2], i65[2], i89[2])
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(5): LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(i223[5] <= 0 && i65[5] + 1 > 0, java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])
(6): COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6] + 1)

(0) -> (1), if (((i4[0]* i4[1])∧(a1662data[0]* a1662data[1]))∧(i64[0]* i64[1])∧(i63[0]* i63[1])∧(i65[0]* i65[1]))

(1) -> (2), if (((i4[1]* i4[2])∧(a1662data[1]* a1662data[2]))∧(i63[1]* i63[2])∧(i65[1]* i65[2])∧(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0* TRUE)∧(i64[1]* i64[2]))

(2) -> (3), if ((i89[2]* i222[3])∧(i63[2] + 1* i66[3])∧(i64[2]* i64[3])∧((i4[2]* i4[3])∧(a1662data[2]* a5089data[3]))∧(i65[2]* i65[3]))

(2) -> (5), if ((i65[2]* i65[5])∧((i4[2]* i4[5])∧(a1662data[2]* a5089data[5]))∧(i89[2]* i223[5])∧(i63[2] + 1* i66[5])∧(i64[2]* i64[5]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧((i4[3]* i4[4])∧(a5089data[3]* a5089data[4]))∧(i222[3] > 0* TRUE))

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧((i4[4]* i4[3])∧(a5089data[4]* a5089data[3]))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(4) -> (5), if ((i222[4] + -1* i223[5])∧(i64[4]* i64[5])∧(i66[4]* i66[5])∧(i65[4]* i65[5])∧((i4[4]* i4[5])∧(a5089data[4]* a5089data[5])))

(5) -> (6), if ((i66[5]* i66[6])∧(i223[5] <= 0 && i65[5] + 1 > 0* TRUE)∧(i64[5]* i64[6])∧((i4[5]* i4[6])∧(a5089data[5]* a5089data[6]))∧(i65[5]* i65[6])∧(i223[5]* i223[6]))

(6) -> (0), if ((i65[6] + 1* i65[0])∧((i4[6]* i4[0])∧(a5089data[6]* a1662data[0]))∧(i66[6]* i63[0])∧(i64[6]* i64[0]))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (29) 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 LOAD1729(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → LOAD1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) the following chains were created:
• We consider the chain LOAD1729(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]) → LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]), LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) which results in the following constraint:

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

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

(3)    ((UIncreasing(LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])), ≥)∧[(-1)bso_23] ≥ 0)

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

(4)    ((UIncreasing(LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])), ≥)∧[(-1)bso_23] ≥ 0)

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

(5)    ((UIncreasing(LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])), ≥)∧[(-1)bso_23] ≥ 0)

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

(6)    ((UIncreasing(LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

For Pair LOAD1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63, 0), <(i63, i4)), >=(i65, 0)), <(i65, i64)), >(+(i63, 1), 0)), java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) the following chains were created:
• We consider the chain LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]), COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2]) which results in the following constraint:

(7)    (i4[1]=i4[2]a1662data[1]=a1662data[2]i63[1]=i63[2]i65[1]=i65[2]&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0))=TRUEi64[1]=i64[2]LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])≥NonInfC∧LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])≥COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])∧(UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥))

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

(8)    (>(+(i63[1], 1), 0)=TRUE<(i65[1], i64[1])=TRUE>=(i65[1], 0)=TRUE>(i63[1], 0)=TRUE<(i63[1], i4[1])=TRUELOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])≥NonInfC∧LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])≥COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])∧(UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥))

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

(9)    (i63[1] ≥ 0∧i64[1] + [-1] + [-1]i65[1] ≥ 0∧i65[1] ≥ 0∧i63[1] + [-1] ≥ 0∧i4[1] + [-1] + [-1]i63[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]i65[1] + [bni_24]i64[1] + [bni_24]i4[1] + [(-1)bni_24]i63[1] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(10)    (i63[1] ≥ 0∧i64[1] + [-1] + [-1]i65[1] ≥ 0∧i65[1] ≥ 0∧i63[1] + [-1] ≥ 0∧i4[1] + [-1] + [-1]i63[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]i65[1] + [bni_24]i64[1] + [bni_24]i4[1] + [(-1)bni_24]i63[1] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(11)    (i63[1] ≥ 0∧i64[1] + [-1] + [-1]i65[1] ≥ 0∧i65[1] ≥ 0∧i63[1] + [-1] ≥ 0∧i4[1] + [-1] + [-1]i63[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]i65[1] + [bni_24]i64[1] + [bni_24]i4[1] + [(-1)bni_24]i63[1] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(12)    (i63[1] ≥ 0∧i64[1] + [-1] + [-1]i65[1] ≥ 0∧i65[1] ≥ 0∧i63[1] + [-1] ≥ 0∧i4[1] + [-1] + [-1]i63[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧0 = 0∧[(-1)Bound*bni_24] + [(-1)bni_24]i65[1] + [bni_24]i64[1] + [bni_24]i4[1] + [(-1)bni_24]i63[1] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

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

(13)    ([1] + i63[1] ≥ 0∧i64[1] + [-1] + [-1]i65[1] ≥ 0∧i65[1] ≥ 0∧i63[1] ≥ 0∧i4[1] + [-2] + [-1]i63[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧0 = 0∧[(-1)Bound*bni_24 + (-1)bni_24] + [(-1)bni_24]i65[1] + [bni_24]i64[1] + [bni_24]i4[1] + [(-1)bni_24]i63[1] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

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

(14)    ([1] + i63[1] ≥ 0∧i64[1] ≥ 0∧i65[1] ≥ 0∧i63[1] ≥ 0∧i4[1] + [-2] + [-1]i63[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧0 = 0∧[(-1)Bound*bni_24] + [bni_24]i64[1] + [bni_24]i4[1] + [(-1)bni_24]i63[1] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

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

(15)    ([1] + i63[1] ≥ 0∧i64[1] ≥ 0∧i65[1] ≥ 0∧i63[1] ≥ 0∧i4[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧0 = 0∧[(-1)Bound*bni_24 + (2)bni_24] + [bni_24]i64[1] + [bni_24]i4[1] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → LOAD4728(java.lang.Object(ARRAY(i4, a1662data)), +(i63, 1), i64, i65, i89) the following chains were created:
• We consider the chain COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2]) which results in the following constraint:

(16)    (COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2])≥NonInfC∧COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2])≥LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])∧(UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])), ≥))

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

(17)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(18)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(19)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(20)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

For Pair LOAD4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → COND_LOAD4728(>(i222, 0), java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) the following chains were created:
• We consider the chain LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]), COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) which results in the following constraint:

(21)    (i64[3]=i64[4]i222[3]=i222[4]i66[3]=i66[4]i65[3]=i65[4]i4[3]=i4[4]a5089data[3]=a5089data[4]>(i222[3], 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])∧(UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥))

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

(22)    (>(i222[3], 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])∧(UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥))

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

(23)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)Bound*bni_28] + [(-1)bni_28]i66[3] + [(-1)bni_28]i65[3] + [bni_28]i64[3] + [bni_28]i4[3] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(24)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)Bound*bni_28] + [(-1)bni_28]i66[3] + [(-1)bni_28]i65[3] + [bni_28]i64[3] + [bni_28]i4[3] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(25)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)Bound*bni_28] + [(-1)bni_28]i66[3] + [(-1)bni_28]i65[3] + [bni_28]i64[3] + [bni_28]i4[3] ≥ 0∧[(-1)bso_29] ≥ 0)

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

(26)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_28] = 0∧[(-1)bni_28] = 0∧[bni_28] = 0∧0 = 0∧[bni_28] = 0∧[(-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

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

(27)    (i222[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_28] = 0∧[(-1)bni_28] = 0∧[bni_28] = 0∧0 = 0∧[bni_28] = 0∧[(-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → LOAD4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, +(i222, -1)) the following chains were created:
• We consider the chain COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) which results in the following constraint:

(28)    (COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4])≥NonInfC∧COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4])≥LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))∧(UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥))

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

(29)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[(-1)bso_31] ≥ 0)

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

(30)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[(-1)bso_31] ≥ 0)

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

(31)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[(-1)bso_31] ≥ 0)

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

(32)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

For Pair LOAD4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → COND_LOAD47281(&&(<=(i223, 0), >(+(i65, 1), 0)), java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) the following chains were created:
• We consider the chain LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]), COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1)) which results in the following constraint:

(33)    (i66[5]=i66[6]&&(<=(i223[5], 0), >(+(i65[5], 1), 0))=TRUEi64[5]=i64[6]i4[5]=i4[6]a5089data[5]=a5089data[6]i65[5]=i65[6]i223[5]=i223[6]LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])≥COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])∧(UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥))

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

(34)    (<=(i223[5], 0)=TRUE>(+(i65[5], 1), 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])≥COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])∧(UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥))

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

(35)    ([-1]i223[5] ≥ 0∧i65[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥)∧[(-1)Bound*bni_32] + [(-1)bni_32]i66[5] + [(-1)bni_32]i65[5] + [bni_32]i64[5] + [bni_32]i4[5] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(36)    ([-1]i223[5] ≥ 0∧i65[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥)∧[(-1)Bound*bni_32] + [(-1)bni_32]i66[5] + [(-1)bni_32]i65[5] + [bni_32]i64[5] + [bni_32]i4[5] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(37)    ([-1]i223[5] ≥ 0∧i65[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥)∧[(-1)Bound*bni_32] + [(-1)bni_32]i66[5] + [(-1)bni_32]i65[5] + [bni_32]i64[5] + [bni_32]i4[5] ≥ 0∧[(-1)bso_33] ≥ 0)

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

(38)    ([-1]i223[5] ≥ 0∧i65[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥)∧[(-1)bni_32] = 0∧[bni_32] = 0∧0 = 0∧[bni_32] = 0∧[(-1)Bound*bni_32] + [(-1)bni_32]i65[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

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

(39)    (i223[5] ≥ 0∧i65[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥)∧[(-1)bni_32] = 0∧[bni_32] = 0∧0 = 0∧[bni_32] = 0∧[(-1)Bound*bni_32] + [(-1)bni_32]i65[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → LOAD1729(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, +(i65, 1)) the following chains were created:
• We consider the chain COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1)) which results in the following constraint:

(40)    (COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6])≥NonInfC∧COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6])≥LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))∧(UIncreasing(LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))), ≥))

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

(41)    ((UIncreasing(LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))), ≥)∧[1 + (-1)bso_35] ≥ 0)

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

(42)    ((UIncreasing(LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))), ≥)∧[1 + (-1)bso_35] ≥ 0)

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

(43)    ((UIncreasing(LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))), ≥)∧[1 + (-1)bso_35] ≥ 0)

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

(44)    ((UIncreasing(LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_35] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• LOAD1729(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → LOAD1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65)
• ((UIncreasing(LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_23] ≥ 0)

• LOAD1729ARR1(java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63, 0), <(i63, i4)), >=(i65, 0)), <(i65, i64)), >(+(i63, 1), 0)), java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65)
• ([1] + i63[1] ≥ 0∧i64[1] ≥ 0∧i65[1] ≥ 0∧i63[1] ≥ 0∧i4[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])), ≥)∧0 = 0∧[(-1)Bound*bni_24 + (2)bni_24] + [bni_24]i64[1] + [bni_24]i4[1] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

• COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4, a1662data)), i63, i64, i65) → LOAD4728(java.lang.Object(ARRAY(i4, a1662data)), +(i63, 1), i64, i65, i89)
• ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

• LOAD4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → COND_LOAD4728(>(i222, 0), java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222)
• (i222[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_28] = 0∧[(-1)bni_28] = 0∧[bni_28] = 0∧0 = 0∧[bni_28] = 0∧[(-1)Bound*bni_28] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

• COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i222) → LOAD4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, +(i222, -1))
• ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

• LOAD4728(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → COND_LOAD47281(&&(<=(i223, 0), >(+(i65, 1), 0)), java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223)
• (i223[5] ≥ 0∧i65[5] ≥ 0 ⇒ (UIncreasing(COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])), ≥)∧[(-1)bni_32] = 0∧[bni_32] = 0∧0 = 0∧[bni_32] = 0∧[(-1)Bound*bni_32] + [(-1)bni_32]i65[5] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

• COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4, a5089data)), i66, i64, i65, i223) → LOAD1729(java.lang.Object(ARRAY(i4, a5089data)), i66, i64, +(i65, 1))
• ((UIncreasing(LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_35] ≥ 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(LOAD1729(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [-1]x1 + [-1]x2
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1] + [-1]x1
POL(LOAD1729ARR1(x1, x2, x3, x4)) = [-1] + [-1]x4 + x3 + [-1]x1 + [-1]x2
POL(COND_LOAD1729ARR1(x1, x2, x3, x4, x5)) = [-1] + [-1]x5 + x4 + [-1]x2 + [-1]x3
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(<(x1, x2)) = [-1]
POL(>=(x1, x2)) = [-1]
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(LOAD4728(x1, x2, x3, x4, x5)) = [-1] + [-1]x2 + [-1]x4 + x3 + [-1]x1
POL(COND_LOAD4728(x1, x2, x3, x4, x5, x6)) = [-1] + [-1]x5 + x4 + [-1]x3 + [-1]x2
POL(-1) = [-1]
POL(COND_LOAD47281(x1, x2, x3, x4, x5, x6)) = [-1] + [-1]x5 + x4 + [-1]x3 + [-1]x2
POL(<=(x1, x2)) = [-1]

The following pairs are in P>:

COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), +(i63[2], 1), i64[2], i65[2], i89[2])
COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], +(i65[6], 1))

The following pairs are in Pbound:

LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])

The following pairs are in P:

LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(&&(&&(&&(&&(>(i63[1], 0), <(i63[1], i4[1])), >=(i65[1], 0)), <(i65[1], i64[1])), >(+(i63[1], 1), 0)), java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])
LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))
LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(&&(<=(i223[5], 0), >(+(i65[5], 1), 0)), java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])

There are no usable rules.

### (31) 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): LOAD1729(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]) → LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])
(1): LOAD1729ARR1(java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1]) → COND_LOAD1729ARR1(i63[1] > 0 && i63[1] < i4[1] && i65[1] >= 0 && i65[1] < i64[1] && i63[1] + 1 > 0, java.lang.Object(ARRAY(i4[1], a1662data[1])), i63[1], i64[1], i65[1])
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(5): LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(i223[5] <= 0 && i65[5] + 1 > 0, java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])

(0) -> (1), if (((i4[0]* i4[1])∧(a1662data[0]* a1662data[1]))∧(i64[0]* i64[1])∧(i63[0]* i63[1])∧(i65[0]* i65[1]))

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧((i4[4]* i4[3])∧(a5089data[4]* a5089data[3]))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧((i4[3]* i4[4])∧(a5089data[3]* a5089data[4]))∧(i222[3] > 0* TRUE))

(4) -> (5), if ((i222[4] + -1* i223[5])∧(i64[4]* i64[5])∧(i66[4]* i66[5])∧(i65[4]* i65[5])∧((i4[4]* i4[5])∧(a5089data[4]* a5089data[5])))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (32) IDependencyGraphProof (EQUIVALENT transformation)

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

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

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧((i4[4]* i4[3])∧(a5089data[4]* a5089data[3]))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧((i4[3]* i4[4])∧(a5089data[3]* a5089data[4]))∧(i222[3] > 0* TRUE))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (34) 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 COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) the following chains were created:
• We consider the chain COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) which results in the following constraint:

(1)    (COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4])≥NonInfC∧COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4])≥LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))∧(UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥))

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

(2)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[2 + (-1)bso_10] ≥ 0)

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

(3)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[2 + (-1)bso_10] ≥ 0)

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

(4)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[2 + (-1)bso_10] ≥ 0)

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

(5)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧0 = 0∧[2 + (-1)bso_10] ≥ 0)

For Pair LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) the following chains were created:
• We consider the chain LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]), COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) which results in the following constraint:

(6)    (i64[3]=i64[4]i222[3]=i222[4]i66[3]=i66[4]i65[3]=i65[4]i4[3]=i4[4]a5089data[3]=a5089data[4]>(i222[3], 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])∧(UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥))

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

(7)    (>(i222[3], 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])∧(UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥))

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

(8)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i222[3] ≥ 0∧[(-1)bso_12] ≥ 0)

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

(9)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i222[3] ≥ 0∧[(-1)bso_12] ≥ 0)

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

(10)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i222[3] ≥ 0∧[(-1)bso_12] ≥ 0)

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

(11)    (i222[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i222[3] ≥ 0∧[(-1)bso_12] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))
• ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧0 = 0∧[2 + (-1)bso_10] ≥ 0)

• LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
• (i222[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[bni_11 + (-1)Bound*bni_11] + [(2)bni_11]i222[3] ≥ 0∧[(-1)bso_12] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_LOAD4728(x1, x2, x3, x4, x5, x6)) = [-1] + [2]x6
POL(java.lang.Object(x1)) = [-1]
POL(ARRAY(x1, x2)) = [-1]
POL(LOAD4728(x1, x2, x3, x4, x5)) = [-1] + [2]x5
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0

The following pairs are in P>:

COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))

The following pairs are in Pbound:

LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

The following pairs are in P:

LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

There are no usable rules.

### (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:
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (37) IDependencyGraphProof (EQUIVALENT transformation)

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

### (39) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (40) IDependencyGraphProof (EQUIVALENT transformation)

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

### (42) Obligation:

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

The following domains are used:

Integer, Boolean

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1729(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0]) → LOAD1729ARR1(java.lang.Object(ARRAY(i4[0], a1662data[0])), i63[0], i64[0], i65[0])
(2): COND_LOAD1729ARR1(TRUE, java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2], i64[2], i65[2]) → LOAD4728(java.lang.Object(ARRAY(i4[2], a1662data[2])), i63[2] + 1, i64[2], i65[2], i89[2])
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(5): LOAD4728(java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5]) → COND_LOAD47281(i223[5] <= 0 && i65[5] + 1 > 0, java.lang.Object(ARRAY(i4[5], a5089data[5])), i66[5], i64[5], i65[5], i223[5])
(6): COND_LOAD47281(TRUE, java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6], i223[6]) → LOAD1729(java.lang.Object(ARRAY(i4[6], a5089data[6])), i66[6], i64[6], i65[6] + 1)

(6) -> (0), if ((i65[6] + 1* i65[0])∧((i4[6]* i4[0])∧(a5089data[6]* a1662data[0]))∧(i66[6]* i63[0])∧(i64[6]* i64[0]))

(2) -> (3), if ((i89[2]* i222[3])∧(i63[2] + 1* i66[3])∧(i64[2]* i64[3])∧((i4[2]* i4[3])∧(a1662data[2]* a5089data[3]))∧(i65[2]* i65[3]))

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧((i4[4]* i4[3])∧(a5089data[4]* a5089data[3]))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧((i4[3]* i4[4])∧(a5089data[3]* a5089data[4]))∧(i222[3] > 0* TRUE))

(2) -> (5), if ((i65[2]* i65[5])∧((i4[2]* i4[5])∧(a1662data[2]* a5089data[5]))∧(i89[2]* i223[5])∧(i63[2] + 1* i66[5])∧(i64[2]* i64[5]))

(4) -> (5), if ((i222[4] + -1* i223[5])∧(i64[4]* i64[5])∧(i66[4]* i66[5])∧(i65[4]* i65[5])∧((i4[4]* i4[5])∧(a5089data[4]* a5089data[5])))

(5) -> (6), if ((i66[5]* i66[6])∧(i223[5] <= 0 && i65[5] + 1 > 0* TRUE)∧(i64[5]* i64[6])∧((i4[5]* i4[6])∧(a5089data[5]* a5089data[6]))∧(i65[5]* i65[6])∧(i223[5]* i223[6]))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (43) IDependencyGraphProof (EQUIVALENT transformation)

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

### (44) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

(4) -> (3), if ((i66[4]* i66[3])∧(i64[4]* i64[3])∧((i4[4]* i4[3])∧(a5089data[4]* a5089data[3]))∧(i222[4] + -1* i222[3])∧(i65[4]* i65[3]))

(3) -> (4), if ((i64[3]* i64[4])∧(i222[3]* i222[4])∧(i66[3]* i66[4])∧(i65[3]* i65[4])∧((i4[3]* i4[4])∧(a5089data[3]* a5089data[4]))∧(i222[3] > 0* TRUE))

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (45) 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 COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) the following chains were created:
• We consider the chain COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) which results in the following constraint:

(1)    (COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4])≥NonInfC∧COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4])≥LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))∧(UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥))

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

(2)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[2 + (-1)bso_9] ≥ 0)

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

(3)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[2 + (-1)bso_9] ≥ 0)

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

(4)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧[2 + (-1)bso_9] ≥ 0)

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

(5)    ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

For Pair LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) the following chains were created:
• We consider the chain LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]), COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1)) which results in the following constraint:

(6)    (i64[3]=i64[4]i222[3]=i222[4]i66[3]=i66[4]i65[3]=i65[4]i4[3]=i4[4]a5089data[3]=a5089data[4]>(i222[3], 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])∧(UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥))

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

(7)    (>(i222[3], 0)=TRUELOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥NonInfC∧LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])≥COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])∧(UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥))

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

(8)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(2)bni_10]i222[3] ≥ 0∧[(-1)bso_11] ≥ 0)

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

(9)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(2)bni_10]i222[3] ≥ 0∧[(-1)bso_11] ≥ 0)

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

(10)    (i222[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[(-1)bni_10 + (-1)Bound*bni_10] + [(2)bni_10]i222[3] ≥ 0∧[(-1)bso_11] ≥ 0)

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

(11)    (i222[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[bni_10 + (-1)Bound*bni_10] + [(2)bni_10]i222[3] ≥ 0∧[(-1)bso_11] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))
• ((UIncreasing(LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))), ≥)∧0 = 0∧[2 + (-1)bso_9] ≥ 0)

• LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])
• (i222[3] ≥ 0 ⇒ (UIncreasing(COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])), ≥)∧[bni_10 + (-1)Bound*bni_10] + [(2)bni_10]i222[3] ≥ 0∧[(-1)bso_11] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_LOAD4728(x1, x2, x3, x4, x5, x6)) = [-1] + [2]x6
POL(java.lang.Object(x1)) = [2]
POL(ARRAY(x1, x2)) = [-1]
POL(LOAD4728(x1, x2, x3, x4, x5)) = [-1] + [2]x5
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0

The following pairs are in P>:

COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], +(i222[4], -1))

The following pairs are in Pbound:

LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

The following pairs are in P:

LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(>(i222[3], 0), java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

There are no usable rules.

### (47) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): LOAD4728(java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3]) → COND_LOAD4728(i222[3] > 0, java.lang.Object(ARRAY(i4[3], a5089data[3])), i66[3], i64[3], i65[3], i222[3])

The set Q consists of the following terms:
Cond_Load1729ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load4728(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load4728(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)
Cond_Load47281(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, x5)

### (48) IDependencyGraphProof (EQUIVALENT transformation)

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

### (50) 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:
(4): COND_LOAD4728(TRUE, java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4]) → LOAD4728(java.lang.Object(ARRAY(i4[4], a5089data[4])), i66[4], i64[4], i65[4], i222[4] + -1)

The set Q consists of the following terms: