Termination proof of /tmp/tmpZHLT27/Test7.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 838 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 17 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 377 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 1140 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 TRUE

    ↳12 JBCTerminationSCC

        ↳13 SCCToIntTRSProof (⇒, 69 ms)

        ↳14 intTRS

        ↳15 PolynomialOrderProcessor (⇔, 0 ms)

        ↳16 YES

    ↳17 JBCTerminationSCC

        ↳18 SCCToIntTRSProof (⇒, 65 ms)

        ↳19 intTRS

        ↳20 PolynomialOrderProcessor (⇔, 0 ms)

        ↳21 YES

    ↳22 JBCTerminationSCC

        ↳23 SCCToIntTRSProof (⇒, 264 ms)

        ↳24 intTRS

        ↳25 PolynomialOrderProcessor (⇒, 0 ms)

        ↳26 intTRS

        ↳27 PolynomialOrderProcessor (⇔, 0 ms)

        ↳28 YES

(0) Obligation:

JBC Problem based on JBC Program:

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) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

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

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

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

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 4 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test7.bubble(LList;)V
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail, head]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 131 rules for P and 0 rules for R.

P rules:
f2085_0_bubble_NULL(EOS(STATIC_2085), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub)) → f2087_0_bubble_NULL(EOS(STATIC_2087), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub))
f2087_0_bubble_NULL(EOS(STATIC_2087), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub)) → f2090_0_bubble_Load(EOS(STATIC_2090), o1346, java.lang.Object(o1353sub))
f2090_0_bubble_Load(EOS(STATIC_2090), o1346, java.lang.Object(o1353sub)) → f2093_0_bubble_InvokeMethod(EOS(STATIC_2093), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub))
f2093_0_bubble_InvokeMethod(EOS(STATIC_2093), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub)) → f2097_0_getTail_Load(EOS(STATIC_2097), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub), java.lang.Object(o1353sub))
f2097_0_getTail_Load(EOS(STATIC_2097), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub), java.lang.Object(o1353sub)) → f2107_0_getTail_FieldAccess(EOS(STATIC_2107), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub), java.lang.Object(o1353sub))
f2107_0_getTail_FieldAccess(EOS(STATIC_2107), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub), java.lang.Object(o1353sub)) → f2111_0_getTail_FieldAccess(EOS(STATIC_2111), o1346, java.lang.Object(o1353sub), java.lang.Object(o1353sub), java.lang.Object(o1353sub))
f2107_0_getTail_FieldAccess(EOS(STATIC_2107), java.lang.Object(o1364sub), java.lang.Object(o1364sub), java.lang.Object(o1364sub), java.lang.Object(o1364sub)) → f2112_0_getTail_FieldAccess(EOS(STATIC_2112), java.lang.Object(o1364sub), java.lang.Object(o1364sub), java.lang.Object(o1364sub), java.lang.Object(o1364sub))
f2111_0_getTail_FieldAccess(EOS(STATIC_2111), o1346, java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449))) → f2113_0_getTail_FieldAccess(EOS(STATIC_2113), o1346, java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449)))
f2113_0_getTail_FieldAccess(EOS(STATIC_2113), o1346, java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449))) → f2117_0_getTail_Return(EOS(STATIC_2117), o1346, java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449)), o1366)
f2117_0_getTail_Return(EOS(STATIC_2117), o1346, java.lang.Object(List(EOC, o1366, i449)), java.lang.Object(List(EOC, o1366, i449)), o1366) → f2121_0_bubble_NULL(EOS(STATIC_2121), o1346, java.lang.Object(List(EOC, o1366, i449)), o1366)
f2121_0_bubble_NULL(EOS(STATIC_2121), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(o1379sub)) → f2125_0_bubble_NULL(EOS(STATIC_2125), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(o1379sub))
f2125_0_bubble_NULL(EOS(STATIC_2125), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(o1379sub)) → f2132_0_bubble_Load(EOS(STATIC_2132), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)))
f2132_0_bubble_Load(EOS(STATIC_2132), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449))) → f2142_0_bubble_FieldAccess(EOS(STATIC_2142), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)))
f2142_0_bubble_FieldAccess(EOS(STATIC_2142), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449))) → f2149_0_bubble_Load(EOS(STATIC_2149), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449)
f2149_0_bubble_Load(EOS(STATIC_2149), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449) → f2184_0_bubble_InvokeMethod(EOS(STATIC_2184), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)))
f2184_0_bubble_InvokeMethod(EOS(STATIC_2184), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449))) → f2195_0_getTail_Load(EOS(STATIC_2195), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)))
f2195_0_getTail_Load(EOS(STATIC_2195), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449))) → f2199_0_getTail_FieldAccess(EOS(STATIC_2199), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)))
f2199_0_getTail_FieldAccess(EOS(STATIC_2199), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449))) → f2204_0_getTail_Return(EOS(STATIC_2204), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(o1379sub))
f2204_0_getTail_Return(EOS(STATIC_2204), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), java.lang.Object(o1379sub)) → f2211_0_bubble_FieldAccess(EOS(STATIC_2211), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(o1379sub))
f2211_0_bubble_FieldAccess(EOS(STATIC_2211), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(o1379sub)) → f2216_0_bubble_FieldAccess(EOS(STATIC_2216), o1346, java.lang.Object(List(EOC, java.lang.Object(o1379sub), i449)), i449, java.lang.Object(o1379sub))
f2211_0_bubble_FieldAccess(EOS(STATIC_2211), java.lang.Object(o1435sub), java.lang.Object(List(EOC, java.lang.Object(o1435sub), i449)), i449, java.lang.Object(o1435sub)) → f2217_0_bubble_FieldAccess(EOS(STATIC_2217), java.lang.Object(o1435sub), java.lang.Object(List(EOC, java.lang.Object(o1435sub), i449)), i449, java.lang.Object(o1435sub))
f2216_0_bubble_FieldAccess(EOS(STATIC_2216), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, o1439, i458))) → f2220_0_bubble_FieldAccess(EOS(STATIC_2220), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, o1439, i458)))
f2220_0_bubble_FieldAccess(EOS(STATIC_2220), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, o1439, i458))) → f2224_0_bubble_LE(EOS(STATIC_2224), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458)
f2224_0_bubble_LE(EOS(STATIC_2224), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458) → f2234_0_bubble_LE(EOS(STATIC_2234), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458)
f2224_0_bubble_LE(EOS(STATIC_2224), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458) → f2235_0_bubble_LE(EOS(STATIC_2235), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458)
f2234_0_bubble_LE(EOS(STATIC_2234), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458) → f2240_0_bubble_Load(EOS(STATIC_2240), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) | <=(i449, i458)
f2240_0_bubble_Load(EOS(STATIC_2240), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2463_0_bubble_Load(EOS(STATIC_2463), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)))
f2463_0_bubble_Load(EOS(STATIC_2463), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458))) → f2475_0_bubble_InvokeMethod(EOS(STATIC_2475), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)))
f2475_0_bubble_InvokeMethod(EOS(STATIC_2475), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458))) → f2480_0_getTail_Load(EOS(STATIC_2480), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)))
f2480_0_getTail_Load(EOS(STATIC_2480), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458))) → f2507_0_getTail_FieldAccess(EOS(STATIC_2507), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)))
f2507_0_getTail_FieldAccess(EOS(STATIC_2507), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458))) → f2544_0_getTail_Return(EOS(STATIC_2544), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)), java.lang.Object(List(EOC, o1439, i449)))
f2544_0_getTail_Return(EOS(STATIC_2544), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)), java.lang.Object(List(EOC, o1439, i449))) → f2560_0_bubble_Store(EOS(STATIC_2560), o1346, java.lang.Object(List(EOC, o1439, i449)))
f2560_0_bubble_Store(EOS(STATIC_2560), o1346, java.lang.Object(List(EOC, o1439, i449))) → f2562_0_bubble_JMP(EOS(STATIC_2562), o1346, java.lang.Object(List(EOC, o1439, i449)))
f2562_0_bubble_JMP(EOS(STATIC_2562), o1346, java.lang.Object(List(EOC, o1439, i449))) → f2568_0_bubble_Load(EOS(STATIC_2568), o1346, java.lang.Object(List(EOC, o1439, i449)))
f2568_0_bubble_Load(EOS(STATIC_2568), o1346, java.lang.Object(List(EOC, o1439, i449))) → f2082_0_bubble_Load(EOS(STATIC_2082), o1346, java.lang.Object(List(EOC, o1439, i449)))
f2082_0_bubble_Load(EOS(STATIC_2082), o1346, o1347) → f2085_0_bubble_NULL(EOS(STATIC_2085), o1346, o1347, o1347)
f2235_0_bubble_LE(EOS(STATIC_2235), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, i458) → f2242_0_bubble_Load(EOS(STATIC_2242), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) | >(i449, i458)
f2242_0_bubble_Load(EOS(STATIC_2242), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2252_0_bubble_FieldAccess(EOS(STATIC_2252), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)))
f2252_0_bubble_FieldAccess(EOS(STATIC_2252), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2261_0_bubble_Store(EOS(STATIC_2261), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449)
f2261_0_bubble_Store(EOS(STATIC_2261), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449) → f2268_0_bubble_Load(EOS(STATIC_2268), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449)
f2268_0_bubble_Load(EOS(STATIC_2268), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449) → f2278_0_bubble_Load(EOS(STATIC_2278), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)))
f2278_0_bubble_Load(EOS(STATIC_2278), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2292_0_bubble_InvokeMethod(EOS(STATIC_2292), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)))
f2292_0_bubble_InvokeMethod(EOS(STATIC_2292), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2305_0_getTail_Load(EOS(STATIC_2305), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)))
f2305_0_getTail_Load(EOS(STATIC_2305), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2323_0_getTail_FieldAccess(EOS(STATIC_2323), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)))
f2323_0_getTail_FieldAccess(EOS(STATIC_2323), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449))) → f2348_0_getTail_Return(EOS(STATIC_2348), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, o1439, i458)))
f2348_0_getTail_Return(EOS(STATIC_2348), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, o1439, i458))) → f2357_0_bubble_FieldAccess(EOS(STATIC_2357), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, o1439, i458)))
f2357_0_bubble_FieldAccess(EOS(STATIC_2357), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), java.lang.Object(List(EOC, o1439, i458))) → f2364_0_bubble_FieldAccess(EOS(STATIC_2364), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i458)
f2364_0_bubble_FieldAccess(EOS(STATIC_2364), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i449)), i458) → f2372_0_bubble_Load(EOS(STATIC_2372), o1346put, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449)
f2372_0_bubble_Load(EOS(STATIC_2372), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449) → f2380_0_bubble_InvokeMethod(EOS(STATIC_2380), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)))
f2380_0_bubble_InvokeMethod(EOS(STATIC_2380), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458))) → f2387_0_getTail_Load(EOS(STATIC_2387), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)))
f2387_0_getTail_Load(EOS(STATIC_2387), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458))) → f2407_0_getTail_FieldAccess(EOS(STATIC_2407), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)))
f2407_0_getTail_FieldAccess(EOS(STATIC_2407), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458))) → f2432_0_getTail_Return(EOS(STATIC_2432), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, o1439, i458)))
f2432_0_getTail_Return(EOS(STATIC_2432), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, o1439, i458))) → f2441_0_bubble_Load(EOS(STATIC_2441), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, o1439, i458)))
f2441_0_bubble_Load(EOS(STATIC_2441), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), i449, java.lang.Object(List(EOC, o1439, i458))) → f2446_0_bubble_FieldAccess(EOS(STATIC_2446), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, o1439, i458)), i449)
f2446_0_bubble_FieldAccess(EOS(STATIC_2446), o1346, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i458)), i458)), java.lang.Object(List(EOC, o1439, i458)), i449) → f2463_0_bubble_Load(EOS(STATIC_2463), o1346put, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1439, i449)), i458)))
f2217_0_bubble_FieldAccess(EOS(STATIC_2217), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, o1441, i459))) → f2222_0_bubble_FieldAccess(EOS(STATIC_2222), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, o1441, i459)))
f2222_0_bubble_FieldAccess(EOS(STATIC_2222), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, o1441, i459))) → f2228_0_bubble_LE(EOS(STATIC_2228), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459)
f2228_0_bubble_LE(EOS(STATIC_2228), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459) → f2236_0_bubble_LE(EOS(STATIC_2236), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459)
f2228_0_bubble_LE(EOS(STATIC_2228), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459) → f2237_0_bubble_LE(EOS(STATIC_2237), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459)
f2236_0_bubble_LE(EOS(STATIC_2236), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459) → f2244_0_bubble_Load(EOS(STATIC_2244), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) | <=(i449, i459)
f2244_0_bubble_Load(EOS(STATIC_2244), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2470_0_bubble_Load(EOS(STATIC_2470), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)))
f2470_0_bubble_Load(EOS(STATIC_2470), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459))) → f2477_0_bubble_InvokeMethod(EOS(STATIC_2477), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)))
f2477_0_bubble_InvokeMethod(EOS(STATIC_2477), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459))) → f2482_0_getTail_Load(EOS(STATIC_2482), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)))
f2482_0_getTail_Load(EOS(STATIC_2482), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459))) → f2524_0_getTail_FieldAccess(EOS(STATIC_2524), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)))
f2524_0_getTail_FieldAccess(EOS(STATIC_2524), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459))) → f2555_0_getTail_Return(EOS(STATIC_2555), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)), java.lang.Object(List(EOC, o1441, i449)))
f2555_0_getTail_Return(EOS(STATIC_2555), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)), java.lang.Object(List(EOC, o1441, i449))) → f2561_0_bubble_Store(EOS(STATIC_2561), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449)))
f2561_0_bubble_Store(EOS(STATIC_2561), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449))) → f2564_0_bubble_JMP(EOS(STATIC_2564), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449)))
f2564_0_bubble_JMP(EOS(STATIC_2564), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449))) → f2572_0_bubble_Load(EOS(STATIC_2572), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449)))
f2572_0_bubble_Load(EOS(STATIC_2572), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449))) → f2082_0_bubble_Load(EOS(STATIC_2082), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, o1441, i449)))
f2237_0_bubble_LE(EOS(STATIC_2237), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, i459) → f2245_0_bubble_Load(EOS(STATIC_2245), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) | >(i449, i459)
f2245_0_bubble_Load(EOS(STATIC_2245), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2256_0_bubble_FieldAccess(EOS(STATIC_2256), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)))
f2256_0_bubble_FieldAccess(EOS(STATIC_2256), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2265_0_bubble_Store(EOS(STATIC_2265), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449)
f2265_0_bubble_Store(EOS(STATIC_2265), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449) → f2269_0_bubble_Load(EOS(STATIC_2269), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449)
f2269_0_bubble_Load(EOS(STATIC_2269), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449) → f2283_0_bubble_Load(EOS(STATIC_2283), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)))
f2283_0_bubble_Load(EOS(STATIC_2283), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2297_0_bubble_InvokeMethod(EOS(STATIC_2297), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)))
f2297_0_bubble_InvokeMethod(EOS(STATIC_2297), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2307_0_getTail_Load(EOS(STATIC_2307), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)))
f2307_0_getTail_Load(EOS(STATIC_2307), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2336_0_getTail_FieldAccess(EOS(STATIC_2336), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)))
f2336_0_getTail_FieldAccess(EOS(STATIC_2336), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449))) → f2354_0_getTail_Return(EOS(STATIC_2354), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, o1441, i459)))
f2354_0_getTail_Return(EOS(STATIC_2354), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, o1441, i459))) → f2360_0_bubble_FieldAccess(EOS(STATIC_2360), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, o1441, i459)))
f2360_0_bubble_FieldAccess(EOS(STATIC_2360), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), java.lang.Object(List(EOC, o1441, i459))) → f2366_0_bubble_FieldAccess(EOS(STATIC_2366), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i459)
f2366_0_bubble_FieldAccess(EOS(STATIC_2366), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i449)), i459) → f2376_0_bubble_Load(EOS(STATIC_2376), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449)
f2376_0_bubble_Load(EOS(STATIC_2376), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449) → f2383_0_bubble_InvokeMethod(EOS(STATIC_2383), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)))
f2383_0_bubble_InvokeMethod(EOS(STATIC_2383), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459))) → f2389_0_getTail_Load(EOS(STATIC_2389), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)))
f2389_0_getTail_Load(EOS(STATIC_2389), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459))) → f2418_0_getTail_FieldAccess(EOS(STATIC_2418), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)))
f2418_0_getTail_FieldAccess(EOS(STATIC_2418), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459))) → f2438_0_getTail_Return(EOS(STATIC_2438), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, o1441, i459)))
f2438_0_getTail_Return(EOS(STATIC_2438), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, o1441, i459))) → f2444_0_bubble_Load(EOS(STATIC_2444), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, o1441, i459)))
f2444_0_bubble_Load(EOS(STATIC_2444), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), i449, java.lang.Object(List(EOC, o1441, i459))) → f2448_0_bubble_FieldAccess(EOS(STATIC_2448), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, o1441, i459)), i449)
f2448_0_bubble_FieldAccess(EOS(STATIC_2448), java.lang.Object(List(EOC, o1441, i459)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i459)), i459)), java.lang.Object(List(EOC, o1441, i459)), i449) → f2470_0_bubble_Load(EOS(STATIC_2470), java.lang.Object(List(EOC, o1441, i449)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1441, i449)), i459)))
f2112_0_getTail_FieldAccess(EOS(STATIC_2112), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450))) → f2115_0_getTail_FieldAccess(EOS(STATIC_2115), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)))
f2115_0_getTail_FieldAccess(EOS(STATIC_2115), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450))) → f2118_0_getTail_Return(EOS(STATIC_2118), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), o1368)
f2118_0_getTail_Return(EOS(STATIC_2118), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), o1368) → f2124_0_bubble_NULL(EOS(STATIC_2124), java.lang.Object(List(EOC, o1368, i450)), java.lang.Object(List(EOC, o1368, i450)), o1368)
f2124_0_bubble_NULL(EOS(STATIC_2124), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(o1380sub)) → f2129_0_bubble_NULL(EOS(STATIC_2129), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(o1380sub))
f2129_0_bubble_NULL(EOS(STATIC_2129), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(o1380sub)) → f2138_0_bubble_Load(EOS(STATIC_2138), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)))
f2138_0_bubble_Load(EOS(STATIC_2138), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450))) → f2146_0_bubble_FieldAccess(EOS(STATIC_2146), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)))
f2146_0_bubble_FieldAccess(EOS(STATIC_2146), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450))) → f2161_0_bubble_Load(EOS(STATIC_2161), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450)
f2161_0_bubble_Load(EOS(STATIC_2161), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450) → f2194_0_bubble_InvokeMethod(EOS(STATIC_2194), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)))
f2194_0_bubble_InvokeMethod(EOS(STATIC_2194), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450))) → f2197_0_getTail_Load(EOS(STATIC_2197), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)))
f2197_0_getTail_Load(EOS(STATIC_2197), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450))) → f2202_0_getTail_FieldAccess(EOS(STATIC_2202), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)))
f2202_0_getTail_FieldAccess(EOS(STATIC_2202), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450))) → f2209_0_getTail_Return(EOS(STATIC_2209), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(o1380sub))
f2209_0_getTail_Return(EOS(STATIC_2209), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(o1380sub)) → f2212_0_bubble_FieldAccess(EOS(STATIC_2212), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), java.lang.Object(List(EOC, java.lang.Object(o1380sub), i450)), i450, java.lang.Object(o1380sub))
f2212_0_bubble_FieldAccess(EOS(STATIC_2212), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, o1437, i457))) → f2218_0_bubble_FieldAccess(EOS(STATIC_2218), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, o1437, i457)))
f2218_0_bubble_FieldAccess(EOS(STATIC_2218), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, o1437, i457))) → f2223_0_bubble_LE(EOS(STATIC_2223), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457)
f2223_0_bubble_LE(EOS(STATIC_2223), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457) → f2230_0_bubble_LE(EOS(STATIC_2230), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457)
f2223_0_bubble_LE(EOS(STATIC_2223), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457) → f2231_0_bubble_LE(EOS(STATIC_2231), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457)
f2230_0_bubble_LE(EOS(STATIC_2230), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457) → f2238_0_bubble_Load(EOS(STATIC_2238), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) | <=(i450, i457)
f2238_0_bubble_Load(EOS(STATIC_2238), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2453_0_bubble_Load(EOS(STATIC_2453), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)))
f2453_0_bubble_Load(EOS(STATIC_2453), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457))) → f2473_0_bubble_InvokeMethod(EOS(STATIC_2473), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)))
f2473_0_bubble_InvokeMethod(EOS(STATIC_2473), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457))) → f2479_0_getTail_Load(EOS(STATIC_2479), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)))
f2479_0_getTail_Load(EOS(STATIC_2479), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457))) → f2491_0_getTail_FieldAccess(EOS(STATIC_2491), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)))
f2491_0_getTail_FieldAccess(EOS(STATIC_2491), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457))) → f2533_0_getTail_Return(EOS(STATIC_2533), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, o1437, i450)))
f2533_0_getTail_Return(EOS(STATIC_2533), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, o1437, i450))) → f2556_0_bubble_Store(EOS(STATIC_2556), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, o1437, i450)))
f2556_0_bubble_Store(EOS(STATIC_2556), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, o1437, i450))) → f2560_0_bubble_Store(EOS(STATIC_2560), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, o1437, i450)))
f2231_0_bubble_LE(EOS(STATIC_2231), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, i457) → f2239_0_bubble_Load(EOS(STATIC_2239), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) | >(i450, i457)
f2239_0_bubble_Load(EOS(STATIC_2239), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2248_0_bubble_FieldAccess(EOS(STATIC_2248), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)))
f2248_0_bubble_FieldAccess(EOS(STATIC_2248), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2259_0_bubble_Store(EOS(STATIC_2259), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450)
f2259_0_bubble_Store(EOS(STATIC_2259), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450) → f2266_0_bubble_Load(EOS(STATIC_2266), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450)
f2266_0_bubble_Load(EOS(STATIC_2266), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450) → f2273_0_bubble_Load(EOS(STATIC_2273), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)))
f2273_0_bubble_Load(EOS(STATIC_2273), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2287_0_bubble_InvokeMethod(EOS(STATIC_2287), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)))
f2287_0_bubble_InvokeMethod(EOS(STATIC_2287), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2300_0_getTail_Load(EOS(STATIC_2300), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)))
f2300_0_getTail_Load(EOS(STATIC_2300), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2314_0_getTail_FieldAccess(EOS(STATIC_2314), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)))
f2314_0_getTail_FieldAccess(EOS(STATIC_2314), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450))) → f2341_0_getTail_Return(EOS(STATIC_2341), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, o1437, i457)))
f2341_0_getTail_Return(EOS(STATIC_2341), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, o1437, i457))) → f2355_0_bubble_FieldAccess(EOS(STATIC_2355), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, o1437, i457)))
f2355_0_bubble_FieldAccess(EOS(STATIC_2355), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, o1437, i457))) → f2361_0_bubble_FieldAccess(EOS(STATIC_2361), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i457)
f2361_0_bubble_FieldAccess(EOS(STATIC_2361), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i450)), i457) → f2369_0_bubble_Load(EOS(STATIC_2369), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450)
f2369_0_bubble_Load(EOS(STATIC_2369), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450) → f2378_0_bubble_InvokeMethod(EOS(STATIC_2378), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)))
f2378_0_bubble_InvokeMethod(EOS(STATIC_2378), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457))) → f2385_0_getTail_Load(EOS(STATIC_2385), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)))
f2385_0_getTail_Load(EOS(STATIC_2385), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457))) → f2398_0_getTail_FieldAccess(EOS(STATIC_2398), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)))
f2398_0_getTail_FieldAccess(EOS(STATIC_2398), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457))) → f2423_0_getTail_Return(EOS(STATIC_2423), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, o1437, i457)))
f2423_0_getTail_Return(EOS(STATIC_2423), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, o1437, i457))) → f2439_0_bubble_Load(EOS(STATIC_2439), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, o1437, i457)))
f2439_0_bubble_Load(EOS(STATIC_2439), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), i450, java.lang.Object(List(EOC, o1437, i457))) → f2445_0_bubble_FieldAccess(EOS(STATIC_2445), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, o1437, i457)), i450)
f2445_0_bubble_FieldAccess(EOS(STATIC_2445), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i457)), i457)), java.lang.Object(List(EOC, o1437, i457)), i450) → f2453_0_bubble_Load(EOS(STATIC_2453), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1437, i450)), i457)))
R rules:

Combined rules. Obtained 6 conditional rules for P and 0 conditional rules for R.

P rules:
f2085_0_bubble_NULL(EOS(STATIC_2085), x0, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3))) → f2085_0_bubble_NULL(EOS(STATIC_2085), x0, java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2))) | <=(x3, x2)
f2085_0_bubble_NULL(EOS(STATIC_2085), x0, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3))) → f2085_0_bubble_NULL(EOS(STATIC_2085), x4, java.lang.Object(List(EOC, x1, x3)), java.lang.Object(List(EOC, x1, x3))) | >(x3, x2)
f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, x0, x1))) | <=(x2, x1)
f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, x0, x2)), java.lang.Object(List(EOC, x0, x2)), java.lang.Object(List(EOC, x0, x2))) | >(x2, x1)
f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, x0, x1))) | <=(x2, x1)
f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → f2085_0_bubble_NULL(EOS(STATIC_2085), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x2)), x1)), java.lang.Object(List(EOC, x0, x2)), java.lang.Object(List(EOC, x0, x2))) | >(x2, x1)
R rules:

Filtered ground terms:

f2085_0_bubble_NULL(x1, x2, x3, x4) → f2085_0_bubble_NULL(x2, x3, x4)
Cond_f2085_0_bubble_NULL(x1, x2, x3, x4, x5) → Cond_f2085_0_bubble_NULL(x1, x3, x4, x5)
Cond_f2085_0_bubble_NULL1(x1, x2, x3, x4, x5, x6) → Cond_f2085_0_bubble_NULL1(x1, x3, x4, x5, x6)
Cond_f2085_0_bubble_NULL2(x1, x2, x3, x4, x5) → Cond_f2085_0_bubble_NULL2(x1, x3, x4, x5)
Cond_f2085_0_bubble_NULL3(x1, x2, x3, x4, x5) → Cond_f2085_0_bubble_NULL3(x1, x3, x4, x5)
Cond_f2085_0_bubble_NULL4(x1, x2, x3, x4, x5) → Cond_f2085_0_bubble_NULL4(x1, x3, x4, x5)
Cond_f2085_0_bubble_NULL5(x1, x2, x3, x4, x5) → Cond_f2085_0_bubble_NULL5(x1, x3, x4, x5)
EOS(x1) → EOS
List(x1, x2, x3) → List(x2, x3)

Filtered unneeded arguments:

Cond_f2085_0_bubble_NULL1(x1, x2, x3, x4, x5) → Cond_f2085_0_bubble_NULL1(x1, x3, x4, x5)

Filtered duplicate args:

f2085_0_bubble_NULL(x1, x2, x3) → f2085_0_bubble_NULL(x1, x3)
Cond_f2085_0_bubble_NULL(x1, x2, x3, x4) → Cond_f2085_0_bubble_NULL(x1, x2, x4)
Cond_f2085_0_bubble_NULL1(x1, x2, x3, x4) → Cond_f2085_0_bubble_NULL1(x1, x3, x4)
Cond_f2085_0_bubble_NULL2(x1, x2, x3, x4) → Cond_f2085_0_bubble_NULL2(x1, x4)
Cond_f2085_0_bubble_NULL3(x1, x2, x3, x4) → Cond_f2085_0_bubble_NULL3(x1, x4)
Cond_f2085_0_bubble_NULL4(x1, x2, x3, x4) → Cond_f2085_0_bubble_NULL4(x1, x4)
Cond_f2085_0_bubble_NULL5(x1, x2, x3, x4) → Cond_f2085_0_bubble_NULL5(x1, x4)

Combined rules. Obtained 6 conditional rules for P and 0 conditional rules for R.

P rules:
F2085_0_BUBBLE_NULL(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → F2085_0_BUBBLE_NULL(x0, java.lang.Object(List(x1, x2))) | <=(x3, x2)
F2085_0_BUBBLE_NULL(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → F2085_0_BUBBLE_NULL(x4, java.lang.Object(List(x1, x3))) | >(x3, x2)
F2085_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)), java.lang.Object(List(x0, x1))) | <=(x2, x1)
F2085_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL(java.lang.Object(List(x0, x2)), java.lang.Object(List(x0, x2))) | >(x2, x1)
F2085_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(x0, x1))) | <=(x2, x1)
F2085_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1)), java.lang.Object(List(x0, x2))) | >(x2, x1)
R rules:

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

P rules:
F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → COND_F2085_0_BUBBLE_NULL(<=(x3, x2), x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)))
COND_F2085_0_BUBBLE_NULL(TRUE, x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(x1, x2)))
F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → COND_F2085_0_BUBBLE_NULL1(>(x3, x2), x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)), x4)
COND_F2085_0_BUBBLE_NULL1(TRUE, x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)), x4) → F2085_0_BUBBLE_NULL'(x4, java.lang.Object(List(x1, x3)))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL2(<=(x2, x1), java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(x0, x1)))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL3(>(x2, x1), java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x2)), java.lang.Object(List(x0, x2)))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL4(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(x0, x1)))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL5(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1)), java.lang.Object(List(x0, x2)))
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → COND_F2085_0_BUBBLE_NULL(x3[0] <= x2[0], x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))
(1): COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1]))) → F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))
(2): F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(x3[2] > x2[2], x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])
(3): COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))
(4): F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → COND_F2085_0_BUBBLE_NULL2(x2[4] <= x1[4], java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))
(5): COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))
(6): F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → COND_F2085_0_BUBBLE_NULL3(x2[6] > x1[6], java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))
(7): COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))
(8): F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) → COND_F2085_0_BUBBLE_NULL4(x2[8] <= x1[8], java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))
(9): COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))
(10): F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) → COND_F2085_0_BUBBLE_NULL5(x2[10] > x1[10], java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))
(11): COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))

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

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

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

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

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

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

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

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

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

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

(3) -> (4), if (x4[3] →^* java.lang.Object(List(x0[4], x1[4]))∧java.lang.Object(List(x1[3], x3[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))

(3) -> (6), if (x4[3] →^* java.lang.Object(List(x0[6], x1[6]))∧java.lang.Object(List(x1[3], x3[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))

(3) -> (8), if (x4[3] →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))∧java.lang.Object(List(x1[3], x3[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))

(3) -> (10), if (x4[3] →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))∧java.lang.Object(List(x1[3], x3[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))

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

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

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

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

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

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

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

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

(7) -> (0), if (java.lang.Object(List(x0[7], x2[7])) →^* x0[0]∧java.lang.Object(List(x0[7], x2[7])) →^* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))

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

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

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

(7) -> (8), if (java.lang.Object(List(x0[7], x2[7])) →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))

(7) -> (10), if (java.lang.Object(List(x0[7], x2[7])) →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))

(8) -> (9), if (x2[8] <= x1[8] ∧java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])) →^* java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])))

(9) -> (0), if (java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])) →^* x0[0]∧java.lang.Object(List(x0[9], x1[9])) →^* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))

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

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

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

(9) -> (8), if (java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])) →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))∧java.lang.Object(List(x0[9], x1[9])) →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))

(9) -> (10), if (java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])) →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))∧java.lang.Object(List(x0[9], x1[9])) →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))

(10) -> (11), if (x2[10] > x1[10] ∧java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])) →^* java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])))

(11) -> (0), if (java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])) →^* x0[0]∧java.lang.Object(List(x0[11], x2[11])) →^* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))

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

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

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

(11) -> (8), if (java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])) →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))∧java.lang.Object(List(x0[11], x2[11])) →^* java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))

(11) -> (10), if (java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])) →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))∧java.lang.Object(List(x0[11], x2[11])) →^* java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))

The set Q is empty.

(8) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: true Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@1ad1e0c7 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

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 F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → COND_F2085_0_BUBBLE_NULL(<=(x3, x2), x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))), COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1]))) → F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1]))) which results in the following constraint:
(1)    (<=(x3[0], x2[0])=TRUE∧x0[0]=x0[1]∧java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))=java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1])) ⇒ F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))≥COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (<=(x3[0], x2[0])=TRUE ⇒ F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))≥COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥)∧[(10)bni_34 + (-1)Bound*bni_34] + [(32)bni_34]x1[0] ≥ 0∧[1 + (-1)bso_35] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥)∧[(10)bni_34 + (-1)Bound*bni_34] + [(32)bni_34]x1[0] ≥ 0∧[1 + (-1)bso_35] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥)∧[(10)bni_34 + (-1)Bound*bni_34] + [(32)bni_34]x1[0] ≥ 0∧[1 + (-1)bso_35] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_34] ≥ 0∧0 ≥ 0∧[(10)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_35] ≥ 0)

For Pair COND_F2085_0_BUBBLE_NULL(TRUE, x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(x1, x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))), COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1]))) → F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1]))) which results in the following constraint:
(7)    (<=(x3[0], x2[0])=TRUE∧x0[0]=x0[1]∧java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))=java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1])) ⇒ COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1])))≥F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥))

We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:
(8)    (<=(x3[0], x2[0])=TRUE ⇒ COND_F2085_0_BUBBLE_NULL(TRUE, x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL(TRUE, x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))≥F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(x1[0], x2[0])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥)∧[(9)bni_36 + (-1)Bound*bni_36] + [(32)bni_36]x1[0] ≥ 0∧[7 + (-1)bso_37] + [24]x1[0] ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥)∧[(9)bni_36 + (-1)Bound*bni_36] + [(32)bni_36]x1[0] ≥ 0∧[7 + (-1)bso_37] + [24]x1[0] ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥)∧[(9)bni_36 + (-1)Bound*bni_36] + [(32)bni_36]x1[0] ≥ 0∧[7 + (-1)bso_37] + [24]x1[0] ≥ 0)

We simplified constraint (11) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_36] ≥ 0∧0 ≥ 0∧[(9)bni_36 + (-1)Bound*bni_36] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_37] ≥ 0∧[1] ≥ 0)

For Pair F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → COND_F2085_0_BUBBLE_NULL1(>(x3, x2), x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)), x4) the following chains were created:

We consider the chain COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1]))) → F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(13)    (x0[1]=x0[2]∧java.lang.Object(List(x1[1], x2[1]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))∧>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3]))∧x4[2]=x4[3] ⇒ F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (13) using rules (I), (II), (III), (IV) which results in the following new constraint:
(14)    (>(x3[2], x2[2])=TRUE ⇒ F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[1], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(19)    (x4[3]=x0[2]∧java.lang.Object(List(x1[3], x3[3]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))∧>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]1∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3]1, x2[3]1)), x3[3]1))∧x4[2]=x4[3]1 ⇒ F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (19) using rules (I), (II), (III), (IV) which results in the following new constraint:
(20)    (>(x3[2], x2[2])=TRUE ⇒ F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x4[3], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(25)    (java.lang.Object(List(x0[5], x1[5]))=x0[2]∧java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))∧>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3]))∧x4[2]=x4[3] ⇒ F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (25) using rules (I), (II), (III), (IV) which results in the following new constraint:
(26)    (>(x3[2], x2[2])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(31)    (java.lang.Object(List(x0[7], x2[7]))=x0[2]∧java.lang.Object(List(x0[7], x2[7]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))∧>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3]))∧x4[2]=x4[3] ⇒ F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (31) using rules (I), (II), (III), (IV) which results in the following new constraint:
(32)    (>(x3[2], x2[2])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (35) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(36)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(37)    (java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))=x0[2]∧java.lang.Object(List(x0[9], x1[9]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))∧>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3]))∧x4[2]=x4[3] ⇒ F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (37) using rules (I), (II), (III), (IV) which results in the following new constraint:
(38)    (>(x3[2], x2[2])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x2[9])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x2[9])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x2[9])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (41) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(42)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(43)    (java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11]))=x0[2]∧java.lang.Object(List(x0[11], x2[11]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))∧>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3]))∧x4[2]=x4[3] ⇒ F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (43) using rules (I), (II), (III), (IV) which results in the following new constraint:
(44)    (>(x3[2], x2[2])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x1[11])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x1[11])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])))≥COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x1[11])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])∧(U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥))

We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧[(10)bni_38 + (-1)Bound*bni_38] + [(32)bni_38]x1[2] ≥ 0∧[1 + (-1)bso_39] ≥ 0)

We simplified constraint (47) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(48)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)

For Pair COND_F2085_0_BUBBLE_NULL1(TRUE, x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)), x4) → F2085_0_BUBBLE_NULL'(x4, java.lang.Object(List(x1, x3))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]), COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3]))) which results in the following constraint:
(49)    (>(x3[2], x2[2])=TRUE∧x0[2]=x0[3]∧java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))=java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3]))∧x4[2]=x4[3] ⇒ COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3])≥NonInfC∧COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3])≥F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥))

We simplified constraint (49) using rules (I), (II), (III) which results in the following new constraint:
(50)    (>(x3[2], x2[2])=TRUE ⇒ COND_F2085_0_BUBBLE_NULL1(TRUE, x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])≥NonInfC∧COND_F2085_0_BUBBLE_NULL1(TRUE, x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])≥F2085_0_BUBBLE_NULL'(x4[2], java.lang.Object(List(x1[2], x3[2])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥)∧[(9)bni_40 + (-1)Bound*bni_40] + [(32)bni_40]x1[2] ≥ 0∧[7 + (-1)bso_41] + [24]x1[2] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥)∧[(9)bni_40 + (-1)Bound*bni_40] + [(32)bni_40]x1[2] ≥ 0∧[7 + (-1)bso_41] + [24]x1[2] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥)∧[(9)bni_40 + (-1)Bound*bni_40] + [(32)bni_40]x1[2] ≥ 0∧[7 + (-1)bso_41] + [24]x1[2] ≥ 0)

We simplified constraint (53) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(54)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(32)bni_40] ≥ 0∧0 ≥ 0∧[(9)bni_40 + (-1)Bound*bni_40] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_41] ≥ 0∧[1] ≥ 0)

For Pair F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL2(<=(x2, x1), java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))), COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))) which results in the following constraint:
(55)    (<=(x2[4], x1[4])=TRUE∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(x0[5], x1[5]))∧java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥))

We simplified constraint (55) using rules (I), (II), (IV) which results in the following new constraint:
(56)    (<=(x2[4], x1[4])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥)∧[(10)bni_42 + (-1)Bound*bni_42] + [(32)bni_42]x0[4] ≥ 0∧[7 + (-1)bso_43] + [20]x0[4] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥)∧[(10)bni_42 + (-1)Bound*bni_42] + [(32)bni_42]x0[4] ≥ 0∧[7 + (-1)bso_43] + [20]x0[4] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥)∧[(10)bni_42 + (-1)Bound*bni_42] + [(32)bni_42]x0[4] ≥ 0∧[7 + (-1)bso_43] + [20]x0[4] ≥ 0)

We simplified constraint (59) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(60)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_42] ≥ 0∧[(10)bni_42 + (-1)Bound*bni_42] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_43] ≥ 0∧[1] ≥ 0)

For Pair COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(x0, x1))) the following chains were created:

We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) which results in the following constraint:
(61)    (java.lang.Object(List(x0[5], x1[5]))=x0[0]∧java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])) ⇒ COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (61) using rules (I), (II), (III), (IV) which results in the following new constraint:
(62)    (COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x1[5])), java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(63)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x1[0] ≥ 0)

We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(64)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x1[0] ≥ 0)

We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(65)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x1[0] ≥ 0)

We simplified constraint (65) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(66)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2]) which results in the following constraint:
(67)    (java.lang.Object(List(x0[5], x1[5]))=x0[2]∧java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])) ⇒ COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (67) using rules (I), (II), (III), (IV) which results in the following new constraint:
(68)    (COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x1[5])), java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(69)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x1[2] ≥ 0)

We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(70)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x1[2] ≥ 0)

We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(71)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x1[2] ≥ 0)

We simplified constraint (71) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(72)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) which results in the following constraint:
(73)    (java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(x0[4], x1[4]))∧java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])) ⇒ COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (73) using rules (I), (II), (III), (IV) which results in the following new constraint:
(74)    (COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (74) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(75)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[5] ≥ 0)

We simplified constraint (75) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(76)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[5] ≥ 0)

We simplified constraint (76) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(77)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[5] ≥ 0)

We simplified constraint (77) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(78)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) which results in the following constraint:
(79)    (java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(x0[6], x1[6]))∧java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])) ⇒ COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (79) using rules (I), (II), (III), (IV) which results in the following new constraint:
(80)    (COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (80) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(81)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[5] ≥ 0)

We simplified constraint (81) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(82)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[5] ≥ 0)

We simplified constraint (82) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(83)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[5] ≥ 0)

We simplified constraint (83) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(84)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) → COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) which results in the following constraint:
(85)    (java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])) ⇒ COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (85) using rules (I), (II), (III), (IV) which results in the following new constraint:
(86)    (COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x1[5])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (86) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(87)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[8] ≥ 0)

We simplified constraint (87) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(88)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[8] ≥ 0)

We simplified constraint (88) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(89)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[8] ≥ 0)

We simplified constraint (89) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(90)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
We consider the chain COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5]))), F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) → COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) which results in the following constraint:
(91)    (java.lang.Object(List(x0[5], x1[5]))=java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])) ⇒ COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (91) using rules (I), (II), (III), (IV) which results in the following new constraint:
(92)    (COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x1[5])), x2[5])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x1[5])), java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x1[5])), x2[5])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x1[5])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x1[5])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥))

We simplified constraint (92) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(93)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[10] ≥ 0)

We simplified constraint (93) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(94)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[10] ≥ 0)

We simplified constraint (94) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(95)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧[5 + (-1)bso_45] + [16]x0[10] ≥ 0)

We simplified constraint (95) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(96)    ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)

For Pair F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL3(>(x2, x1), java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))), COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7]))) which results in the following constraint:
(97)    (>(x2[6], x1[6])=TRUE∧java.lang.Object(List(x0[6], x1[6]))=java.lang.Object(List(x0[7], x1[7]))∧java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))=java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7])) ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥))

We simplified constraint (97) using rules (I), (II), (IV) which results in the following new constraint:
(98)    (>(x2[6], x1[6])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥))

We simplified constraint (98) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(99)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥)∧[(10)bni_46 + (-1)Bound*bni_46] + [(32)bni_46]x0[6] ≥ 0∧[7 + (-1)bso_47] + [20]x0[6] ≥ 0)

We simplified constraint (99) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(100)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥)∧[(10)bni_46 + (-1)Bound*bni_46] + [(32)bni_46]x0[6] ≥ 0∧[7 + (-1)bso_47] + [20]x0[6] ≥ 0)

We simplified constraint (100) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(101)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥)∧[(10)bni_46 + (-1)Bound*bni_46] + [(32)bni_46]x0[6] ≥ 0∧[7 + (-1)bso_47] + [20]x0[6] ≥ 0)

We simplified constraint (101) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(102)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_46] ≥ 0∧[(10)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_47] ≥ 0∧[1] ≥ 0)

For Pair COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x2)), java.lang.Object(List(x0, x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))), COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7]))) which results in the following constraint:
(103)    (>(x2[6], x1[6])=TRUE∧java.lang.Object(List(x0[6], x1[6]))=java.lang.Object(List(x0[7], x1[7]))∧java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))=java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7])) ⇒ COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥))

We simplified constraint (103) using rules (I), (II), (III) which results in the following new constraint:
(104)    (>(x2[6], x1[6])=TRUE ⇒ COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x2[6])), java.lang.Object(List(x0[6], x2[6])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥))

We simplified constraint (104) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(105)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥)∧[(3)bni_48 + (-1)Bound*bni_48] + [(12)bni_48]x0[6] ≥ 0∧[1 + (-1)bso_49] + [4]x0[6] ≥ 0)

We simplified constraint (105) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(106)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥)∧[(3)bni_48 + (-1)Bound*bni_48] + [(12)bni_48]x0[6] ≥ 0∧[1 + (-1)bso_49] + [4]x0[6] ≥ 0)

We simplified constraint (106) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(107)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥)∧[(3)bni_48 + (-1)Bound*bni_48] + [(12)bni_48]x0[6] ≥ 0∧[1 + (-1)bso_49] + [4]x0[6] ≥ 0)

We simplified constraint (107) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(108)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(12)bni_48] ≥ 0∧[(3)bni_48 + (-1)Bound*bni_48] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_49] ≥ 0∧[1] ≥ 0)

For Pair F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL4(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) → COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))), COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9]))) which results in the following constraint:
(109)    (<=(x2[8], x1[8])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))=java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])) ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))≥COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥))

We simplified constraint (109) using rules (I), (II), (IV) which results in the following new constraint:
(110)    (<=(x2[8], x1[8])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))≥COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥))

We simplified constraint (110) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(111)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥)∧[(10)bni_50 + (-1)Bound*bni_50] + [(32)bni_50]x0[8] ≥ 0∧[1 + (-1)bso_51] ≥ 0)

We simplified constraint (111) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(112)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥)∧[(10)bni_50 + (-1)Bound*bni_50] + [(32)bni_50]x0[8] ≥ 0∧[1 + (-1)bso_51] ≥ 0)

We simplified constraint (112) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(113)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥)∧[(10)bni_50 + (-1)Bound*bni_50] + [(32)bni_50]x0[8] ≥ 0∧[1 + (-1)bso_51] ≥ 0)

We simplified constraint (113) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(114)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_50] ≥ 0∧[(10)bni_50 + (-1)Bound*bni_50] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_51] ≥ 0)

For Pair COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(x0, x1))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) → COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))), COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9]))) which results in the following constraint:
(115)    (<=(x2[8], x1[8])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))=java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])) ⇒ COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥))

We simplified constraint (115) using rules (I), (II), (III) which results in the following new constraint:
(116)    (<=(x2[8], x1[8])=TRUE ⇒ COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(x0[8], x1[8])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥))

We simplified constraint (116) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(117)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥)∧[(9)bni_52 + (-1)Bound*bni_52] + [(32)bni_52]x0[8] ≥ 0∧[7 + (-1)bso_53] + [24]x0[8] ≥ 0)

We simplified constraint (117) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(118)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥)∧[(9)bni_52 + (-1)Bound*bni_52] + [(32)bni_52]x0[8] ≥ 0∧[7 + (-1)bso_53] + [24]x0[8] ≥ 0)

We simplified constraint (118) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(119)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥)∧[(9)bni_52 + (-1)Bound*bni_52] + [(32)bni_52]x0[8] ≥ 0∧[7 + (-1)bso_53] + [24]x0[8] ≥ 0)

We simplified constraint (119) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(120)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_52] ≥ 0∧[(9)bni_52 + (-1)Bound*bni_52] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_53] ≥ 0∧[1] ≥ 0)

For Pair F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL5(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) → COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))), COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11]))) which results in the following constraint:
(121)    (>(x2[10], x1[10])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))=java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])) ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))≥COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥))

We simplified constraint (121) using rules (I), (II), (IV) which results in the following new constraint:
(122)    (>(x2[10], x1[10])=TRUE ⇒ F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))≥NonInfC∧F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))≥COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))∧(U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥))

We simplified constraint (122) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(123)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥)∧[(10)bni_54 + (-1)Bound*bni_54] + [(32)bni_54]x0[10] ≥ 0∧[4 + (-1)bso_55] + [16]x0[10] ≥ 0)

We simplified constraint (123) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(124)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥)∧[(10)bni_54 + (-1)Bound*bni_54] + [(32)bni_54]x0[10] ≥ 0∧[4 + (-1)bso_55] + [16]x0[10] ≥ 0)

We simplified constraint (124) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(125)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥)∧[(10)bni_54 + (-1)Bound*bni_54] + [(32)bni_54]x0[10] ≥ 0∧[4 + (-1)bso_55] + [16]x0[10] ≥ 0)

We simplified constraint (125) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(126)    (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_54] ≥ 0∧[(10)bni_54 + (-1)Bound*bni_54] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_55] ≥ 0∧[1] ≥ 0)

For Pair COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1)), java.lang.Object(List(x0, x2))) the following chains were created:

We consider the chain F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) → COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))), COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11]))) which results in the following constraint:
(127)    (>(x2[10], x1[10])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))=java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])) ⇒ COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥))

We simplified constraint (127) using rules (I), (II), (III) which results in the following new constraint:
(128)    (>(x2[10], x1[10])=TRUE ⇒ COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))≥NonInfC∧COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))≥F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x2[10])), x1[10])), java.lang.Object(List(x0[10], x2[10])))∧(U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥))

We simplified constraint (128) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(129)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥)∧[(6)bni_56 + (-1)Bound*bni_56] + [(16)bni_56]x0[10] ≥ 0∧[4 + (-1)bso_57] + [8]x0[10] ≥ 0)

We simplified constraint (129) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(130)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥)∧[(6)bni_56 + (-1)Bound*bni_56] + [(16)bni_56]x0[10] ≥ 0∧[4 + (-1)bso_57] + [8]x0[10] ≥ 0)

We simplified constraint (130) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(131)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥)∧[(6)bni_56 + (-1)Bound*bni_56] + [(16)bni_56]x0[10] ≥ 0∧[4 + (-1)bso_57] + [8]x0[10] ≥ 0)

We simplified constraint (131) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(132)    (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_56] ≥ 0∧[(6)bni_56 + (-1)Bound*bni_56] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_57] ≥ 0∧[1] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → COND_F2085_0_BUBBLE_NULL(<=(x3, x2), x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_34] ≥ 0∧0 ≥ 0∧[(10)bni_34 + (-1)Bound*bni_34] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_35] ≥ 0)
COND_F2085_0_BUBBLE_NULL(TRUE, x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(x1, x2)))
- (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_36] ≥ 0∧0 ≥ 0∧[(9)bni_36 + (-1)Bound*bni_36] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_37] ≥ 0∧[1] ≥ 0)
F2085_0_BUBBLE_NULL'(x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → COND_F2085_0_BUBBLE_NULL1(>(x3, x2), x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)), x4)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_38] ≥ 0∧0 ≥ 0∧[(10)bni_38 + (-1)Bound*bni_38] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_39] ≥ 0)
COND_F2085_0_BUBBLE_NULL1(TRUE, x0, java.lang.Object(List(java.lang.Object(List(x1, x2)), x3)), x4) → F2085_0_BUBBLE_NULL'(x4, java.lang.Object(List(x1, x3)))
- (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(32)bni_40] ≥ 0∧0 ≥ 0∧[(9)bni_40 + (-1)Bound*bni_40] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_41] ≥ 0∧[1] ≥ 0)
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL2(<=(x2, x1), java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_42] ≥ 0∧[(10)bni_42 + (-1)Bound*bni_42] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_43] ≥ 0∧[1] ≥ 0)
COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(x0, x1)))
- ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))), ≥)∧[bni_44] = 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[5 + (-1)bso_45] ≥ 0∧[1] ≥ 0)
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL3(>(x2, x1), java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_46] ≥ 0∧[(10)bni_46 + (-1)Bound*bni_46] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_47] ≥ 0∧[1] ≥ 0)
COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0, x1)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0, x2)), java.lang.Object(List(x0, x2)))
- (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(12)bni_48] ≥ 0∧[(3)bni_48 + (-1)Bound*bni_48] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_49] ≥ 0∧[1] ≥ 0)
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL4(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_50] ≥ 0∧[(10)bni_50 + (-1)Bound*bni_50] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_51] ≥ 0)
COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(x0, x1)))
- (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_52] ≥ 0∧[(9)bni_52 + (-1)Bound*bni_52] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[7 + (-1)bso_53] ≥ 0∧[1] ≥ 0)
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_F2085_0_BUBBLE_NULL5(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_54] ≥ 0∧[(10)bni_54 + (-1)Bound*bni_54] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_55] ≥ 0∧[1] ≥ 0)
COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1)), java.lang.Object(List(x0, x2)))
- (0 ≥ 0 ⇒ (U^Increasing(F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_56] ≥ 0∧[(6)bni_56 + (-1)Bound*bni_56] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_57] ≥ 0∧[1] ≥ 0)

The constraints for P_> respective P_bound 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 P_bound.
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(F2085_0_BUBBLE_NULL'(x₁, x₂)) = [2]x₂
POL(java.lang.Object(x₁)) = [1] + [2]x₁
POL(List(x₁, x₂)) = [2]x₁
POL(COND_F2085_0_BUBBLE_NULL(x₁, x₂, x₃)) = [-1] + [2]x₃
POL(<=(x₁, x₂)) = 0
POL(COND_F2085_0_BUBBLE_NULL1(x₁, x₂, x₃, x₄)) = [-1] + [2]x₃
POL(>(x₁, x₂)) = 0
POL(COND_F2085_0_BUBBLE_NULL2(x₁, x₂, x₃)) = [-1] + x₃ + [-1]x₂
POL(COND_F2085_0_BUBBLE_NULL3(x₁, x₂, x₃)) = [-1] + x₃ + [-1]x₂
POL(COND_F2085_0_BUBBLE_NULL4(x₁, x₂, x₃)) = [-1] + x₃ + x₂
POL(COND_F2085_0_BUBBLE_NULL5(x₁, x₂, x₃)) = [1] + x₂

The following pairs are in P_>:

F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))
COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1]))) → F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))
F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])
COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))
COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))
COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) → COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))
COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) → COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))
COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))

The following pairs are in P_bound:

F2085_0_BUBBLE_NULL'(x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → COND_F2085_0_BUBBLE_NULL(<=(x3[0], x2[0]), x0[0], java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))
COND_F2085_0_BUBBLE_NULL(TRUE, x0[1], java.lang.Object(List(java.lang.Object(List(x1[1], x2[1])), x3[1]))) → F2085_0_BUBBLE_NULL'(x0[1], java.lang.Object(List(x1[1], x2[1])))
F2085_0_BUBBLE_NULL'(x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2]))) → COND_F2085_0_BUBBLE_NULL1(>(x3[2], x2[2]), x0[2], java.lang.Object(List(java.lang.Object(List(x1[2], x2[2])), x3[2])), x4[2])
COND_F2085_0_BUBBLE_NULL1(TRUE, x0[3], java.lang.Object(List(java.lang.Object(List(x1[3], x2[3])), x3[3])), x4[3]) → F2085_0_BUBBLE_NULL'(x4[3], java.lang.Object(List(x1[3], x3[3])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → COND_F2085_0_BUBBLE_NULL2(<=(x2[4], x1[4]), java.lang.Object(List(x0[4], x1[4])), java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → COND_F2085_0_BUBBLE_NULL3(>(x2[6], x1[6]), java.lang.Object(List(x0[6], x1[6])), java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))
COND_F2085_0_BUBBLE_NULL3(TRUE, java.lang.Object(List(x0[7], x1[7])), java.lang.Object(List(java.lang.Object(List(x0[7], x1[7])), x2[7]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[7], x2[7])), java.lang.Object(List(x0[7], x2[7])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8]))) → COND_F2085_0_BUBBLE_NULL4(<=(x2[8], x1[8]), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])), java.lang.Object(List(java.lang.Object(List(x0[8], x1[8])), x2[8])))
COND_F2085_0_BUBBLE_NULL4(TRUE, java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[9], x1[9])), x2[9])), java.lang.Object(List(x0[9], x1[9])))
F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10]))) → COND_F2085_0_BUBBLE_NULL5(>(x2[10], x1[10]), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])), java.lang.Object(List(java.lang.Object(List(x0[10], x1[10])), x2[10])))
COND_F2085_0_BUBBLE_NULL5(TRUE, java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11])), java.lang.Object(List(java.lang.Object(List(x0[11], x1[11])), x2[11]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(java.lang.Object(List(x0[11], x2[11])), x1[11])), java.lang.Object(List(x0[11], x2[11])))

The following pairs are in P_≥:
none

There are no usable rules.

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:
(5): COND_F2085_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → F2085_0_BUBBLE_NULL'(java.lang.Object(List(x0[5], x1[5])), java.lang.Object(List(x0[5], x1[5])))

The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

(11) TRUE

(12) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test7.length(LList;)I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [tail]
Marker field analysis yielded the following relations that could be markers:

(13) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 22 IRules

P rules:
f1197_0_length_NULL(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub)) → f1198_0_length_NULL(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub))
f1198_0_length_NULL(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub)) → f1201_0_length_Load(EOS, o284, java.lang.Object(o297sub))
f1201_0_length_Load(EOS, o284, java.lang.Object(o297sub)) → f1204_0_length_InvokeMethod(EOS, o284, java.lang.Object(o297sub))
f1204_0_length_InvokeMethod(EOS, o284, java.lang.Object(o297sub)) → f1207_0_getTail_Load(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub))
f1207_0_getTail_Load(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub)) → f1219_0_getTail_FieldAccess(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub))
f1219_0_getTail_FieldAccess(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub)) → f1226_0_getTail_FieldAccess(EOS, o284, java.lang.Object(o297sub), java.lang.Object(o297sub))
f1219_0_getTail_FieldAccess(EOS, java.lang.Object(o309sub), java.lang.Object(o309sub), java.lang.Object(o309sub)) → f1227_0_getTail_FieldAccess(EOS, java.lang.Object(o309sub), java.lang.Object(o309sub), java.lang.Object(o309sub))
f1226_0_getTail_FieldAccess(EOS, o284, java.lang.Object(List(EOC, o311)), java.lang.Object(List(EOC, o311))) → f1230_0_getTail_FieldAccess(EOS, o284, java.lang.Object(List(EOC, o311)), java.lang.Object(List(EOC, o311)))
f1230_0_getTail_FieldAccess(EOS, o284, java.lang.Object(List(EOC, o311)), java.lang.Object(List(EOC, o311))) → f1237_0_getTail_Return(EOS, o284, java.lang.Object(List(EOC, o311)), o311)
f1237_0_getTail_Return(EOS, o284, java.lang.Object(List(EOC, o311)), o311) → f1244_0_length_Store(EOS, o284, o311)
f1244_0_length_Store(EOS, o284, o311) → f1253_0_length_Inc(EOS, o284, o311)
f1253_0_length_Inc(EOS, o284, o311) → f1260_0_length_JMP(EOS, o284, o311)
f1260_0_length_JMP(EOS, o284, o311) → f1267_0_length_Load(EOS, o284, o311)
f1267_0_length_Load(EOS, o284, o311) → f1193_0_length_Load(EOS, o284, o311)
f1193_0_length_Load(EOS, o284, o285) → f1197_0_length_NULL(EOS, o284, o285, o285)
f1227_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313))) → f1234_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313)))
f1234_0_getTail_FieldAccess(EOS, java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313))) → f1241_0_getTail_Return(EOS, java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313)), o313)
f1241_0_getTail_Return(EOS, java.lang.Object(List(EOC, o313)), java.lang.Object(List(EOC, o313)), o313) → f1248_0_length_Store(EOS, java.lang.Object(List(EOC, o313)), o313)
f1248_0_length_Store(EOS, java.lang.Object(List(EOC, o313)), o313) → f1257_0_length_Inc(EOS, java.lang.Object(List(EOC, o313)), o313)
f1257_0_length_Inc(EOS, java.lang.Object(List(EOC, o313)), o313) → f1264_0_length_JMP(EOS, java.lang.Object(List(EOC, o313)), o313)
f1264_0_length_JMP(EOS, java.lang.Object(List(EOC, o313)), o313) → f1274_0_length_Load(EOS, java.lang.Object(List(EOC, o313)), o313)
f1274_0_length_Load(EOS, java.lang.Object(List(EOC, o313)), o313) → f1193_0_length_Load(EOS, java.lang.Object(List(EOC, o313)), o313)

Combined rules. Obtained 2 IRules

P rules:
f1197_0_length_NULL(EOS, x0, java.lang.Object(List(EOC, x1)), java.lang.Object(List(EOC, x1))) → f1197_0_length_NULL(EOS, x0, x1, x1)
f1197_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0))) → f1197_0_length_NULL(EOS, java.lang.Object(List(EOC, x0)), x0, x0)

Filtered ground terms:

f1197_0_length_NULL(x1, x2, x3, x4) → f1197_0_length_NULL(x2, x3, x4)
List(x1, x2) → List(x2)

Filtered duplicate terms:

f1197_0_length_NULL(x1, x2, x3) → f1197_0_length_NULL(x1, x3)

Prepared 2 rules for path length conversion:

P rules:
f1197_0_length_NULL(x0, java.lang.Object(List(x1))) → f1197_0_length_NULL(x0, x1)
f1197_0_length_NULL(java.lang.Object(List(x0)), java.lang.Object(List(x0))) → f1197_0_length_NULL(java.lang.Object(List(x0)), x0)

Finished conversion. Obtained 2 rules.

P rules:
f1197_0_length_NULL(v5, v6) → f1197_0_length_NULL(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 0)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 0))
f1197_0_length_NULL(v9, v10) → f1197_0_length_NULL(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(14) Obligation:

Rules:
f1197_0_length_NULL(v5, v6) → f1197_0_length_NULL(v7, v8) | &&(&&(&&(&&(&&(>(+(v8, 1), 0), <=(+(v8, 1), v6)), >(+(v7, 1), 0)), <=(v7, v5)), >(+(v6, 1), 1)), >(+(v5, 1), 0))
f1197_0_length_NULL(v9, v10) → f1197_0_length_NULL(v11, v12) | &&(&&(&&(&&(&&(&&(&&(>=(v9, +(v12, 1)), >=(v9, v11)), >(+(v9, 1), 1)), >(+(v12, 1), 0)), <=(+(v12, 1), v10)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1197_0_length_NULL(x9, x11)] = x11

Therefore the following rule(s) have been dropped:

f1197_0_length_NULL(x0, x1) → f1197_0_length_NULL(x2, x3) | &&(&&(&&(&&(&&(>(+(x3, 1), 0), <=(+(x3, 1), x1)), >(+(x2, 1), 0)), <=(x2, x0)), >(+(x1, 1), 1)), >(+(x0, 1), 0))
f1197_0_length_NULL(x4, x5) → f1197_0_length_NULL(x6, x7) | &&(&&(&&(&&(&&(&&(&&(>=(x4, +(x7, 1)), >=(x4, x6)), >(+(x4, 1), 1)), >(+(x7, 1), 0)), <=(+(x7, 1), x5)), >(+(x6, 1), 1)), <=(x6, x5)), >(+(x5, 1), 1))

(16) YES

(17) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: List.mk(I)LList;
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(18) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f828_0_mk_Inc(EOS, i111, i111) → f835_0_mk_LE(EOS, +(i111, -1), i111)
f835_0_mk_LE(EOS, i113, i117) → f842_0_mk_LE(EOS, i113, i117)
f842_0_mk_LE(EOS, i113, i117) → f850_0_mk_New(EOS, i113) | >(i117, 0)
f850_0_mk_New(EOS, i113) → f874_0_mk_Duplicate(EOS, i113)
f874_0_mk_Duplicate(EOS, i113) → f893_0_mk_Load(EOS, i113)
f893_0_mk_Load(EOS, i113) → f951_0_mk_Load(EOS, i113, i113)
f951_0_mk_Load(EOS, i113, i113) → f962_0_mk_InvokeMethod(EOS, i113, i113)
f962_0_mk_InvokeMethod(EOS, i113, i113) → f976_0__init__Load(EOS, i113, i113, i113)
f976_0__init__Load(EOS, i113, i113, i113) → f996_0__init__InvokeMethod(EOS, i113, i113, i113)
f996_0__init__InvokeMethod(EOS, i113, i113, i113) → f999_0__init__Load(EOS, i113, i113, i113)
f999_0__init__Load(EOS, i113, i113, i113) → f1003_0__init__Load(EOS, i113, i113, i113)
f1003_0__init__Load(EOS, i113, i113, i113) → f1008_0__init__FieldAccess(EOS, i113, i113, i113)
f1008_0__init__FieldAccess(EOS, i113, i113, i113) → f1013_0__init__Load(EOS, i113, i113)
f1013_0__init__Load(EOS, i113, i113) → f1016_0__init__Load(EOS, i113, i113)
f1016_0__init__Load(EOS, i113, i113) → f1019_0__init__FieldAccess(EOS, i113, i113)
f1019_0__init__FieldAccess(EOS, i113, i113) → f1024_0__init__Return(EOS, i113, i113)
f1024_0__init__Return(EOS, i113, i113) → f1036_0_mk_Store(EOS, i113)
f1036_0_mk_Store(EOS, i113) → f1038_0_mk_JMP(EOS, i113)
f1038_0_mk_JMP(EOS, i113) → f1042_0_mk_Load(EOS, i113)
f1042_0_mk_Load(EOS, i113) → f822_0_mk_Load(EOS, i113)
f822_0_mk_Load(EOS, i111) → f828_0_mk_Inc(EOS, i111, i111)

Combined rules. Obtained 1 IRules

P rules:
f828_0_mk_Inc(EOS, x0, x0) → f828_0_mk_Inc(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f828_0_mk_Inc(x1, x2, x3) → f828_0_mk_Inc(x2, x3)
Cond_f828_0_mk_Inc(x1, x2, x3, x4) → Cond_f828_0_mk_Inc(x1, x3, x4)

Filtered duplicate terms:

f828_0_mk_Inc(x1, x2) → f828_0_mk_Inc(x2)
Cond_f828_0_mk_Inc(x1, x2, x3) → Cond_f828_0_mk_Inc(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f828_0_mk_Inc(x0) → f828_0_mk_Inc(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f828_0_mk_Inc(x0) → f828_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(19) Obligation:

Rules:
f828_0_mk_Inc(x0) → f828_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f828_0_mk_Inc(x2)] = x2

Therefore the following rule(s) have been dropped:

f828_0_mk_Inc(x0) → f828_0_mk_Inc(-(x0, 1)) | >(x0, 0)

(21) YES

(22) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Test7.main([Ljava/lang/String;)V
SCC calls the following helper methods: Test7.length(LList;)I, Test7.bubble(LList;)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(23) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 45 IRules

P rules:
f1146_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i170, i170) → f1154_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(3)), i170, i170, java.lang.Object(ARRAY(3))) | =(matching1, 3)
f1154_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(matching1)), i170, i170, java.lang.Object(ARRAY(matching2))) → f1158_0_main_GE(EOS, java.lang.Object(ARRAY(3)), i170, i170, 3) | &&(&&(>=(3, 0), =(matching1, 3)), =(matching2, 3))
f1158_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i178, i178, matching2) → f1161_0_main_GE(EOS, java.lang.Object(ARRAY(3)), i178, i178, 3) | &&(=(matching1, 3), =(matching2, 3))
f1161_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i178, i178, matching2) → f1165_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178) | &&(&&(<(i178, 3), =(matching1, 3)), =(matching2, 3))
f1165_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178) → f1171_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(3)), i178, java.lang.Object(ARRAY(3))) | =(matching1, 3)
f1171_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i178, java.lang.Object(ARRAY(matching2))) → f1175_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(3)), i178, java.lang.Object(ARRAY(3)), 0) | &&(=(matching1, 3), =(matching2, 3))
f1175_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i178, java.lang.Object(ARRAY(matching2)), matching3) → f1179_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(3)), i178, o256) | &&(&&(&&(<(0, 3), =(matching1, 3)), =(matching2, 3)), =(matching3, 0))
f1179_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), i178, o256) → f1182_0_length_ConstantStackPush(EOS, o256, o256) | =(matching1, 3)
f1179_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), i178, o256) → f1182_1_length_ConstantStackPush(EOS, java.lang.Object(ARRAY(3)), i178, o256, o256) | =(matching1, 3)
f1182_0_length_ConstantStackPush(EOS, o256, o256) → f1186_0_length_ConstantStackPush(EOS, o256, o256)
f1220_0_length_Return(EOS, java.lang.Object(ARRAY(matching1)), i178, o306, i183) → f1228_0_main_Store(EOS, java.lang.Object(ARRAY(3)), i178, i183) | =(matching1, 3)
f1228_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i178, i183) → f1232_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(3)), i178, i183) | =(matching1, 3)
f1232_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i178, i183) → f1235_0_main_Store(EOS, java.lang.Object(ARRAY(3)), i178, i183, 0) | =(matching1, 3)
f1235_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i178, i183, matching2) → f1239_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i183, 0) | &&(=(matching1, 3), =(matching2, 0))
f1239_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i183, matching2) → f1319_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i183, 0) | &&(=(matching1, 3), =(matching2, 0))
f1319_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i197) → f1430_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i197) | =(matching1, 3)
f1430_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i209) → f1531_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i209) | =(matching1, 3)
f1531_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i215) → f1646_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i215) | =(matching1, 3)
f1646_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241) → f1649_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, i241) | =(matching1, 3)
f1649_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, i241) → f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, i241, i196) | =(matching1, 3)
f1651_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, i241, i196) → f1653_0_main_GE(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, i241, i196) | =(matching1, 3)
f1651_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, i241, i196) → f1654_0_main_GE(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, i241, i196) | =(matching1, 3)
f1653_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, i241, i196) → f1655_0_main_Inc(EOS, java.lang.Object(ARRAY(3)), i178) | &&(>=(i241, i196), =(matching1, 3))
f1655_0_main_Inc(EOS, java.lang.Object(ARRAY(matching1)), i178) → f1662_0_main_JMP(EOS, java.lang.Object(ARRAY(3)), +(i178, 1)) | &&(>=(i178, 0), =(matching1, 3))
f1662_0_main_JMP(EOS, java.lang.Object(ARRAY(matching1)), i244) → f1670_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i244) | =(matching1, 3)
f1670_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i244) → f1142_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i244) | =(matching1, 3)
f1142_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i170) → f1146_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i170, i170) | =(matching1, 3)
f1654_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, i241, i196) → f1659_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241) | &&(<(i241, i196), =(matching1, 3))
f1659_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241) → f1664_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, java.lang.Object(ARRAY(3))) | =(matching1, 3)
f1664_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, java.lang.Object(ARRAY(matching2))) → f1673_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, java.lang.Object(ARRAY(3)), 0) | &&(=(matching1, 3), =(matching2, 3))
f1673_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, java.lang.Object(ARRAY(matching2)), matching3) → f1677_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, o504) | &&(&&(&&(<(0, 3), =(matching1, 3)), =(matching2, 3)), =(matching3, 0))
f1677_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o504) → f1685_0_bubble_Load(EOS, o504, o504) | =(matching1, 3)
f1677_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o504) → f1685_1_bubble_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, o504, o504) | =(matching1, 3)
f1685_0_bubble_Load(EOS, o504, o504) → f1689_0_bubble_Load(EOS, o504, o504)
f2106_0_bubble_Return(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o1354) → f1724_0_bubble_Return(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, o1354) | =(matching1, 3)
f1724_0_bubble_Return(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o566) → f1746_0_main_Inc(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241) | =(matching1, 3)
f1746_0_main_Inc(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241) → f1750_0_main_JMP(EOS, java.lang.Object(ARRAY(3)), i178, i196, +(i241, 1)) | &&(>=(i241, 0), =(matching1, 3))
f1750_0_main_JMP(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i253) → f1757_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i253) | =(matching1, 3)
f1757_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i253) → f1646_0_main_Load(EOS, java.lang.Object(ARRAY(3)), i178, i196, i253) | =(matching1, 3)
f2170_0_bubble_Return(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o1389) → f1724_0_bubble_Return(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, o1389) | =(matching1, 3)
f2192_0_bubble_Return(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, java.lang.Object(List(EOC))) → f1724_0_bubble_Return(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, java.lang.Object(List(EOC))) | =(matching1, 3)
f1182_1_length_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i178, o306, o306) → f1220_0_length_Return(EOS, java.lang.Object(ARRAY(3)), i178, o306, i183) | =(matching1, 3)
f1685_1_bubble_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o504, o504) → f2106_0_bubble_Return(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, o1354) | =(matching1, 3)
f1685_1_bubble_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o504, o504) → f2170_0_bubble_Return(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, o1389) | =(matching1, 3)
f1685_1_bubble_Load(EOS, java.lang.Object(ARRAY(matching1)), i178, i196, i241, o504, o504) → f2192_0_bubble_Return(EOS, java.lang.Object(ARRAY(3)), i178, i196, i241, java.lang.Object(List(EOC))) | =(matching1, 3)

Combined rules. Obtained 4 IRules

P rules:
f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), x1, x2, x3, x3, x2) → f1186_0_length_ConstantStackPush(EOS, x4, x4) | &&(&&(>=(x3, x2), <(x1, 2)), >(+(x1, 1), 0))
f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), x1, x2, x3, x3, x2) → f1689_0_bubble_Load(EOS, x4, x4) | <(x3, x2)
f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), x1, x2, x3, x3, x2) → f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), +(x1, 1), x4, 0, 0, x4) | &&(&&(>=(x3, x2), <(x1, 2)), >(+(x1, 1), 0))
f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), x1, x2, x3, x3, x2) → f1651_0_main_GE(EOS, java.lang.Object(ARRAY(3)), x1, x2, +(x3, 1), +(x3, 1), x2) | &&(<(x3, x2), >(+(x3, 1), 0))

Filtered ground terms:

f1651_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → f1651_0_main_GE(x3, x4, x5, x6, x7)
Cond_f1651_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1651_0_main_GE(x1, x4, x5, x6, x7, x8, x9)
f1186_0_length_ConstantStackPush(x1, x2, x3) → f1186_0_length_ConstantStackPush(x2, x3)
Cond_f1651_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1651_0_main_GE1(x1, x4, x5, x6, x7, x8, x9)
f1689_0_bubble_Load(x1, x2, x3) → f1689_0_bubble_Load(x2, x3)
Cond_f1651_0_main_GE2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1651_0_main_GE2(x1, x4, x5, x6, x7, x8, x9)
Cond_f1651_0_main_GE3(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1651_0_main_GE3(x1, x4, x5, x6, x7, x8)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY

Filtered duplicate terms:

f1651_0_main_GE(x1, x2, x3, x4, x5) → f1651_0_main_GE(x1, x4, x5)
Cond_f1651_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_f1651_0_main_GE(x1, x2, x5, x6, x7)
f1186_0_length_ConstantStackPush(x1, x2) → f1186_0_length_ConstantStackPush(x2)
Cond_f1651_0_main_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f1651_0_main_GE1(x1, x2, x5, x6, x7)
f1689_0_bubble_Load(x1, x2) → f1689_0_bubble_Load(x2)
Cond_f1651_0_main_GE2(x1, x2, x3, x4, x5, x6, x7) → Cond_f1651_0_main_GE2(x1, x2, x5, x6, x7)
Cond_f1651_0_main_GE3(x1, x2, x3, x4, x5, x6) → Cond_f1651_0_main_GE3(x1, x2, x5, x6)

Filtered unneeded terms:

Cond_f1651_0_main_GE(x1, x2, x3, x4, x5) → Cond_f1651_0_main_GE(x1)
Cond_f1651_0_main_GE1(x1, x2, x3, x4, x5) → Cond_f1651_0_main_GE1(x1)
Cond_f1651_0_main_GE2(x1, x2, x3, x4, x5) → Cond_f1651_0_main_GE2(x1, x2, x5)

Prepared 4 rules for path length conversion:

P rules:
f1651_0_main_GE(x1, x3, x2) → f1186_0_length_ConstantStackPush(x4) | &&(&&(>=(x3, x2), <(x1, 2)), >(+(x1, 1), 0))
f1651_0_main_GE(x1, x3, x2) → f1689_0_bubble_Load(x4) | <(x3, x2)
f1651_0_main_GE(x1, x3, x2) → f1651_0_main_GE(+(x1, 1), 0, x4) | &&(&&(>=(x3, x2), <(x1, 2)), >(+(x1, 1), 0))
f1651_0_main_GE(x1, x3, x2) → f1651_0_main_GE(x1, +(x3, 1), x2) | &&(<(x3, x2), >(+(x3, 1), 0))

Finished conversion. Obtained 2 rules.

P rules:
f1651_0_main_GE(x8, x9, x10) → f1651_0_main_GE(+(x8, 1), 0, x11) | &&(&&(>=(x9, x10), <(x8, 2)), >(x8, -1))
f1651_0_main_GE(x12, x13, x14) → f1651_0_main_GE(x12, +(x13, 1), x14) | &&(>(x13, -1), >(x14, x13))

(24) Obligation:

Rules:
f1651_0_main_GE(x8, x9, x10) → f1651_0_main_GE(+(x8, 1), 0, x11) | &&(&&(>=(x9, x10), <(x8, 2)), >(x8, -1))
f1651_0_main_GE(x12, x13, x14) → f1651_0_main_GE(x12, +(x13, 1), x14) | &&(>(x13, -1), >(x14, x13))

(25) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f1651_0_main_GE(x8, x10, x12)] = 1 - x8

Therefore the following rule(s) have been dropped:

f1651_0_main_GE(x0, x1, x2) → f1651_0_main_GE(+(x0, 1), 0, x3) | &&(&&(>=(x1, x2), <(x0, 2)), >(x0, -1))

(26) Obligation:

Rules:
f1651_0_main_GE(x4, x5, x6) → f1651_0_main_GE(x4, +(x5, 1), x6) | &&(>(x5, -1), >(x6, x5))

(27) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1651_0_main_GE(x4, x6, x8)] = -x6 + x8

Therefore the following rule(s) have been dropped:

f1651_0_main_GE(x0, x1, x2) → f1651_0_main_GE(x0, +(x1, 1), x2) | &&(>(x1, -1), >(x2, x1))

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) TRUE

(12) Obligation:

(13) SCCToIntTRSProof (SOUND transformation)

(14) Obligation:

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

(16) YES

(17) Obligation:

(18) SCCToIntTRSProof (SOUND transformation)

(19) Obligation:

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

(21) YES

(22) Obligation:

(23) SCCToIntTRSProof (SOUND transformation)

(24) Obligation:

(25) PolynomialOrderProcessor (SOUND transformation)

(26) Obligation:

(27) PolynomialOrderProcessor (EQUIVALENT transformation)

(28) YES