Termination proof of /tmp/tmp1SIoE6/MergeSort.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 2466 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 239 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 138 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 56 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇔, 0 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIntTRSProof (⇒, 1349 ms)

        ↳22 intTRS

        ↳23 PolynomialOrderProcessor (⇒, 55 ms)

        ↳24 intTRS

        ↳25 TerminationGraphProcessor (⇔, 0 ms)

        ↳26 YES

    ↳27 JBCTerminationSCC

        ↳28 SCCToIntTRSProof (⇒, 137 ms)

        ↳29 intTRS

        ↳30 PolynomialOrderProcessor (⇔, 0 ms)

        ↳31 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class MergeSort {
    
    static void merge(int g, int d, int m, int T[]) {
	int TT[] = new int[T.length];
	int i, j;
	for (i = g; i <= m; i++) TT[i] = T[i];
	for (i = m+1; i <= d; i++) TT[d+m+1-i] = T[i];
	i = g; j = d;
	for (int k = g; k <= d; k++)
	    if (TT[i] < TT[j]) { T[k] = TT[i]; i++; }
	    else { T[k] = TT[j]; j--; }
    }
    

    static void sort(int g, int d, int T[]) {
	if (g < d) {
	    int m = (g+d)/2;
	    if (m-g < d-g) sort(g, m, T);
	    if (d - (m+1) < d-g) sort(m+1, d, T);
	    merge(g,d,m,T);
	}
    }

    public static void main(String args[]) {	
	int n = args.length;

	int T[] = new int[n];
	for (int i = 0; i < n; i++)
	    T[i] = args[i].length();

	/*
	for (int i = 0; i < n; i++)
	    System.out.print(T[i] + " ");
	System.out.println();
	*/

	sort(0, n-1, T);
	
	/*
	for (int i = 0; i < n; i++)
	    System.out.print(T[i] + " ");
	System.out.println();
	*/
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

MergeSort.sort(II[I)V: Graph of 157 nodes with 0 SCCs.

MergeSort.merge(III[I)V: Graph of 515 nodes with 3 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 5 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: MergeSort.merge(III[I)V
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:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 45 IRules

P rules:
f8312_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, i1771) → f8315_0_merge_GT(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, i1771, i805)
f8315_0_merge_GT(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, i1771, i805) → f8317_0_merge_GT(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, i1771, i805)
f8317_0_merge_GT(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, i1771, i805) → f8321_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771) | <=(i1771, i805)
f8321_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771) → f8324_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, java.lang.Object(ARRAY(i313)))
f8324_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, java.lang.Object(ARRAY(i313))) → f8334_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, java.lang.Object(ARRAY(i313)), i1769)
f8334_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, java.lang.Object(ARRAY(i313)), i1797) → f8345_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, java.lang.Object(ARRAY(i313)), i1797)
f8345_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, java.lang.Object(ARRAY(i313)), i1797) → f8350_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, java.lang.Object(ARRAY(i313)), i1797)
f8350_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, java.lang.Object(ARRAY(i313)), i1797) → f8354_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, i1798) | <(i1797, i313)
f8354_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, i1798) → f8377_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, i1798, java.lang.Object(ARRAY(i313)))
f8377_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, i1798, java.lang.Object(ARRAY(i313))) → f8381_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1770, i1771, i1798, java.lang.Object(ARRAY(i313)), i1770)
f8381_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, java.lang.Object(ARRAY(i313)), i1803) → f8404_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, java.lang.Object(ARRAY(i313)), i1803)
f8404_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, java.lang.Object(ARRAY(i313)), i1803) → f8430_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, java.lang.Object(ARRAY(i313)), i1803)
f8430_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, java.lang.Object(ARRAY(i313)), i1803) → f8436_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805) | <(i1803, i313)
f8436_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805) → f8481_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805)
f8436_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805) → f8482_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805)
f8481_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805) → f8507_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771) | >=(i1798, i1805)
f8507_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771) → f8536_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)))
f8536_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313))) → f8587_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771)
f8587_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771) → f8617_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)))
f8617_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313))) → f8651_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1803)
f8651_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1803) → f8704_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1803)
f8704_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1803) → f8733_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771) | <(i1803, i313)
f8733_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819, java.lang.Object(ARRAY(i313)), i1819) → f8790_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819, java.lang.Object(ARRAY(i313)), i1819)
f8790_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819, java.lang.Object(ARRAY(i313)), i1819) → f8862_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819, java.lang.Object(ARRAY(i313)), i1819)
f8862_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819, java.lang.Object(ARRAY(i313)), i1819) → f8954_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819) | <(i1819, i313)
f8954_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1819) → f9067_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, +(i1803, -1), i1819) | >=(i1803, 0)
f9067_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1830, i1819) → f9171_0_merge_JMP(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1830, +(i1819, 1)) | >=(i1819, 0)
f9171_0_merge_JMP(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1830, i1833) → f9346_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1830, i1833)
f9346_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1830, i1833) → f8300_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1830, i1833)
f8300_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771) → f8312_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1769, i1770, i1771, i1771)
f8482_0_merge_GE(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, i1798, i1805) → f8508_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771) | <(i1798, i1805)
f8508_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771) → f8538_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)))
f8538_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313))) → f8588_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771)
f8588_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771) → f8619_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)))
f8619_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313))) → f8654_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1797)
f8654_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1797) → f8707_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1797)
f8707_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771, java.lang.Object(ARRAY(i313)), i1797) → f8738_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1771, java.lang.Object(ARRAY(i313)), i1771) | <(i1797, i313)
f8738_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821, java.lang.Object(ARRAY(i313)), i1821) → f8794_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821, java.lang.Object(ARRAY(i313)), i1821)
f8794_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821, java.lang.Object(ARRAY(i313)), i1821) → f8890_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821, java.lang.Object(ARRAY(i313)), i1821)
f8890_0_merge_ArrayAccess(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821, java.lang.Object(ARRAY(i313)), i1821) → f8958_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821) | <(i1821, i313)
f8958_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1797, i1803, i1821) → f9101_0_merge_JMP(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), +(i1797, 1), i1803, i1821) | >=(i1797, 0)
f9101_0_merge_JMP(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1821) → f9226_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1821)
f9226_0_merge_Inc(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1821) → f9352_0_merge_JMP(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, +(i1821, 1)) | >=(i1821, 0)
f9352_0_merge_JMP(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1838) → f9481_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1838)
f9481_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1838) → f8300_0_merge_Load(EOS, i805, java.lang.Object(ARRAY(i313)), i805, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i1831, i1803, i1838)

Combined rules. Obtained 2 IRules

P rules:
f8312_0_merge_Load(EOS, x0, java.lang.Object(ARRAY(x1)), x0, java.lang.Object(ARRAY(x1)), java.lang.Object(ARRAY(x1)), x2, x3, x4, x4) → f8312_0_merge_Load(EOS, x0, java.lang.Object(ARRAY(x1)), x0, java.lang.Object(ARRAY(x1)), java.lang.Object(ARRAY(x1)), x2, -(x3, 1), +(x4, 1), +(x4, 1)) | &&(&&(&&(&&(&&(>(+(x4, 1), 0), <=(x4, x0)), <(x4, x1)), >(+(x3, 1), 0)), <(x3, x1)), <(x2, x1))
f8312_0_merge_Load(EOS, x0, java.lang.Object(ARRAY(x1)), x0, java.lang.Object(ARRAY(x1)), java.lang.Object(ARRAY(x1)), x2, x3, x4, x4) → f8312_0_merge_Load(EOS, x0, java.lang.Object(ARRAY(x1)), x0, java.lang.Object(ARRAY(x1)), java.lang.Object(ARRAY(x1)), +(x2, 1), x3, +(x4, 1), +(x4, 1)) | &&(&&(&&(&&(&&(>(+(x4, 1), 0), <=(x4, x0)), <(x4, x1)), <(x3, x1)), >(+(x2, 1), 0)), <(x2, x1))

Filtered ground terms:

f8312_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f8312_0_merge_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f8312_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f8312_0_merge_Load(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)
Cond_f8312_0_merge_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f8312_0_merge_Load1(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)

Filtered duplicate terms:

f8312_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f8312_0_merge_Load(x3, x5, x6, x7, x9)
Cond_f8312_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f8312_0_merge_Load(x1, x4, x6, x7, x8, x10)
Cond_f8312_0_merge_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f8312_0_merge_Load1(x1, x4, x6, x7, x8, x10)

Prepared 2 rules for path length conversion:

P rules:
f8312_0_merge_Load(x0, java.lang.Object(ARRAY(x1)), x2, x3, x4, x1) → f8312_0_merge_Load(x0, java.lang.Object(ARRAY(x1)), x2, -(x3, 1), +(x4, 1), x1) | &&(&&(&&(&&(&&(>(+(x4, 1), 0), <=(x4, x0)), <(x4, x1)), >(+(x3, 1), 0)), <(x3, x1)), <(x2, x1))
f8312_0_merge_Load(x0, java.lang.Object(ARRAY(x1)), x2, x3, x4, x1) → f8312_0_merge_Load(x0, java.lang.Object(ARRAY(x1)), +(x2, 1), x3, +(x4, 1), x1) | &&(&&(&&(&&(&&(>(+(x4, 1), 0), <=(x4, x0)), <(x4, x1)), <(x3, x1)), >(+(x2, 1), 0)), <(x2, x1))

Finished conversion. Obtained 2 rules.

P rules:
f8312_0_merge_Load(x0, v16, x2, x3, x4, x1) → f8312_0_merge_Load(x0, v17, x2, -(x3, 1), +(x4, 1), x1) | &&(&&(&&(&&(&&(&&(&&(&&(>(x4, -1), <=(x4, x0)), <(x4, x1)), >(x3, -1)), <(x3, x1)), <(x2, x1)), >(+(v17, 1), 1)), <=(v17, v16)), >(+(v16, 1), 1))
f8312_0_merge_Load(x5, v18, x7, x8, x9, x6) → f8312_0_merge_Load(x5, v19, +(x7, 1), x8, +(x9, 1), x6) | &&(&&(&&(&&(&&(&&(&&(&&(>(x9, -1), <=(x9, x5)), <(x9, x6)), <(x8, x6)), >(x7, -1)), <(x7, x6)), >(+(v19, 1), 1)), <=(v19, v18)), >(+(v18, 1), 1))

(7) Obligation:

Rules:
f8312_0_merge_Load(x0, v16, x2, x3, x4, x1) → f8312_0_merge_Load(x0, v17, x2, -(x3, 1), +(x4, 1), x1) | &&(&&(&&(&&(&&(&&(&&(&&(>(x4, -1), <=(x4, x0)), <(x4, x1)), >(x3, -1)), <(x3, x1)), <(x2, x1)), >(+(v17, 1), 1)), <=(v17, v16)), >(+(v16, 1), 1))
f8312_0_merge_Load(x5, v18, x7, x8, x9, x6) → f8312_0_merge_Load(x5, v19, +(x7, 1), x8, +(x9, 1), x6) | &&(&&(&&(&&(&&(&&(&&(&&(>(x9, -1), <=(x9, x5)), <(x9, x6)), <(x8, x6)), >(x7, -1)), <(x7, x6)), >(+(v19, 1), 1)), <=(v19, v18)), >(+(v18, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f8312_0_merge_Load(x15, x17, x19, x21, x23, x25)] = x15 - x23

Therefore the following rule(s) have been dropped:

f8312_0_merge_Load(x0, x1, x2, x3, x4, x5) → f8312_0_merge_Load(x0, x6, x2, -(x3, 1), +(x4, 1), x5) | &&(&&(&&(&&(&&(&&(&&(&&(>(x4, -1), <=(x4, x0)), <(x4, x5)), >(x3, -1)), <(x3, x5)), <(x2, x5)), >(+(x6, 1), 1)), <=(x6, x1)), >(+(x1, 1), 1))
f8312_0_merge_Load(x7, x8, x9, x10, x11, x12) → f8312_0_merge_Load(x7, x13, +(x9, 1), x10, +(x11, 1), x12) | &&(&&(&&(&&(&&(&&(&&(&&(>(x11, -1), <=(x11, x7)), <(x11, x12)), <(x10, x12)), >(x9, -1)), <(x9, x12)), >(+(x13, 1), 1)), <=(x13, x8)), >(+(x8, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: MergeSort.merge(III[I)V
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:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f2327_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, i350) → f2331_0_merge_GT(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, i350, i311)
f2331_0_merge_GT(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, i350, i311) → f2338_0_merge_GT(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, i350, i311)
f2338_0_merge_GT(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, i350, i311) → f2346_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350) | <=(i350, i311)
f2346_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350) → f2354_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)))
f2354_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313))) → f2367_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i311)
f2367_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i311) → f2374_0_merge_IntArithmetic(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i311, i312)
f2374_0_merge_IntArithmetic(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i311, i312) → f2389_0_merge_ConstantStackPush(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), +(i311, i312))
f2389_0_merge_ConstantStackPush(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i358) → f2400_0_merge_IntArithmetic(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i358, 1)
f2400_0_merge_IntArithmetic(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i358, matching1) → f2406_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), +(i358, 1)) | =(matching1, 1)
f2406_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i359) → f2416_0_merge_IntArithmetic(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i359, i350)
f2416_0_merge_IntArithmetic(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i359, i350) → f2429_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), -(i359, i350))
f2429_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i360) → f2436_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)))
f2436_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313))) → f2450_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)), i350)
f2450_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)), i364) → f2465_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)), i364)
f2465_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)), i364) → f2492_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)), i364)
f2492_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i360, java.lang.Object(ARRAY(i313)), i364) → f2552_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i360) | <(i364, i313)
f2552_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i424) → f2574_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i424)
f2574_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i424) → f2589_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i424)
f2589_0_merge_ArrayAccess(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364, java.lang.Object(ARRAY(i313)), i424) → f2625_0_merge_Inc(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364) | <(i424, i313)
f2625_0_merge_Inc(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i364) → f2680_0_merge_JMP(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), +(i364, 1)) | >=(i364, 0)
f2680_0_merge_JMP(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i433) → f2709_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i433)
f2709_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i433) → f2322_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i433)
f2322_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350) → f2327_0_merge_Load(EOS, i311, i312, java.lang.Object(ARRAY(i313)), i311, i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i350, i350)

Combined rules. Obtained 1 IRules

P rules:
f2327_0_merge_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), java.lang.Object(ARRAY(x2)), x3, x3) → f2327_0_merge_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), java.lang.Object(ARRAY(x2)), +(x3, 1), +(x3, 1)) | &&(&&(&&(>(+(x3, 1), 0), <=(x3, x0)), >(x2, -(+(+(x0, x1), 1), x3))), <(x3, x2))

Filtered ground terms:

f2327_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f2327_0_merge_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f2327_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_f2327_0_merge_Load(x1, x3, x4, x5, x6, x7, x8, x9, x10, x11)

Filtered duplicate terms:

f2327_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f2327_0_merge_Load(x4, x5, x7, x9)
Cond_f2327_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f2327_0_merge_Load(x1, x5, x6, x8, x10)

Prepared 1 rules for path length conversion:

P rules:
f2327_0_merge_Load(x0, x1, java.lang.Object(ARRAY(x2)), x3, x2) → f2327_0_merge_Load(x0, x1, java.lang.Object(ARRAY(x2)), +(x3, 1), x2) | &&(&&(&&(>(+(x3, 1), 0), <=(x3, x0)), >(x2, -(+(+(x0, x1), 1), x3))), <(x3, x2))

Finished conversion. Obtained 1 rules.

P rules:
f2327_0_merge_Load(x0, x1, v9, x3, x2) → f2327_0_merge_Load(x0, x1, v10, +(x3, 1), x2) | &&(&&(&&(&&(&&(&&(>(x3, -1), <=(x3, x0)), <(x3, x2)), >(x2, -(+(+(x0, x1), 1), x3))), >=(v9, v10)), >(+(v9, 1), 1)), >(+(v10, 1), 1))

(12) Obligation:

Rules:
f2327_0_merge_Load(x0, x1, v9, x3, x2) → f2327_0_merge_Load(x0, x1, v10, +(x3, 1), x2) | &&(&&(&&(&&(&&(&&(>(x3, -1), <=(x3, x0)), <(x3, x2)), >(x2, -(+(+(x0, x1), 1), x3))), >=(v9, v10)), >(+(v9, 1), 1)), >(+(v10, 1), 1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2327_0_merge_Load(x7, x9, x11, x13, x15)] = -x13 + x7

Therefore the following rule(s) have been dropped:

f2327_0_merge_Load(x0, x1, x2, x3, x4) → f2327_0_merge_Load(x0, x1, x5, +(x3, 1), x4) | &&(&&(&&(&&(&&(&&(>(x3, -1), <=(x3, x0)), <(x3, x4)), >(x4, -(+(+(x0, x1), 1), x3))), >=(x2, x5)), >(+(x2, 1), 1)), >(+(x5, 1), 1))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: MergeSort.merge(III[I)V
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:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 16 IRules

P rules:
f2302_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, i345) → f2304_0_merge_GT(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, i345, i312)
f2304_0_merge_GT(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, i345, i312) → f2307_0_merge_GT(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, i345, i312)
f2307_0_merge_GT(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, i345, i312) → f2311_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345) | <=(i345, i312)
f2311_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345) → f2314_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)))
f2314_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313))) → f2317_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)), i345)
f2317_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)), i345) → f2321_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)))
f2321_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313))) → f2325_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)), i345, java.lang.Object(ARRAY(i313)), i345)
f2325_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354) → f2329_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354)
f2329_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354) → f2335_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354)
f2335_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354) → f2341_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354) | <(i354, i313)
f2341_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354) → f2350_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354)
f2350_0_merge_ArrayAccess(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354, java.lang.Object(ARRAY(i313)), i354) → f2358_0_merge_Inc(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354) | <(i354, i313)
f2358_0_merge_Inc(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i354) → f2369_0_merge_JMP(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), +(i354, 1)) | >=(i354, 0)
f2369_0_merge_JMP(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i356) → f2380_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i356)
f2380_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i356) → f2298_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i356)
f2298_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345) → f2302_0_merge_Load(EOS, i312, java.lang.Object(ARRAY(i313)), i312, java.lang.Object(ARRAY(i313)), java.lang.Object(ARRAY(i313)), i345, i345)

Combined rules. Obtained 1 IRules

P rules:
f2302_0_merge_Load(EOS, x0, java.lang.Object(ARRAY(x1)), x0, java.lang.Object(ARRAY(x1)), java.lang.Object(ARRAY(x1)), x2, x2) → f2302_0_merge_Load(EOS, x0, java.lang.Object(ARRAY(x1)), x0, java.lang.Object(ARRAY(x1)), java.lang.Object(ARRAY(x1)), +(x2, 1), +(x2, 1)) | &&(&&(>(+(x2, 1), 0), <=(x2, x0)), <(x2, x1))

Filtered ground terms:

f2302_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f2302_0_merge_Load(x2, x3, x4, x5, x6, x7, x8)
Cond_f2302_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f2302_0_merge_Load(x1, x3, x4, x5, x6, x7, x8, x9)

Filtered duplicate terms:

f2302_0_merge_Load(x1, x2, x3, x4, x5, x6, x7) → f2302_0_merge_Load(x3, x5, x7)
Cond_f2302_0_merge_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2302_0_merge_Load(x1, x4, x6, x8)

Prepared 1 rules for path length conversion:

P rules:
f2302_0_merge_Load(x0, java.lang.Object(ARRAY(x1)), x2, x1) → f2302_0_merge_Load(x0, java.lang.Object(ARRAY(x1)), +(x2, 1), x1) | &&(&&(>(+(x2, 1), 0), <=(x2, x0)), <(x2, x1))

Finished conversion. Obtained 1 rules.

P rules:
f2302_0_merge_Load(x0, v7, x2, x1) → f2302_0_merge_Load(x0, v8, +(x2, 1), x1) | &&(&&(&&(&&(&&(>(x2, -1), <=(x2, x0)), <(x2, x1)), >(+(v8, 1), 1)), <=(v8, v7)), >(+(v7, 1), 1))

(17) Obligation:

Rules:
f2302_0_merge_Load(x0, v7, x2, x1) → f2302_0_merge_Load(x0, v8, +(x2, 1), x1) | &&(&&(&&(&&(&&(>(x2, -1), <=(x2, x0)), <(x2, x1)), >(+(v8, 1), 1)), <=(v8, v7)), >(+(v7, 1), 1))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2302_0_merge_Load(x6, x8, x10, x12)] = -x10 + x6

Therefore the following rule(s) have been dropped:

f2302_0_merge_Load(x0, x1, x2, x3) → f2302_0_merge_Load(x0, x4, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <=(x2, x0)), <(x2, x3)), >(+(x4, 1), 1)), <=(x4, x1)), >(+(x1, 1), 1))

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: MergeSort.sort(II[I)V
SCC calls the following helper methods: MergeSort.sort(II[I)V, MergeSort.merge(III[I)V
Performed SCC analyses:

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

(21) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 59 IRules

P rules:
f1405_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237) → f1409_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237, i160)
f1409_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237, i160) → f1415_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237, i160)
f1415_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237, i160) → f1427_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238))) | <(i237, i160)
f1427_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238))) → f1454_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237)
f1454_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237) → f1459_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237, i160)
f1459_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237, i160) → f1466_0_sort_ConstantStackPush(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), +(i237, i160))
f1466_0_sort_ConstantStackPush(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i249) → f1472_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i249, 2)
f1472_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i249, matching1) → f1477_0_sort_Store(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), /(i249, 2)) | =(matching1, 2)
f1477_0_sort_Store(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250) → f1484_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250)
f1484_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250) → f1488_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i250)
f1488_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i250) → f1493_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i250, i237)
f1493_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i250, i237) → f1497_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, -(i250, i237))
f1497_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257) → f1504_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i160)
f1504_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i160) → f1510_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i160, i237)
f1510_0_sort_IntArithmetic(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i160, i237) → f1517_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, -(i160, i237))
f1517_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i265) → f1524_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i265)
f1517_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i265) → f1525_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i265)
f1524_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i265) → f1531_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250) | >=(i257, i265)
f1531_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250) → f1683_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250)
f1683_0_sort_Load(EOS, i277, i160, java.lang.Object(ARRAY(i279)), i277, i160, java.lang.Object(ARRAY(i279)), i281) → f5226_0_sort_Load(EOS, i277, i160, java.lang.Object(ARRAY(i279)), i277, i160, java.lang.Object(ARRAY(i279)), i281)
f5226_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893) → f5241_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160)
f5241_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160) → f5254_0_sort_ConstantStackPush(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160, i893)
f5254_0_sort_ConstantStackPush(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160, i893) → f5256_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160, i893, 1)
f5256_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160, i893, matching1) → f5259_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160, +(i893, 1)) | =(matching1, 1)
f5259_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i160, i914) → f5263_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, -(i160, i914))
f5263_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916) → f5267_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i160)
f5267_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i160) → f5271_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i160, i891)
f5271_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i160, i891) → f5278_0_sort_GE(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, -(i160, i891))
f5278_0_sort_GE(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i917) → f5300_0_sort_GE(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i917)
f5300_0_sort_GE(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i916, i917) → f5305_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893) | <(i916, i917)
f5305_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893) → f5312_0_sort_ConstantStackPush(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i893)
f5312_0_sort_ConstantStackPush(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i893) → f5339_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i893, 1)
f5339_0_sort_IntArithmetic(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i893, matching1) → f5347_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, +(i893, 1)) | =(matching1, 1)
f5347_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923) → f5386_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160)
f5386_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160) → f5397_0_sort_InvokeMethod(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160, java.lang.Object(ARRAY(i892)))
f5397_0_sort_InvokeMethod(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160, java.lang.Object(ARRAY(i892))) → f5404_0_sort_Load(EOS, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892)))
f5397_0_sort_InvokeMethod(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160, java.lang.Object(ARRAY(i892))) → f5404_1_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892)))
f5404_0_sort_Load(EOS, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892))) → f5410_0_sort_Load(EOS, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892)))
f5410_0_sort_Load(EOS, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892))) → f1397_0_sort_Load(EOS, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892)))
f1397_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238))) → f1405_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i237)
f1525_0_sort_GE(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i257, i265) → f1538_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250) | <(i257, i265)
f1538_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250) → f1552_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237)
f1552_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237) → f1562_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237, i250)
f1562_0_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237, i250) → f1575_0_sort_InvokeMethod(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237, i250, java.lang.Object(ARRAY(i238)))
f1575_0_sort_InvokeMethod(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237, i250, java.lang.Object(ARRAY(i238))) → f1589_0_sort_Load(EOS, i237, i250, java.lang.Object(ARRAY(i238)), i237, i250, java.lang.Object(ARRAY(i238)))
f1575_0_sort_InvokeMethod(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237, i250, java.lang.Object(ARRAY(i238))) → f1589_1_sort_Load(EOS, i237, i160, java.lang.Object(ARRAY(i238)), i237, i160, java.lang.Object(ARRAY(i238)), i250, i237, i250, java.lang.Object(ARRAY(i238)), i237, i250, java.lang.Object(ARRAY(i238)))
f1589_0_sort_Load(EOS, i237, i250, java.lang.Object(ARRAY(i238)), i237, i250, java.lang.Object(ARRAY(i238))) → f1601_0_sort_Load(EOS, i237, i250, java.lang.Object(ARRAY(i238)), i237, i250, java.lang.Object(ARRAY(i238)))
f1601_0_sort_Load(EOS, i237, i250, java.lang.Object(ARRAY(i238)), i237, i250, java.lang.Object(ARRAY(i238))) → f1397_0_sort_Load(EOS, i237, i250, java.lang.Object(ARRAY(i238)), i237, i250, java.lang.Object(ARRAY(i238)))
f1663_0_sort_Return(EOS, i277, i160, java.lang.Object(ARRAY(i279)), i277, i160, java.lang.Object(ARRAY(i279)), i281, i277, i281, java.lang.Object(ARRAY(i279))) → f5162_0_sort_Return(EOS, i277, i160, java.lang.Object(ARRAY(i279)), i277, i160, java.lang.Object(ARRAY(i279)), i281, i277, i281, java.lang.Object(ARRAY(i279)))
f5162_0_sort_Return(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i891, i893, java.lang.Object(ARRAY(i892))) → f5226_0_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893)
f2544_0_sort_Return(EOS, i395, i160, java.lang.Object(ARRAY(i397)), i395, i160, java.lang.Object(ARRAY(i397)), i399, i395, i399, java.lang.Object(ARRAY(i397))) → f1663_0_sort_Return(EOS, i395, i160, java.lang.Object(ARRAY(i397)), i395, i160, java.lang.Object(ARRAY(i397)), i399, i395, i399, java.lang.Object(ARRAY(i397)))
f5161_0_sort_Return(EOS, i855, i160, java.lang.Object(ARRAY(i852)), i855, i160, java.lang.Object(ARRAY(i852)), i857, i855, i857, java.lang.Object(ARRAY(i852))) → f5162_0_sort_Return(EOS, i855, i160, java.lang.Object(ARRAY(i852)), i855, i160, java.lang.Object(ARRAY(i852)), i857, i855, i857, java.lang.Object(ARRAY(i852)))
f6243_0_sort_Return(EOS, i1172, i160, java.lang.Object(ARRAY(i1170)), i1172, i160, java.lang.Object(ARRAY(i1170)), i1174, i1172, i1174, java.lang.Object(ARRAY(i1170))) → f5162_0_sort_Return(EOS, i1172, i160, java.lang.Object(ARRAY(i1170)), i1172, i160, java.lang.Object(ARRAY(i1170)), i1174, i1172, i1174, java.lang.Object(ARRAY(i1170)))
f7773_0_sort_Return(EOS, i1599, i160, java.lang.Object(ARRAY(i1597)), i1599, i160, java.lang.Object(ARRAY(i1597)), i1601, i1599, i1601, java.lang.Object(ARRAY(i1597))) → f5162_0_sort_Return(EOS, i1599, i160, java.lang.Object(ARRAY(i1597)), i1599, i160, java.lang.Object(ARRAY(i1597)), i1601, i1599, i1601, java.lang.Object(ARRAY(i1597)))
f1589_1_sort_Load(EOS, i277, i160, java.lang.Object(ARRAY(i279)), i277, i160, java.lang.Object(ARRAY(i279)), i281, i277, i281, java.lang.Object(ARRAY(i279)), i277, i281, java.lang.Object(ARRAY(i279))) → f1663_0_sort_Return(EOS, i277, i160, java.lang.Object(ARRAY(i279)), i277, i160, java.lang.Object(ARRAY(i279)), i281, i277, i281, java.lang.Object(ARRAY(i279)))
f1589_1_sort_Load(EOS, i395, i160, java.lang.Object(ARRAY(i397)), i395, i160, java.lang.Object(ARRAY(i397)), i399, i395, i399, java.lang.Object(ARRAY(i397)), i395, i399, java.lang.Object(ARRAY(i397))) → f2544_0_sort_Return(EOS, i395, i160, java.lang.Object(ARRAY(i397)), i395, i160, java.lang.Object(ARRAY(i397)), i399, i395, i399, java.lang.Object(ARRAY(i397)))
f1589_1_sort_Load(EOS, i855, i160, java.lang.Object(ARRAY(i238)), i855, i160, java.lang.Object(ARRAY(i238)), i857, i855, i857, java.lang.Object(ARRAY(i238)), i855, i857, java.lang.Object(ARRAY(i238))) → f5161_0_sort_Return(EOS, i855, i160, java.lang.Object(ARRAY(i852)), i855, i160, java.lang.Object(ARRAY(i852)), i857, i855, i857, java.lang.Object(ARRAY(i852)))
f1589_1_sort_Load(EOS, i1172, i160, java.lang.Object(ARRAY(i238)), i1172, i160, java.lang.Object(ARRAY(i238)), i1174, i1172, i1174, java.lang.Object(ARRAY(i238)), i1172, i1174, java.lang.Object(ARRAY(i238))) → f6243_0_sort_Return(EOS, i1172, i160, java.lang.Object(ARRAY(i1170)), i1172, i160, java.lang.Object(ARRAY(i1170)), i1174, i1172, i1174, java.lang.Object(ARRAY(i1170)))
f1589_1_sort_Load(EOS, i1599, i160, java.lang.Object(ARRAY(i238)), i1599, i160, java.lang.Object(ARRAY(i238)), i1601, i1599, i1601, java.lang.Object(ARRAY(i238)), i1599, i1601, java.lang.Object(ARRAY(i238))) → f7773_0_sort_Return(EOS, i1599, i160, java.lang.Object(ARRAY(i1597)), i1599, i160, java.lang.Object(ARRAY(i1597)), i1601, i1599, i1601, java.lang.Object(ARRAY(i1597)))

Combined rules. Obtained 6 IRules

P rules:
f5397_0_sort_InvokeMethod(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160, java.lang.Object(ARRAY(i892))) → f5404_1_sort_Load(EOS, i891, i160, java.lang.Object(ARRAY(i892)), i891, i160, java.lang.Object(ARRAY(i892)), i893, i923, i160, java.lang.Object(ARRAY(i892)), i923, i160, java.lang.Object(ARRAY(i892)))
f1405_0_sort_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x0) → f5397_0_sort_InvokeMethod(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), /(+(x0, x1), 2), +(/(+(x0, x1), 2), 1), x1, java.lang.Object(ARRAY(x2))) | &&(<(-(x1, +(/(+(x0, x1), 2), 1)), -(x1, x0)), >(x1, x0))
f5397_0_sort_InvokeMethod(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x3, x4, x1, java.lang.Object(ARRAY(x2))) → f1405_0_sort_Load(EOS, x4, x1, java.lang.Object(ARRAY(x2)), x4, x1, java.lang.Object(ARRAY(x2)), x4)
f1405_0_sort_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x0) → f1405_0_sort_Load(EOS, x0, /(+(x0, x1), 2), java.lang.Object(ARRAY(x2)), x0, /(+(x0, x1), 2), java.lang.Object(ARRAY(x2)), x0) | &&(>(-(x1, x0), -(/(+(x0, x1), 2), x0)), >(x1, x0))
f1405_0_sort_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x0) → f5397_0_sort_InvokeMethod(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), /(+(x0, x1), 2), +(/(+(x0, x1), 2), 1), x1, java.lang.Object(ARRAY(x2))) | &&(&&(>(x1, x0), <(-(x1, +(/(+(x0, x1), 2), 1)), -(x1, x0))), >(-(x1, x0), -(/(+(x0, x1), 2), x0)))
f1405_0_sort_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x0) → f5397_0_sort_InvokeMethod(EOS, x0, x1, java.lang.Object(ARRAY(x3)), x0, x1, java.lang.Object(ARRAY(x3)), /(+(x0, x1), 2), +(/(+(x0, x1), 2), 1), x1, java.lang.Object(ARRAY(x3))) | &&(&&(>(x1, x0), <(-(x1, +(/(+(x0, x1), 2), 1)), -(x1, x0))), >(-(x1, x0), -(/(+(x0, x1), 2), x0)))

Filtered ground terms:

f5397_0_sort_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → f5397_0_sort_InvokeMethod(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)
f5404_1_sort_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → f5404_1_sort_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14)
f1405_0_sort_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f1405_0_sort_Load(x2, x3, x4, x5, x6, x7, x8)
Cond_f1405_0_sort_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1405_0_sort_Load(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1405_0_sort_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1405_0_sort_Load1(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1405_0_sort_Load2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1405_0_sort_Load2(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f1405_0_sort_Load3(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f1405_0_sort_Load3(x1, x3, x4, x5, x6, x7, x8, x9, x10)

Filtered duplicate terms:

f5397_0_sort_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f5397_0_sort_InvokeMethod(x4, x7, x8, x9, x10)
f5404_1_sort_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → f5404_1_sort_Load(x4, x7, x11, x12, x13)
f1405_0_sort_Load(x1, x2, x3, x4, x5, x6, x7) → f1405_0_sort_Load(x5, x6, x7)
Cond_f1405_0_sort_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1405_0_sort_Load(x1, x6, x7, x8)
Cond_f1405_0_sort_Load1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1405_0_sort_Load1(x1, x6, x7, x8)
Cond_f1405_0_sort_Load2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1405_0_sort_Load2(x1, x6, x7, x8)
Cond_f1405_0_sort_Load3(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1405_0_sort_Load3(x1, x6, x7, x8, x9)

Filtered unneeded terms:

Cond_f1405_0_sort_Load(x1, x2, x3, x4) → Cond_f1405_0_sort_Load(x1, x2, x4)
Cond_f1405_0_sort_Load1(x1, x2, x3, x4) → Cond_f1405_0_sort_Load1(x1, x2, x4)
Cond_f1405_0_sort_Load2(x1, x2, x3, x4) → Cond_f1405_0_sort_Load2(x1, x2, x4)
Cond_f1405_0_sort_Load3(x1, x2, x3, x4, x5) → Cond_f1405_0_sort_Load3(x1, x2, x4)
f1405_0_sort_Load(x1, x2, x3) → f1405_0_sort_Load(x1, x3)
f5397_0_sort_InvokeMethod(x1, x2, x3, x4, x5) → f5397_0_sort_InvokeMethod(x3, x4)

Prepared 5 rules for path length conversion:

P rules:
f5397_0_sort_InvokeMethod(i923, i160) → f5404_1_sort_Load(i891, i893, i923, i160, java.lang.Object(ARRAY(i892)))
f1405_0_sort_Load(x1, x0) → f5397_0_sort_InvokeMethod(+(/(+(x0, x1), 2), 1), x1) | &&(<(-(x1, +(/(+(x0, x1), 2), 1)), -(x1, x0)), >(x1, x0))
f5397_0_sort_InvokeMethod(x4, x1) → f1405_0_sort_Load(x1, x4)
f1405_0_sort_Load(x1, x0) → f1405_0_sort_Load(/(+(x0, x1), 2), x0) | &&(>(-(x1, x0), -(/(+(x0, x1), 2), x0)), >(x1, x0))
f1405_0_sort_Load(x1, x0) → f5397_0_sort_InvokeMethod(+(/(+(x0, x1), 2), 1), x1) | &&(&&(>(x1, x0), <(-(x1, +(/(+(x0, x1), 2), 1)), -(x1, x0))), >(-(x1, x0), -(/(+(x0, x1), 2), x0)))

Finished conversion. Obtained 7 rules.

P rules:
f1405_0_sort_Load(x5, x6) → f1405_0_sort_Load'(x5, x6) | &&(>(-(x5, x6), -(x5, +(div, 1))), <(x6, x5))
f1405_0_sort_Load'(x5, x6) → f5397_0_sort_InvokeMethod(+(div1, 1), x5) | &&(&&(&&(&&(&&(<(x6, x5), >=(-(+(x6, x5), *(2, div1)), 0)), <(-(+(x6, x5), *(2, div1)), 2)), >=(-(+(x6, x5), *(2, div)), 0)), >(-(x5, x6), -(x5, +(div, 1)))), <(-(+(x6, x5), *(2, div)), 2))
f5397_0_sort_InvokeMethod(x7, x8) → f1405_0_sort_Load(x8, x7)
f1405_0_sort_Load(x9, x10) → f1405_0_sort_Load'(x9, x10) | &&(>(-(x9, x10), -(div, x10)), >(x9, x10))
f1405_0_sort_Load'(x9, x10) → f1405_0_sort_Load(arith, x10) | &&(&&(&&(&&(&&(>(x9, x10), >(-(x9, x10), -(div, x10))), >=(-(+(x10, x9), *(2, div)), 0)), <(-(+(x10, x9), *(2, div)), 2)), <(-(+(x10, x9), *(2, arith)), 2)), >=(-(+(x10, x9), *(2, arith)), 0))
f1405_0_sort_Load(x11, x12) → f1405_0_sort_Load'(x11, x12) | &&(&&(<(x12, x11), >(-(x11, x12), -(div1, x12))), >(-(x11, x12), -(x11, +(div, 1))))
f1405_0_sort_Load'(x11, x12) → f5397_0_sort_InvokeMethod(+(div2, 1), x11) | &&(&&(&&(&&(&&(&&(&&(&&(<(x12, x11), >=(-(+(x12, x11), *(2, div2)), 0)), <(-(+(x12, x11), *(2, div2)), 2)), >=(-(+(x12, x11), *(2, div1)), 0)), <(-(+(x12, x11), *(2, div1)), 2)), >=(-(+(x12, x11), *(2, div)), 0)), <(-(+(x12, x11), *(2, div)), 2)), >(-(x11, x12), -(div1, x12))), >(-(x11, x12), -(x11, +(div, 1))))

(22) Obligation:

Rules:
f1405_0_sort_Load(x5, x6) → f1405_0_sort_Load'(x5, x6) | &&(>(-(x5, x6), -(x5, +(div, 1))), <(x6, x5))
f1405_0_sort_Load'(x5, x6) → f5397_0_sort_InvokeMethod(+(div1, 1), x5) | &&(&&(&&(&&(&&(<(x6, x5), >=(-(+(x6, x5), *(2, div1)), 0)), <(-(+(x6, x5), *(2, div1)), 2)), >=(-(+(x6, x5), *(2, div)), 0)), >(-(x5, x6), -(x5, +(div, 1)))), <(-(+(x6, x5), *(2, div)), 2))
f5397_0_sort_InvokeMethod(x7, x8) → f1405_0_sort_Load(x8, x7)
f1405_0_sort_Load(x9, x10) → f1405_0_sort_Load'(x9, x10) | &&(>(-(x9, x10), -(div, x10)), >(x9, x10))
f1405_0_sort_Load'(x9, x10) → f1405_0_sort_Load(arith, x10) | &&(&&(&&(&&(&&(>(x9, x10), >(-(x9, x10), -(div, x10))), >=(-(+(x10, x9), *(2, div)), 0)), <(-(+(x10, x9), *(2, div)), 2)), <(-(+(x10, x9), *(2, arith)), 2)), >=(-(+(x10, x9), *(2, arith)), 0))
f1405_0_sort_Load(x11, x12) → f1405_0_sort_Load'(x11, x12) | &&(&&(<(x12, x11), >(-(x11, x12), -(div1, x12))), >(-(x11, x12), -(x11, +(div, 1))))
f1405_0_sort_Load'(x11, x12) → f5397_0_sort_InvokeMethod(+(div2, 1), x11) | &&(&&(&&(&&(&&(&&(&&(&&(<(x12, x11), >=(-(+(x12, x11), *(2, div2)), 0)), <(-(+(x12, x11), *(2, div2)), 2)), >=(-(+(x12, x11), *(2, div1)), 0)), <(-(+(x12, x11), *(2, div1)), 2)), >=(-(+(x12, x11), *(2, div)), 0)), <(-(+(x12, x11), *(2, div)), 2)), >(-(x11, x12), -(div1, x12))), >(-(x11, x12), -(x11, +(div, 1))))

(23) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f1405_0_sort_Load(x26, x28)] = -2 + 2·x26 - 2·x28
[f1405_0_sort_Load'(x31, x33)] = -2 + x31 - x33
[f5397_0_sort_InvokeMethod(x36, x38)] = -2 - 2·x36 + 2·x38

Therefore the following rule(s) have been dropped:

f1405_0_sort_Load(x0, x1) → f1405_0_sort_Load'(x0, x1) | &&(>(-(x0, x1), -(x0, +(x2, 1))), <(x1, x0))
f1405_0_sort_Load(x9, x10) → f1405_0_sort_Load'(x9, x10) | &&(>(-(x9, x10), -(x11, x10)), >(x9, x10))
f1405_0_sort_Load(x16, x17) → f1405_0_sort_Load'(x16, x17) | &&(&&(<(x17, x16), >(-(x16, x17), -(x18, x17))), >(-(x16, x17), -(x16, +(x19, 1))))

(24) Obligation:

Rules:
f1405_0_sort_Load'(x3, x4) → f5397_0_sort_InvokeMethod(+(x5, 1), x3) | &&(&&(&&(&&(&&(<(x4, x3), >=(-(+(x4, x3), *(2, x5)), 0)), <(-(+(x4, x3), *(2, x5)), 2)), >=(-(+(x4, x3), *(2, x6)), 0)), >(-(x3, x4), -(x3, +(x6, 1)))), <(-(+(x4, x3), *(2, x6)), 2))
f5397_0_sort_InvokeMethod(x7, x8) → f1405_0_sort_Load(x8, x7) | TRUE
f1405_0_sort_Load'(x12, x13) → f1405_0_sort_Load(x14, x13) | &&(&&(&&(&&(&&(>(x12, x13), >(-(x12, x13), -(x15, x13))), >=(-(+(x13, x12), *(2, x15)), 0)), <(-(+(x13, x12), *(2, x15)), 2)), <(-(+(x13, x12), *(2, x14)), 2)), >=(-(+(x13, x12), *(2, x14)), 0))
f1405_0_sort_Load'(x20, x21) → f5397_0_sort_InvokeMethod(+(x22, 1), x20) | &&(&&(&&(&&(&&(&&(&&(&&(<(x21, x20), >=(-(+(x21, x20), *(2, x22)), 0)), <(-(+(x21, x20), *(2, x22)), 2)), >=(-(+(x21, x20), *(2, x23)), 0)), <(-(+(x21, x20), *(2, x23)), 2)), >=(-(+(x21, x20), *(2, x24)), 0)), <(-(+(x21, x20), *(2, x24)), 2)), >(-(x20, x21), -(x23, x21))), >(-(x20, x21), -(x20, +(x24, 1))))

(25) TerminationGraphProcessor (EQUIVALENT transformation)

Constructed the termination graph and obtained no non-trivial SCC(s).

(26) YES

(27) Obligation:

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

Used field analysis yielded the following read fields:
- java.lang.String: [count]
Marker field analysis yielded the following relations that could be markers:

(28) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f1272_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, i220) → f1278_0_main_GE(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, i220, i26)
f1278_0_main_GE(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, i220, i26) → f1284_0_main_GE(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, i220, i26)
f1284_0_main_GE(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, i220, i26) → f1295_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220) | <(i220, i26)
f1295_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220) → f1323_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)))
f1323_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26))) → f1332_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220)
f1332_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220) → f1340_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)))
f1340_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26))) → f1353_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220)
f1353_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220) → f1366_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220)
f1366_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220) → f1378_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, o151) | <(i220, i26)
f1378_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(o156sub)) → f1402_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(o156sub))
f1402_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(o156sub)) → f1419_0_length_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(o156sub), java.lang.Object(o156sub))
f1419_0_length_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(o156sub), java.lang.Object(o156sub)) → f1482_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(o156sub), java.lang.Object(o156sub))
f1482_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(java.lang.String(o164sub, i262)), java.lang.Object(java.lang.String(o164sub, i262))) → f1502_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(java.lang.String(o164sub, i262)), java.lang.Object(java.lang.String(o164sub, i262)))
f1502_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(java.lang.String(o164sub, i262)), java.lang.Object(java.lang.String(o164sub, i262))) → f1529_0_length_Return(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(java.lang.String(o164sub, i262)))
f1529_0_length_Return(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(java.lang.String(o164sub, i262))) → f1550_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220)
f1550_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220) → f1568_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220)
f1568_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, java.lang.Object(ARRAY(i26)), i220) → f1587_0_main_Inc(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220) | <(i220, i26)
f1587_0_main_Inc(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220) → f1612_0_main_JMP(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), +(i220, 1)) | >=(i220, 0)
f1612_0_main_JMP(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i270) → f1661_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i270)
f1661_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i270) → f1251_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i270)
f1251_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220) → f1272_0_main_Load(EOS, java.lang.Object(ARRAY(i26)), java.lang.Object(ARRAY(i26)), i26, java.lang.Object(ARRAY(i26)), i220, i220)

Combined rules. Obtained 1 IRules

P rules:
f1272_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x0, java.lang.Object(ARRAY(x0)), x1, x1) → f1272_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x0, java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(>(+(x1, 1), 0), <(x1, x0))

Filtered ground terms:

f1272_0_main_Load(x1, x2, x3, x4, x5, x6, x7) → f1272_0_main_Load(x2, x3, x4, x5, x6, x7)
Cond_f1272_0_main_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f1272_0_main_Load(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate terms:

f1272_0_main_Load(x1, x2, x3, x4, x5, x6) → f1272_0_main_Load(x4, x6)
Cond_f1272_0_main_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f1272_0_main_Load(x1, x5, x7)

Prepared 1 rules for path length conversion:

P rules:
f1272_0_main_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f1272_0_main_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(>(+(x1, 1), 0), <(x1, x0))

Finished conversion. Obtained 1 rules.

P rules:
f1272_0_main_Load(v5, x1, x0) → f1272_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(29) Obligation:

Rules:
f1272_0_main_Load(v5, x1, x0) → f1272_0_main_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(30) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1272_0_main_Load(x5, x7, x9)] = -x7 + x9

Therefore the following rule(s) have been dropped:

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

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIntTRSProof (SOUND transformation)

(22) Obligation:

(23) PolynomialOrderProcessor (SOUND transformation)

(24) Obligation:

(25) TerminationGraphProcessor (EQUIVALENT transformation)

(26) YES

(27) Obligation:

(28) SCCToIntTRSProof (SOUND transformation)

(29) Obligation:

(30) PolynomialOrderProcessor (EQUIVALENT transformation)

(31) YES