Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
public class Test12 {
    public static void main(String[] args) {
	Random.args = args;

	int x = args.length * 100, y = args.length * 200 / 13;

	rec(x, y);
    }

    private static void rec(int x, int y) {
	if (x + y > 0) {
	    if (Random.random() * Random.random() > 9)
		rec(x - 1, y);
	    else
		rec(x, y - 1);
	}
    }
}

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:
Test12.main([Ljava/lang/String;)V: Graph of 80 nodes with 0 SCCs.

Test12.rec(II)V: Graph of 370 nodes with 0 SCCs.


(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: Test12.rec(II)V
SCC calls the following helper methods: Test12.rec(II)V
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:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 132 IRules

P rules:
f10133_0_rec_Load(EOS, i6904, i1125, i6904, i1125, i6904) → f10134_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6904, i1125)
f10134_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6904, i1125) → f10137_0_rec_LE(EOS, i6904, i1125, i6904, i1125, +(i6904, i1125))
f10137_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i6909) → f10140_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i6909)
f10140_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i6909) → f10142_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i1125) | >(i6909, 0)
f10142_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i1125) → f10144_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125)
f10144_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125) → f10150_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6903)
f10150_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6903) → f10152_0_random_ArrayLength(EOS, i6904, i1125, i6904, i1125, i6903, java.lang.Object(ARRAY(i286)))
f10152_0_random_ArrayLength(EOS, i6904, i1125, i6904, i1125, i6903, java.lang.Object(ARRAY(i286))) → f10153_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286) | >=(i286, 0)
f10153_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286) → f10154_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286)
f10153_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286) → f10155_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286)
f10154_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286) → f10157_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125) | <(i6903, i286)
f10157_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125) → f10159_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(ARRAY(i286)))
f10159_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(ARRAY(i286))) → f10161_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(ARRAY(i286)), i6903)
f10161_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(ARRAY(i286)), i6903) → f10163_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(ARRAY(i286)), i6903)
f10163_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(ARRAY(i286)), i6903) → f10168_0_random_Store(EOS, i6904, i1125, i6904, i1125, o4435)
f10168_0_random_Store(EOS, i6904, i1125, i6904, i1125, o4435) → f10171_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, o4435)
f10171_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, o4435) → f10175_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, o4435, i6903)
f10175_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, o4435, i6903) → f10178_0_random_IntArithmetic(EOS, i6904, i1125, i6904, i1125, o4435, i6903, 1)
f10178_0_random_IntArithmetic(EOS, i6904, i1125, i6904, i1125, o4435, i6903, matching1) → f10184_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, o4435, +(i6903, 1)) | &&(>=(i6903, 0), =(matching1, 1))
f10184_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, o4435, i6924) → f10189_0_random_Load(EOS, i6904, i1125, i6904, i1125, o4435)
f10189_0_random_Load(EOS, i6904, i1125, i6904, i1125, o4435) → f10195_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, o4435)
f10195_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, java.lang.Object(o4446sub)) → f10200_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, java.lang.Object(o4446sub))
f10200_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, java.lang.Object(o4446sub)) → f10208_0_length_Load(EOS, i6904, i1125, i6904, i1125, java.lang.Object(o4446sub), java.lang.Object(o4446sub))
f10208_0_length_Load(EOS, i6904, i1125, i6904, i1125, java.lang.Object(o4446sub), java.lang.Object(o4446sub)) → f10224_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(o4446sub), java.lang.Object(o4446sub))
f10224_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(java.lang.String(o4458sub, i6933)), java.lang.Object(java.lang.String(o4458sub, i6933))) → f10228_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(java.lang.String(o4458sub, i6933)), java.lang.Object(java.lang.String(o4458sub, i6933))) | >=(i6933, 0)
f10228_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, java.lang.Object(java.lang.String(o4458sub, i6933)), java.lang.Object(java.lang.String(o4458sub, i6933))) → f10237_0_length_Return(EOS, i6904, i1125, i6904, i1125, java.lang.Object(java.lang.String(o4458sub, i6933)), i6933)
f10237_0_length_Return(EOS, i6904, i1125, i6904, i1125, java.lang.Object(java.lang.String(o4458sub, i6933)), i6933) → f10245_0_random_Return(EOS, i6904, i1125, i6904, i1125, i6933)
f10245_0_random_Return(EOS, i6904, i1125, i6904, i1125, i6933) → f10249_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i1125, i6933)
f10249_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i1125, i6933) → f10260_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933)
f10260_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933) → f10276_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, i6924)
f10276_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, i6924) → f10286_0_random_ArrayLength(EOS, i6904, i1125, i6904, i1125, i6933, i6924, java.lang.Object(ARRAY(i286)))
f10286_0_random_ArrayLength(EOS, i6904, i1125, i6904, i1125, i6933, i6924, java.lang.Object(ARRAY(i286))) → f10304_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286) | >=(i286, 0)
f10304_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286) → f10310_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286)
f10304_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286) → f10311_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286)
f10310_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286) → f10324_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933) | <(i6924, i286)
f10324_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933) → f10338_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(ARRAY(i286)))
f10338_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(ARRAY(i286))) → f10359_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(ARRAY(i286)), i6924)
f10359_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(ARRAY(i286)), i6924) → f10372_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(ARRAY(i286)), i6924)
f10372_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(ARRAY(i286)), i6924) → f10388_0_random_Store(EOS, i6904, i1125, i6904, i1125, i6933, o4557)
f10388_0_random_Store(EOS, i6904, i1125, i6904, i1125, i6933, o4557) → f10399_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, o4557)
f10399_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, o4557) → f10410_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, i6933, o4557, i6924)
f10410_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, i6933, o4557, i6924) → f10424_0_random_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6933, o4557, i6924, 1)
f10424_0_random_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6933, o4557, i6924, matching1) → f10432_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, o4557, +(i6924, 1)) | &&(>(i6924, 0), =(matching1, 1))
f10432_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, o4557, i7026) → f10460_0_random_Load(EOS, i6904, i1125, i6904, i1125, i6933, o4557)
f10460_0_random_Load(EOS, i6904, i1125, i6904, i1125, i6933, o4557) → f10474_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, i6933, o4557)
f10474_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(o4647sub)) → f10488_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(o4647sub))
f10488_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(o4647sub)) → f10498_0_length_Load(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(o4647sub), java.lang.Object(o4647sub))
f10498_0_length_Load(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(o4647sub), java.lang.Object(o4647sub)) → f10578_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(o4647sub), java.lang.Object(o4647sub))
f10578_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(java.lang.String(o4741sub, i7220)), java.lang.Object(java.lang.String(o4741sub, i7220))) → f10599_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(java.lang.String(o4741sub, i7220)), java.lang.Object(java.lang.String(o4741sub, i7220))) | >=(i7220, 0)
f10599_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(java.lang.String(o4741sub, i7220)), java.lang.Object(java.lang.String(o4741sub, i7220))) → f10617_0_length_Return(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(java.lang.String(o4741sub, i7220)), i7220)
f10617_0_length_Return(EOS, i6904, i1125, i6904, i1125, i6933, java.lang.Object(java.lang.String(o4741sub, i7220)), i7220) → f10629_0_random_Return(EOS, i6904, i1125, i6904, i1125, i6933, i7220)
f10629_0_random_Return(EOS, i6904, i1125, i6904, i1125, i6933, i7220) → f10687_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6933, i7220)
f10687_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6933, i7220) → f10728_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, *(i6933, i7220))
f10728_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, i7485) → f10754_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7485, 9)
f10754_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7543, matching1) → f10767_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7543, 9) | =(matching1, 9)
f10754_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7544, matching1) → f10768_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7544, 9) | =(matching1, 9)
f10767_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7543, matching1) → f10865_0_rec_Load(EOS, i6904, i1125, i6904, i1125) | &&(<=(i7543, 9), =(matching1, 9))
f10865_0_rec_Load(EOS, i6904, i1125, i6904, i1125) → f10921_0_rec_Load(EOS, i6904, i1125, i1125, i6904)
f10921_0_rec_Load(EOS, i6904, i1125, i1125, i6904) → f10937_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125)
f10937_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125) → f10952_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, 1)
f10952_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, matching1) → f10961_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, -(i1125, 1)) | =(matching1, 1)
f10961_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i7911) → f10999_0_rec_Load(EOS, i6904, i7911, i6904, i7911)
f10961_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i7911) → f10999_1_rec_Load(EOS, i6904, i1125, i6904, i7911, i6904, i7911)
f10999_0_rec_Load(EOS, i6904, i7911, i6904, i7911) → f11016_0_rec_Load(EOS, i6904, i7911, i6904, i7911)
f11016_0_rec_Load(EOS, i6904, i7911, i6904, i7911) → f10131_0_rec_Load(EOS, i6904, i7911, i6904, i7911)
f10131_0_rec_Load(EOS, i6904, i1125, i6904, i1125) → f10133_0_rec_Load(EOS, i6904, i1125, i6904, i1125, i6904)
f10768_0_rec_LE(EOS, i6904, i1125, i6904, i1125, i7544, matching1) → f10867_0_rec_Load(EOS, i6904, i1125, i6904, i1125) | &&(>(i7544, 9), =(matching1, 9))
f10867_0_rec_Load(EOS, i6904, i1125, i6904, i1125) → f10922_0_rec_ConstantStackPush(EOS, i6904, i1125, i1125, i6904)
f10922_0_rec_ConstantStackPush(EOS, i6904, i1125, i1125, i6904) → f10939_0_rec_IntArithmetic(EOS, i6904, i1125, i1125, i6904, 1)
f10939_0_rec_IntArithmetic(EOS, i6904, i1125, i1125, i6904, matching1) → f10953_0_rec_Load(EOS, i6904, i1125, i1125, -(i6904, 1)) | =(matching1, 1)
f10953_0_rec_Load(EOS, i6904, i1125, i1125, i7909) → f10962_0_rec_InvokeMethod(EOS, i6904, i1125, i7909, i1125)
f10962_0_rec_InvokeMethod(EOS, i6904, i1125, i7909, i1125) → f11000_0_rec_Load(EOS, i7909, i1125, i7909, i1125)
f10962_0_rec_InvokeMethod(EOS, i6904, i1125, i7909, i1125) → f11000_1_rec_Load(EOS, i6904, i1125, i7909, i1125, i7909, i1125)
f11000_0_rec_Load(EOS, i7909, i1125, i7909, i1125) → f11017_0_rec_Load(EOS, i7909, i1125, i7909, i1125)
f11017_0_rec_Load(EOS, i7909, i1125, i7909, i1125) → f10131_0_rec_Load(EOS, i7909, i1125, i7909, i1125)
f10311_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6933, i6924, i286) → f10326_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, i6933) | >=(i6924, i286)
f10326_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, i6933) → f10340_0_random_Return(EOS, i6904, i1125, i6904, i1125, i6933, 0)
f10340_0_random_Return(EOS, i6904, i1125, i6904, i1125, i6933, matching1) → f10360_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6933, 0) | =(matching1, 0)
f10360_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, i6933, matching1) → f10374_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10374_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, matching1) → f10380_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10380_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, matching1) → f10394_0_rec_LE(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10394_0_rec_LE(EOS, i6904, i1125, i6904, i1125, matching1) → f10404_0_rec_Load(EOS, i6904, i1125, i6904, i1125) | =(matching1, 0)
f10404_0_rec_Load(EOS, i6904, i1125, i6904, i1125) → f10417_0_rec_Load(EOS, i6904, i1125, i1125, i6904)
f10417_0_rec_Load(EOS, i6904, i1125, i1125, i6904) → f10430_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125)
f10430_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125) → f10449_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, 1)
f10449_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, matching1) → f10465_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, -(i1125, 1)) | =(matching1, 1)
f10465_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i7055) → f10479_0_rec_Load(EOS, i6904, i7055, i6904, i7055)
f10465_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i7055) → f10479_1_rec_Load(EOS, i6904, i1125, i6904, i7055, i6904, i7055)
f10479_0_rec_Load(EOS, i6904, i7055, i6904, i7055) → f10493_0_rec_Load(EOS, i6904, i7055, i6904, i7055)
f10493_0_rec_Load(EOS, i6904, i7055, i6904, i7055) → f10131_0_rec_Load(EOS, i6904, i7055, i6904, i7055)
f10155_0_random_LT(EOS, i6904, i1125, i6904, i1125, i6903, i286) → f10158_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125) | >=(i6903, i286)
f10158_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125) → f10160_0_random_Return(EOS, i6904, i1125, i6904, i1125, 0)
f10160_0_random_Return(EOS, i6904, i1125, i6904, i1125, matching1) → f10162_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10162_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i1125, matching1) → f10165_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10165_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1) → f10174_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0, i6903) | =(matching1, 0)
f10174_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1, i6903) → f10177_0_random_ArrayLength(EOS, i6904, i1125, i6904, i1125, 0, i6903, java.lang.Object(ARRAY(i286))) | =(matching1, 0)
f10177_0_random_ArrayLength(EOS, i6904, i1125, i6904, i1125, matching1, i6903, java.lang.Object(ARRAY(i286))) → f10183_0_random_LT(EOS, i6904, i1125, i6904, i1125, 0, i6903, i286) | &&(>=(i286, 0), =(matching1, 0))
f10183_0_random_LT(EOS, i6904, i1125, i6904, i1125, matching1, i6903, i286) → f10186_0_random_LT(EOS, i6904, i1125, i6904, i1125, 0, i6903, i286) | =(matching1, 0)
f10183_0_random_LT(EOS, i6904, i1125, i6904, i1125, matching1, i6903, i286) → f10187_0_random_LT(EOS, i6904, i1125, i6904, i1125, 0, i6903, i286) | =(matching1, 0)
f10186_0_random_LT(EOS, i6904, i1125, i6904, i1125, matching1, i6903, i286) → f10192_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0) | &&(<(i6903, i286), =(matching1, 0))
f10192_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1) → f10198_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(ARRAY(i286))) | =(matching1, 0)
f10198_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(ARRAY(i286))) → f10204_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(ARRAY(i286)), i6903) | =(matching1, 0)
f10204_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(ARRAY(i286)), i6903) → f10212_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(ARRAY(i286)), i6903) | =(matching1, 0)
f10212_0_random_ArrayAccess(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(ARRAY(i286)), i6903) → f10219_0_random_Store(EOS, i6904, i1125, i6904, i1125, 0, o4451) | =(matching1, 0)
f10219_0_random_Store(EOS, i6904, i1125, i6904, i1125, matching1, o4451) → f10226_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0, o4451) | =(matching1, 0)
f10226_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1, o4451) → f10232_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, 0, o4451, i6903) | =(matching1, 0)
f10232_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, matching1, o4451, i6903) → f10241_0_random_IntArithmetic(EOS, i6904, i1125, i6904, i1125, 0, o4451, i6903, 1) | =(matching1, 0)
f10241_0_random_IntArithmetic(EOS, i6904, i1125, i6904, i1125, matching1, o4451, i6903, matching2) → f10247_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0, o4451, +(i6903, 1)) | &&(&&(>=(i6903, 0), =(matching1, 0)), =(matching2, 1))
f10247_0_random_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1, o4451, i6935) → f10254_0_random_Load(EOS, i6904, i1125, i6904, i1125, 0, o4451) | =(matching1, 0)
f10254_0_random_Load(EOS, i6904, i1125, i6904, i1125, matching1, o4451) → f10265_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, 0, o4451) | =(matching1, 0)
f10265_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(o4482sub)) → f10272_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(o4482sub)) | =(matching1, 0)
f10272_0_random_InvokeMethod(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(o4482sub)) → f10281_0_length_Load(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(o4482sub), java.lang.Object(o4482sub)) | =(matching1, 0)
f10281_0_length_Load(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(o4482sub), java.lang.Object(o4482sub)) → f10307_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(o4482sub), java.lang.Object(o4482sub)) | =(matching1, 0)
f10307_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(java.lang.String(o4507sub, i6969)), java.lang.Object(java.lang.String(o4507sub, i6969))) → f10315_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(java.lang.String(o4507sub, i6969)), java.lang.Object(java.lang.String(o4507sub, i6969))) | &&(>=(i6969, 0), =(matching1, 0))
f10315_0_length_FieldAccess(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(java.lang.String(o4507sub, i6969)), java.lang.Object(java.lang.String(o4507sub, i6969))) → f10333_0_length_Return(EOS, i6904, i1125, i6904, i1125, 0, java.lang.Object(java.lang.String(o4507sub, i6969)), i6969) | =(matching1, 0)
f10333_0_length_Return(EOS, i6904, i1125, i6904, i1125, matching1, java.lang.Object(java.lang.String(o4507sub, i6969)), i6969) → f10344_0_random_Return(EOS, i6904, i1125, i6904, i1125, 0, i6969) | =(matching1, 0)
f10344_0_random_Return(EOS, i6904, i1125, i6904, i1125, matching1, i6969) → f10364_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, 0, i6969) | =(matching1, 0)
f10364_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, matching1, i6969) → f10380_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10187_0_random_LT(EOS, i6904, i1125, i6904, i1125, matching1, i6903, i286) → f10193_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, 0) | &&(>=(i6903, i286), =(matching1, 0))
f10193_0_random_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, matching1) → f10199_0_random_Return(EOS, i6904, i1125, i6904, i1125, 0, 0) | =(matching1, 0)
f10199_0_random_Return(EOS, i6904, i1125, i6904, i1125, matching1, matching2) → f10205_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f10205_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, matching1, matching2) → f10214_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, 0) | &&(=(matching1, 0), =(matching2, 0))
f10214_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125, matching1) → f10221_0_rec_LE(EOS, i6904, i1125, i6904, i1125, 0) | =(matching1, 0)
f10221_0_rec_LE(EOS, i6904, i1125, i6904, i1125, matching1) → f10227_0_rec_Load(EOS, i6904, i1125, i6904, i1125) | =(matching1, 0)
f10227_0_rec_Load(EOS, i6904, i1125, i6904, i1125) → f10236_0_rec_Load(EOS, i6904, i1125, i1125, i6904)
f10236_0_rec_Load(EOS, i6904, i1125, i1125, i6904) → f10243_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125)
f10243_0_rec_ConstantStackPush(EOS, i6904, i1125, i6904, i1125) → f10248_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, 1)
f10248_0_rec_IntArithmetic(EOS, i6904, i1125, i6904, i1125, matching1) → f10258_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, -(i1125, 1)) | =(matching1, 1)
f10258_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i6938) → f10268_0_rec_Load(EOS, i6904, i6938, i6904, i6938)
f10258_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i6938) → f10268_1_rec_Load(EOS, i6904, i1125, i6904, i6938, i6904, i6938)
f10268_0_rec_Load(EOS, i6904, i6938, i6904, i6938) → f10275_0_rec_Load(EOS, i6904, i6938, i6904, i6938)
f10275_0_rec_Load(EOS, i6904, i6938, i6904, i6938) → f10131_0_rec_Load(EOS, i6904, i6938, i6904, i6938)

Combined rules. Obtained 8 IRules

P rules:
f10465_0_rec_InvokeMethod(EOS, i6904, i1125, i6904, i7055) → f10479_1_rec_Load(EOS, i6904, i1125, i6904, i7055, i6904, i7055)
f10133_0_rec_Load(EOS, x0, x1, x0, x1, x0) → f10999_1_rec_Load(EOS, x0, x1, x0, -(x1, 1), x0, -(x1, 1)) | >(+(x0, x1), 0)
f10133_0_rec_Load(EOS, x0, x1, x0, x1, x0) → f10133_0_rec_Load(EOS, x0, -(x1, 1), x0, -(x1, 1), x0) | >(+(x0, x1), 0)
f10133_0_rec_Load(EOS, x0, x1, x0, x1, x0) → f11000_1_rec_Load(EOS, x0, x1, -(x0, 1), x1, -(x0, 1), x1) | >(+(x0, x1), 0)
f10133_0_rec_Load(EOS, x0, x1, x0, x1, x0) → f10133_0_rec_Load(EOS, -(x0, 1), x1, -(x0, 1), x1, -(x0, 1)) | >(+(x0, x1), 0)
f10133_0_rec_Load(EOS, x0, x1, x0, x1, x0) → f10465_0_rec_InvokeMethod(EOS, x0, x1, x0, -(x1, 1)) | >(+(x0, x1), 0)
f10465_0_rec_InvokeMethod(EOS, x0, x1, x0, x2) → f10133_0_rec_Load(EOS, x0, x2, x0, x2, x0)
f10133_0_rec_Load(EOS, x0, x1, x0, x1, x0) → f10268_1_rec_Load(EOS, x0, x1, x0, -(x1, 1), x0, -(x1, 1)) | >(+(x0, x1), 0)

Filtered ground terms:


f10465_0_rec_InvokeMethod(x1, x2, x3, x4, x5) → f10465_0_rec_InvokeMethod(x2, x3, x4, x5)
f10479_1_rec_Load(x1, x2, x3, x4, x5, x6, x7) → f10479_1_rec_Load(x2, x3, x4, x5, x6, x7)
f10133_0_rec_Load(x1, x2, x3, x4, x5, x6) → f10133_0_rec_Load(x2, x3, x4, x5, x6)
Cond_f10133_0_rec_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f10133_0_rec_Load(x1, x3, x4, x5, x6, x7)
f10999_1_rec_Load(x1, x2, x3, x4, x5, x6, x7) → f10999_1_rec_Load(x2, x3, x4, x5, x6, x7)
Cond_f10133_0_rec_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f10133_0_rec_Load1(x1, x3, x4, x5, x6, x7)
Cond_f10133_0_rec_Load2(x1, x2, x3, x4, x5, x6, x7) → Cond_f10133_0_rec_Load2(x1, x3, x4, x5, x6, x7)
f11000_1_rec_Load(x1, x2, x3, x4, x5, x6, x7) → f11000_1_rec_Load(x2, x3, x4, x5, x6, x7)
Cond_f10133_0_rec_Load3(x1, x2, x3, x4, x5, x6, x7) → Cond_f10133_0_rec_Load3(x1, x3, x4, x5, x6, x7)
Cond_f10133_0_rec_Load4(x1, x2, x3, x4, x5, x6, x7) → Cond_f10133_0_rec_Load4(x1, x3, x4, x5, x6, x7)
Cond_f10133_0_rec_Load5(x1, x2, x3, x4, x5, x6, x7) → Cond_f10133_0_rec_Load5(x1, x3, x4, x5, x6, x7)
f10268_1_rec_Load(x1, x2, x3, x4, x5, x6, x7) → f10268_1_rec_Load(x2, x3, x4, x5, x6, x7)

Filtered duplicate terms:


f10465_0_rec_InvokeMethod(x1, x2, x3, x4) → f10465_0_rec_InvokeMethod(x2, x3, x4)
f10479_1_rec_Load(x1, x2, x3, x4, x5, x6) → f10479_1_rec_Load(x2, x5, x6)
f10133_0_rec_Load(x1, x2, x3, x4, x5) → f10133_0_rec_Load(x4, x5)
Cond_f10133_0_rec_Load(x1, x2, x3, x4, x5, x6) → Cond_f10133_0_rec_Load(x1, x5, x6)
f10999_1_rec_Load(x1, x2, x3, x4, x5, x6) → f10999_1_rec_Load(x5, x6)
Cond_f10133_0_rec_Load1(x1, x2, x3, x4, x5, x6) → Cond_f10133_0_rec_Load1(x1, x5, x6)
Cond_f10133_0_rec_Load2(x1, x2, x3, x4, x5, x6) → Cond_f10133_0_rec_Load2(x1, x5, x6)
f11000_1_rec_Load(x1, x2, x3, x4, x5, x6) → f11000_1_rec_Load(x5, x6)
Cond_f10133_0_rec_Load3(x1, x2, x3, x4, x5, x6) → Cond_f10133_0_rec_Load3(x1, x5, x6)
Cond_f10133_0_rec_Load4(x1, x2, x3, x4, x5, x6) → Cond_f10133_0_rec_Load4(x1, x5, x6)
Cond_f10133_0_rec_Load5(x1, x2, x3, x4, x5, x6) → Cond_f10133_0_rec_Load5(x1, x5, x6)
f10268_1_rec_Load(x1, x2, x3, x4, x5, x6) → f10268_1_rec_Load(x5, x6)

Filtered unneeded terms:


Cond_f10133_0_rec_Load(x1, x2, x3) → Cond_f10133_0_rec_Load(x1)
Cond_f10133_0_rec_Load2(x1, x2, x3) → Cond_f10133_0_rec_Load2(x1)
Cond_f10133_0_rec_Load5(x1, x2, x3) → Cond_f10133_0_rec_Load5(x1)
f10465_0_rec_InvokeMethod(x1, x2, x3) → f10465_0_rec_InvokeMethod(x2, x3)

Prepared 8 rules for path length conversion:

P rules:
f10465_0_rec_InvokeMethod(i6904, i7055) → f10479_1_rec_Load(i1125, i6904, i7055)
f10133_0_rec_Load(x1, x0) → f10999_1_rec_Load(x0, -(x1, 1)) | >(+(x0, x1), 0)
f10133_0_rec_Load(x1, x0) → f10133_0_rec_Load(-(x1, 1), x0) | >(+(x0, x1), 0)
f10133_0_rec_Load(x1, x0) → f11000_1_rec_Load(-(x0, 1), x1) | >(+(x0, x1), 0)
f10133_0_rec_Load(x1, x0) → f10133_0_rec_Load(x1, -(x0, 1)) | >(+(x0, x1), 0)
f10133_0_rec_Load(x1, x0) → f10465_0_rec_InvokeMethod(x0, -(x1, 1)) | >(+(x0, x1), 0)
f10465_0_rec_InvokeMethod(x0, x2) → f10133_0_rec_Load(x2, x0)
f10133_0_rec_Load(x1, x0) → f10268_1_rec_Load(x0, -(x1, 1)) | >(+(x0, x1), 0)

Finished conversion. Obtained 4 rules.

P rules:
f10133_0_rec_Load(x5, x6) → f10133_0_rec_Load(-(x5, 1), x6) | >(+(x6, x5), 0)
f10133_0_rec_Load(x9, x10) → f10133_0_rec_Load(x9, -(x10, 1)) | >(+(x10, x9), 0)
f10133_0_rec_Load(x11, x12) → f10465_0_rec_InvokeMethod(x12, -(x11, 1)) | >(+(x12, x11), 0)
f10465_0_rec_InvokeMethod(x13, x14) → f10133_0_rec_Load(x14, x13)

(6) Obligation:

Rules:
f10133_0_rec_Load(x5, x6) → f10133_0_rec_Load(-(x5, 1), x6) | >(+(x6, x5), 0)
f10133_0_rec_Load(x9, x10) → f10133_0_rec_Load(x9, -(x10, 1)) | >(+(x10, x9), 0)
f10133_0_rec_Load(x11, x12) → f10465_0_rec_InvokeMethod(x12, -(x11, 1)) | >(+(x12, x11), 0)
f10465_0_rec_InvokeMethod(x13, x14) → f10133_0_rec_Load(x14, x13)

(7) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f10133_0_rec_Load(x9, x11)] = -1 + x11 + x9
[f10465_0_rec_InvokeMethod(x14, x16)] = -1 + x14 + x16

Therefore the following rule(s) have been dropped:


f10133_0_rec_Load(x0, x1) → f10133_0_rec_Load(-(x0, 1), x1) | >(+(x1, x0), 0)
f10133_0_rec_Load(x2, x3) → f10133_0_rec_Load(x2, -(x3, 1)) | >(+(x3, x2), 0)
f10133_0_rec_Load(x4, x5) → f10465_0_rec_InvokeMethod(x5, -(x4, 1)) | >(+(x5, x4), 0)

(8) Obligation:

Rules:
f10465_0_rec_InvokeMethod(x6, x7) → f10133_0_rec_Load(x7, x6) | TRUE

(9) TerminationGraphProcessor (EQUIVALENT transformation)

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


(10) YES