Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 2994 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 516 ms)
↳6 intTRS
↳7 PolynomialOrderProcessor (⇒, 0 ms)
↳8 intTRS
↳9 PolynomialOrderProcessor (⇔, 0 ms)
↳10 YES

(0) Obligation:

JBC Problem based on JBC Program:
class BubbleSort {
    public static void main(String[] args) {
	sort(new int[100]);
    }

    public static void sort(int[] x) {
	int n = x.length;
	for (int pass=1; pass < n; pass++)  // count how many times
	    // This next loop becomes shorter and shorter
	    for (int i=0; i < n - pass; i++)
		if (x[i] > x[i+1]) {
		    // exchange elements
		    int temp = x[i]; x[i] = x[i+1];  x[i+1] = temp;
		}
    }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BubbleSort.main([Ljava/lang/String;)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:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 59 IRules

P rules:
f2810_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i110, i110) → f2813_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i110, i110, 100) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f2813_0_sort_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i114, matching4) → f2815_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i114, 100) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f2815_0_sort_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i114, matching4) → f2818_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114) | &&(&&(&&(&&(<(i114, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f2818_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114) → f2822_0_sort_Store(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, 0) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f2822_0_sort_Store(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, matching4) → f2825_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, 0) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 0))
f2825_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, matching4) → f2883_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, 0) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 0))
f2883_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i117) → f3867_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i117) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f3867_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i135) → f5256_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i135) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5256_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i153) → f5696_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i153) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5696_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171) → f5699_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, i171) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5699_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171) → f5700_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, i171, 100) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5700_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171, matching4) → f5702_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, i171, 100, i114) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f5702_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171, matching4, i114) → f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, i171, -(100, i114)) | &&(&&(&&(&&(>(i114, 0), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171, i173) → f5705_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, i171, i173) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171, i173) → f5706_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, i171, i173) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5705_0_sort_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171, i173) → f5707_0_sort_Inc(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114) | &&(&&(&&(>=(i171, i173), =(matching1, 100)), =(matching2, 100)), =(matching3, 100))
f5707_0_sort_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114) → f5710_0_sort_JMP(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, +(i114, 1)) | &&(&&(&&(>(i114, 0), =(matching1, 100)), =(matching2, 100)), =(matching3, 100))
f5710_0_sort_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i174) → f5725_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i174) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5725_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i174) → f2807_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i174) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f2807_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i110) → f2810_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i110, i110) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5706_0_sort_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, i171, i173) → f5709_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171) | &&(&&(&&(<(i171, i173), =(matching1, 100)), =(matching2, 100)), =(matching3, 100))
f5709_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171) → f5711_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, java.lang.Object(ARRAY(100))) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f5711_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i171, java.lang.Object(ARRAY(matching4))) → f5727_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i171, java.lang.Object(ARRAY(100)), i171) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f5727_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187) → f6071_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6071_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187) → f6074_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189) | &&(&&(&&(&&(<(i187, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6074_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189) → f6078_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, java.lang.Object(ARRAY(100))) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6078_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, java.lang.Object(ARRAY(matching4))) → f6089_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6089_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, java.lang.Object(ARRAY(matching4)), i187) → f6092_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, java.lang.Object(ARRAY(100)), i187, 1) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6092_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, java.lang.Object(ARRAY(matching4)), i187, matching5) → f6096_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, java.lang.Object(ARRAY(100)), +(i187, 1)) | &&(&&(&&(&&(&&(>=(i187, 0), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 1))
f6096_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, java.lang.Object(ARRAY(matching4)), i192) → f6098_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, java.lang.Object(ARRAY(100)), i192) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6098_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, java.lang.Object(ARRAY(matching4)), i192) → f6103_0_sort_LE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, i193) | &&(&&(&&(&&(<(i192, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6103_0_sort_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, i193) → f6107_0_sort_LE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, i193) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6103_0_sort_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, i193) → f6108_0_sort_LE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, i189, i193) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6107_0_sort_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, i193) → f6110_0_sort_Inc(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(&&(<=(i189, i193), =(matching1, 100)), =(matching2, 100)), =(matching3, 100))
f6110_0_sort_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187) → f6928_0_sort_Inc(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6928_0_sort_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187) → f6937_0_sort_JMP(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, +(i187, 1)) | &&(&&(&&(>=(i187, 0), =(matching1, 100)), =(matching2, 100)), =(matching3, 100))
f6937_0_sort_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i225) → f6965_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i225) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6965_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i225) → f5696_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i225) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6108_0_sort_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, i189, i193) → f6112_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(&&(>(i189, i193), =(matching1, 100)), =(matching2, 100)), =(matching3, 100))
f6112_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187) → f6124_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100))) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6124_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4))) → f6140_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6140_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187) → f6653_0_sort_Store(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(&&(&&(<(i187, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6653_0_sort_Store(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187) → f6659_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6659_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187) → f6664_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100))) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6664_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4))) → f6665_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6665_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187) → f6671_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187, java.lang.Object(ARRAY(100))) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6671_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187, java.lang.Object(ARRAY(matching5))) → f6676_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 100))
f6676_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187, java.lang.Object(ARRAY(matching5)), i187) → f6679_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187, java.lang.Object(ARRAY(100)), i187, 1) | &&(&&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 100))
f6679_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187, java.lang.Object(ARRAY(matching5)), i187, matching6) → f6685_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187, java.lang.Object(ARRAY(100)), +(i187, 1)) | &&(&&(&&(&&(&&(&&(>=(i187, 0), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 100)), =(matching6, 1))
f6685_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187, java.lang.Object(ARRAY(matching5)), i220) → f6700_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187, java.lang.Object(ARRAY(100)), i220) | &&(&&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 100))
f6700_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187, java.lang.Object(ARRAY(matching5)), i220) → f6705_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(&&(&&(<(i220, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 100))
f6705_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187) → f6860_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(&&(&&(<(i187, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6860_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187) → f6865_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100))) | &&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100))
f6865_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4))) → f6872_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6872_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187) → f6877_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i187, 1) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6877_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i187, matching5) → f6891_0_sort_Load(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), +(i187, 1)) | &&(&&(&&(&&(&&(>=(i187, 0), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100)), =(matching5, 1))
f6891_0_sort_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i222) → f6898_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i222) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6898_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i224) → f6904_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187, java.lang.Object(ARRAY(100)), i224) | &&(&&(&&(=(matching1, 100), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))
f6904_0_sort_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), matching3, i114, i187, java.lang.Object(ARRAY(matching4)), i224) → f6928_0_sort_Inc(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, i114, i187) | &&(&&(&&(&&(<(i224, 100), =(matching1, 100)), =(matching2, 100)), =(matching3, 100)), =(matching4, 100))

Combined rules. Obtained 3 IRules

P rules:
f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, x3, x4, x4, x5) → f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, +(x3, 1), 0, 0, -(100, +(x3, 1))) | &&(&&(<=(x5, x4), <(x3, 99)), >(x3, 0))
f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, x3, x4, x4, x5) → f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, x3, +(x4, 1), +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(+(x4, 1), 0)), <(x4, 99)), >(x3, 0)), <(x4, 100))
f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, x3, x4, x4, x5) → f5703_0_sort_GE(EOS, java.lang.Object(ARRAY(100)), java.lang.Object(ARRAY(100)), 100, x3, +(x4, 1), +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(+(x4, 1), 0)), <(x4, 99)), <(x4, 100)), >(x3, 0))

Filtered ground terms:


f5703_0_sort_GE(x1, x2, x3, x4, x5, x6, x7, x8) → f5703_0_sort_GE(x5, x6, x7, x8)
Cond_f5703_0_sort_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f5703_0_sort_GE(x1, x6, x7, x8, x9)
Cond_f5703_0_sort_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f5703_0_sort_GE1(x1, x6, x7, x8, x9)
Cond_f5703_0_sort_GE2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f5703_0_sort_GE2(x1, x6, x7, x8, x9)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY

Filtered duplicate terms:


f5703_0_sort_GE(x1, x2, x3, x4) → f5703_0_sort_GE(x1, x3, x4)
Cond_f5703_0_sort_GE(x1, x2, x3, x4, x5) → Cond_f5703_0_sort_GE(x1, x2, x4, x5)
Cond_f5703_0_sort_GE1(x1, x2, x3, x4, x5) → Cond_f5703_0_sort_GE1(x1, x2, x4, x5)
Cond_f5703_0_sort_GE2(x1, x2, x3, x4, x5) → Cond_f5703_0_sort_GE2(x1, x2, x4, x5)

Filtered unneeded terms:


Cond_f5703_0_sort_GE(x1, x2, x3, x4) → Cond_f5703_0_sort_GE(x1, x2)
Cond_f5703_0_sort_GE1(x1, x2, x3, x4) → Cond_f5703_0_sort_GE1(x1, x2, x3)
Cond_f5703_0_sort_GE2(x1, x2, x3, x4) → Cond_f5703_0_sort_GE2(x1, x2, x3)

Prepared 3 rules for path length conversion:

P rules:
f5703_0_sort_GE(x3, x4, x5) → f5703_0_sort_GE(+(x3, 1), 0, -(100, +(x3, 1))) | &&(&&(<=(x5, x4), <(x3, 99)), >(x3, 0))
f5703_0_sort_GE(x3, x4, x5) → f5703_0_sort_GE(x3, +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(+(x4, 1), 0)), <(x4, 99)), >(x3, 0)), <(x4, 100))
f5703_0_sort_GE(x3, x4, x5) → f5703_0_sort_GE(x3, +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(+(x4, 1), 0)), <(x4, 99)), <(x4, 100)), >(x3, 0))

Finished conversion. Obtained 3 rules.

P rules:
f5703_0_sort_GE(x0, x1, x2) → f5703_0_sort_GE(+(x0, 1), 0, -(100, +(x0, 1))) | &&(&&(<=(x2, x1), <(x0, 99)), >(x0, 0))
f5703_0_sort_GE(x3, x4, x5) → f5703_0_sort_GE(x3, +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(x4, -1)), <(x4, 99)), >(x3, 0)), <(x4, 100))
f5703_0_sort_GE(x6, x7, x8) → f5703_0_sort_GE(x6, +(x7, 1), -(100, x6)) | &&(&&(&&(&&(>(x8, x7), >(x7, -1)), <(x7, 99)), >(x6, 0)), <(x7, 100))

(6) Obligation:

Rules:
f5703_0_sort_GE(x0, x1, x2) → f5703_0_sort_GE(+(x0, 1), 0, -(100, +(x0, 1))) | &&(&&(<=(x2, x1), <(x0, 99)), >(x0, 0))
f5703_0_sort_GE(x3, x4, x5) → f5703_0_sort_GE(x3, +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(x4, -1)), <(x4, 99)), >(x3, 0)), <(x4, 100))
f5703_0_sort_GE(x6, x7, x8) → f5703_0_sort_GE(x6, +(x7, 1), -(100, x6)) | &&(&&(&&(&&(>(x8, x7), >(x7, -1)), <(x7, 99)), >(x6, 0)), <(x7, 100))

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f5703_0_sort_GE(x10, x12, x14)] = 98 - x10

Therefore the following rule(s) have been dropped:


f5703_0_sort_GE(x0, x1, x2) → f5703_0_sort_GE(+(x0, 1), 0, -(100, +(x0, 1))) | &&(&&(<=(x2, x1), <(x0, 99)), >(x0, 0))

(8) Obligation:

Rules:
f5703_0_sort_GE(x3, x4, x5) → f5703_0_sort_GE(x3, +(x4, 1), -(100, x3)) | &&(&&(&&(&&(>(x5, x4), >(x4, -1)), <(x4, 99)), >(x3, 0)), <(x4, 100))

(9) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f5703_0_sort_GE(x4, x6, x8)] = 98 - x6

Therefore the following rule(s) have been dropped:


f5703_0_sort_GE(x0, x1, x2) → f5703_0_sort_GE(x0, +(x1, 1), -(100, x0)) | &&(&&(&&(&&(>(x2, x1), >(x1, -1)), <(x1, 99)), >(x0, 0)), <(x1, 100))

(10) YES