Termination proof of /tmp/tmp0pZIeV/BubbleSortR.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1673 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 377 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 238 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 3 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 216 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇔, 0 ms)

        ↳19 YES

(0) Obligation:

JBC Problem based on JBC Program:

class BubbleSortR {
    public static void main(String[] args) {
	Random.args = args;
	int dim = Random.random()*Random.random();
	int[] t = new int[dim] ;
	for(int i = 0; i < t.length; i++)
	    t[i] = Random.random();
	sort(t);
    }

    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
	    aux(0,n-pass,x);
	//for (int i = 0; i < x.length; i++)
	//    System.out.print(x[i]+ " ");
		}

    private static void aux(int min, int max, int[] x) {
	if (min >= max) return;
	int i = min;
	if (x[i] > x[i+1]) {
	    // exchange elements
	    int temp = x[i]; x[i] = x[i+1];  x[i+1] = temp;
	}
	aux(min+1,max,x);
    }
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
BubbleSortR.main([Ljava/lang/String;)V: Graph of 382 nodes with 2 SCCs.

BubbleSortR.aux(II[I)V: Graph of 223 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 3 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BubbleSortR.aux(II[I)V
SCC calls the following helper methods: BubbleSortR.aux(II[I)V
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 52 IRules

P rules:
f5360_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f5364_0_aux_LT(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428)
f5364_0_aux_LT(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428) → f5366_0_aux_LT(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428)
f5366_0_aux_LT(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428) → f5377_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) | <(i1427, i1428)
f5377_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) → f5391_0_aux_Store(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427)
f5391_0_aux_Store(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f5416_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427)
f5416_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f5444_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)))
f5444_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429))) → f5454_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f5454_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f5592_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f5592_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f5671_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504) | <(i1427, i1429)
f5671_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504) → f5678_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)))
f5678_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429))) → f5688_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1427)
f5688_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1427) → f5702_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1427, 1)
f5702_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1427, matching1) → f5712_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), +(i1427, 1)) | &&(>=(i1427, 0), =(matching1, 1))
f5712_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1514) → f5724_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1514)
f5724_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, java.lang.Object(ARRAY(i1429)), i1514) → f5741_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523) | <(i1514, i1429)
f5741_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523) → f5759_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523)
f5741_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523) → f5760_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523)
f5759_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523) → f5789_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) | <=(i1504, i1523)
f5789_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) → f6849_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)))
f6849_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) → f6873_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1428, java.lang.Object(ARRAY(i1429)), i1427)
f6873_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1428, java.lang.Object(ARRAY(i1429)), i1427) → f6909_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1428, java.lang.Object(ARRAY(i1429)), i1427, 1)
f6909_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1428, java.lang.Object(ARRAY(i1429)), i1427, matching1) → f6951_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1428, java.lang.Object(ARRAY(i1429)), +(i1427, 1)) | &&(>=(i1427, 0), =(matching1, 1))
f6951_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1428, java.lang.Object(ARRAY(i1429)), i1837) → f6964_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1837, i1428)
f6964_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1837, i1428) → f6998_0_aux_InvokeMethod(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)))
f6998_0_aux_InvokeMethod(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429))) → f7051_0_aux_Load(EOS, i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)))
f6998_0_aux_InvokeMethod(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429))) → f7051_1_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)))
f7051_0_aux_Load(EOS, i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429))) → f7065_0_aux_Load(EOS, i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)))
f7065_0_aux_Load(EOS, i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429))) → f5335_0_aux_Load(EOS, i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)))
f5335_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) → f5360_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427)
f5760_0_aux_LE(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1504, i1523) → f5795_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) | >(i1504, i1523)
f5795_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f5815_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)))
f5815_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429))) → f5862_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f5862_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f5878_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f5878_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f5914_0_aux_Store(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) | <(i1427, i1429)
f5914_0_aux_Store(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f5940_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427)
f5940_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f5963_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)))
f5963_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429))) → f5995_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f5995_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f6017_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)))
f6017_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429))) → f6060_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f6060_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f6103_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, 1)
f6103_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, matching1) → f6136_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), +(i1427, 1)) | &&(>=(i1427, 0), =(matching1, 1))
f6136_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1628) → f6188_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1628)
f6188_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1628) → f6263_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) | <(i1628, i1429)
f6263_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f6292_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427)
f6292_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)), i1427) → f6318_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) | <(i1427, i1429)
f6318_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427) → f6392_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429)))
f6392_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, java.lang.Object(ARRAY(i1429))) → f6467_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1427)
f6467_0_aux_ConstantStackPush(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1427) → f6705_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1427, 1)
f6705_0_aux_IntArithmetic(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1427, matching1) → f6728_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), +(i1427, 1)) | &&(>=(i1427, 0), =(matching1, 1))
f6728_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1800) → f6745_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1800)
f6745_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1800) → f6809_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1800)
f6809_0_aux_ArrayAccess(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429)), java.lang.Object(ARRAY(i1429)), i1800) → f6849_0_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1427, i1428, java.lang.Object(ARRAY(i1429))) | <(i1800, i1429)

Combined rules. Obtained 3 IRules

P rules:
f6998_0_aux_InvokeMethod(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429))) → f7051_1_aux_Load(EOS, i1427, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)), i1837, i1428, java.lang.Object(ARRAY(i1429)))
f6998_0_aux_InvokeMethod(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x3, x1, java.lang.Object(ARRAY(x2))) → f6998_0_aux_InvokeMethod(EOS, x3, x1, java.lang.Object(ARRAY(x2)), +(x3, 1), x1, java.lang.Object(ARRAY(x2))) | &&(&&(>(+(x3, 1), 0), <(+(x3, 1), x2)), <(x3, x1))
f6998_0_aux_InvokeMethod(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x3, x1, java.lang.Object(ARRAY(x2))) → f6998_0_aux_InvokeMethod(EOS, x3, x1, java.lang.Object(ARRAY(x2)), +(x3, 1), x1, java.lang.Object(ARRAY(x2))) | &&(&&(>(+(x3, 1), 0), <(x3, x1)), <(+(x3, 1), x2))

Filtered ground terms:

f6998_0_aux_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → f6998_0_aux_InvokeMethod(x2, x3, x4, x5, x6, x7)
f7051_1_aux_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f7051_1_aux_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f6998_0_aux_InvokeMethod(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6998_0_aux_InvokeMethod(x1, x3, x4, x5, x6, x7, x8)
Cond_f6998_0_aux_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f6998_0_aux_InvokeMethod1(x1, x3, x4, x5, x6, x7, x8)

Filtered duplicate terms:

f6998_0_aux_InvokeMethod(x1, x2, x3, x4, x5, x6) → f6998_0_aux_InvokeMethod(x1, x4, x5, x6)
f7051_1_aux_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f7051_1_aux_Load(x1, x7, x8, x9)
Cond_f6998_0_aux_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_f6998_0_aux_InvokeMethod(x1, x2, x5, x6, x7)
Cond_f6998_0_aux_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_f6998_0_aux_InvokeMethod1(x1, x2, x5, x6, x7)

Filtered unneeded terms:

Cond_f6998_0_aux_InvokeMethod(x1, x2, x3, x4, x5) → Cond_f6998_0_aux_InvokeMethod(x1, x3, x4, x5)
Cond_f6998_0_aux_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_f6998_0_aux_InvokeMethod1(x1, x3, x4, x5)
f6998_0_aux_InvokeMethod(x1, x2, x3, x4) → f6998_0_aux_InvokeMethod(x2, x3, x4)

Prepared 3 rules for path length conversion:

P rules:
f6998_0_aux_InvokeMethod(i1837, i1428, java.lang.Object(ARRAY(i1429)), i1429) → f7051_1_aux_Load(i1427, i1837, i1428, java.lang.Object(ARRAY(i1429)))
f6998_0_aux_InvokeMethod(x3, x1, java.lang.Object(ARRAY(x2)), x2) → f6998_0_aux_InvokeMethod(+(x3, 1), x1, java.lang.Object(ARRAY(x2)), x2) | &&(&&(>(+(x3, 1), 0), <(+(x3, 1), x2)), <(x3, x1))
f6998_0_aux_InvokeMethod(x3, x1, java.lang.Object(ARRAY(x2)), x2) → f6998_0_aux_InvokeMethod(+(x3, 1), x1, java.lang.Object(ARRAY(x2)), x2) | &&(&&(>(+(x3, 1), 0), <(x3, x1)), <(+(x3, 1), x2))

Finished conversion. Obtained 2 rules.

P rules:
f6998_0_aux_InvokeMethod(x4, x5, v14, x6) → f6998_0_aux_InvokeMethod(+(x4, 1), x5, v15, x6) | &&(&&(&&(&&(&&(>(x6, +(x4, 1)), >(x5, x4)), >(x4, -1)), >(+(v15, 1), 1)), <=(v15, v14)), >(+(v14, 1), 1))
f6998_0_aux_InvokeMethod(x7, x8, v16, x9) → f6998_0_aux_InvokeMethod(+(x7, 1), x8, v17, x9) | &&(&&(&&(&&(&&(>(x9, +(x7, 1)), >(x8, x7)), >(x7, -1)), >(+(v17, 1), 1)), <=(v17, v16)), >(+(v16, 1), 1))

(7) Obligation:

Rules:
f6998_0_aux_InvokeMethod(x4, x5, v14, x6) → f6998_0_aux_InvokeMethod(+(x4, 1), x5, v15, x6) | &&(&&(&&(&&(&&(>(x6, +(x4, 1)), >(x5, x4)), >(x4, -1)), >(+(v15, 1), 1)), <=(v15, v14)), >(+(v14, 1), 1))
f6998_0_aux_InvokeMethod(x7, x8, v16, x9) → f6998_0_aux_InvokeMethod(+(x7, 1), x8, v17, x9) | &&(&&(&&(&&(&&(>(x9, +(x7, 1)), >(x8, x7)), >(x7, -1)), >(+(v17, 1), 1)), <=(v17, v16)), >(+(v16, 1), 1))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f6998_0_aux_InvokeMethod(x11, x13, x15, x17)] = -x11 + x17

Therefore the following rule(s) have been dropped:

f6998_0_aux_InvokeMethod(x0, x1, x2, x3) → f6998_0_aux_InvokeMethod(+(x0, 1), x1, x4, x3) | &&(&&(&&(&&(&&(>(x3, +(x0, 1)), >(x1, x0)), >(x0, -1)), >(+(x4, 1), 1)), <=(x4, x2)), >(+(x2, 1), 1))
f6998_0_aux_InvokeMethod(x5, x6, x7, x8) → f6998_0_aux_InvokeMethod(+(x5, 1), x6, x9, x8) | &&(&&(&&(&&(&&(>(x8, +(x5, 1)), >(x6, x5)), >(x5, -1)), >(+(x9, 1), 1)), <=(x9, x7)), >(+(x7, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BubbleSortR.main([Ljava/lang/String;)V
SCC calls the following helper methods: BubbleSortR.aux(II[I)V
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 22 IRules

P rules:
f7528_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, i2079) → f7530_0_sort_GE(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, i2079, i2078)
f7530_0_sort_GE(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, i2079, i2078) → f7543_0_sort_GE(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, i2079, i2078)
f7543_0_sort_GE(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, i2079, i2078) → f7568_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079) | <(i2079, i2078)
f7568_0_sort_ConstantStackPush(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079) → f7594_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, 0)
f7594_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1) → f7616_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, 0, i2078) | =(matching1, 0)
f7616_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2078) → f7629_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, 0, i2078, i2079) | =(matching1, 0)
f7629_0_sort_IntArithmetic(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2078, i2079) → f7642_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, 0, -(i2078, i2079)) | &&(&&(>=(i2078, 0), >(i2079, 0)), =(matching1, 0))
f7642_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2119) → f7657_0_sort_InvokeMethod(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, 0, i2119, java.lang.Object(ARRAY(i2077))) | =(matching1, 0)
f7657_0_sort_InvokeMethod(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2119, java.lang.Object(ARRAY(i2077))) → f7660_0_aux_Load(EOS, 0, i2119, java.lang.Object(ARRAY(i2077)), 0, i2119, java.lang.Object(ARRAY(i2077))) | =(matching1, 0)
f7657_0_sort_InvokeMethod(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2119, java.lang.Object(ARRAY(i2077))) → f7660_1_aux_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, 0, i2119, java.lang.Object(ARRAY(i2077)), 0, i2119, java.lang.Object(ARRAY(i2077))) | =(matching1, 0)
f7660_0_aux_Load(EOS, matching1, i2119, java.lang.Object(ARRAY(i2077)), matching2, i2119, java.lang.Object(ARRAY(i2077))) → f7663_0_aux_Load(EOS, 0, i2119, java.lang.Object(ARRAY(i2077)), 0, i2119, java.lang.Object(ARRAY(i2077))) | &&(=(matching1, 0), =(matching2, 0))
f7842_0_aux_Return(EOS, java.lang.Object(ARRAY(i2146)), java.lang.Object(ARRAY(i2146)), i2078, i2079, matching1, i2148, java.lang.Object(ARRAY(i2146)), matching2, i2148, java.lang.Object(ARRAY(i2146))) → f7961_0_sort_Inc(EOS, java.lang.Object(ARRAY(i2146)), java.lang.Object(ARRAY(i2146)), i2078, i2079) | &&(=(matching1, 0), =(matching2, 0))
f7961_0_sort_Inc(EOS, java.lang.Object(ARRAY(i2146)), java.lang.Object(ARRAY(i2146)), i2078, i2079) → f8013_0_sort_Inc(EOS, java.lang.Object(ARRAY(i2146)), java.lang.Object(ARRAY(i2146)), i2078, i2079)
f8013_0_sort_Inc(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2079) → f8128_0_sort_JMP(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, +(i2079, 1)) | >(i2079, 0)
f8128_0_sort_JMP(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2389) → f8175_0_sort_Load(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2389)
f8175_0_sort_Load(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2389) → f7519_0_sort_Load(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2389)
f7519_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079) → f7528_0_sort_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, i2079)
f7911_0_aux_Return(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2079, matching1, i2200, java.lang.Object(ARRAY(i2193))) → f8013_0_sort_Inc(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2079) | =(matching1, 0)
f7938_0_aux_Return(EOS, java.lang.Object(ARRAY(i2230)), java.lang.Object(ARRAY(i2230)), i2078, i2079, matching1, i2239, java.lang.Object(ARRAY(i2230))) → f7911_0_aux_Return(EOS, java.lang.Object(ARRAY(i2230)), java.lang.Object(ARRAY(i2230)), i2078, i2079, 0, i2239, java.lang.Object(ARRAY(i2230))) | =(matching1, 0)
f7660_1_aux_Load(EOS, java.lang.Object(ARRAY(i2146)), java.lang.Object(ARRAY(i2146)), i2078, i2079, matching1, i2148, java.lang.Object(ARRAY(i2146)), matching2, i2148, java.lang.Object(ARRAY(i2146))) → f7842_0_aux_Return(EOS, java.lang.Object(ARRAY(i2146)), java.lang.Object(ARRAY(i2146)), i2078, i2079, 0, i2148, java.lang.Object(ARRAY(i2146)), 0, i2148, java.lang.Object(ARRAY(i2146))) | &&(=(matching1, 0), =(matching2, 0))
f7660_1_aux_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2200, java.lang.Object(ARRAY(i2077)), matching2, i2200, java.lang.Object(ARRAY(i2077))) → f7911_0_aux_Return(EOS, java.lang.Object(ARRAY(i2193)), java.lang.Object(ARRAY(i2193)), i2078, i2079, 0, i2200, java.lang.Object(ARRAY(i2193))) | &&(=(matching1, 0), =(matching2, 0))
f7660_1_aux_Load(EOS, java.lang.Object(ARRAY(i2077)), java.lang.Object(ARRAY(i2077)), i2078, i2079, matching1, i2239, java.lang.Object(ARRAY(i2077)), matching2, i2239, java.lang.Object(ARRAY(i2077))) → f7938_0_aux_Return(EOS, java.lang.Object(ARRAY(i2230)), java.lang.Object(ARRAY(i2230)), i2078, i2079, 0, i2239, java.lang.Object(ARRAY(i2230))) | &&(=(matching1, 0), =(matching2, 0))

Combined rules. Obtained 3 IRules

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

Filtered ground terms:

f7528_0_sort_Load(x1, x2, x3, x4, x5, x6) → f7528_0_sort_Load(x2, x3, x4, x5, x6)
Cond_f7528_0_sort_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f7528_0_sort_Load(x1, x3, x4, x5, x6, x7)
f7663_0_aux_Load(x1, x2, x3, x4, x5, x6, x7) → f7663_0_aux_Load(x3, x4, x6, x7)
Cond_f7528_0_sort_Load1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f7528_0_sort_Load1(x1, x3, x4, x5, x6, x7, x8)
Cond_f7528_0_sort_Load2(x1, x2, x3, x4, x5, x6, x7) → Cond_f7528_0_sort_Load2(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:

f7528_0_sort_Load(x1, x2, x3, x4, x5) → f7528_0_sort_Load(x2, x3, x5)
Cond_f7528_0_sort_Load(x1, x2, x3, x4, x5, x6) → Cond_f7528_0_sort_Load(x1, x3, x4, x6)
f7663_0_aux_Load(x1, x2, x3, x4) → f7663_0_aux_Load(x3, x4)
Cond_f7528_0_sort_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f7528_0_sort_Load1(x1, x3, x4, x6, x7)
Cond_f7528_0_sort_Load2(x1, x2, x3, x4, x5, x6) → Cond_f7528_0_sort_Load2(x1, x3, x4, x6)

Filtered unneeded terms:

Cond_f7528_0_sort_Load(x1, x2, x3, x4) → Cond_f7528_0_sort_Load(x1)
Cond_f7528_0_sort_Load1(x1, x2, x3, x4, x5) → Cond_f7528_0_sort_Load1(x1, x3, x4)
Cond_f7528_0_sort_Load2(x1, x2, x3, x4) → Cond_f7528_0_sort_Load2(x1, x3, x4)
f7528_0_sort_Load(x1, x2, x3) → f7528_0_sort_Load(x2, x3)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

P rules:
f7528_0_sort_Load(x3, x4) → f7528_0_sort_Load(x3, +(x4, 1)) | &&(&&(>(x4, 0), >(x3, -1)), <(x4, x3))

(12) Obligation:

Rules:
f7528_0_sort_Load(x3, x4) → f7528_0_sort_Load(x3, +(x4, 1)) | &&(&&(>(x4, 0), >(x3, -1)), <(x4, x3))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f7528_0_sort_Load(x3, x5)] = x3 - x5

Therefore the following rule(s) have been dropped:

f7528_0_sort_Load(x0, x1) → f7528_0_sort_Load(x0, +(x1, 1)) | &&(&&(>(x1, 0), >(x0, -1)), <(x1, x0))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: BubbleSortR.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:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 44 IRules

P rules:
f4447_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161) → f4460_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161, java.lang.Object(ARRAY(i79)))
f4460_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161, java.lang.Object(ARRAY(i79))) → f4477_0_main_GE(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161, i79) | >=(i79, 0)
f4477_0_main_GE(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161, i79) → f4487_0_main_GE(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161, i79)
f4487_0_main_GE(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161, i79) → f4511_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) | <(i1161, i79)
f4511_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) → f4524_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)))
f4524_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79))) → f4537_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f4537_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4543_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f4543_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4604_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160)
f4604_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160) → f4631_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, java.lang.Object(ARRAY(i333)))
f4631_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, java.lang.Object(ARRAY(i333))) → f4652_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333) | >=(i333, 0)
f4652_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333) → f4660_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333)
f4652_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333) → f4662_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333)
f4660_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333) → f4673_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) | <(i1160, i333)
f4673_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4698_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i333)))
f4698_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i333))) → f4714_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i333)), i1160)
f4714_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i333)), i1160) → f4741_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i333)), i1160)
f4741_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i333)), i1160) → f4759_0_random_Store(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227)
f4759_0_random_Store(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227) → f4780_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227)
f4780_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227) → f4799_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227, i1160)
f4799_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227, i1160) → f4855_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227, i1160, 1)
f4855_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227, i1160, matching1) → f4996_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227, +(i1160, 1)) | &&(>(i1160, 0), =(matching1, 1))
f4996_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227, i1328) → f5013_0_random_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227)
f5013_0_random_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227) → f5045_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, o1227)
f5045_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(o1269sub)) → f5071_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(o1269sub))
f5071_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(o1269sub)) → f5088_0_length_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(o1269sub), java.lang.Object(o1269sub))
f5088_0_length_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(o1269sub), java.lang.Object(o1269sub)) → f5144_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(o1269sub), java.lang.Object(o1269sub))
f5144_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(java.lang.String(o1289sub, i1371)), java.lang.Object(java.lang.String(o1289sub, i1371))) → f5159_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(java.lang.String(o1289sub, i1371)), java.lang.Object(java.lang.String(o1289sub, i1371)))
f5159_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(java.lang.String(o1289sub, i1371)), java.lang.Object(java.lang.String(o1289sub, i1371))) → f5214_0_length_Return(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(java.lang.String(o1289sub, i1371)))
f5214_0_length_Return(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(java.lang.String(o1289sub, i1371))) → f5249_0_random_Return(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f5249_0_random_Return(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f5270_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f5270_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f5296_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f5296_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f5347_0_main_Inc(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) | <(i1161, i79)
f5347_0_main_Inc(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) → f5362_0_main_JMP(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), +(i1161, 1)) | >=(i1161, 0)
f5362_0_main_JMP(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1439) → f5406_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1439)
f5406_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1439) → f4412_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1439)
f4412_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) → f4447_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, i1161)
f4662_0_random_LT(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161, i1160, i333) → f4680_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) | >=(i1160, i333)
f4680_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4705_0_random_Return(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f4705_0_random_Return(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4737_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f4737_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4751_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161)
f4751_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161, java.lang.Object(ARRAY(i79)), i1161) → f4770_0_main_Inc(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) | <(i1161, i79)
f4770_0_main_Inc(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1161) → f4791_0_main_JMP(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), +(i1161, 1)) | >=(i1161, 0)
f4791_0_main_JMP(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1286) → f4845_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1286)
f4845_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1286) → f4412_0_main_Load(EOS, java.lang.Object(ARRAY(i333)), java.lang.Object(ARRAY(i79)), i1286)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:

f4447_0_main_Load(x1, x2, x3, x4, x5) → f4447_0_main_Load(x2, x3, x4, x5)
Cond_f4447_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f4447_0_main_Load(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f4447_0_main_Load(x1, x2, x3, x4) → f4447_0_main_Load(x1, x2, x4)
Cond_f4447_0_main_Load(x1, x2, x3, x4, x5) → Cond_f4447_0_main_Load(x1, x2, x3, x5)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(17) Obligation:

Rules:
f4447_0_main_Load(v8, v9, x2, x0, x1) → f4447_0_main_Load(v10, v11, +(x2, 1), x0, x1) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x2, -1), <(x2, x1)), >(x1, -1)), >(x0, -1)), >=(v9, v11)), >=(v9, v10)), >(+(v9, 1), 1)), >=(v8, v11)), >=(v8, v10)), >(+(v8, 1), 1)), >(+(v10, 1), 1)), >(+(v11, 1), 1))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f4447_0_main_Load(x8, x10, x12, x14, x16)] = -x12 + x16

Therefore the following rule(s) have been dropped:

f4447_0_main_Load(x0, x1, x2, x3, x4) → f4447_0_main_Load(x5, x6, +(x2, 1), x3, x4) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x2, -1), <(x2, x4)), >(x4, -1)), >(x3, -1)), >=(x1, x6)), >=(x1, x5)), >(+(x1, 1), 1)), >=(x0, x6)), >=(x0, x5)), >(+(x0, 1), 1)), >(+(x5, 1), 1)), >(+(x6, 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