### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: CyclicList
`/** * This class represents a list. The function get(n) can be used to access * the n-th element.  * @author Marc Brockschmidt */public class CyclicList {	/**	 * A reference to the next list element.	 */	private CyclicList next;		public static void main(String[] args) {		CyclicList list = CyclicList.create(args.length);		list.get(args[0].length());	}		/**	 * Create a new list element.	 * @param n a reference to the next element.	 */	public CyclicList(final CyclicList n) {		this.next = n;	}		/**	 * Create a new cyclical list of a length l.	 * @param l some length	 * @return cyclical list of length max(1, l)	 */	public static CyclicList create(int x) {		CyclicList last, current;		last = current = new CyclicList(null);		while (--x > 0)			current = new CyclicList(current);		return last.next = current;	}	public CyclicList get(int n) {		CyclicList cur = this;		while (--n > 0) {			cur = cur.next;		}		return cur;	}	}`

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
CyclicList.main([Ljava/lang/String;)V: Graph of 157 nodes with 2 SCCs.

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 24 rules for P and 27 rules for R.

Combined rules. Obtained 4 rules for P and 0 rules for R.

Filtered ground terms:

CyclicList(x1, x2) → CyclicList(x2)
567_0_get_Load(x1, x2, x3) → 567_0_get_Load(x2, x3)
Cond_567_1_main_InvokeMethod3(x1, x2, x3) → Cond_567_1_main_InvokeMethod3(x1, x2)

Combined rules. Obtained 4 rules for P and 0 rules for R.

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

Log for SCC 1:

Generated 17 rules for P and 122 rules for R.

Combined rules. Obtained 1 rules for P and 0 rules for R.

Filtered ground terms:

CyclicList(x1) → CyclicList
160_0_create_Load(x1, x2, x3, x4) → 160_0_create_Load(x2, x4)

Combined rules. Obtained 1 rules for P and 0 rules for R.

Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.

### (5) 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): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(x0[0] > 0, 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))
(2): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(x0[2] > 0, 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(4): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(x0[4] > 0, 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(6): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(x0[6] > 0, 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))
(7): COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

(0) -> (1), if ((x0[0] > 0* TRUE)∧(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))) →* 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))))∧(java.lang.Object(x2[0]) →* java.lang.Object(x2[1])))

(1) -> (0), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x2[1]) →* java.lang.Object(x2[0])))

(1) -> (2), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →* java.lang.Object(x1[2])))

(1) -> (4), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x2[1]) →* java.lang.Object(CyclicList(x1[4]))))

(1) -> (6), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →* java.lang.Object(CyclicList(java.lang.Object(EOR)))))

(2) -> (3), if ((x0[2] > 0* TRUE)∧(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[2]) →* java.lang.Object(x1[3])))

(3) -> (0), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x1[3]) →* java.lang.Object(x2[0])))

(3) -> (2), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[3]) →* java.lang.Object(x1[2])))

(3) -> (4), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x1[3]) →* java.lang.Object(CyclicList(x1[4]))))

(3) -> (6), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[3]) →* java.lang.Object(CyclicList(java.lang.Object(EOR)))))

(4) -> (5), if ((x0[4] > 0* TRUE)∧(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))) →* 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))))∧(java.lang.Object(CyclicList(x1[4])) →* java.lang.Object(CyclicList(x1[5]))))

(5) -> (0), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(x2[0])))

(5) -> (2), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(x1[2])))

(5) -> (4), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(CyclicList(x1[4]))))

(5) -> (6), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(CyclicList(java.lang.Object(EOR)))))

(6) -> (7), if ((x0[6] > 0* TRUE)∧(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR))))))

(7) -> (0), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →* java.lang.Object(x2[0])))

(7) -> (2), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →* java.lang.Object(x1[2])))

(7) -> (4), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →* java.lang.Object(CyclicList(x1[4]))))

(7) -> (6), if (567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))))

The set Q is empty.

### (6) 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 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → COND_567_1_MAIN_INVOKEMETHOD(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])), COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:

(1)    (>(x0[0], 0)=TRUE567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0])))=567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1])))∧java.lang.Object(x2[0])=java.lang.Object(x2[1]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

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

(2)    (>(x0[0], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

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

(3)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[0] + [bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

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

(4)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[0] + [bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

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

(5)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)Bound*bni_16] + [(-1)bni_16]x2[0] + [bni_16]x0[0] ≥ 0∧[(-1)bso_17] ≥ 0)

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

(6)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)bni_16] = 0∧0 = 0∧[(-1)Bound*bni_16] + [bni_16]x0[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

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

(7)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)bni_16] = 0∧0 = 0∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x0[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x3), java.lang.Object(x2)) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:

(8)    (COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥))

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

(9)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(10)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(11)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[1 + (-1)bso_19] ≥ 0)

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

(12)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])), COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:

(13)    (>(x0[2], 0)=TRUE567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR))))=567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR))))∧java.lang.Object(x1[2])=java.lang.Object(x1[3]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

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

(14)    (>(x0[2], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

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

(15)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)Bound*bni_20] + [(-1)bni_20]x1[2] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

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

(16)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)Bound*bni_20] + [(-1)bni_20]x1[2] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

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

(17)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)Bound*bni_20] + [(-1)bni_20]x1[2] + [bni_20]x0[2] ≥ 0∧[(-1)bso_21] ≥ 0)

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

(18)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)bni_20] = 0∧[(-1)Bound*bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

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

(19)    (x0[2] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)bni_20] = 0∧[(-1)Bound*bni_20 + bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:

(20)    (COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥))

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

(21)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[1 + (-1)bso_23] ≥ 0)

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

(22)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[1 + (-1)bso_23] ≥ 0)

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

(23)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[1 + (-1)bso_23] ≥ 0)

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

(24)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))), COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:

(25)    (>(x0[4], 0)=TRUE567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4])))=567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5])))∧java.lang.Object(CyclicList(x1[4]))=java.lang.Object(CyclicList(x1[5])) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

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

(26)    (>(x0[4], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

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

(27)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x1[4] + [bni_24]x0[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(28)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x1[4] + [bni_24]x0[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(29)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)Bound*bni_24] + [(-1)bni_24]x1[4] + [bni_24]x0[4] ≥ 0∧[(-1)bso_25] ≥ 0)

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

(30)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)bni_24] = 0∧[(-1)Bound*bni_24] + [bni_24]x0[4] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

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

(31)    (x0[4] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)bni_24] = 0∧[(-1)Bound*bni_24 + bni_24] + [bni_24]x0[4] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x2), java.lang.Object(CyclicList(x1))) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:

(32)    (COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥))

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

(33)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(34)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(35)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[1 + (-1)bso_27] ≥ 0)

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

(36)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))), COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) which results in the following constraint:

(37)    (>(x0[6], 0)=TRUE567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR))))=567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥))

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

(38)    (>(x0[6], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥))

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

(39)    (x0[6] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

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

(40)    (x0[6] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

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

(41)    (x0[6] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

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

(42)    (x0[6] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) which results in the following constraint:

(43)    (COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥))

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

(44)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(-1)bso_31] ≥ 0)

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

(45)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(-1)bso_31] ≥ 0)

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

(46)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(-1)bso_31] ≥ 0)

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

(47)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧0 = 0∧[(-1)bso_31] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → COND_567_1_MAIN_INVOKEMETHOD(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2))
• (x0[0] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[(-1)bni_16] = 0∧0 = 0∧[(-1)Bound*bni_16 + bni_16] + [bni_16]x0[0] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

• COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(x2)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x3), java.lang.Object(x2))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1))
• (x0[2] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[(-1)bni_20] = 0∧[(-1)Bound*bni_20 + bni_20] + [bni_20]x0[2] ≥ 0∧0 = 0∧[(-1)bso_21] ≥ 0)

• COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1)) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1)))
• (x0[4] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[(-1)bni_24] = 0∧[(-1)Bound*bni_24 + bni_24] + [bni_24]x0[4] ≥ 0∧0 = 0∧[(-1)bso_25] ≥ 0)

• COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(x1))), java.lang.Object(CyclicList(x1))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), x2), java.lang.Object(CyclicList(x1)))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0, 0), 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))
• (x0[6] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧[(2)bni_28 + (-1)Bound*bni_28] + [bni_28]x0[6] ≥ 0∧[1 + (-1)bso_29] ≥ 0)

• COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0, -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))), ≥)∧0 = 0∧[(-1)bso_31] ≥ 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(567_1_MAIN_INVOKEMETHOD(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(567_0_get_Load(x1, x2)) = [-1] + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(CyclicList(x1)) = x1
POL(COND_567_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(EOR) = [-1]
POL(COND_567_1_MAIN_INVOKEMETHOD1(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(COND_567_1_MAIN_INVOKEMETHOD2(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(COND_567_1_MAIN_INVOKEMETHOD3(x1, x2, x3)) = [-1] + [-1]x2

The following pairs are in P>:

COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))
COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

The following pairs are in Pbound:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → COND_567_1_MAIN_INVOKEMETHOD3(>(x0[6], 0), 567_0_get_Load(x0[6], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

The following pairs are in P:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[7], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

There are no usable rules.

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

R is empty.

The integer pair graph contains the following rules and edges:
(0): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(x0[0] > 0, 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))
(2): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(x0[2] > 0, 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(4): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(x0[4] > 0, 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(7): COND_567_1_MAIN_INVOKEMETHOD3(TRUE, 567_0_get_Load(x0[7], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR)))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(CyclicList(java.lang.Object(EOR))))

(1) -> (0), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x2[1]) →* java.lang.Object(x2[0])))

(3) -> (0), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x1[3]) →* java.lang.Object(x2[0])))

(5) -> (0), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(x2[0])))

(7) -> (0), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →* java.lang.Object(x2[0])))

(0) -> (1), if ((x0[0] > 0* TRUE)∧(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))) →* 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))))∧(java.lang.Object(x2[0]) →* java.lang.Object(x2[1])))

(1) -> (2), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →* java.lang.Object(x1[2])))

(3) -> (2), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[3]) →* java.lang.Object(x1[2])))

(5) -> (2), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(x1[2])))

(7) -> (2), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →* java.lang.Object(x1[2])))

(2) -> (3), if ((x0[2] > 0* TRUE)∧(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[2]) →* java.lang.Object(x1[3])))

(1) -> (4), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x2[1]) →* java.lang.Object(CyclicList(x1[4]))))

(3) -> (4), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x1[3]) →* java.lang.Object(CyclicList(x1[4]))))

(5) -> (4), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(CyclicList(x1[4]))))

(7) -> (4), if ((567_0_get_Load(x0[7] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(java.lang.Object(EOR))) →* java.lang.Object(CyclicList(x1[4]))))

(4) -> (5), if ((x0[4] > 0* TRUE)∧(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))) →* 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))))∧(java.lang.Object(CyclicList(x1[4])) →* java.lang.Object(CyclicList(x1[5]))))

The set Q is empty.

### (8) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(4): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(x0[4] > 0, 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(2): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(x0[2] > 0, 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))
(0): 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(x0[0] > 0, 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))

(1) -> (0), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x2[1]) →* java.lang.Object(x2[0])))

(3) -> (0), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(x1[3]) →* java.lang.Object(x2[0])))

(5) -> (0), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(x2[0])))

(0) -> (1), if ((x0[0] > 0* TRUE)∧(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))) →* 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))))∧(java.lang.Object(x2[0]) →* java.lang.Object(x2[1])))

(1) -> (2), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x2[1]) →* java.lang.Object(x1[2])))

(3) -> (2), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[3]) →* java.lang.Object(x1[2])))

(5) -> (2), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(x1[2])))

(2) -> (3), if ((x0[2] > 0* TRUE)∧(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))))∧(java.lang.Object(x1[2]) →* java.lang.Object(x1[3])))

(1) -> (4), if ((567_0_get_Load(x0[1] + -1, x3[1]) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x2[1]) →* java.lang.Object(CyclicList(x1[4]))))

(3) -> (4), if ((567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(x1[3]) →* java.lang.Object(CyclicList(x1[4]))))

(5) -> (4), if ((567_0_get_Load(x0[5] + -1, x2[5]) →* 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))))∧(java.lang.Object(CyclicList(x1[5])) →* java.lang.Object(CyclicList(x1[4]))))

(4) -> (5), if ((x0[4] > 0* TRUE)∧(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))) →* 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))))∧(java.lang.Object(CyclicList(x1[4])) →* java.lang.Object(CyclicList(x1[5]))))

The set Q is empty.

### (10) IDPNonInfProof (SOUND transformation)

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

For Pair COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:

(1)    (COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5])))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥))

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

(2)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(3)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(4)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧[(-1)bso_17] ≥ 0)

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

(5)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))), COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5]))) which results in the following constraint:

(6)    (>(x0[4], 0)=TRUE567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4])))=567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5])))∧java.lang.Object(CyclicList(x1[4]))=java.lang.Object(CyclicList(x1[5])) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

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

(7)    (>(x0[4], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))≥COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥))

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

(8)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

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

(9)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

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

(10)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧[1 + (-1)bso_19] ≥ 0)

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

(11)    (x0[4] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧0 = 0∧[bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

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

(12)    (x0[4] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:

(13)    (COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥))

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

(14)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[(-1)bso_21] ≥ 0)

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

(15)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[(-1)bso_21] ≥ 0)

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

(16)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧[(-1)bso_21] ≥ 0)

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

(17)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])), COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) which results in the following constraint:

(18)    (>(x0[2], 0)=TRUE567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR))))=567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR))))∧java.lang.Object(x1[2])=java.lang.Object(x1[3]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

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

(19)    (>(x0[2], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))≥COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥))

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

(20)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

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

(21)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

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

(22)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

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

(23)    (x0[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧0 = 0∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

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

(24)    (x0[2] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧0 = 0∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

For Pair COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) the following chains were created:
• We consider the chain COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:

(25)    (COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥NonInfC∧COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1]))≥567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))∧(UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥))

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

(26)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[(-1)bso_25] ≥ 0)

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

(27)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[(-1)bso_25] ≥ 0)

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

(28)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧[(-1)bso_25] ≥ 0)

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

(29)    ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) the following chains were created:
• We consider the chain 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])), COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1])) which results in the following constraint:

(30)    (>(x0[0], 0)=TRUE567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0])))=567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1])))∧java.lang.Object(x2[0])=java.lang.Object(x2[1]) ⇒ 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

We simplified constraint (30) using rules (I), (II), (IV) which results in the following new constraint:

(31)    (>(x0[0], 0)=TRUE567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥NonInfC∧567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))≥COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))∧(UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥))

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

(32)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

(33)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

(34)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧[1 + (-1)bso_27] ≥ 0)

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

(35)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧0 = 0∧0 = 0∧[bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

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

(36)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧0 = 0∧0 = 0∧[(2)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_17] ≥ 0)

• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
• (x0[4] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))), ≥)∧0 = 0∧[(2)bni_18 + (-1)Bound*bni_18] + [bni_18]x0[4] ≥ 0∧0 = 0∧[1 + (-1)bso_19] ≥ 0)

• COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))), ≥)∧0 = 0∧0 = 0∧[(-1)bso_21] ≥ 0)

• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
• (x0[2] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))), ≥)∧0 = 0∧[(2)bni_22 + (-1)Bound*bni_22] + [bni_22]x0[2] ≥ 0∧0 = 0∧[1 + (-1)bso_23] ≥ 0)

• COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))
• ((UIncreasing(567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

• 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))
• (x0[0] ≥ 0 ⇒ (UIncreasing(COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))), ≥)∧0 = 0∧0 = 0∧[(2)bni_26 + (-1)Bound*bni_26] + [bni_26]x0[0] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_27] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_567_1_MAIN_INVOKEMETHOD2(x1, x2, x3)) = [-1] + [-1]x2
POL(567_0_get_Load(x1, x2)) = [-1] + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(CyclicList(x1)) = x1
POL(567_1_MAIN_INVOKEMETHOD(x1, x2)) = [-1]x1
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(COND_567_1_MAIN_INVOKEMETHOD1(x1, x2, x3)) = [-1] + [-1]x2
POL(EOR) = [-1]
POL(COND_567_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [-1] + [-1]x2

The following pairs are in P>:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))

The following pairs are in Pbound:

567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4]))) → COND_567_1_MAIN_INVOKEMETHOD2(>(x0[4], 0), 567_0_get_Load(x0[4], java.lang.Object(CyclicList(x1[4]))), java.lang.Object(CyclicList(x1[4])))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2])) → COND_567_1_MAIN_INVOKEMETHOD1(>(x0[2], 0), 567_0_get_Load(x0[2], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[2]))
567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0])) → COND_567_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 567_0_get_Load(x0[0], java.lang.Object(CyclicList(x1[0]))), java.lang.Object(x2[0]))

The following pairs are in P:

COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[5], -1), x2[5]), java.lang.Object(CyclicList(x1[5])))
COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[3], -1), java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(+(x0[1], -1), x3[1]), java.lang.Object(x2[1]))

There are no usable rules.

### (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:
(5): COND_567_1_MAIN_INVOKEMETHOD2(TRUE, 567_0_get_Load(x0[5], java.lang.Object(CyclicList(x1[5]))), java.lang.Object(CyclicList(x1[5]))) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[5] + -1, x2[5]), java.lang.Object(CyclicList(x1[5])))
(3): COND_567_1_MAIN_INVOKEMETHOD1(TRUE, 567_0_get_Load(x0[3], java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[3] + -1, java.lang.Object(CyclicList(java.lang.Object(EOR)))), java.lang.Object(x1[3]))
(1): COND_567_1_MAIN_INVOKEMETHOD(TRUE, 567_0_get_Load(x0[1], java.lang.Object(CyclicList(x1[1]))), java.lang.Object(x2[1])) → 567_1_MAIN_INVOKEMETHOD(567_0_get_Load(x0[1] + -1, x3[1]), java.lang.Object(x2[1]))

The set Q is empty.

### (12) IDependencyGraphProof (EQUIVALENT transformation)

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

### (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:
(0): 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(x0[0] > 0, 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))
(1): COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[1] + -1, java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))

(0) -> (1), if ((x0[0] > 0* TRUE)∧(160_0_create_Load(x0[0], java.lang.Object(x1[0])) →* 160_0_create_Load(x0[1], java.lang.Object(x1[1])))∧(java.lang.Object(ARRAY(x2[0], x3[0])) →* java.lang.Object(ARRAY(x2[1], x3[1]))))

(1) -> (0), if ((160_0_create_Load(x0[1] + -1, java.lang.Object(CyclicList)) →* 160_0_create_Load(x0[0], java.lang.Object(x1[0])))∧(java.lang.Object(ARRAY(x2[1], x3[1])) →* java.lang.Object(ARRAY(x2[0], x3[0]))))

The set Q is empty.

### (15) IDPNonInfProof (SOUND transformation)

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

For Pair 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0, 0), 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) the following chains were created:
• We consider the chain 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))), COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1]))) which results in the following constraint:

(1)    (>(x0[0], 0)=TRUE160_0_create_Load(x0[0], java.lang.Object(x1[0]))=160_0_create_Load(x0[1], java.lang.Object(x1[1]))∧java.lang.Object(ARRAY(x2[0], x3[0]))=java.lang.Object(ARRAY(x2[1], x3[1])) ⇒ 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥NonInfC∧160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))∧(UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥))

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

(2)    (>(x0[0], 0)=TRUE160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥NonInfC∧160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))≥COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))∧(UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥))

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

(3)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)

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

(4)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)

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

(5)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧[(-1)bso_14] ≥ 0)

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

(6)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧0 = 0∧[(3)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

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

(7)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧0 = 0∧[(4)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

For Pair COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0, -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2, x3))) the following chains were created:
• We consider the chain COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1]))) which results in the following constraint:

(8)    (COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1])))≥NonInfC∧COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1])))≥160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))∧(UIncreasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥))

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

(9)    ((UIncreasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧[1 + (-1)bso_16] ≥ 0)

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

(10)    ((UIncreasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧[1 + (-1)bso_16] ≥ 0)

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

(11)    ((UIncreasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧[1 + (-1)bso_16] ≥ 0)

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

(12)    ((UIncreasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0, 0), 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3)))
• (x0[0] ≥ 0 ⇒ (UIncreasing(COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))), ≥)∧0 = 0∧[(4)bni_13 + (-1)Bound*bni_13] + [bni_13]x0[0] ≥ 0∧0 = 0∧[(-1)bso_14] ≥ 0)

• COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0, java.lang.Object(x1)), java.lang.Object(ARRAY(x2, x3))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0, -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2, x3)))
• ((UIncreasing(160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_16] ≥ 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(160_1_MAIN_INVOKEMETHOD(x1, x2)) = [2] + [-1]x1
POL(160_0_create_Load(x1, x2)) = [-1] + [-1]x1
POL(java.lang.Object(x1)) = x1
POL(ARRAY(x1, x2)) = [-1]
POL(COND_160_1_MAIN_INVOKEMETHOD(x1, x2, x3)) = [2] + [-1]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(CyclicList) = [-1]

The following pairs are in P>:

COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(+(x0[1], -1), java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))

The following pairs are in Pbound:

160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))

The following pairs are in P:

160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(>(x0[0], 0), 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))

There are no usable rules.

### (17) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0]))) → COND_160_1_MAIN_INVOKEMETHOD(x0[0] > 0, 160_0_create_Load(x0[0], java.lang.Object(x1[0])), java.lang.Object(ARRAY(x2[0], x3[0])))

The set Q is empty.

### (18) IDependencyGraphProof (EQUIVALENT transformation)

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

### (20) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_160_1_MAIN_INVOKEMETHOD(TRUE, 160_0_create_Load(x0[1], java.lang.Object(x1[1])), java.lang.Object(ARRAY(x2[1], x3[1]))) → 160_1_MAIN_INVOKEMETHOD(160_0_create_Load(x0[1] + -1, java.lang.Object(CyclicList)), java.lang.Object(ARRAY(x2[1], x3[1])))

The set Q is empty.

### (21) IDependencyGraphProof (EQUIVALENT transformation)

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