Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 820 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 3 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 0 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 267 ms)
        ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇒, 0 ms)
        ↳14 intTRS
        ↳15 PolynomialOrderProcessor (⇔, 0 ms)
        ↳16 YES
    ↳17 JBCTerminationSCC
        ↳18 SCCToIntTRSProof (⇒, 22 ms)
        ↳19 intTRS
        ↳20 PolynomialOrderProcessor (⇔, 0 ms)
        ↳21 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class ListContentTail{

  public static void main(String[] args) {
    Random.args = args;
    IntList l = IntList.createIntList();

    int m = IntList.nth(Random.random(),l);

    while (m > 0) {

      l = l.next;
      m = IntList.nth(Random.random(),l);
    }
  }
}

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 static int nth(int n, IntList l){

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

    if (l == null) return 0;
    else           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:
ListContentTail.main([Ljava/lang/String;)V: Graph of 311 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:
f2210_0_createIntList_LE(EOS, i488, i488) → f2214_0_createIntList_LE(EOS, i488, i488)
f2214_0_createIntList_LE(EOS, i488, i488) → f2222_0_createIntList_New(EOS, i488) | >(i488, 0)
f2222_0_createIntList_New(EOS, i488) → f2233_0_createIntList_Duplicate(EOS, i488)
f2233_0_createIntList_Duplicate(EOS, i488) → f2240_0_createIntList_InvokeMethod(EOS, i488)
f2240_0_createIntList_InvokeMethod(EOS, i488) → f2253_0_random_FieldAccess(EOS, i488)
f2253_0_random_FieldAccess(EOS, i488) → f2259_0_random_FieldAccess(EOS, i488)
f2259_0_random_FieldAccess(EOS, i488) → f2266_0_random_ArrayAccess(EOS, i488)
f2266_0_random_ArrayAccess(EOS, i488) → f2270_0_random_ArrayAccess(EOS, i488)
f2270_0_random_ArrayAccess(EOS, i488) → f2276_0_random_Store(EOS, i488, o695)
f2276_0_random_Store(EOS, i488, o695) → f2288_0_random_FieldAccess(EOS, i488, o695)
f2288_0_random_FieldAccess(EOS, i488, o695) → f2297_0_random_ConstantStackPush(EOS, i488, o695)
f2297_0_random_ConstantStackPush(EOS, i488, o695) → f2305_0_random_IntArithmetic(EOS, i488, o695)
f2305_0_random_IntArithmetic(EOS, i488, o695) → f2314_0_random_FieldAccess(EOS, i488, o695)
f2314_0_random_FieldAccess(EOS, i488, o695) → f2321_0_random_Load(EOS, i488, o695)
f2321_0_random_Load(EOS, i488, o695) → f2334_0_random_InvokeMethod(EOS, i488, o695)
f2334_0_random_InvokeMethod(EOS, i488, java.lang.Object(o724sub)) → f2344_0_random_InvokeMethod(EOS, i488, java.lang.Object(o724sub))
f2344_0_random_InvokeMethod(EOS, i488, java.lang.Object(o724sub)) → f2352_0_length_Load(EOS, i488, java.lang.Object(o724sub), java.lang.Object(o724sub))
f2352_0_length_Load(EOS, i488, java.lang.Object(o724sub), java.lang.Object(o724sub)) → f2374_0_length_FieldAccess(EOS, i488, java.lang.Object(o724sub), java.lang.Object(o724sub))
f2374_0_length_FieldAccess(EOS, i488, java.lang.Object(java.lang.String(o745sub, i555)), java.lang.Object(java.lang.String(o745sub, i555))) → f2397_0_length_FieldAccess(EOS, i488, java.lang.Object(java.lang.String(o745sub, i555)), java.lang.Object(java.lang.String(o745sub, i555)))
f2397_0_length_FieldAccess(EOS, i488, java.lang.Object(java.lang.String(o745sub, i555)), java.lang.Object(java.lang.String(o745sub, i555))) → f2409_0_length_Return(EOS, i488, java.lang.Object(java.lang.String(o745sub, i555)))
f2409_0_length_Return(EOS, i488, java.lang.Object(java.lang.String(o745sub, i555))) → f2423_0_random_Return(EOS, i488)
f2423_0_random_Return(EOS, i488) → f2428_0_createIntList_Load(EOS, i488)
f2428_0_createIntList_Load(EOS, i488) → f2446_0_createIntList_InvokeMethod(EOS, i488)
f2446_0_createIntList_InvokeMethod(EOS, i488) → f2457_0__init__Load(EOS, i488)
f2457_0__init__Load(EOS, i488) → f2479_0__init__InvokeMethod(EOS, i488)
f2479_0__init__InvokeMethod(EOS, i488) → f2499_0__init__Load(EOS, i488)
f2499_0__init__Load(EOS, i488) → f2513_0__init__Load(EOS, i488)
f2513_0__init__Load(EOS, i488) → f2531_0__init__FieldAccess(EOS, i488)
f2531_0__init__FieldAccess(EOS, i488) → f2546_0__init__Load(EOS, i488)
f2546_0__init__Load(EOS, i488) → f2560_0__init__Load(EOS, i488)
f2560_0__init__Load(EOS, i488) → f2575_0__init__FieldAccess(EOS, i488)
f2575_0__init__FieldAccess(EOS, i488) → f2589_0__init__Return(EOS, i488)
f2589_0__init__Return(EOS, i488) → f2600_0_createIntList_Store(EOS, i488)
f2600_0_createIntList_Store(EOS, i488) → f2625_0_createIntList_Inc(EOS, i488)
f2625_0_createIntList_Inc(EOS, i488) → f2637_0_createIntList_JMP(EOS, +(i488, -1)) | >(i488, 0)
f2637_0_createIntList_JMP(EOS, i630) → f2650_0_createIntList_Load(EOS, i630)
f2650_0_createIntList_Load(EOS, i630) → f2199_0_createIntList_Load(EOS, i630)
f2199_0_createIntList_Load(EOS, i483) → f2210_0_createIntList_LE(EOS, i483, i483)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f2210_0_createIntList_LE(x1, x2, x3) → f2210_0_createIntList_LE(x2, x3)
Cond_f2210_0_createIntList_LE(x1, x2, x3, x4) → Cond_f2210_0_createIntList_LE(x1, x3, x4)

Filtered duplicate terms:


f2210_0_createIntList_LE(x1, x2) → f2210_0_createIntList_LE(x2)
Cond_f2210_0_createIntList_LE(x1, x2, x3) → Cond_f2210_0_createIntList_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

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

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f2210_0_createIntList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


f2210_0_createIntList_LE(x0) → f2210_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: ListContentTail.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • IntList: [next, value]
    • java.lang.String: [count]
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 80 IRules

P rules:
f2599_0_main_LE(EOS, o738, i628) → f2628_0_main_LE(EOS, o738, i628)
f2628_0_main_LE(EOS, o738, i628) → f2635_0_main_Load(EOS, o738) | >(i628, 0)
f2635_0_main_Load(EOS, o738) → f2642_0_main_FieldAccess(EOS, o738)
f2642_0_main_FieldAccess(EOS, java.lang.Object(o866sub)) → f2645_0_main_FieldAccess(EOS, java.lang.Object(o866sub))
f2645_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, o870, i634))) → f2653_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, o870, i634)))
f2653_0_main_FieldAccess(EOS, java.lang.Object(IntList(EOC, o870, i634))) → f2668_0_main_Store(EOS, o870)
f2668_0_main_Store(EOS, o870) → f2687_0_main_InvokeMethod(EOS, o870)
f2687_0_main_InvokeMethod(EOS, o870) → f2701_0_random_FieldAccess(EOS, o870)
f2701_0_random_FieldAccess(EOS, o870) → f2723_0_random_FieldAccess(EOS, o870)
f2723_0_random_FieldAccess(EOS, o870) → f2728_0_random_ArrayAccess(EOS, o870)
f2728_0_random_ArrayAccess(EOS, o870) → f2733_0_random_ArrayAccess(EOS, o870)
f2733_0_random_ArrayAccess(EOS, o870) → f2737_0_random_Store(EOS, o870, o914)
f2737_0_random_Store(EOS, o870, o914) → f2742_0_random_FieldAccess(EOS, o870, o914)
f2742_0_random_FieldAccess(EOS, o870, o914) → f2746_0_random_ConstantStackPush(EOS, o870, o914)
f2746_0_random_ConstantStackPush(EOS, o870, o914) → f2753_0_random_IntArithmetic(EOS, o870, o914)
f2753_0_random_IntArithmetic(EOS, o870, o914) → f2756_0_random_FieldAccess(EOS, o870, o914)
f2756_0_random_FieldAccess(EOS, o870, o914) → f2762_0_random_Load(EOS, o870, o914)
f2762_0_random_Load(EOS, o870, o914) → f2773_0_random_InvokeMethod(EOS, o870, o914)
f2773_0_random_InvokeMethod(EOS, o870, java.lang.Object(o939sub)) → f2779_0_random_InvokeMethod(EOS, o870, java.lang.Object(o939sub))
f2779_0_random_InvokeMethod(EOS, o870, java.lang.Object(o939sub)) → f2783_0_length_Load(EOS, o870, java.lang.Object(o939sub), java.lang.Object(o939sub))
f2783_0_length_Load(EOS, o870, java.lang.Object(o939sub), java.lang.Object(o939sub)) → f2804_0_length_FieldAccess(EOS, o870, java.lang.Object(o939sub), java.lang.Object(o939sub))
f2804_0_length_FieldAccess(EOS, o870, java.lang.Object(java.lang.String(o957sub, i674)), java.lang.Object(java.lang.String(o957sub, i674))) → f2810_0_length_FieldAccess(EOS, o870, java.lang.Object(java.lang.String(o957sub, i674)), java.lang.Object(java.lang.String(o957sub, i674))) | >=(i674, 0)
f2810_0_length_FieldAccess(EOS, o870, java.lang.Object(java.lang.String(o957sub, i674)), java.lang.Object(java.lang.String(o957sub, i674))) → f2820_0_length_Return(EOS, o870, java.lang.Object(java.lang.String(o957sub, i674)), i674)
f2820_0_length_Return(EOS, o870, java.lang.Object(java.lang.String(o957sub, i674)), i674) → f2826_0_random_Return(EOS, o870, i674)
f2826_0_random_Return(EOS, o870, i674) → f2832_0_main_Load(EOS, o870, i674)
f2832_0_main_Load(EOS, o870, i674) → f2845_0_main_InvokeMethod(EOS, o870, i674, o870)
f2845_0_main_InvokeMethod(EOS, o870, i674, o870) → f2853_0_nth_Load(EOS, o870, i674, o870, i674, o870)
f2853_0_nth_Load(EOS, o870, i674, o870, i674, o870) → f3080_0_nth_Load(EOS, o870, i674, o870, i674, o870)
f3080_0_nth_Load(EOS, o1130, i717, o1130, i716, o1129) → f3090_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, i716, o1129, i716)
f3090_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, i716, o1129, i716) → f3098_0_nth_LE(EOS, o1130, i717, o1130, i716, o1129, i716, 1)
f3098_0_nth_LE(EOS, o1130, i717, o1130, i728, o1129, i728, matching1) → f3102_0_nth_LE(EOS, o1130, i717, o1130, i728, o1129, i728, 1) | =(matching1, 1)
f3098_0_nth_LE(EOS, o1130, i717, o1130, i729, o1129, i729, matching1) → f3103_0_nth_LE(EOS, o1130, i717, o1130, i729, o1129, i729, 1) | =(matching1, 1)
f3102_0_nth_LE(EOS, o1130, i717, o1130, i728, o1129, i728, matching1) → f3109_0_nth_Load(EOS, o1130, i717, o1130, o1129) | &&(<=(i728, 1), =(matching1, 1))
f3109_0_nth_Load(EOS, o1130, i717, o1130, o1129) → f3117_0_nth_NONNULL(EOS, o1130, i717, o1130, o1129, o1129)
f3117_0_nth_NONNULL(EOS, o1130, i717, o1130, java.lang.Object(o1162sub), java.lang.Object(o1162sub)) → f3124_0_nth_NONNULL(EOS, o1130, i717, o1130, java.lang.Object(o1162sub), java.lang.Object(o1162sub))
f3117_0_nth_NONNULL(EOS, o1130, i717, o1130, NULL, NULL) → f3125_0_nth_NONNULL(EOS, o1130, i717, o1130, NULL, NULL)
f3124_0_nth_NONNULL(EOS, o1130, i717, o1130, java.lang.Object(o1162sub), java.lang.Object(o1162sub)) → f3132_0_nth_Load(EOS, o1130, i717, o1130, java.lang.Object(o1162sub))
f3132_0_nth_Load(EOS, o1130, i717, o1130, java.lang.Object(o1162sub)) → f3144_0_nth_FieldAccess(EOS, o1130, i717, o1130, java.lang.Object(o1162sub))
f3144_0_nth_FieldAccess(EOS, o1130, i717, o1130, java.lang.Object(o1162sub)) → f3158_0_nth_FieldAccess(EOS, o1130, i717, o1130, java.lang.Object(o1162sub))
f3144_0_nth_FieldAccess(EOS, java.lang.Object(o1186sub), i717, java.lang.Object(o1186sub), java.lang.Object(o1186sub)) → f3160_0_nth_FieldAccess(EOS, java.lang.Object(o1186sub), i717, java.lang.Object(o1186sub), java.lang.Object(o1186sub))
f3158_0_nth_FieldAccess(EOS, o1130, i717, o1130, java.lang.Object(IntList(EOC, o1196, i743))) → f3174_0_nth_FieldAccess(EOS, o1130, i717, o1130, java.lang.Object(IntList(EOC, o1196, i743)))
f3174_0_nth_FieldAccess(EOS, o1130, i717, o1130, java.lang.Object(IntList(EOC, o1196, i743))) → f3192_0_nth_Return(EOS, o1130, i717, o1130, i743)
f3192_0_nth_Return(EOS, o1130, i717, o1130, i743) → f3206_0_main_Store(EOS, o1130, i743)
f3206_0_main_Store(EOS, o1130, i743) → f3219_0_main_JMP(EOS, o1130, i743)
f3219_0_main_JMP(EOS, o1130, i743) → f3235_0_main_Load(EOS, o1130, i743)
f3235_0_main_Load(EOS, o1130, i743) → f2582_0_main_Load(EOS, o1130, i743)
f2582_0_main_Load(EOS, o738, i583) → f2599_0_main_LE(EOS, o738, i583)
f3160_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i717, java.lang.Object(IntList(EOC, o1198, i744)), java.lang.Object(IntList(EOC, o1198, i744))) → f3176_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i717, java.lang.Object(IntList(EOC, o1198, i744)), java.lang.Object(IntList(EOC, o1198, i744)))
f3176_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i717, java.lang.Object(IntList(EOC, o1198, i744)), java.lang.Object(IntList(EOC, o1198, i744))) → f3195_0_nth_Return(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i717, java.lang.Object(IntList(EOC, o1198, i744)), i744)
f3195_0_nth_Return(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i717, java.lang.Object(IntList(EOC, o1198, i744)), i744) → f3210_0_main_Store(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744)
f3210_0_main_Store(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744) → f3221_0_main_JMP(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744)
f3221_0_main_JMP(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744) → f3240_0_main_Load(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744)
f3240_0_main_Load(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744) → f2582_0_main_Load(EOS, java.lang.Object(IntList(EOC, o1198, i744)), i744)
f3125_0_nth_NONNULL(EOS, o1130, i717, o1130, NULL, NULL) → f3135_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, NULL)
f3135_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, NULL) → f3172_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, NULL)
f3172_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, NULL) → f3188_0_nth_Return(EOS, o1130, i717, o1130, NULL, 0)
f3188_0_nth_Return(EOS, o1130, i717, o1130, NULL, matching1) → f3203_0_main_Store(EOS, o1130, 0) | =(matching1, 0)
f3203_0_main_Store(EOS, o1130, matching1) → f3206_0_main_Store(EOS, o1130, 0) | =(matching1, 0)
f3103_0_nth_LE(EOS, o1130, i717, o1130, i729, o1129, i729, matching1) → f3112_0_nth_Load(EOS, o1130, i717, o1130, i729, o1129) | &&(>(i729, 1), =(matching1, 1))
f3112_0_nth_Load(EOS, o1130, i717, o1130, i729, o1129) → f3122_0_nth_NULL(EOS, o1130, i717, o1130, i729, o1129, o1129)
f3122_0_nth_NULL(EOS, o1130, i717, o1130, i729, java.lang.Object(o1163sub), java.lang.Object(o1163sub)) → f3127_0_nth_NULL(EOS, o1130, i717, o1130, i729, java.lang.Object(o1163sub), java.lang.Object(o1163sub))
f3122_0_nth_NULL(EOS, o1130, i717, o1130, i729, NULL, NULL) → f3128_0_nth_NULL(EOS, o1130, i717, o1130, i729, NULL, NULL)
f3127_0_nth_NULL(EOS, o1130, i717, o1130, i729, java.lang.Object(o1163sub), java.lang.Object(o1163sub)) → f3137_0_nth_Inc(EOS, o1130, i717, o1130, i729, java.lang.Object(o1163sub))
f3137_0_nth_Inc(EOS, o1130, i717, o1130, i729, java.lang.Object(o1163sub)) → f3147_0_nth_Load(EOS, o1130, i717, o1130, +(i729, -1), java.lang.Object(o1163sub)) | >(i729, 0)
f3147_0_nth_Load(EOS, o1130, i717, o1130, i738, java.lang.Object(o1163sub)) → f3165_0_nth_FieldAccess(EOS, o1130, i717, o1130, i738, java.lang.Object(o1163sub))
f3165_0_nth_FieldAccess(EOS, o1130, i717, o1130, i738, java.lang.Object(o1163sub)) → f3184_0_nth_FieldAccess(EOS, o1130, i717, o1130, i738, java.lang.Object(o1163sub))
f3165_0_nth_FieldAccess(EOS, java.lang.Object(o1201sub), i717, java.lang.Object(o1201sub), i738, java.lang.Object(o1201sub)) → f3185_0_nth_FieldAccess(EOS, java.lang.Object(o1201sub), i717, java.lang.Object(o1201sub), i738, java.lang.Object(o1201sub))
f3184_0_nth_FieldAccess(EOS, o1130, i717, o1130, i738, java.lang.Object(IntList(EOC, o1212, i748))) → f3199_0_nth_FieldAccess(EOS, o1130, i717, o1130, i738, java.lang.Object(IntList(EOC, o1212, i748)))
f3199_0_nth_FieldAccess(EOS, o1130, i717, o1130, i738, java.lang.Object(IntList(EOC, o1212, i748))) → f3213_0_nth_Store(EOS, o1130, i717, o1130, i738, o1212)
f3213_0_nth_Store(EOS, o1130, i717, o1130, i738, o1212) → f3225_0_nth_JMP(EOS, o1130, i717, o1130, i738, o1212)
f3225_0_nth_JMP(EOS, o1130, i717, o1130, i738, o1212) → f3249_0_nth_Load(EOS, o1130, i717, o1130, i738, o1212)
f3249_0_nth_Load(EOS, o1130, i717, o1130, i738, o1212) → f3080_0_nth_Load(EOS, o1130, i717, o1130, i738, o1212)
f3185_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, java.lang.Object(IntList(EOC, o1214, i749))) → f3200_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, java.lang.Object(IntList(EOC, o1214, i749)))
f3200_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, java.lang.Object(IntList(EOC, o1214, i749))) → f3217_0_nth_Store(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214)
f3217_0_nth_Store(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214) → f3230_0_nth_JMP(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214)
f3230_0_nth_JMP(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214) → f3256_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214)
f3256_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214) → f3080_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o1214, i749)), i717, java.lang.Object(IntList(EOC, o1214, i749)), i738, o1214)
f3128_0_nth_NULL(EOS, o1130, i717, o1130, i729, NULL, NULL) → f3140_0_nth_Load(EOS, o1130, i717, o1130, NULL)
f3140_0_nth_Load(EOS, o1130, i717, o1130, NULL) → f3150_0_nth_NONNULL(EOS, o1130, i717, o1130, NULL, NULL)
f3150_0_nth_NONNULL(EOS, o1130, i717, o1130, NULL, NULL) → f3172_0_nth_ConstantStackPush(EOS, o1130, i717, o1130, NULL)

Combined rules. Obtained 4 IRules

P rules:
f3098_0_nth_LE(EOS, java.lang.Object(IntList(EOC, x0, x1)), x2, java.lang.Object(IntList(EOC, x0, x1)), x3, java.lang.Object(IntList(EOC, x4, x5)), x3, 1) → f3098_0_nth_LE(EOS, x0, x7, x0, x7, x0, x7, 1) | &&(&&(>(+(x7, 1), 0), <=(x3, 1)), >(x5, 0))
f3098_0_nth_LE(EOS, java.lang.Object(IntList(EOC, x0, x1)), x2, java.lang.Object(IntList(EOC, x0, x1)), x3, java.lang.Object(IntList(EOC, x0, x1)), x3, 1) → f3098_0_nth_LE(EOS, x0, x5, x0, x5, x0, x5, 1) | &&(&&(>(+(x5, 1), 0), >(x1, 0)), <=(x3, 1))
f3098_0_nth_LE(EOS, x0, x1, x0, x2, java.lang.Object(IntList(EOC, x3, x4)), x2, 1) → f3098_0_nth_LE(EOS, x0, x1, x0, -(x2, 1), x3, -(x2, 1), 1) | >(x2, 1)
f3098_0_nth_LE(EOS, java.lang.Object(IntList(EOC, x0, x1)), x2, java.lang.Object(IntList(EOC, x0, x1)), x3, java.lang.Object(IntList(EOC, x0, x1)), x3, 1) → f3098_0_nth_LE(EOS, java.lang.Object(IntList(EOC, x0, x1)), x2, java.lang.Object(IntList(EOC, x0, x1)), -(x3, 1), x0, -(x3, 1), 1) | >(x3, 1)

Filtered ground terms:


f3098_0_nth_LE(x1, x2, x3, x4, x5, x6, x7, x8) → f3098_0_nth_LE(x2, x3, x4, x5, x6, x7)
Cond_f3098_0_nth_LE(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f3098_0_nth_LE(x1, x3, x4, x5, x6, x7, x8, x10)
Cond_f3098_0_nth_LE1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f3098_0_nth_LE1(x1, x3, x4, x5, x6, x7, x8, x10)
Cond_f3098_0_nth_LE2(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f3098_0_nth_LE2(x1, x3, x4, x5, x6, x7, x8)
Cond_f3098_0_nth_LE3(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f3098_0_nth_LE3(x1, x3, x4, x5, x6, x7, x8)
IntList(x1, x2, x3) → IntList(x2, x3)

Filtered duplicate terms:


f3098_0_nth_LE(x1, x2, x3, x4, x5, x6) → f3098_0_nth_LE(x2, x3, x5, x6)
Cond_f3098_0_nth_LE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f3098_0_nth_LE(x1, x3, x4, x6, x7, x8)
Cond_f3098_0_nth_LE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f3098_0_nth_LE1(x1, x3, x6, x7, x8)
Cond_f3098_0_nth_LE2(x1, x2, x3, x4, x5, x6, x7) → Cond_f3098_0_nth_LE2(x1, x3, x4, x6, x7)
Cond_f3098_0_nth_LE3(x1, x2, x3, x4, x5, x6, x7) → Cond_f3098_0_nth_LE3(x1, x3, x6, x7)

Filtered unneeded terms:


f3098_0_nth_LE(x1, x2, x3, x4) → f3098_0_nth_LE(x2, x3, x4)
Cond_f3098_0_nth_LE(x1, x2, x3, x4, x5, x6) → Cond_f3098_0_nth_LE(x1, x3, x6)
Cond_f3098_0_nth_LE1(x1, x2, x3, x4, x5) → Cond_f3098_0_nth_LE1(x1, x3, x5)
Cond_f3098_0_nth_LE2(x1, x2, x3, x4, x5) → Cond_f3098_0_nth_LE2(x1, x3, x4, x5)
Cond_f3098_0_nth_LE3(x1, x2, x3, x4) → Cond_f3098_0_nth_LE3(x1, x3, x4)

Prepared 4 rules for path length conversion:

P rules:
f3098_0_nth_LE(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x4, x5)), x3) → f3098_0_nth_LE(x0, x0, x7) | &&(&&(>(+(x7, 1), 0), <=(x3, 1)), >(x5, 0))
f3098_0_nth_LE(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x0, x1)), x3) → f3098_0_nth_LE(x0, x0, x5) | &&(&&(>(+(x5, 1), 0), >(x1, 0)), <=(x3, 1))
f3098_0_nth_LE(x0, java.lang.Object(IntList(x3, x4)), x2) → f3098_0_nth_LE(x0, x3, -(x2, 1)) | >(x2, 1)
f3098_0_nth_LE(java.lang.Object(IntList(x0, x1)), java.lang.Object(IntList(x0, x1)), x3) → f3098_0_nth_LE(java.lang.Object(IntList(x0, x1)), x0, -(x3, 1)) | >(x3, 1)

Finished conversion. Obtained 4 rules.

P rules:
f3098_0_nth_LE(v20, v21, x4) → f3098_0_nth_LE(v22, v23, x5) | &&(&&(&&(&&(&&(&&(&&(&&(>(x5, -1), <=(x4, 1)), >(x3, 0)), >(+(v23, 1), 0)), <=(+(v23, 1), v20)), >(+(v22, 1), 0)), <=(+(v22, 1), v20)), >(+(v21, 1), 1)), >(+(v20, 1), 1))
f3098_0_nth_LE(v24, v25, x8) → f3098_0_nth_LE(v26, v27, x9) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x9, -1), <=(x8, 1)), >(x7, 0)), >(+(v27, 1), 0)), <=(+(v27, 1), v25)), <=(+(v27, 1), v24)), >(+(v26, 1), 0)), <=(+(v26, 1), v25)), <=(+(v26, 1), v24)), >(+(v25, 1), 1)), >(+(v24, 1), 1))
f3098_0_nth_LE(v28, v29, x13) → f3098_0_nth_LE(v30, v31, -(x13, 1)) | &&(&&(&&(&&(&&(&&(>(x13, 1), >(+(v31, 1), 0)), <=(+(v31, 1), v29)), >(+(v30, 1), 0)), <=(v30, v28)), >(+(v29, 1), 1)), >(+(v28, 1), 0))
f3098_0_nth_LE(v32, v33, x16) → f3098_0_nth_LE(v34, v35, -(x16, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x16, 1), >(+(v35, 1), 0)), <=(+(v35, 1), v33)), <=(+(v35, 1), v32)), >(+(v34, 1), 1)), <=(v34, v33)), <=(v34, v32)), >(+(v33, 1), 1)), >(+(v32, 1), 1))

(12) Obligation:

Rules:
f3098_0_nth_LE(v20, v21, x4) → f3098_0_nth_LE(v22, v23, x5) | &&(&&(&&(&&(&&(&&(&&(&&(>(x5, -1), <=(x4, 1)), >(x3, 0)), >(+(v23, 1), 0)), <=(+(v23, 1), v20)), >(+(v22, 1), 0)), <=(+(v22, 1), v20)), >(+(v21, 1), 1)), >(+(v20, 1), 1))
f3098_0_nth_LE(v24, v25, x8) → f3098_0_nth_LE(v26, v27, x9) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x9, -1), <=(x8, 1)), >(x7, 0)), >(+(v27, 1), 0)), <=(+(v27, 1), v25)), <=(+(v27, 1), v24)), >(+(v26, 1), 0)), <=(+(v26, 1), v25)), <=(+(v26, 1), v24)), >(+(v25, 1), 1)), >(+(v24, 1), 1))
f3098_0_nth_LE(v28, v29, x13) → f3098_0_nth_LE(v30, v31, -(x13, 1)) | &&(&&(&&(&&(&&(&&(>(x13, 1), >(+(v31, 1), 0)), <=(+(v31, 1), v29)), >(+(v30, 1), 0)), <=(v30, v28)), >(+(v29, 1), 1)), >(+(v28, 1), 0))
f3098_0_nth_LE(v32, v33, x16) → f3098_0_nth_LE(v34, v35, -(x16, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x16, 1), >(+(v35, 1), 0)), <=(+(v35, 1), v33)), <=(+(v35, 1), v32)), >(+(v34, 1), 1)), <=(v34, v33)), <=(v34, v32)), >(+(v33, 1), 1)), >(+(v32, 1), 1))

(13) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:


[f3098_0_nth_LE(x25, x27, x29)] = -1 + x25

Therefore the following rule(s) have been dropped:


f3098_0_nth_LE(x0, x1, x2) → f3098_0_nth_LE(x3, x4, x5) | &&(&&(&&(&&(&&(&&(&&(&&(>(x5, -1), <=(x2, 1)), >(x6, 0)), >(+(x4, 1), 0)), <=(+(x4, 1), x0)), >(+(x3, 1), 0)), <=(+(x3, 1), x0)), >(+(x1, 1), 1)), >(+(x0, 1), 1))
f3098_0_nth_LE(x7, x8, x9) → f3098_0_nth_LE(x10, x11, x12) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(x12, -1), <=(x9, 1)), >(x13, 0)), >(+(x11, 1), 0)), <=(+(x11, 1), x8)), <=(+(x11, 1), x7)), >(+(x10, 1), 0)), <=(+(x10, 1), x8)), <=(+(x10, 1), x7)), >(+(x8, 1), 1)), >(+(x7, 1), 1))

(14) Obligation:

Rules:
f3098_0_nth_LE(x14, x15, x16) → f3098_0_nth_LE(x17, x18, -(x16, 1)) | &&(&&(&&(&&(&&(&&(>(x16, 1), >(+(x18, 1), 0)), <=(+(x18, 1), x15)), >(+(x17, 1), 0)), <=(x17, x14)), >(+(x15, 1), 1)), >(+(x14, 1), 0))
f3098_0_nth_LE(x19, x20, x21) → f3098_0_nth_LE(x22, x23, -(x21, 1)) | &&(&&(&&(&&(&&(&&(&&(&&(>(x21, 1), >(+(x23, 1), 0)), <=(+(x23, 1), x20)), <=(+(x23, 1), x19)), >(+(x22, 1), 1)), <=(x22, x20)), <=(x22, x19)), >(+(x20, 1), 1)), >(+(x19, 1), 1))

(15) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


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

Therefore the following rule(s) have been dropped:


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

(16) YES

(17) Obligation:

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

(18) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f2401_0_nth_ConstantStackPush(EOS, o738, o738, i546, o737, i546) → f2411_0_nth_LE(EOS, o738, o738, i546, o737, i546, 1)
f2411_0_nth_LE(EOS, o738, o738, i564, o737, i564, matching1) → f2421_0_nth_LE(EOS, o738, o738, i564, o737, i564, 1) | =(matching1, 1)
f2421_0_nth_LE(EOS, o738, o738, i564, o737, i564, matching1) → f2427_0_nth_Load(EOS, o738, o738, i564, o737) | &&(>(i564, 1), =(matching1, 1))
f2427_0_nth_Load(EOS, o738, o738, i564, o737) → f2437_0_nth_NULL(EOS, o738, o738, i564, o737, o737)
f2437_0_nth_NULL(EOS, o738, o738, i564, java.lang.Object(o763sub), java.lang.Object(o763sub)) → f2448_0_nth_NULL(EOS, o738, o738, i564, java.lang.Object(o763sub), java.lang.Object(o763sub))
f2448_0_nth_NULL(EOS, o738, o738, i564, java.lang.Object(o763sub), java.lang.Object(o763sub)) → f2458_0_nth_Inc(EOS, o738, o738, i564, java.lang.Object(o763sub))
f2458_0_nth_Inc(EOS, o738, o738, i564, java.lang.Object(o763sub)) → f2472_0_nth_Load(EOS, o738, o738, +(i564, -1), java.lang.Object(o763sub)) | >(i564, 0)
f2472_0_nth_Load(EOS, o738, o738, i574, java.lang.Object(o763sub)) → f2497_0_nth_FieldAccess(EOS, o738, o738, i574, java.lang.Object(o763sub))
f2497_0_nth_FieldAccess(EOS, o738, o738, i574, java.lang.Object(o763sub)) → f2523_0_nth_FieldAccess(EOS, o738, o738, i574, java.lang.Object(o763sub))
f2497_0_nth_FieldAccess(EOS, java.lang.Object(o798sub), java.lang.Object(o798sub), i574, java.lang.Object(o798sub)) → f2524_0_nth_FieldAccess(EOS, java.lang.Object(o798sub), java.lang.Object(o798sub), i574, java.lang.Object(o798sub))
f2523_0_nth_FieldAccess(EOS, o738, o738, i574, java.lang.Object(IntList(EOC, o810))) → f2545_0_nth_FieldAccess(EOS, o738, o738, i574, java.lang.Object(IntList(EOC, o810)))
f2545_0_nth_FieldAccess(EOS, o738, o738, i574, java.lang.Object(IntList(EOC, o810))) → f2568_0_nth_Store(EOS, o738, o738, i574, o810)
f2568_0_nth_Store(EOS, o738, o738, i574, o810) → f2591_0_nth_JMP(EOS, o738, o738, i574, o810)
f2591_0_nth_JMP(EOS, o738, o738, i574, o810) → f2614_0_nth_Load(EOS, o738, o738, i574, o810)
f2614_0_nth_Load(EOS, o738, o738, i574, o810) → f2391_0_nth_Load(EOS, o738, o738, i574, o810)
f2391_0_nth_Load(EOS, o738, o738, i546, o737) → f2401_0_nth_ConstantStackPush(EOS, o738, o738, i546, o737, i546)
f2524_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, java.lang.Object(IntList(EOC, o812))) → f2547_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, java.lang.Object(IntList(EOC, o812)))
f2547_0_nth_FieldAccess(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, java.lang.Object(IntList(EOC, o812))) → f2573_0_nth_Store(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812)
f2573_0_nth_Store(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812) → f2595_0_nth_JMP(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812)
f2595_0_nth_JMP(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812) → f2624_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812)
f2624_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812) → f2391_0_nth_Load(EOS, java.lang.Object(IntList(EOC, o812)), java.lang.Object(IntList(EOC, o812)), i574, o812)

Combined rules. Obtained 2 IRules

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

Filtered ground terms:


f2401_0_nth_ConstantStackPush(x1, x2, x3, x4, x5, x6) → f2401_0_nth_ConstantStackPush(x2, x3, x4, x5, x6)
Cond_f2401_0_nth_ConstantStackPush(x1, x2, x3, x4, x5, x6, x7) → Cond_f2401_0_nth_ConstantStackPush(x1, x3, x4, x5, x6, x7)
Cond_f2401_0_nth_ConstantStackPush1(x1, x2, x3, x4, x5, x6, x7) → Cond_f2401_0_nth_ConstantStackPush1(x1, x3, x4, x5, x6, x7)
IntList(x1, x2) → IntList(x2)

Filtered duplicate terms:


f2401_0_nth_ConstantStackPush(x1, x2, x3, x4, x5) → f2401_0_nth_ConstantStackPush(x2, x4, x5)
Cond_f2401_0_nth_ConstantStackPush(x1, x2, x3, x4, x5, x6) → Cond_f2401_0_nth_ConstantStackPush(x1, x3, x5, x6)
Cond_f2401_0_nth_ConstantStackPush1(x1, x2, x3, x4, x5, x6) → Cond_f2401_0_nth_ConstantStackPush1(x1, x5, x6)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 2 rules.

P rules:
f2401_0_nth_ConstantStackPush(v8, v9, x2) → f2401_0_nth_ConstantStackPush(v10, v11, -(x2, 1)) | &&(&&(&&(&&(&&(&&(>(x2, 1), >=(v9, +(v11, 1))), >(+(v9, 1), 1)), >=(v8, v10)), >(+(v8, 1), 0)), >(+(v10, 1), 0)), >(+(v11, 1), 0))
f2401_0_nth_ConstantStackPush(v12, v13, x4) → f2401_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))

(19) Obligation:

Rules:
f2401_0_nth_ConstantStackPush(v8, v9, x2) → f2401_0_nth_ConstantStackPush(v10, v11, -(x2, 1)) | &&(&&(&&(&&(&&(&&(>(x2, 1), >=(v9, +(v11, 1))), >(+(v9, 1), 1)), >=(v8, v10)), >(+(v8, 1), 0)), >(+(v10, 1), 0)), >(+(v11, 1), 0))
f2401_0_nth_ConstantStackPush(v12, v13, x4) → f2401_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))

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


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

Therefore the following rule(s) have been dropped:


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

(21) YES