Termination of the given JBC could be proven:

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

(0) Obligation:

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

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

	while (x + y > 0) {
	    if (Random.random() * Random.random() > 9)
		x--;
	    else
		y--;
	}
    }
}

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:
Test11.main([Ljava/lang/String;)V: Graph of 309 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: Test11.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:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 112 IRules

P rules:
f9897_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2587) → f9899_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2587, i966)
f9899_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2587, i966) → f9901_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, +(i2587, i966))
f9901_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2734) → f9903_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2734)
f9903_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2734) → f9907_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | >(i2734, 0)
f9907_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9910_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9910_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9912_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586)
f9912_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586) → f9913_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, java.lang.Object(ARRAY(i310)))
f9913_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, java.lang.Object(ARRAY(i310))) → f9915_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) | >=(i310, 0)
f9915_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9917_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310)
f9915_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9918_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310)
f9917_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9919_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | <(i2586, i310)
f9919_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9922_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)))
f9922_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310))) → f9925_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586)
f9925_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586) → f9928_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586)
f9928_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586) → f9933_0_random_Store(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735)
f9933_0_random_Store(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735) → f9937_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735)
f9937_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735) → f9942_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735, i2586)
f9942_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735, i2586) → f9949_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735, i2586, 1)
f9949_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735, i2586, matching1) → f9955_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735, +(i2586, 1)) | &&(>=(i2586, 0), =(matching1, 1))
f9955_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735, i2739) → f9959_0_random_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735)
f9959_0_random_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735) → f9969_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2735)
f9969_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2746sub)) → f9978_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2746sub))
f9978_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2746sub)) → f9989_0_length_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2746sub), java.lang.Object(o2746sub))
f9989_0_length_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2746sub), java.lang.Object(o2746sub)) → f10010_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2746sub), java.lang.Object(o2746sub))
f10010_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2758sub, i2756)), java.lang.Object(java.lang.String(o2758sub, i2756))) → f10019_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2758sub, i2756)), java.lang.Object(java.lang.String(o2758sub, i2756))) | >=(i2756, 0)
f10019_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2758sub, i2756)), java.lang.Object(java.lang.String(o2758sub, i2756))) → f10034_0_length_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2758sub, i2756)), i2756)
f10034_0_length_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2758sub, i2756)), i2756) → f10048_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756)
f10048_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10412_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756)
f10412_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10425_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756)
f10425_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10443_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739)
f10443_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739) → f10459_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, java.lang.Object(ARRAY(i310)))
f10459_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, java.lang.Object(ARRAY(i310))) → f10471_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310) | >=(i310, 0)
f10471_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310) → f10481_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310)
f10471_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310) → f10483_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310)
f10481_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310) → f10504_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) | <(i2739, i310)
f10504_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10524_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(ARRAY(i310)))
f10524_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(ARRAY(i310))) → f10545_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(ARRAY(i310)), i2739)
f10545_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(ARRAY(i310)), i2739) → f10568_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(ARRAY(i310)), i2739)
f10568_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(ARRAY(i310)), i2739) → f10599_0_random_Store(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920)
f10599_0_random_Store(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920) → f10622_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920)
f10622_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920) → f10647_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920, i2739)
f10647_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920, i2739) → f10669_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920, i2739, 1)
f10669_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920, i2739, matching1) → f10687_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920, +(i2739, 1)) | &&(>(i2739, 0), =(matching1, 1))
f10687_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920, i3054) → f10975_0_random_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920)
f10975_0_random_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920) → f10994_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, o2920)
f10994_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(o3028sub)) → f11008_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(o3028sub))
f11008_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(o3028sub)) → f11023_0_length_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(o3028sub), java.lang.Object(o3028sub))
f11023_0_length_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(o3028sub), java.lang.Object(o3028sub)) → f11059_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(o3028sub), java.lang.Object(o3028sub))
f11059_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(java.lang.String(o3070sub, i3160)), java.lang.Object(java.lang.String(o3070sub, i3160))) → f11074_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(java.lang.String(o3070sub, i3160)), java.lang.Object(java.lang.String(o3070sub, i3160))) | >=(i3160, 0)
f11074_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(java.lang.String(o3070sub, i3160)), java.lang.Object(java.lang.String(o3070sub, i3160))) → f11086_0_length_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(java.lang.String(o3070sub, i3160)), i3160)
f11086_0_length_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, java.lang.Object(java.lang.String(o3070sub, i3160)), i3160) → f11098_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i3160)
f11098_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i3160) → f11107_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i3160)
f11107_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i3160) → f11120_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, *(i2756, i3160))
f11120_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3180) → f11132_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3180, 9)
f11132_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3192, matching1) → f11139_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3192, 9) | =(matching1, 9)
f11132_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3193, matching1) → f11140_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3193, 9) | =(matching1, 9)
f11139_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3192, matching1) → f11151_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | &&(<=(i3192, 9), =(matching1, 9))
f11151_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f11162_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i2587, +(i966, -1))
f11162_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i2587, i3204) → f11172_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i3204)
f11172_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i3204) → f9701_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i3204)
f9701_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9897_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2587)
f11140_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i3193, matching1) → f11152_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | &&(>(i3193, 9), =(matching1, 9))
f11152_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f11164_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), +(i2587, -1), i966)
f11164_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i3205, i966) → f11178_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i3205, i966)
f11178_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i3205, i966) → f9701_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i3205, i966)
f10483_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756, i2739, i310) → f10509_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) | >=(i2739, i310)
f10509_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10528_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756)
f10528_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10547_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756)
f10547_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2756) → f10573_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10573_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10586_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10586_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10611_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10611_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10632_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10632_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10656_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i2587, +(i966, -1))
f10656_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i2587, i3049) → f10680_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i3049)
f10680_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i3049) → f9701_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i3049)
f9918_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9921_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | >=(i2586, i310)
f9921_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9923_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9923_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9927_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9927_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9931_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9931_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9940_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586)
f9940_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586) → f9947_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, java.lang.Object(ARRAY(i310)))
f9947_0_random_ArrayLength(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, java.lang.Object(ARRAY(i310))) → f9953_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) | >=(i310, 0)
f9953_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9957_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310)
f9953_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9958_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310)
f9957_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9964_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | <(i2586, i310)
f9964_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9973_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)))
f9973_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310))) → f9985_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586)
f9985_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586) → f9993_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586)
f9993_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(ARRAY(i310)), i2586) → f10004_0_random_Store(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751)
f10004_0_random_Store(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751) → f10014_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751)
f10014_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751) → f10027_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751, i2586)
f10027_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751, i2586) → f10039_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751, i2586, 1)
f10039_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751, i2586, matching1) → f10051_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751, +(i2586, 1)) | &&(>=(i2586, 0), =(matching1, 1))
f10051_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751, i2763) → f10419_0_random_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751)
f10419_0_random_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751) → f10433_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, o2751)
f10433_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2858sub)) → f10438_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2858sub))
f10438_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2858sub)) → f10449_0_length_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2858sub), java.lang.Object(o2858sub))
f10449_0_length_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2858sub), java.lang.Object(o2858sub)) → f10480_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(o2858sub), java.lang.Object(o2858sub))
f10480_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2879sub, i3022)), java.lang.Object(java.lang.String(o2879sub, i3022))) → f10491_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2879sub, i3022)), java.lang.Object(java.lang.String(o2879sub, i3022)))
f10491_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2879sub, i3022)), java.lang.Object(java.lang.String(o2879sub, i3022))) → f10517_0_length_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2879sub, i3022)))
f10517_0_length_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, java.lang.Object(java.lang.String(o2879sub, i3022))) → f10536_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10536_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10556_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10556_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10586_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9958_0_random_LT(EOS, java.lang.Object(ARRAY(i310)), i2587, i966, i2586, i310) → f9968_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) | >=(i2586, i310)
f9968_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9976_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9976_0_random_Return(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9987_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9987_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f9996_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f9996_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10008_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10008_0_main_LE(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10016_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966)
f10016_0_main_Inc(EOS, java.lang.Object(ARRAY(i310)), i2587, i966) → f10032_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i2587, +(i966, -1))
f10032_0_main_JMP(EOS, java.lang.Object(ARRAY(i310)), i2587, i2761) → f10046_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i2761)
f10046_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i2761) → f9701_0_main_Load(EOS, java.lang.Object(ARRAY(i310)), i2587, i2761)

Combined rules. Obtained 2 IRules

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

Filtered ground terms:


f9897_0_main_Load(x1, x2, x3, x4, x5) → f9897_0_main_Load(x2, x3, x4, x5)
Cond_f9897_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f9897_0_main_Load(x1, x3, x4, x5, x6)
Cond_f9897_0_main_Load1(x1, x2, x3, x4, x5, x6) → Cond_f9897_0_main_Load1(x1, x3, x4, x5, x6)

Filtered duplicate terms:


f9897_0_main_Load(x1, x2, x3, x4) → f9897_0_main_Load(x1, x3, x4)
Cond_f9897_0_main_Load(x1, x2, x3, x4, x5) → Cond_f9897_0_main_Load(x1, x2, x4, x5)
Cond_f9897_0_main_Load1(x1, x2, x3, x4, x5) → Cond_f9897_0_main_Load1(x1, x2, x4, x5)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 2 rules.

P rules:
f9897_0_main_Load(v10, x1, x2, x0) → f9897_0_main_Load(v11, -(x1, 1), x2, x0) | &&(&&(&&(&&(>(+(x2, x1), 0), >(x0, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f9897_0_main_Load(v12, x4, x5, x3) → f9897_0_main_Load(v13, x4, -(x5, 1), x3) | &&(&&(&&(&&(>(+(x5, x4), 0), >(x3, -1)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(6) Obligation:

Rules:
f9897_0_main_Load(v10, x1, x2, x0) → f9897_0_main_Load(v11, -(x1, 1), x2, x0) | &&(&&(&&(&&(>(+(x2, x1), 0), >(x0, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f9897_0_main_Load(v12, x4, x5, x3) → f9897_0_main_Load(v13, x4, -(x5, 1), x3) | &&(&&(&&(&&(>(+(x5, x4), 0), >(x3, -1)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f9897_0_main_Load(x11, x13, x15, x17)] = x13 + x15

Therefore the following rule(s) have been dropped:


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

(8) YES