(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Test7
`public class Test7 {    public static void main(String[] args) {	List[] ls = { List.mk(args.length), List.mk(args.length), List.mk(args.length) };	for (int k = 0; k < ls.length; k++) {	    int len = length(ls[0]);	    for (int i = 0; i < len; i++)		bubble(ls[0]);	}    }    private static void bubble(List l) {	for (List cursor = l; cursor != null && cursor.getTail() != null; cursor = cursor.getTail())	    if (cursor.head > cursor.getTail().head) {		int temp = cursor.head;		cursor.head = cursor.getTail().head;		cursor.getTail().head = temp;	    }    }    private static int length(List list) {	int len = 0;	while (list != null) {	    list = list.getTail();	    len++;	}	return len;    }}public class List {    public int head;    private List tail;    public List(int head, List tail) {	this.head = head;	this.tail = tail;    }    public List getTail() {	return tail;    }    public static List mk(int len) {	List result = null;	while (len-- > 0)	    result = new List(len, result);	return result;    }}`

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Test7.main([Ljava/lang/String;)V: Graph of 81 nodes with 1 SCC.

List.mk(I)LList;: Graph of 30 nodes with 1 SCC.

Test7.length(LList;)I: Graph of 27 nodes with 1 SCC.

Test7.bubble(LList;)V: Graph of 137 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 131 rules for P and 8 rules for R.

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

Filtered ground terms:

List(x1, x2, x3) → List(x2, x3)
Cond_3413_0_bubble_NULL3(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL3(x1, x3, x4)
3413_0_bubble_NULL(x1, x2, x3) → 3413_0_bubble_NULL(x2, x3)
Cond_3413_0_bubble_NULL2(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL2(x1, x3, x4)
Cond_3413_0_bubble_NULL1(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL1(x1, x3, x4)
Cond_3413_0_bubble_NULL(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL(x1, x3, x4)
3425_0_bubble_Return(x1) → 3425_0_bubble_Return

Filtered duplicate args:

Cond_3413_0_bubble_NULL3(x1, x2, x3) → Cond_3413_0_bubble_NULL3(x1, x3)
3413_0_bubble_NULL(x1, x2) → 3413_0_bubble_NULL(x2)
Cond_3413_0_bubble_NULL2(x1, x2, x3) → Cond_3413_0_bubble_NULL2(x1, x3)
Cond_3413_0_bubble_NULL1(x1, x2, x3) → Cond_3413_0_bubble_NULL1(x1, x3)
Cond_3413_0_bubble_NULL(x1, x2, x3) → Cond_3413_0_bubble_NULL(x1, x3)

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

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

Log for SCC 1:

Generated 19 rules for P and 3 rules for R.

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

Filtered ground terms:

816_0_length_Store(x1, x2) → 816_0_length_Store(x2)
732_0_length_NULL(x1, x2, x3) → 732_0_length_NULL(x2, x3)
List(x1, x2) → List(x2)
775_0_length_Return(x1) → 775_0_length_Return

Filtered duplicate args:

732_0_length_NULL(x1, x2) → 732_0_length_NULL(x2)

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

Log for SCC 2:

Generated 21 rules for P and 3 rules for R.

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

Filtered ground terms:

398_0_mk_Inc(x1, x2, x3, x4) → 398_0_mk_Inc(x2, x3, x4)
List(x1) → List
java.lang.Object(x1) → java.lang.Object
Cond_398_0_mk_Inc(x1, x2, x3, x4, x5) → Cond_398_0_mk_Inc(x1, x3, x4, x5)

Filtered duplicate args:

398_0_mk_Inc(x1, x2, x3) → 398_0_mk_Inc(x2, x3)
Cond_398_0_mk_Inc(x1, x2, x3, x4) → Cond_398_0_mk_Inc(x1, x3, x4)

Filtered unneeded arguments:

398_0_mk_Inc(x1, x2) → 398_0_mk_Inc(x2)
Cond_398_0_mk_Inc(x1, x2, x3) → Cond_398_0_mk_Inc(x1, x3)

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.

Log for SCC 3:

Generated 36 rules for P and 176 rules for R.

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

Filtered ground terms:

1190_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → 1190_0_main_GE(x2, x3, x4, x5, x6, x7)
ARRAY(x1, x2) → ARRAY(x2)
Cond_1243_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_1243_1_main_InvokeMethod(x1, x3, x4, x5, x6, x7)
3425_0_bubble_Return(x1) → 3425_0_bubble_Return
Cond_1190_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_1190_0_main_GE1(x1, x3, x4, x5, x6, x7, x8)
893_0_length_ConstantStackPush(x1, x2) → 893_0_length_ConstantStackPush(x2)
Cond_1190_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_1190_0_main_GE(x1, x3, x4, x5, x6, x7, x8)
775_0_length_Return(x1, x2) → 775_0_length_Return(x2)
3513_0_bubble_Return(x1) → 3513_0_bubble_Return
732_0_length_NULL(x1, x2, x3, x4) → 732_0_length_NULL(x2, x3, x4)
Cond_732_0_length_NULL(x1, x2, x3, x4, x5) → Cond_732_0_length_NULL(x1, x4)
List(x1) → List
Cond_805_1_length_InvokeMethod(x1, x2, x3, x4) → Cond_805_1_length_InvokeMethod(x1, x2, x3)
805_0_getTail_Return(x1, x2) → 805_0_getTail_Return(x2)
805_1_length_InvokeMethod(x1, x2, x3) → 805_1_length_InvokeMethod(x1, x2)
3413_0_bubble_NULL(x1, x2, x3) → 3413_0_bubble_NULL(x2, x3)
Cond_3746_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3746_0_bubble_LE(x1, x4, x5)
3746_0_bubble_LE(x1, x2, x3, x4) → 3746_0_bubble_LE(x3, x4)
Cond_3738_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3738_0_bubble_LE(x1, x4, x5)
3738_0_bubble_LE(x1, x2, x3, x4) → 3738_0_bubble_LE(x3, x4)
Cond_3756_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3756_0_bubble_LE(x1, x4, x5)
3756_0_bubble_LE(x1, x2, x3, x4) → 3756_0_bubble_LE(x3, x4)
Cond_3752_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3752_0_bubble_LE(x1, x4, x5)
3752_0_bubble_LE(x1, x2, x3, x4) → 3752_0_bubble_LE(x3, x4)
Cond_3728_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3728_0_bubble_LE(x1, x4, x5)
3728_0_bubble_LE(x1, x2, x3, x4) → 3728_0_bubble_LE(x3, x4)
Cond_3723_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3723_0_bubble_LE(x1, x4, x5)
3723_0_bubble_LE(x1, x2, x3, x4) → 3723_0_bubble_LE(x3, x4)

Filtered duplicate args:

1190_0_main_GE(x1, x2, x3, x4, x5, x6) → 1190_0_main_GE(x1, x2, x5, x6)
Cond_1190_0_main_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_1190_0_main_GE1(x1, x2, x3, x6, x7)
Cond_1190_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_1190_0_main_GE(x1, x2, x3, x6, x7)
732_0_length_NULL(x1, x2, x3) → 732_0_length_NULL(x2, x3)
3413_0_bubble_NULL(x1, x2) → 3413_0_bubble_NULL(x2)

Filtered unneeded arguments:

Cond_1190_0_main_GE(x1, x2, x3, x4, x5) → Cond_1190_0_main_GE(x1, x2, x3)
Cond_3723_0_bubble_LE(x1, x2, x3) → Cond_3723_0_bubble_LE(x1)
Cond_3728_0_bubble_LE(x1, x2, x3) → Cond_3728_0_bubble_LE(x1)
Cond_3752_0_bubble_LE(x1, x2, x3) → Cond_3752_0_bubble_LE(x1)
Cond_3756_0_bubble_LE(x1, x2, x3) → Cond_3756_0_bubble_LE(x1)
Cond_3738_0_bubble_LE(x1, x2, x3) → Cond_3738_0_bubble_LE(x1)
Cond_3746_0_bubble_LE(x1, x2, x3) → Cond_3746_0_bubble_LE(x1)

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

Finished conversion. Obtained 4 rules for P and 22 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

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(x2[0] <= x1[0], java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
(1): COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
(2): 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(x2[2] > x1[2], java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
(3): COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
(4): 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))
(5): 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(x2[5] > x1[5], java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))
(6): COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

(0) -> (1), if ((x2[0] <= x1[0]* TRUE)∧(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) →* java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))))

(1) -> (0), if ((java.lang.Object(List(x0[1], x1[1])) →* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))))

(1) -> (2), if ((java.lang.Object(List(x0[1], x1[1])) →* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))))

(1) -> (5), if ((java.lang.Object(List(x0[1], x1[1])) →* java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))))

(2) -> (3), if ((x2[2] > x1[2]* TRUE)∧(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) →* java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))))

(3) -> (0), if ((java.lang.Object(List(x0[3], x2[3])) →* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))))

(3) -> (2), if ((java.lang.Object(List(x0[3], x2[3])) →* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))))

(3) -> (5), if ((java.lang.Object(List(x0[3], x2[3])) →* java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))))

(4) -> (0), if ((java.lang.Object(List(x0[4], x1[4])) →* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))))

(4) -> (2), if ((java.lang.Object(List(x0[4], x1[4])) →* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))))

(4) -> (5), if ((java.lang.Object(List(x0[4], x1[4])) →* java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))))

(5) -> (6), if ((x2[5] > x1[5]* TRUE)∧(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) →* java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))))

(6) -> (4), if ((java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])) →* java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))))

The set Q consists of the following terms:
3413_0_bubble_NULL(NULL)

(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 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:
• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))) which results in the following constraint:

(1)    (<=(x2[0], x1[0])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])) ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))∧(UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥))

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

(2)    (<=(x2[0], x1[0])=TRUE3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))∧(UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥))

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

(3)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(20)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

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

(4)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(20)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

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

(5)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(20)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

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

(6)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_23] ≥ 0∧[(20)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_24] ≥ 0)

For Pair COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1))) the following chains were created:
• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) which results in the following constraint:

(7)    (<=(x2[0], x1[0])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x2[0]1)) ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

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

(8)    (<=(x2[0], x1[0])=TRUECOND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])), x2[0])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])), x2[0])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

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

(9)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[0]1 ≥ 0∧[63 + (-1)bso_26] + [48]x0[0]1 ≥ 0)

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

(10)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[0]1 ≥ 0∧[63 + (-1)bso_26] + [48]x0[0]1 ≥ 0)

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

(11)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[0]1 ≥ 0∧[63 + (-1)bso_26] + [48]x0[0]1 ≥ 0)

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

(12)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) which results in the following constraint:

(13)    (<=(x2[0], x1[0])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

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

(14)    (<=(x2[0], x1[0])=TRUECOND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])), x2[0])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])), x2[0])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

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

(15)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[2] ≥ 0∧[63 + (-1)bso_26] + [48]x0[2] ≥ 0)

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

(16)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[2] ≥ 0∧[63 + (-1)bso_26] + [48]x0[2] ≥ 0)

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

(17)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[2] ≥ 0∧[63 + (-1)bso_26] + [48]x0[2] ≥ 0)

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

(18)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) which results in the following constraint:

(19)    (<=(x2[0], x1[0])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

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

(20)    (<=(x2[0], x1[0])=TRUECOND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[0])), x2[0])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[0])), x2[0])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[0])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

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

(21)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[5] ≥ 0∧[63 + (-1)bso_26] + [48]x0[5] ≥ 0)

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

(22)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[5] ≥ 0∧[63 + (-1)bso_26] + [48]x0[5] ≥ 0)

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

(23)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[5] ≥ 0∧[63 + (-1)bso_26] + [48]x0[5] ≥ 0)

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

(24)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

For Pair 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL1(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:
• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))) which results in the following constraint:

(25)    (>(x2[2], x1[2])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])) ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))∧(UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥))

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

(26)    (>(x2[2], x1[2])=TRUE3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))∧(UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥))

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

(27)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(20)bni_27 + (-1)Bound*bni_27] + [(16)bni_27]x0[2] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

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

(28)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(20)bni_27 + (-1)Bound*bni_27] + [(16)bni_27]x0[2] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

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

(29)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(20)bni_27 + (-1)Bound*bni_27] + [(16)bni_27]x0[2] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

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

(30)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_27] ≥ 0∧[(20)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_28] ≥ 0)

For Pair COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x2))) the following chains were created:
• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) which results in the following constraint:

(31)    (>(x2[2], x1[2])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

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

(32)    (>(x2[2], x1[2])=TRUECOND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x1[2])), x2[2])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x1[2])), x2[2])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[2])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

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

(33)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[0] ≥ 0∧[63 + (-1)bso_30] + [48]x0[0] ≥ 0)

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

(34)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[0] ≥ 0∧[63 + (-1)bso_30] + [48]x0[0] ≥ 0)

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

(35)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[0] ≥ 0∧[63 + (-1)bso_30] + [48]x0[0] ≥ 0)

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

(36)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)

• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) which results in the following constraint:

(37)    (>(x2[2], x1[2])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x2[2]1)) ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

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

(38)    (>(x2[2], x1[2])=TRUECOND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x1[2])), x2[2])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x1[2])), x2[2])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x2[2])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

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

(39)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[2]1 ≥ 0∧[63 + (-1)bso_30] + [48]x0[2]1 ≥ 0)

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

(40)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[2]1 ≥ 0∧[63 + (-1)bso_30] + [48]x0[2]1 ≥ 0)

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

(41)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[2]1 ≥ 0∧[63 + (-1)bso_30] + [48]x0[2]1 ≥ 0)

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

(42)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)

• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) which results in the following constraint:

(43)    (>(x2[2], x1[2])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

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

(44)    (>(x2[2], x1[2])=TRUECOND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[2])), x2[2])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[2])), x2[2])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[2])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

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

(45)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[5] ≥ 0∧[63 + (-1)bso_30] + [48]x0[5] ≥ 0)

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

(46)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[5] ≥ 0∧[63 + (-1)bso_30] + [48]x0[5] ≥ 0)

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

(47)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[5] ≥ 0∧[63 + (-1)bso_30] + [48]x0[5] ≥ 0)

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

(48)    (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)

For Pair 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1))) the following chains were created:
• We consider the chain COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) which results in the following constraint:

(49)    (java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) ⇒ 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

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

(50)    (5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[6])), x1[6])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[6])), x1[6])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[6])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

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

(51)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[0] ≥ 0)

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

(52)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[0] ≥ 0)

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

(53)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[0] ≥ 0)

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

(54)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)

• We consider the chain COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) which results in the following constraint:

(55)    (java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) ⇒ 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

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

(56)    (5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[6])), x1[6])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[6])), x1[6])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[6])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

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

(57)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[2] ≥ 0)

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

(58)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[2] ≥ 0)

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

(59)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[2] ≥ 0)

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

(60)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)

• We consider the chain COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) which results in the following constraint:

(61)    (java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

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

(62)    (5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[6])), x1[6])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[6])), x1[6])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[6])))∧(UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

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

(63)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[5] ≥ 0)

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

(64)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[5] ≥ 0)

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

(65)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[5] ≥ 0)

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

(66)    ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)

For Pair 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL2(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:
• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))), COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))) which results in the following constraint:

(67)    (>(x2[5], x1[5])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))=java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])) ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))∧(UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥))

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

(68)    (>(x2[5], x1[5])=TRUE3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))∧(UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥))

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

(69)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧[(20)bni_33 + (-1)Bound*bni_33] + [(16)bni_33]x0[5] ≥ 0∧[1 + (-1)bso_34] ≥ 0)

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

(70)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧[(20)bni_33 + (-1)Bound*bni_33] + [(16)bni_33]x0[5] ≥ 0∧[1 + (-1)bso_34] ≥ 0)

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

(71)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧[(20)bni_33 + (-1)Bound*bni_33] + [(16)bni_33]x0[5] ≥ 0∧[1 + (-1)bso_34] ≥ 0)

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

(72)    (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_33] ≥ 0∧[(20)bni_33 + (-1)Bound*bni_33] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_34] ≥ 0)

For Pair COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1))) the following chains were created:
• We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))), COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))) which results in the following constraint:

(73)    (>(x2[5], x1[5])=TRUEjava.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))=java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))∧java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])) ⇒ COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥NonInfC∧COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))∧(UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥))

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

(74)    (>(x2[5], x1[5])=TRUECOND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[5], x2[5])), x1[5])))∧(UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥))

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

(75)    (0 ≥ 0 ⇒ (UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧[(19)bni_35 + (-1)Bound*bni_35] + [(16)bni_35]x0[5] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(76)    (0 ≥ 0 ⇒ (UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧[(19)bni_35 + (-1)Bound*bni_35] + [(16)bni_35]x0[5] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(77)    (0 ≥ 0 ⇒ (UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧[(19)bni_35 + (-1)Bound*bni_35] + [(16)bni_35]x0[5] ≥ 0∧[(-1)bso_36] ≥ 0)

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

(78)    (0 ≥ 0 ⇒ (UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_35] ≥ 0∧[(19)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_36] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
• (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_23] ≥ 0∧[(20)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_24] ≥ 0)

• COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)))
• (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

• 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL1(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
• (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_27] ≥ 0∧[(20)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_28] ≥ 0)

• COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x2)))
• (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
• (0 ≥ 0 ⇒ (UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)

• 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)))
• ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
• ((UIncreasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)

• 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL2(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
• (0 ≥ 0 ⇒ (UIncreasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_33] ≥ 0∧[(20)bni_33 + (-1)Bound*bni_33] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_34] ≥ 0)

• COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1)))
• (0 ≥ 0 ⇒ (UIncreasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_35] ≥ 0∧[(19)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_36] ≥ 0)

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

POL(TRUE) = 0
POL(FALSE) = 0
POL(3413_0_bubble_NULL(x1)) = 0
POL(NULL) = 0
POL(3425_0_bubble_Return) = 0
POL(3413_0_BUBBLE_NULL(x1)) = x1
POL(java.lang.Object(x1)) = [2]x1
POL(List(x1, x2)) = [2] + [2]x1
POL(COND_3413_0_BUBBLE_NULL(x1, x2)) = [-1] + x2
POL(<=(x1, x2)) = 0
POL(COND_3413_0_BUBBLE_NULL1(x1, x2)) = [-1] + x2
POL(>(x1, x2)) = 0
POL(COND_3413_0_BUBBLE_NULL2(x1, x2)) = [-1] + x2

The following pairs are in P>:

3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))

The following pairs are in Pbound:

3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))
COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

The following pairs are in P:

COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

There are no usable rules.

(8) Obligation:

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

The following domains are used:
none

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

The set Q consists of the following terms:
3413_0_bubble_NULL(NULL)

(9) IDependencyGraphProof (EQUIVALENT transformation)

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

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

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(4): 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))

The set Q consists of the following terms:
3413_0_bubble_NULL(NULL)

(12) IDependencyGraphProof (EQUIVALENT transformation)

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

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

The ITRS R consists of the following rules:
732_0_length_NULL(NULL) → 775_0_length_Return

The integer pair graph contains the following rules and edges:
(0): 816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
(1): 732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
(2): 732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

(0) -> (1), if ((x0[0]* java.lang.Object(List(x0[1]))))

(0) -> (2), if ((x0[0]* java.lang.Object(List(x0[2]))))

(1) -> (1), if ((x0[1]* java.lang.Object(List(x0[1]'))))

(1) -> (2), if ((x0[1]* java.lang.Object(List(x0[2]))))

(2) -> (0), if ((x0[2]* x0[0]))

The set Q consists of the following terms:
732_0_length_NULL(NULL)

(15) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

The TRS R consists of the following rules:

732_0_length_NULL(NULL) → 775_0_length_Return

The set Q consists of the following terms:

732_0_length_NULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

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

732_0_length_NULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(19) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

732_0_length_NULL(NULL)

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• 732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])
The graph contains the following edges 1 > 1

• 732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
The graph contains the following edges 1 > 1

• 816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
The graph contains the following edges 1 >= 1

(23) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(x0[0] > 0, x0[0])
(1): COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(x0[1] + -1)

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

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

The set Q is empty.

(24) 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 398_0_MK_INC(x0) → COND_398_0_MK_INC(>(x0, 0), x0) the following chains were created:
• We consider the chain 398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(>(x0[0], 0), x0[0]), COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(+(x0[1], -1)) which results in the following constraint:

(1)    (>(x0[0], 0)=TRUEx0[0]=x0[1]398_0_MK_INC(x0[0])≥NonInfC∧398_0_MK_INC(x0[0])≥COND_398_0_MK_INC(>(x0[0], 0), x0[0])∧(UIncreasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥))

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

(2)    (>(x0[0], 0)=TRUE398_0_MK_INC(x0[0])≥NonInfC∧398_0_MK_INC(x0[0])≥COND_398_0_MK_INC(>(x0[0], 0), x0[0])∧(UIncreasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥))

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

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

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

(4)    (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 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_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

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

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

For Pair COND_398_0_MK_INC(TRUE, x0) → 398_0_MK_INC(+(x0, -1)) the following chains were created:
• We consider the chain COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(+(x0[1], -1)) which results in the following constraint:

(7)    (COND_398_0_MK_INC(TRUE, x0[1])≥NonInfC∧COND_398_0_MK_INC(TRUE, x0[1])≥398_0_MK_INC(+(x0[1], -1))∧(UIncreasing(398_0_MK_INC(+(x0[1], -1))), ≥))

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

(8)    ((UIncreasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

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

(9)    ((UIncreasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

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

(10)    ((UIncreasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

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

(11)    ((UIncreasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

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

• COND_398_0_MK_INC(TRUE, x0) → 398_0_MK_INC(+(x0, -1))
• ((UIncreasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

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

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

The following pairs are in P>:

COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(+(x0[1], -1))

The following pairs are in Pbound:

398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(>(x0[0], 0), x0[0])

The following pairs are in P:

398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(>(x0[0], 0), x0[0])

There are no usable rules.

(26) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(x0[0] > 0, x0[0])

The set Q is empty.

(27) IDependencyGraphProof (EQUIVALENT transformation)

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

(29) Obligation:

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(x0[1] + -1)

The set Q is empty.

(30) IDependencyGraphProof (EQUIVALENT transformation)

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

(32) Obligation:

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

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
(1): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(x6[1] >= x5[1] && x4[1] >= 0 && 3 > x4[1] + 1, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])
(2): COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2] + 1, x1[2])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])

(0) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x5[0]* x4[1])∧(0* x6[1])∧(x0[0]* x5[1]))

(0) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x5[0]* x4[3])∧(0* x6[3])∧(x0[0]* x5[3]))

(1) -> (2), if ((x6[1] >= x5[1] && x4[1] >= 0 && 3 > x4[1] + 1* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →* java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))))∧(x4[1]* x4[2])∧(x6[1]* x6[2])∧(x5[1]* x5[2]))

(2) -> (0), if ((893_0_length_ConstantStackPush(x1[2]) →* 775_0_length_Return(x0[0]))∧(java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))) →* java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))))∧(x4[2] + 1* x5[0])∧(x1[2]* x2[0]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

(6) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x4[6]* x4[1])∧(x6[6] + 1* x6[1])∧(x5[6]* x5[1]))

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(33) 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 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0), java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, x2) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, 0, x0) the following chains were created:
• We consider the chain 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0]) which results in the following constraint:

(1)    (893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0])≥NonInfC∧893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])∧(UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥))

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

(2)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧[(-1)bso_42] ≥ 0)

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

(3)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧[(-1)bso_42] ≥ 0)

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

(4)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧[(-1)bso_42] ≥ 0)

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

(5)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE(&&(&&(>=(x6, x5), >=(x4, 0)), >(3, +(x4, 1))), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) the following chains were created:
• We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]), COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2]) which results in the following constraint:

(6)    (&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1)))=TRUEjava.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1])))=java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2])))∧x4[1]=x4[2]x6[1]=x6[2]x5[1]=x5[2]1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])∧(UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥))

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

(7)    (>(3, +(x4[1], 1))=TRUE>=(x6[1], x5[1])=TRUE>=(x4[1], 0)=TRUE1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])∧(UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥))

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

(8)    ([1] + [-1]x4[1] ≥ 0∧x6[1] + [-1]x5[1] ≥ 0∧x4[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

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

(9)    ([1] + [-1]x4[1] ≥ 0∧x6[1] + [-1]x5[1] ≥ 0∧x4[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

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

(10)    ([1] + [-1]x4[1] ≥ 0∧x6[1] + [-1]x5[1] ≥ 0∧x4[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

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

(11)    ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

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

(12)    ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

(13)    ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

For Pair COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), +(x4, 1), x1) the following chains were created:
• We consider the chain COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2]) which results in the following constraint:

(14)    (COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2])≥NonInfC∧COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2])≥893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])∧(UIncreasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥))

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

(15)    ((UIncreasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧[1 + (-1)bso_46] ≥ 0)

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

(16)    ((UIncreasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧[1 + (-1)bso_46] ≥ 0)

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

(17)    ((UIncreasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧[1 + (-1)bso_46] ≥ 0)

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

(18)    ((UIncreasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_46] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE1(<(x6, x5), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) the following chains were created:
• We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]), COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:

(19)    (<(x6[3], x5[3])=TRUEjava.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))=java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))∧x4[3]=x4[4]x6[3]=x6[4]x5[3]=x5[4]1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

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

(20)    (<(x6[3], x5[3])=TRUE1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

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

(21)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x4[3] ≥ 0∧[(-1)bso_48] ≥ 0)

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

(22)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x4[3] ≥ 0∧[(-1)bso_48] ≥ 0)

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

(23)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x4[3] ≥ 0∧[(-1)bso_48] ≥ 0)

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

(24)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

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

(25)    (x5[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

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

(26)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

(27)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

For Pair COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) the following chains were created:
• We consider the chain COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:

(28)    (COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥NonInfC∧COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])∧(UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥))

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

(29)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_50] ≥ 0)

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

(30)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_50] ≥ 0)

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

(31)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_50] ≥ 0)

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

(32)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)

For Pair 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6, 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) the following chains were created:
• We consider the chain 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]), COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:

(33)    (>=(x6[5], 0)=TRUEjava.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))=java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))∧x4[5]=x4[6]x5[5]=x5[6]x6[5]=x6[6]x1[5]=x1[6]1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

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

(34)    (>=(x6[5], 0)=TRUE1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

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

(35)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x4[5] ≥ 0∧[(-1)bso_52] ≥ 0)

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

(36)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x4[5] ≥ 0∧[(-1)bso_52] ≥ 0)

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

(37)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x4[5] ≥ 0∧[(-1)bso_52] ≥ 0)

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

(38)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧0 = 0∧[(-1)bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

For Pair COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7, x2, x3))), x4, +(x6, 1), x5) the following chains were created:
• We consider the chain COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:

(39)    (COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥NonInfC∧COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])∧(UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥))

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

(40)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[(-1)bso_54] ≥ 0)

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

(41)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[(-1)bso_54] ≥ 0)

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

(42)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[(-1)bso_54] ≥ 0)

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

(43)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0), java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, x2) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, 0, x0)
• ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)

• 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE(&&(&&(>=(x6, x5), >=(x4, 0)), >(3, +(x4, 1))), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5)
• ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)
• ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

• COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), +(x4, 1), x1)
• ((UIncreasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_46] ≥ 0)

• 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE1(<(x6, x5), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5)
• (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)
• (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

• COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1)
• ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)

• 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6, 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1)
• (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧0 = 0∧[(-1)bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

• COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7, x2, x3))), x4, +(x6, 1), x5)
• ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 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(893_0_length_ConstantStackPush(x1)) = [-1]
POL(732_0_length_NULL(x1, x2)) = [-1] + [-1]x1
POL(0) = 0
POL(3413_0_bubble_NULL(x1)) = [-1]
POL(NULL) = [-1]
POL(3425_0_bubble_Return) = [-1]
POL(java.lang.Object(x1)) = [-1]
POL(List) = [-1]
POL(3723_0_bubble_LE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(3728_0_bubble_LE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(Cond_3723_0_bubble_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(>=(x1, x2)) = [-1]
POL(<(x1, x2)) = [-1]
POL(3513_0_bubble_Return) = [-1]
POL(775_0_length_Return(x1)) = x1
POL(805_1_length_InvokeMethod(x1, x2)) = [-1] + [-1]x2
POL(805_0_getTail_Return(x1)) = [-1]
POL(Cond_805_1_length_InvokeMethod(x1, x2, x3)) = [-1] + [-1]x3
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(Cond_732_0_length_NULL(x1, x2, x3)) = [-1] + [-1]x2
POL(893_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4)) = [-1] + [-1]x3
POL(ARRAY(x1)) = [-1]
POL(DATA_3(x1, x2, x3)) = [-1]
POL(1190_0_MAIN_GE(x1, x2, x3, x4)) = [-1] + [-1]x2
POL(COND_1190_0_MAIN_GE(x1, x2, x3, x4, x5)) = [-1] + [-1]x3
POL(&&(x1, x2)) = [-1]
POL(>(x1, x2)) = [-1]
POL(3) = [3]
POL(COND_1190_0_MAIN_GE1(x1, x2, x3, x4, x5)) = [-1] + [-1]x3
POL(1243_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6)) = [-1] + [-1]x3
POL(COND_1243_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6, x7)) = [-1] + [-1]x4

The following pairs are in P>:

COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])

The following pairs are in Pbound:

1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])

The following pairs are in P:

893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])

There are no usable rules.

(35) Obligation:

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

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
(1): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(x6[1] >= x5[1] && x4[1] >= 0 && 3 > x4[1] + 1, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])

(0) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x5[0]* x4[1])∧(0* x6[1])∧(x0[0]* x5[1]))

(6) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x4[6]* x4[1])∧(x6[6] + 1* x6[1])∧(x5[6]* x5[1]))

(0) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x5[0]* x4[3])∧(0* x6[3])∧(x0[0]* x5[3]))

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(36) IDependencyGraphProof (EQUIVALENT transformation)

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

(37) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(40) 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_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) the following chains were created:
• We consider the chain COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:

(1)    (COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥NonInfC∧COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])∧(UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥))

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

(2)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_25] ≥ 0)

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

(3)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_25] ≥ 0)

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

(4)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_25] ≥ 0)

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

(5)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)

For Pair 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) the following chains were created:
• We consider the chain 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]), COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:

(6)    (>=(x6[5], 0)=TRUEjava.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))=java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))∧x4[5]=x4[6]x5[5]=x5[6]x6[5]=x6[6]x1[5]=x1[6]1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

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

(7)    (>=(x6[5], 0)=TRUE1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

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

(8)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x5[5] + [(-1)bni_26]x6[5] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(9)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x5[5] + [(-1)bni_26]x6[5] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(10)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x5[5] + [(-1)bni_26]x6[5] ≥ 0∧[(-1)bso_27] ≥ 0)

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

(11)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x6[5] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) the following chains were created:
• We consider the chain COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:

(12)    (COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥NonInfC∧COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])∧(UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥))

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

(13)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_29] ≥ 0)

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

(14)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_29] ≥ 0)

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

(15)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_29] ≥ 0)

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

(16)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) the following chains were created:
• We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]), COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:

(17)    (<(x6[3], x5[3])=TRUEjava.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))=java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))∧x4[3]=x4[4]x6[3]=x6[4]x5[3]=x5[4]1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

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

(18)    (<(x6[3], x5[3])=TRUE1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

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

(19)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x6[3] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(20)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x6[3] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(21)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x6[3] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(22)    (x5[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

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

(23)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

(24)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])
• ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)

• 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
• (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x6[5] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

• COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
• ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

• 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
• (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)
• (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 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(3413_0_bubble_NULL(x1)) = [-1]
POL(NULL) = [-1]
POL(3425_0_bubble_Return) = [-1]
POL(java.lang.Object(x1)) = [-1]
POL(List) = [-1]
POL(3723_0_bubble_LE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(Cond_3723_0_bubble_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(>=(x1, x2)) = [-1]
POL(3728_0_bubble_LE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(<(x1, x2)) = [-1]
POL(3513_0_bubble_Return) = [-1]
POL(COND_1243_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x5 + [-1]x6
POL(ARRAY(x1)) = [-1]
POL(DATA_3(x1, x2, x3)) = [-1]
POL(1190_0_MAIN_GE(x1, x2, x3, x4)) = [-1] + [-1]x3 + x4
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(1243_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6)) = [-1] + x4 + [-1]x5
POL(0) = 0
POL(COND_1190_0_MAIN_GE1(x1, x2, x3, x4, x5)) = [-1] + x5 + [-1]x4

The following pairs are in P>:

COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])

The following pairs are in Pbound:

1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

The following pairs are in P:

1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

There are no usable rules.

(42) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(43) IDependencyGraphProof (EQUIVALENT transformation)

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

(45) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(46) IDependencyGraphProof (EQUIVALENT transformation)

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

(48) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
(2): COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2] + 1, x1[2])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])

(2) -> (0), if ((893_0_length_ConstantStackPush(x1[2]) →* 775_0_length_Return(x0[0]))∧(java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))) →* java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))))∧(x4[2] + 1* x5[0])∧(x1[2]* x2[0]))

(0) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x5[0]* x4[3])∧(0* x6[3])∧(x0[0]* x5[3]))

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(49) IDependencyGraphProof (EQUIVALENT transformation)

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

(50) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(51) UsableRulesProof (EQUIVALENT transformation)

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

(52) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6]* x4[3])∧(x6[6] + 1* x6[3])∧(x5[6]* x5[3]))

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(53) 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_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) the following chains were created:
• We consider the chain COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:

(1)    (COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥NonInfC∧COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])∧(UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥))

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

(2)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_22] ≥ 0)

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

(3)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_22] ≥ 0)

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

(4)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_22] ≥ 0)

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

(5)    ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

For Pair 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) the following chains were created:
• We consider the chain 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]), COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:

(6)    (>=(x6[5], 0)=TRUEjava.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))=java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))∧x4[5]=x4[6]x5[5]=x5[6]x6[5]=x6[6]x1[5]=x1[6]1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

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

(7)    (>=(x6[5], 0)=TRUE1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

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

(8)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x5[5] + [(-1)bni_23]x6[5] ≥ 0∧[(-1)bso_24] ≥ 0)

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

(9)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x5[5] + [(-1)bni_23]x6[5] ≥ 0∧[(-1)bso_24] ≥ 0)

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

(10)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x5[5] + [(-1)bni_23]x6[5] ≥ 0∧[(-1)bso_24] ≥ 0)

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

(11)    (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x6[5] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)

For Pair COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) the following chains were created:
• We consider the chain COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:

(12)    (COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥NonInfC∧COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])∧(UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥))

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

(13)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_26] ≥ 0)

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

(14)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_26] ≥ 0)

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

(15)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_26] ≥ 0)

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

(16)    ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) the following chains were created:
• We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]), COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:

(17)    (<(x6[3], x5[3])=TRUEjava.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))=java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))∧x4[3]=x4[4]x6[3]=x6[4]x5[3]=x5[4]1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

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

(18)    (<(x6[3], x5[3])=TRUE1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

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

(19)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x6[3] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

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

(20)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x6[3] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

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

(21)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x6[3] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

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

(22)    (x5[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

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

(23)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

(24)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])
• ((UIncreasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

• 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
• (x6[5] ≥ 0 ⇒ (UIncreasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x6[5] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)

• COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
• ((UIncreasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

• 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
• (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)
• (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (UIncreasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 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(3413_0_bubble_NULL(x1)) = [-1]
POL(NULL) = [-1]
POL(3425_0_bubble_Return) = [-1]
POL(java.lang.Object(x1)) = [-1]
POL(List) = [-1]
POL(3723_0_bubble_LE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(Cond_3723_0_bubble_LE(x1, x2, x3)) = [-1] + [-1]x3 + [-1]x2
POL(>=(x1, x2)) = [-1]
POL(3728_0_bubble_LE(x1, x2)) = [-1] + [-1]x2 + [-1]x1
POL(<(x1, x2)) = [-1]
POL(3513_0_bubble_Return) = [-1]
POL(COND_1243_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6, x7)) = [-1] + x5 + [-1]x6
POL(ARRAY(x1)) = [1]
POL(DATA_3(x1, x2, x3)) = [-1]
POL(1190_0_MAIN_GE(x1, x2, x3, x4)) = [-1] + [-1]x3 + x4
POL(+(x1, x2)) = x1 + x2
POL(1) = [1]
POL(1243_1_MAIN_INVOKEMETHOD(x1, x2, x3, x4, x5, x6)) = [-1] + x4 + [-1]x5
POL(0) = 0
POL(COND_1190_0_MAIN_GE1(x1, x2, x3, x4, x5)) = [-1] + x5 + [-1]x4

The following pairs are in P>:

COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])

The following pairs are in Pbound:

1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

The following pairs are in P:

1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

There are no usable rules.

(55) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(3) -> (4), if ((x6[3] < x5[3]* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3]* x4[4])∧(x6[3]* x6[4])∧(x5[3]* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(56) IDependencyGraphProof (EQUIVALENT transformation)

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

(58) Obligation:

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

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4]* x4[5])∧(x5[4]* x5[5])∧(x6[4]* x6[5])∧(x1[4]* x1[5]))

(5) -> (6), if ((x6[5] >= 0* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5]* x4[6])∧(x5[5]* x5[6])∧(x6[5]* x6[6])∧(x1[5]* x1[6]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(59) IDependencyGraphProof (EQUIVALENT transformation)

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