Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class ListContentArbitrary{

  public static void main(String[] args) {
    Random.args = args;
    IntList l = IntList.createIntList();
    int n = Random.random();
    int m = l.nth(n);

    while (m > 0) m--;
  }

}

class IntList {
  int value;
  IntList next;

  public IntList(int value, IntList next) {
    this.value = value;
    this.next = next;
  }

  public static IntList createIntList() {

    int i = Random.random();
    IntList l = null;

    while (i > 0) {
      l = new IntList(Random.random(), l);
      i--;
    }

    return l;
  }

  public int nth(int n){

    IntList l = this;

    while (n > 1) {
      n--;
      l = l.next;
    }

    return l.value;
  }
}



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

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

IntList.createIntList()LIntList;: Graph of 163 nodes with 1 SCC.

(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: IntList.createIntList()LIntList;
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:
  

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 38 IRules

P rules:
f2192_0_createIntList_LE(EOS, i537, i537) → f2195_0_createIntList_LE(EOS, i537, i537)
f2195_0_createIntList_LE(EOS, i537, i537) → f2204_0_createIntList_New(EOS, i537) | >(i537, 0)
f2204_0_createIntList_New(EOS, i537) → f2214_0_createIntList_Duplicate(EOS, i537)
f2214_0_createIntList_Duplicate(EOS, i537) → f2223_0_createIntList_InvokeMethod(EOS, i537)
f2223_0_createIntList_InvokeMethod(EOS, i537) → f2236_0_random_FieldAccess(EOS, i537)
f2236_0_random_FieldAccess(EOS, i537) → f2243_0_random_FieldAccess(EOS, i537)
f2243_0_random_FieldAccess(EOS, i537) → f2250_0_random_ArrayAccess(EOS, i537)
f2250_0_random_ArrayAccess(EOS, i537) → f2254_0_random_ArrayAccess(EOS, i537)
f2254_0_random_ArrayAccess(EOS, i537) → f2261_0_random_Store(EOS, i537, o675)
f2261_0_random_Store(EOS, i537, o675) → f2267_0_random_FieldAccess(EOS, i537, o675)
f2267_0_random_FieldAccess(EOS, i537, o675) → f2274_0_random_ConstantStackPush(EOS, i537, o675)
f2274_0_random_ConstantStackPush(EOS, i537, o675) → f2282_0_random_IntArithmetic(EOS, i537, o675)
f2282_0_random_IntArithmetic(EOS, i537, o675) → f2289_0_random_FieldAccess(EOS, i537, o675)
f2289_0_random_FieldAccess(EOS, i537, o675) → f2295_0_random_Load(EOS, i537, o675)
f2295_0_random_Load(EOS, i537, o675) → f2303_0_random_InvokeMethod(EOS, i537, o675)
f2303_0_random_InvokeMethod(EOS, i537, java.lang.Object(o702sub)) → f2311_0_random_InvokeMethod(EOS, i537, java.lang.Object(o702sub))
f2311_0_random_InvokeMethod(EOS, i537, java.lang.Object(o702sub)) → f2316_0_length_Load(EOS, i537, java.lang.Object(o702sub), java.lang.Object(o702sub))
f2316_0_length_Load(EOS, i537, java.lang.Object(o702sub), java.lang.Object(o702sub)) → f2338_0_length_FieldAccess(EOS, i537, java.lang.Object(o702sub), java.lang.Object(o702sub))
f2338_0_length_FieldAccess(EOS, i537, java.lang.Object(java.lang.String(o723sub, i607)), java.lang.Object(java.lang.String(o723sub, i607))) → f2361_0_length_FieldAccess(EOS, i537, java.lang.Object(java.lang.String(o723sub, i607)), java.lang.Object(java.lang.String(o723sub, i607)))
f2361_0_length_FieldAccess(EOS, i537, java.lang.Object(java.lang.String(o723sub, i607)), java.lang.Object(java.lang.String(o723sub, i607))) → f2373_0_length_Return(EOS, i537, java.lang.Object(java.lang.String(o723sub, i607)))
f2373_0_length_Return(EOS, i537, java.lang.Object(java.lang.String(o723sub, i607))) → f2388_0_random_Return(EOS, i537)
f2388_0_random_Return(EOS, i537) → f2401_0_createIntList_Load(EOS, i537)
f2401_0_createIntList_Load(EOS, i537) → f2419_0_createIntList_InvokeMethod(EOS, i537)
f2419_0_createIntList_InvokeMethod(EOS, i537) → f2432_0__init__Load(EOS, i537)
f2432_0__init__Load(EOS, i537) → f2462_0__init__InvokeMethod(EOS, i537)
f2462_0__init__InvokeMethod(EOS, i537) → f2474_0__init__Load(EOS, i537)
f2474_0__init__Load(EOS, i537) → f2491_0__init__Load(EOS, i537)
f2491_0__init__Load(EOS, i537) → f2502_0__init__FieldAccess(EOS, i537)
f2502_0__init__FieldAccess(EOS, i537) → f2516_0__init__Load(EOS, i537)
f2516_0__init__Load(EOS, i537) → f2532_0__init__Load(EOS, i537)
f2532_0__init__Load(EOS, i537) → f2546_0__init__FieldAccess(EOS, i537)
f2546_0__init__FieldAccess(EOS, i537) → f2557_0__init__Return(EOS, i537)
f2557_0__init__Return(EOS, i537) → f2566_0_createIntList_Store(EOS, i537)
f2566_0_createIntList_Store(EOS, i537) → f2580_0_createIntList_Inc(EOS, i537)
f2580_0_createIntList_Inc(EOS, i537) → f2594_0_createIntList_JMP(EOS, +(i537, -1)) | >(i537, 0)
f2594_0_createIntList_JMP(EOS, i679) → f2608_0_createIntList_Load(EOS, i679)
f2608_0_createIntList_Load(EOS, i679) → f2179_0_createIntList_Load(EOS, i679)
f2179_0_createIntList_Load(EOS, i528) → f2192_0_createIntList_LE(EOS, i528, i528)

Combined rules. Obtained 1 IRules

P rules:
f2192_0_createIntList_LE(EOS, x0, x0) → f2192_0_createIntList_LE(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f2192_0_createIntList_LE(x1, x2, x3) → f2192_0_createIntList_LE(x2, x3)
Cond_f2192_0_createIntList_LE(x1, x2, x3, x4) → Cond_f2192_0_createIntList_LE(x1, x3, x4)

Filtered duplicate terms:

f2192_0_createIntList_LE(x1, x2) → f2192_0_createIntList_LE(x2)
Cond_f2192_0_createIntList_LE(x1, x2, x3) → Cond_f2192_0_createIntList_LE(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f2192_0_createIntList_LE(x0) → f2192_0_createIntList_LE(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f2192_0_createIntList_LE(x0) → f2192_0_createIntList_LE(-(x0, 1)) | >(x0, 0)

(7) Obligation:

Rules:
f2192_0_createIntList_LE(x0) → f2192_0_createIntList_LE(-(x0, 1)) | >(x0, 0)

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2192_0_createIntList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

f2192_0_createIntList_LE(x0) → f2192_0_createIntList_LE(-(x0, 1)) | >(x0, 0)

(9) YES

(10) Obligation:

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

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

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 6 IRules

P rules:
f2581_0_main_LE(EOS, i686, i686) → f2605_0_main_LE(EOS, i686, i686)
f2605_0_main_LE(EOS, i686, i686) → f2628_0_main_Inc(EOS, i686) | >(i686, 0)
f2628_0_main_Inc(EOS, i686) → f2662_0_main_JMP(EOS, +(i686, -1)) | >(i686, 0)
f2662_0_main_JMP(EOS, i710) → f2687_0_main_Load(EOS, i710)
f2687_0_main_Load(EOS, i710) → f2558_0_main_Load(EOS, i710)
f2558_0_main_Load(EOS, i641) → f2581_0_main_LE(EOS, i641, i641)

Combined rules. Obtained 1 IRules

P rules:
f2581_0_main_LE(EOS, x0, x0) → f2581_0_main_LE(EOS, -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f2581_0_main_LE(x1, x2, x3) → f2581_0_main_LE(x2, x3)
Cond_f2581_0_main_LE(x1, x2, x3, x4) → Cond_f2581_0_main_LE(x1, x3, x4)

Filtered duplicate terms:

f2581_0_main_LE(x1, x2) → f2581_0_main_LE(x2)
Cond_f2581_0_main_LE(x1, x2, x3) → Cond_f2581_0_main_LE(x1, x3)

Prepared 1 rules for path length conversion:

P rules:
f2581_0_main_LE(x0) → f2581_0_main_LE(-(x0, 1)) | >(x0, 0)

Finished conversion. Obtained 1 rules.

P rules:
f2581_0_main_LE(x0) → f2581_0_main_LE(-(x0, 1)) | >(x0, 0)

(12) Obligation:

Rules:
f2581_0_main_LE(x0) → f2581_0_main_LE(-(x0, 1)) | >(x0, 0)

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2581_0_main_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

f2581_0_main_LE(x0) → f2581_0_main_LE(-(x0, 1)) | >(x0, 0)

(14) YES

(15) Obligation:

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

• Used field analysis yielded the following read fields:
  
  • IntList: [next]
• Marker field analysis yielded the following relations that could be markers:
  

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 19 IRules

P rules:
f2365_0_nth_ConstantStackPush(EOS, java.lang.Object(o714sub), i598, o713, i598) → f2379_0_nth_LE(EOS, java.lang.Object(o714sub), i598, o713, i598, 1)
f2379_0_nth_LE(EOS, java.lang.Object(o714sub), i619, o713, i619, matching1) → f2391_0_nth_LE(EOS, java.lang.Object(o714sub), i619, o713, i619, 1) | =(matching1, 1)
f2391_0_nth_LE(EOS, java.lang.Object(o714sub), i619, o713, i619, matching1) → f2404_0_nth_Inc(EOS, java.lang.Object(o714sub), i619, o713) | &&(>(i619, 1), =(matching1, 1))
f2404_0_nth_Inc(EOS, java.lang.Object(o714sub), i619, o713) → f2420_0_nth_Load(EOS, java.lang.Object(o714sub), +(i619, -1), o713) | >(i619, 0)
f2420_0_nth_Load(EOS, java.lang.Object(o714sub), i627, o713) → f2434_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, o713)
f2434_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(o761sub)) → f2455_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(o761sub))
f2455_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(o761sub)) → f2480_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(o761sub))
f2455_0_nth_FieldAccess(EOS, java.lang.Object(o775sub), i627, java.lang.Object(o775sub)) → f2481_0_nth_FieldAccess(EOS, java.lang.Object(o775sub), i627, java.lang.Object(o775sub))
f2480_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(IntList(EOC, o787))) → f2505_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(IntList(EOC, o787)))
f2505_0_nth_FieldAccess(EOS, java.lang.Object(o714sub), i627, java.lang.Object(IntList(EOC, o787))) → f2540_0_nth_Store(EOS, java.lang.Object(o714sub), i627, o787)
f2540_0_nth_Store(EOS, java.lang.Object(o714sub), i627, o787) → f2565_0_nth_JMP(EOS, java.lang.Object(o714sub), i627, o787)
f2565_0_nth_JMP(EOS, java.lang.Object(o714sub), i627, o787) → f2591_0_nth_Load(EOS, java.lang.Object(o714sub), i627, o787)
f2591_0_nth_Load(EOS, java.lang.Object(o714sub), i627, o787) → f2351_0_nth_Load(EOS, java.lang.Object(o714sub), i627, o787)
f2351_0_nth_Load(EOS, java.lang.Object(o714sub), i598, o713) → f2365_0_nth_ConstantStackPush(EOS, java.lang.Object(o714sub), i598, o713, i598)
f2481_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o792)), i627, java.lang.Object(IntList(EOC, o792))) → f2510_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o792)), i627, java.lang.Object(IntList(EOC, o792)))
f2510_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o792)), i627, java.lang.Object(IntList(EOC, o792))) → f2544_0_nth_Store(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792)
f2544_0_nth_Store(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792) → f2568_0_nth_JMP(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792)
f2568_0_nth_JMP(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792) → f2597_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792)
f2597_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792) → f2351_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o792)), i627, o792)

Combined rules. Obtained 2 IRules

P rules:
f2365_0_nth_ConstantStackPush(EOS, java.lang.Object(x0), x1, java.lang.Object(IntList(EOC, x2)), x1) → f2365_0_nth_ConstantStackPush(EOS, java.lang.Object(x0), -(x1, 1), x2, -(x1, 1)) | >(x1, 1)
f2365_0_nth_ConstantStackPush(EOS, java.lang.Object(IntList(EOC, x0)), x1, java.lang.Object(IntList(EOC, x0)), x1) → f2365_0_nth_ConstantStackPush(EOS, java.lang.Object(IntList(EOC, x0)), -(x1, 1), x0, -(x1, 1)) | >(x1, 1)

Filtered ground terms:

f2365_0_nth_ConstantStackPush(x1, x2, x3, x4, x5) → f2365_0_nth_ConstantStackPush(x2, x3, x4, x5)
Cond_f2365_0_nth_ConstantStackPush(x1, x2, x3, x4, x5, x6) → Cond_f2365_0_nth_ConstantStackPush(x1, x3, x4, x5, x6)
Cond_f2365_0_nth_ConstantStackPush1(x1, x2, x3, x4, x5, x6) → Cond_f2365_0_nth_ConstantStackPush1(x1, x3, x4, x5, x6)
IntList(x1, x2) → IntList(x2)

Filtered duplicate terms:

f2365_0_nth_ConstantStackPush(x1, x2, x3, x4) → f2365_0_nth_ConstantStackPush(x1, x3, x4)
Cond_f2365_0_nth_ConstantStackPush(x1, x2, x3, x4, x5) → Cond_f2365_0_nth_ConstantStackPush(x1, x2, x4, x5)
Cond_f2365_0_nth_ConstantStackPush1(x1, x2, x3, x4, x5) → Cond_f2365_0_nth_ConstantStackPush1(x1, x4, x5)

Prepared 2 rules for path length conversion:

P rules:
f2365_0_nth_ConstantStackPush(java.lang.Object(x0), java.lang.Object(IntList(x2)), x1) → f2365_0_nth_ConstantStackPush(java.lang.Object(x0), x2, -(x1, 1)) | >(x1, 1)
f2365_0_nth_ConstantStackPush(java.lang.Object(IntList(x0)), java.lang.Object(IntList(x0)), x1) → f2365_0_nth_ConstantStackPush(java.lang.Object(IntList(x0)), x0, -(x1, 1)) | >(x1, 1)

Finished conversion. Obtained 2 rules.

P rules:
f2365_0_nth_ConstantStackPush(v8, v9, x2) → f2365_0_nth_ConstantStackPush(v10, v11, -(x2, 1)) | &&(&&(&&(&&(&&(&&(>(x2, 1), >=(v9, +(v11, 1))), >(+(v9, 1), 1)), >=(v8, v10)), >(+(v8, 1), 1)), >(+(v10, 1), 1)), >(+(v11, 1), 0))
f2365_0_nth_ConstantStackPush(v12, v13, x4) → f2365_0_nth_ConstantStackPush(v14, v15, -(x4, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x4, 1), >(+(v15, 1), 0)), <=(+(v15, 1), v13)), <=(+(v15, 1), v12)), >(+(v14, 1), 1)), <=(v14, v13)), <=(v14, v12)), >(+(v13, 1), 1)), >(+(v12, 1), 1))

(17) Obligation:

Rules:
f2365_0_nth_ConstantStackPush(v8, v9, x2) → f2365_0_nth_ConstantStackPush(v10, v11, -(x2, 1)) | &&(&&(&&(&&(&&(&&(>(x2, 1), >=(v9, +(v11, 1))), >(+(v9, 1), 1)), >=(v8, v10)), >(+(v8, 1), 1)), >(+(v10, 1), 1)), >(+(v11, 1), 0))
f2365_0_nth_ConstantStackPush(v12, v13, x4) → f2365_0_nth_ConstantStackPush(v14, v15, -(x4, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x4, 1), >(+(v15, 1), 0)), <=(+(v15, 1), v13)), <=(+(v15, 1), v12)), >(+(v14, 1), 1)), <=(v14, v13)), <=(v14, v12)), >(+(v13, 1), 1)), >(+(v12, 1), 1))

(18) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2365_0_nth_ConstantStackPush(x11, x13, x15)] = x15

Therefore the following rule(s) have been dropped:

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

(19) YES