Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 341 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
    ↳5 JBCTerminationSCC
        ↳6 SCCToIntTRSProof (⇒, 11 ms)
        ↳7 intTRS
        ↳8 PolynomialOrderProcessor (⇔, 5 ms)
        ↳9 YES
    ↳10 JBCTerminationSCC
        ↳11 SCCToIntTRSProof (⇒, 195 ms)
        ↳12 intTRS
        ↳13 LinearRankingProcessor (⇔, 173 ms)
        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class ObjectList {
  Object value;
  ObjectList next;

  public ObjectList(Object value, ObjectList next) {
    this.value = value;
    this.next = next;
  }

  public static ObjectList createList() {
    ObjectList result = null;
    int length = Random.random();
    while (length > 0) {
      result = new ObjectList(new Object(), result);
      length--;
    }
    return result;
  }
}


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

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


/**
 * Allegedly based on an interview question at Microsoft.
 */
public class RunningPointers {

  public static boolean isCyclic(ObjectList l) {
    if (l == null) {
      return false;
    }
    ObjectList l1, l2;
    l1 = l;
    l2 = l.next;
    while (l2 != null && l1 != l2) {
      l2 = l2.next;
      if (l2 == null) {
        return false;
      }
      else if (l2 == l1) {
        return true;
      }
      else {
        l2 = l2.next;
      }
      l1 = l1.next;
    }
    return l2 != null;
  }

  public static void main(String[] args) {
    Random.args = args;
    ObjectList list = ObjectList.createList();
    isCyclic(list);
  }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
RunningPointers.main([Ljava/lang/String;)V: Graph of 169 nodes with 1 SCC.

ObjectList.createList()LObjectList;: Graph of 97 nodes with 1 SCC.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: ObjectList.createList()LObjectList;
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:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f393_0_createList_LE(EOS, i41, i41) → f397_0_createList_LE(EOS, i41, i41)
f397_0_createList_LE(EOS, i41, i41) → f401_0_createList_New(EOS, i41) | >(i41, 0)
f401_0_createList_New(EOS, i41) → f404_0_createList_Duplicate(EOS, i41)
f404_0_createList_Duplicate(EOS, i41) → f408_0_createList_New(EOS, i41)
f408_0_createList_New(EOS, i41) → f420_0_createList_Duplicate(EOS, i41)
f420_0_createList_Duplicate(EOS, i41) → f429_0_createList_InvokeMethod(EOS, i41)
f429_0_createList_InvokeMethod(EOS, i41) → f431_0_createList_Load(EOS, i41)
f431_0_createList_Load(EOS, i41) → f433_0_createList_InvokeMethod(EOS, i41)
f433_0_createList_InvokeMethod(EOS, i41) → f437_0__init__Load(EOS, i41)
f437_0__init__Load(EOS, i41) → f441_0__init__InvokeMethod(EOS, i41)
f441_0__init__InvokeMethod(EOS, i41) → f446_0__init__Load(EOS, i41)
f446_0__init__Load(EOS, i41) → f451_0__init__Load(EOS, i41)
f451_0__init__Load(EOS, i41) → f456_0__init__FieldAccess(EOS, i41)
f456_0__init__FieldAccess(EOS, i41) → f461_0__init__Load(EOS, i41)
f461_0__init__Load(EOS, i41) → f466_0__init__Load(EOS, i41)
f466_0__init__Load(EOS, i41) → f470_0__init__FieldAccess(EOS, i41)
f470_0__init__FieldAccess(EOS, i41) → f476_0__init__Return(EOS, i41)
f476_0__init__Return(EOS, i41) → f480_0_createList_Store(EOS, i41)
f480_0_createList_Store(EOS, i41) → f484_0_createList_Inc(EOS, i41)
f484_0_createList_Inc(EOS, i41) → f488_0_createList_JMP(EOS, +(i41, -1)) | >(i41, 0)
f488_0_createList_JMP(EOS, i49) → f495_0_createList_Load(EOS, i49)
f495_0_createList_Load(EOS, i49) → f389_0_createList_Load(EOS, i49)
f389_0_createList_Load(EOS, i37) → f393_0_createList_LE(EOS, i37, i37)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f393_0_createList_LE(x1, x2, x3) → f393_0_createList_LE(x2, x3)
Cond_f393_0_createList_LE(x1, x2, x3, x4) → Cond_f393_0_createList_LE(x1, x3, x4)

Filtered duplicate terms:


f393_0_createList_LE(x1, x2) → f393_0_createList_LE(x2)
Cond_f393_0_createList_LE(x1, x2, x3) → Cond_f393_0_createList_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(7) Obligation:

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

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f393_0_createList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: RunningPointers.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • ObjectList: [next]
  • Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 64 IRules

P rules:
f834_0_isCyclic_NULL(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), java.lang.Object(o198sub)) → f837_0_isCyclic_NULL(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), java.lang.Object(o198sub))
f837_0_isCyclic_NULL(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), java.lang.Object(o198sub)) → f840_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub))
f840_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub)) → f843_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), o188)
f843_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), o188) → f850_0_isCyclic_EQ(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), o188, java.lang.Object(o198sub))
f850_0_isCyclic_EQ(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), o188, java.lang.Object(o198sub)) → f861_0_isCyclic_EQ(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), o188, java.lang.Object(o198sub))
f861_0_isCyclic_EQ(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub), o188, java.lang.Object(o198sub)) → f866_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub))
f866_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub)) → f873_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub))
f873_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub)) → f885_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o198sub))
f873_0_isCyclic_FieldAccess(EOS, java.lang.Object(o212sub), o188, java.lang.Object(o212sub)) → f886_0_isCyclic_FieldAccess(EOS, java.lang.Object(o212sub), o188, java.lang.Object(o212sub))
f885_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(ObjectList(EOC, o216))) → f892_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(ObjectList(EOC, o216)))
f892_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(ObjectList(EOC, o216))) → f898_0_isCyclic_Store(EOS, java.lang.Object(o190sub), o188, o216)
f898_0_isCyclic_Store(EOS, java.lang.Object(o190sub), o188, o216) → f904_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, o216)
f904_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, o216) → f912_0_isCyclic_NONNULL(EOS, java.lang.Object(o190sub), o188, o216, o216)
f912_0_isCyclic_NONNULL(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub)) → f924_0_isCyclic_NONNULL(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub))
f924_0_isCyclic_NONNULL(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub)) → f928_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub))
f928_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub)) → f932_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub))
f932_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub)) → f941_0_isCyclic_NE(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub), o188)
f941_0_isCyclic_NE(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub), o188) → f954_0_isCyclic_NE(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub), o188)
f954_0_isCyclic_NE(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub), java.lang.Object(o236sub), o188) → f959_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub))
f959_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub)) → f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub))
f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub)) → f971_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(o236sub))
f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(o248sub), o188, java.lang.Object(o248sub)) → f972_0_isCyclic_FieldAccess(EOS, java.lang.Object(o248sub), o188, java.lang.Object(o248sub))
f971_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(ObjectList(EOC, o253))) → f979_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(ObjectList(EOC, o253)))
f979_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o188, java.lang.Object(ObjectList(EOC, o253))) → f982_0_isCyclic_Store(EOS, java.lang.Object(o190sub), o188, o253)
f982_0_isCyclic_Store(EOS, java.lang.Object(o190sub), o188, o253) → f988_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, o253)
f988_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, o253) → f993_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, o188)
f993_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(o270sub)) → f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(o270sub))
f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(o270sub)) → f1012_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(o270sub))
f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(o273sub), o253, java.lang.Object(o273sub)) → f1013_0_isCyclic_FieldAccess(EOS, java.lang.Object(o273sub), o253, java.lang.Object(o273sub))
f1012_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(o270sub)) → f1022_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(o270sub))
f1012_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), java.lang.Object(o276sub), java.lang.Object(o276sub)) → f1023_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), java.lang.Object(o276sub), java.lang.Object(o276sub))
f1022_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(ObjectList(EOC, o284))) → f1036_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(ObjectList(EOC, o284)))
f1036_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), o253, java.lang.Object(ObjectList(EOC, o284))) → f1044_0_isCyclic_Store(EOS, java.lang.Object(o190sub), o253, o284)
f1044_0_isCyclic_Store(EOS, java.lang.Object(o190sub), o253, o284) → f1056_0_isCyclic_JMP(EOS, java.lang.Object(o190sub), o284, o253)
f1056_0_isCyclic_JMP(EOS, java.lang.Object(o190sub), o284, o253) → f1075_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o284, o253)
f1075_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o284, o253) → f828_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o284, o253)
f828_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o188, o189) → f834_0_isCyclic_NULL(EOS, java.lang.Object(o190sub), o188, o189, o189)
f1023_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), java.lang.Object(ObjectList(EOC, o287)), java.lang.Object(ObjectList(EOC, o287))) → f1038_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), java.lang.Object(ObjectList(EOC, o287)), java.lang.Object(ObjectList(EOC, o287)))
f1038_0_isCyclic_FieldAccess(EOS, java.lang.Object(o190sub), java.lang.Object(ObjectList(EOC, o287)), java.lang.Object(ObjectList(EOC, o287))) → f1047_0_isCyclic_Store(EOS, java.lang.Object(o190sub), java.lang.Object(ObjectList(EOC, o287)), o287)
f1047_0_isCyclic_Store(EOS, java.lang.Object(o190sub), java.lang.Object(ObjectList(EOC, o287)), o287) → f1059_0_isCyclic_JMP(EOS, java.lang.Object(o190sub), o287, java.lang.Object(ObjectList(EOC, o287)))
f1059_0_isCyclic_JMP(EOS, java.lang.Object(o190sub), o287, java.lang.Object(ObjectList(EOC, o287))) → f1081_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o287, java.lang.Object(ObjectList(EOC, o287)))
f1081_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o287, java.lang.Object(ObjectList(EOC, o287))) → f828_0_isCyclic_Load(EOS, java.lang.Object(o190sub), o287, java.lang.Object(ObjectList(EOC, o287)))
f1013_0_isCyclic_FieldAccess(EOS, java.lang.Object(o273sub), o253, java.lang.Object(o273sub)) → f1030_0_isCyclic_FieldAccess(EOS, java.lang.Object(o273sub), o253, java.lang.Object(o273sub))
f1013_0_isCyclic_FieldAccess(EOS, java.lang.Object(o279sub), java.lang.Object(o279sub), java.lang.Object(o279sub)) → f1031_0_isCyclic_FieldAccess(EOS, java.lang.Object(o279sub), java.lang.Object(o279sub), java.lang.Object(o279sub))
f1030_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o290)), o253, java.lang.Object(ObjectList(EOC, o290))) → f1040_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o290)), o253, java.lang.Object(ObjectList(EOC, o290)))
f1040_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o290)), o253, java.lang.Object(ObjectList(EOC, o290))) → f1050_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o290)), o253, o290)
f1050_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o290)), o253, o290) → f1063_0_isCyclic_JMP(EOS, java.lang.Object(ObjectList(EOC, o290)), o290, o253)
f1063_0_isCyclic_JMP(EOS, java.lang.Object(ObjectList(EOC, o290)), o290, o253) → f1088_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o290)), o290, o253)
f1088_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o290)), o290, o253) → f828_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o290)), o290, o253)
f1031_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293))) → f1042_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293)))
f1042_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293))) → f1054_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293)), o293)
f1054_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o293)), java.lang.Object(ObjectList(EOC, o293)), o293) → f1067_0_isCyclic_JMP(EOS, java.lang.Object(ObjectList(EOC, o293)), o293, java.lang.Object(ObjectList(EOC, o293)))
f1067_0_isCyclic_JMP(EOS, java.lang.Object(ObjectList(EOC, o293)), o293, java.lang.Object(ObjectList(EOC, o293))) → f1094_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o293)), o293, java.lang.Object(ObjectList(EOC, o293)))
f1094_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o293)), o293, java.lang.Object(ObjectList(EOC, o293))) → f828_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o293)), o293, java.lang.Object(ObjectList(EOC, o293)))
f972_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, java.lang.Object(ObjectList(EOC, o256))) → f980_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, java.lang.Object(ObjectList(EOC, o256)))
f980_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, java.lang.Object(ObjectList(EOC, o256))) → f985_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, o256)
f985_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, o256) → f991_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, o256)
f991_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o256)), o188, o256) → f999_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o256)), o256, o188)
f999_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o256)), o256, o188) → f993_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o256)), o256, o188)
f886_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, java.lang.Object(ObjectList(EOC, o219))) → f894_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, java.lang.Object(ObjectList(EOC, o219)))
f894_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, java.lang.Object(ObjectList(EOC, o219))) → f900_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219)
f900_0_isCyclic_Store(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219) → f907_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219)
f907_0_isCyclic_Load(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219) → f918_0_isCyclic_NONNULL(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219, o219)
f918_0_isCyclic_NONNULL(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219, o219) → f912_0_isCyclic_NONNULL(EOS, java.lang.Object(ObjectList(EOC, o219)), o188, o219, o219)

Combined rules. Obtained 8 IRules

P rules:
f834_0_isCyclic_NULL(EOS, java.lang.Object(x0), x1, java.lang.Object(ObjectList(EOC, java.lang.Object(x2))), java.lang.Object(ObjectList(EOC, java.lang.Object(x2)))) → f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(x0), x1, java.lang.Object(x2))
f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(x0), java.lang.Object(x1), java.lang.Object(ObjectList(EOC, x2))) → f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(x0), x2, java.lang.Object(x1))
f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(x0), x1, java.lang.Object(ObjectList(EOC, x2))) → f834_0_isCyclic_NULL(EOS, java.lang.Object(x0), x2, x1, x1)
f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(x0), java.lang.Object(ObjectList(EOC, x1)), java.lang.Object(ObjectList(EOC, x1))) → f834_0_isCyclic_NULL(EOS, java.lang.Object(x0), x1, java.lang.Object(ObjectList(EOC, x1)), java.lang.Object(ObjectList(EOC, x1)))
f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, x0)), x1, java.lang.Object(ObjectList(EOC, x0))) → f834_0_isCyclic_NULL(EOS, java.lang.Object(ObjectList(EOC, x0)), x0, x1, x1)
f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, x0)), java.lang.Object(ObjectList(EOC, x0)), java.lang.Object(ObjectList(EOC, x0))) → f834_0_isCyclic_NULL(EOS, java.lang.Object(ObjectList(EOC, x0)), x0, java.lang.Object(ObjectList(EOC, x0)), java.lang.Object(ObjectList(EOC, x0)))
f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, x0)), java.lang.Object(x1), java.lang.Object(ObjectList(EOC, x0))) → f1002_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, x0)), x0, java.lang.Object(x1))
f834_0_isCyclic_NULL(EOS, java.lang.Object(ObjectList(EOC, java.lang.Object(x0))), x1, java.lang.Object(ObjectList(EOC, java.lang.Object(x0))), java.lang.Object(ObjectList(EOC, java.lang.Object(x0)))) → f962_0_isCyclic_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, java.lang.Object(x0))), x1, java.lang.Object(x0))

Filtered ground terms:


f834_0_isCyclic_NULL(x1, x2, x3, x4, x5) → f834_0_isCyclic_NULL(x2, x3, x4, x5)
f962_0_isCyclic_FieldAccess(x1, x2, x3, x4) → f962_0_isCyclic_FieldAccess(x2, x3, x4)
f1002_0_isCyclic_FieldAccess(x1, x2, x3, x4) → f1002_0_isCyclic_FieldAccess(x2, x3, x4)
ObjectList(x1, x2) → ObjectList(x2)

Filtered duplicate terms:


f834_0_isCyclic_NULL(x1, x2, x3, x4) → f834_0_isCyclic_NULL(x1, x2, x4)

Prepared 8 rules for path length conversion:

P rules:
f834_0_isCyclic_NULL(java.lang.Object(x0), x1, java.lang.Object(ObjectList(java.lang.Object(x2)))) → f962_0_isCyclic_FieldAccess(java.lang.Object(x0), x1, java.lang.Object(x2))
f962_0_isCyclic_FieldAccess(java.lang.Object(x0), java.lang.Object(x1), java.lang.Object(ObjectList(x2))) → f1002_0_isCyclic_FieldAccess(java.lang.Object(x0), x2, java.lang.Object(x1))
f1002_0_isCyclic_FieldAccess(java.lang.Object(x0), x1, java.lang.Object(ObjectList(x2))) → f834_0_isCyclic_NULL(java.lang.Object(x0), x2, x1)
f1002_0_isCyclic_FieldAccess(java.lang.Object(x0), java.lang.Object(ObjectList(x1)), java.lang.Object(ObjectList(x1))) → f834_0_isCyclic_NULL(java.lang.Object(x0), x1, java.lang.Object(ObjectList(x1)))
f1002_0_isCyclic_FieldAccess(java.lang.Object(ObjectList(x0)), x1, java.lang.Object(ObjectList(x0))) → f834_0_isCyclic_NULL(java.lang.Object(ObjectList(x0)), x0, x1)
f1002_0_isCyclic_FieldAccess(java.lang.Object(ObjectList(x0)), java.lang.Object(ObjectList(x0)), java.lang.Object(ObjectList(x0))) → f834_0_isCyclic_NULL(java.lang.Object(ObjectList(x0)), x0, java.lang.Object(ObjectList(x0)))
f962_0_isCyclic_FieldAccess(java.lang.Object(ObjectList(x0)), java.lang.Object(x1), java.lang.Object(ObjectList(x0))) → f1002_0_isCyclic_FieldAccess(java.lang.Object(ObjectList(x0)), x0, java.lang.Object(x1))
f834_0_isCyclic_NULL(java.lang.Object(ObjectList(java.lang.Object(x0))), x1, java.lang.Object(ObjectList(java.lang.Object(x0)))) → f962_0_isCyclic_FieldAccess(java.lang.Object(ObjectList(java.lang.Object(x0))), x1, java.lang.Object(x0))

Finished conversion. Obtained 8 rules.

P rules:
f834_0_isCyclic_NULL(v27, v28, v29) → f962_0_isCyclic_FieldAccess(v30, v31, v32) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v32, 1), 1), <=(+(v32, 2), v29)), >(+(v31, 1), 0)), <=(v31, v28)), >(+(v30, 1), 1)), <=(v30, v27)), >(+(v29, 1), 3)), >(+(v28, 1), 0)), >(+(v27, 1), 1))
f962_0_isCyclic_FieldAccess(v33, v34, v35) → f1002_0_isCyclic_FieldAccess(v36, v37, v38) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v38, 1), 1), <=(v38, v34)), >(+(v37, 1), 0)), <=(+(v37, 1), v35)), >(+(v36, 1), 1)), <=(v36, v33)), >(+(v35, 1), 1)), >(+(v34, 1), 1)), >(+(v33, 1), 1))
f1002_0_isCyclic_FieldAccess(v39, v40, v41) → f834_0_isCyclic_NULL(v42, v43, v44) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v44, 1), 0), <=(v44, v40)), >(+(v43, 1), 0)), <=(+(v43, 1), v41)), >(+(v42, 1), 1)), <=(v42, v39)), >(+(v41, 1), 1)), >(+(v40, 1), 0)), >(+(v39, 1), 1))
f1002_0_isCyclic_FieldAccess(v45, v46, v47) → f834_0_isCyclic_NULL(v48, v49, v50) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v50, 1), 1), <=(v50, v47)), <=(v50, v46)), >(+(v49, 1), 0)), <=(+(v49, 1), v47)), <=(+(v49, 1), v46)), >(+(v48, 1), 1)), <=(v48, v45)), >(+(v47, 1), 1)), >(+(v46, 1), 1)), >(+(v45, 1), 1))
f1002_0_isCyclic_FieldAccess(v51, v52, v53) → f834_0_isCyclic_NULL(v54, v55, v56) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v56, 1), 0), <=(v56, v52)), >(+(v55, 1), 0)), <=(+(v55, 1), v53)), <=(+(v55, 1), v51)), >(+(v54, 1), 1)), <=(v54, v53)), <=(v54, v51)), >(+(v53, 1), 1)), >(+(v52, 1), 0)), >(+(v51, 1), 1))
f1002_0_isCyclic_FieldAccess(v57, v58, v59) → f834_0_isCyclic_NULL(v60, v61, v62) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v62, 1), 1), <=(v62, v59)), <=(v62, v58)), <=(v62, v57)), >(+(v61, 1), 0)), <=(+(v61, 1), v59)), <=(+(v61, 1), v58)), <=(+(v61, 1), v57)), >(+(v60, 1), 1)), <=(v60, v59)), <=(v60, v58)), <=(v60, v57)), >(+(v59, 1), 1)), >(+(v58, 1), 1)), >(+(v57, 1), 1))
f962_0_isCyclic_FieldAccess(v63, v64, v65) → f1002_0_isCyclic_FieldAccess(v66, v67, v68) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v68, 1), 1), <=(v68, v64)), >(+(v67, 1), 0)), <=(+(v67, 1), v65)), <=(+(v67, 1), v63)), >(+(v66, 1), 1)), <=(v66, v65)), <=(v66, v63)), >(+(v65, 1), 1)), >(+(v64, 1), 1)), >(+(v63, 1), 1))
f834_0_isCyclic_NULL(v69, v70, v71) → f962_0_isCyclic_FieldAccess(v72, v73, v74) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v74, 1), 1), <=(+(v74, 2), v71)), <=(+(v74, 2), v69)), >(+(v73, 1), 0)), <=(v73, v70)), >(+(v72, 1), 3)), <=(v72, v71)), <=(v72, v69)), >(+(v71, 1), 3)), >(+(v70, 1), 0)), >(+(v69, 1), 3))

(12) Obligation:

Rules:
f834_0_isCyclic_NULL(v27, v28, v29) → f962_0_isCyclic_FieldAccess(v30, v31, v32) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v32, 1), 1), <=(+(v32, 2), v29)), >(+(v31, 1), 0)), <=(v31, v28)), >(+(v30, 1), 1)), <=(v30, v27)), >(+(v29, 1), 3)), >(+(v28, 1), 0)), >(+(v27, 1), 1))
f962_0_isCyclic_FieldAccess(v33, v34, v35) → f1002_0_isCyclic_FieldAccess(v36, v37, v38) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v38, 1), 1), <=(v38, v34)), >(+(v37, 1), 0)), <=(+(v37, 1), v35)), >(+(v36, 1), 1)), <=(v36, v33)), >(+(v35, 1), 1)), >(+(v34, 1), 1)), >(+(v33, 1), 1))
f1002_0_isCyclic_FieldAccess(v39, v40, v41) → f834_0_isCyclic_NULL(v42, v43, v44) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v44, 1), 0), <=(v44, v40)), >(+(v43, 1), 0)), <=(+(v43, 1), v41)), >(+(v42, 1), 1)), <=(v42, v39)), >(+(v41, 1), 1)), >(+(v40, 1), 0)), >(+(v39, 1), 1))
f1002_0_isCyclic_FieldAccess(v45, v46, v47) → f834_0_isCyclic_NULL(v48, v49, v50) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v50, 1), 1), <=(v50, v47)), <=(v50, v46)), >(+(v49, 1), 0)), <=(+(v49, 1), v47)), <=(+(v49, 1), v46)), >(+(v48, 1), 1)), <=(v48, v45)), >(+(v47, 1), 1)), >(+(v46, 1), 1)), >(+(v45, 1), 1))
f1002_0_isCyclic_FieldAccess(v51, v52, v53) → f834_0_isCyclic_NULL(v54, v55, v56) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v56, 1), 0), <=(v56, v52)), >(+(v55, 1), 0)), <=(+(v55, 1), v53)), <=(+(v55, 1), v51)), >(+(v54, 1), 1)), <=(v54, v53)), <=(v54, v51)), >(+(v53, 1), 1)), >(+(v52, 1), 0)), >(+(v51, 1), 1))
f1002_0_isCyclic_FieldAccess(v57, v58, v59) → f834_0_isCyclic_NULL(v60, v61, v62) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v62, 1), 1), <=(v62, v59)), <=(v62, v58)), <=(v62, v57)), >(+(v61, 1), 0)), <=(+(v61, 1), v59)), <=(+(v61, 1), v58)), <=(+(v61, 1), v57)), >(+(v60, 1), 1)), <=(v60, v59)), <=(v60, v58)), <=(v60, v57)), >(+(v59, 1), 1)), >(+(v58, 1), 1)), >(+(v57, 1), 1))
f962_0_isCyclic_FieldAccess(v63, v64, v65) → f1002_0_isCyclic_FieldAccess(v66, v67, v68) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v68, 1), 1), <=(v68, v64)), >(+(v67, 1), 0)), <=(+(v67, 1), v65)), <=(+(v67, 1), v63)), >(+(v66, 1), 1)), <=(v66, v65)), <=(v66, v63)), >(+(v65, 1), 1)), >(+(v64, 1), 1)), >(+(v63, 1), 1))
f834_0_isCyclic_NULL(v69, v70, v71) → f962_0_isCyclic_FieldAccess(v72, v73, v74) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(v74, 1), 1), <=(+(v74, 2), v71)), <=(+(v74, 2), v69)), >(+(v73, 1), 0)), <=(v73, v70)), >(+(v72, 1), 3)), <=(v72, v71)), <=(v72, v69)), >(+(v71, 1), 3)), >(+(v70, 1), 0)), >(+(v69, 1), 3))

(13) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f834_0_isCyclic_NULL(x)] = 3·x2
[f962_0_isCyclic_FieldAccess(x)] = (-1) + 3·x2
[f1002_0_isCyclic_FieldAccess(x)] = (-2) + 3·x3

where x = (x1, ... ,xn).



Therefore the following rule(s) have been dropped:


f834_0_isCyclic_NULL(x0, x1, x2) → f962_0_isCyclic_FieldAccess(x3, x4, x5) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x5, 1), 1), <=(+(x5, 2), x2)), >(+(x4, 1), 0)), <=(x4, x1)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x2, 1), 3)), >(+(x1, 1), 0)), >(+(x0, 1), 1))
f962_0_isCyclic_FieldAccess(x6, x7, x8) → f1002_0_isCyclic_FieldAccess(x9, x10, x11) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x11, 1), 1), <=(x11, x7)), >(+(x10, 1), 0)), <=(+(x10, 1), x8)), >(+(x9, 1), 1)), <=(x9, x6)), >(+(x8, 1), 1)), >(+(x7, 1), 1)), >(+(x6, 1), 1))
f1002_0_isCyclic_FieldAccess(x12, x13, x14) → f834_0_isCyclic_NULL(x15, x16, x17) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x17, 1), 0), <=(x17, x13)), >(+(x16, 1), 0)), <=(+(x16, 1), x14)), >(+(x15, 1), 1)), <=(x15, x12)), >(+(x14, 1), 1)), >(+(x13, 1), 0)), >(+(x12, 1), 1))
f1002_0_isCyclic_FieldAccess(x18, x19, x20) → f834_0_isCyclic_NULL(x21, x22, x23) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x23, 1), 1), <=(x23, x20)), <=(x23, x19)), >(+(x22, 1), 0)), <=(+(x22, 1), x20)), <=(+(x22, 1), x19)), >(+(x21, 1), 1)), <=(x21, x18)), >(+(x20, 1), 1)), >(+(x19, 1), 1)), >(+(x18, 1), 1))
f1002_0_isCyclic_FieldAccess(x24, x25, x26) → f834_0_isCyclic_NULL(x27, x28, x29) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x29, 1), 0), <=(x29, x25)), >(+(x28, 1), 0)), <=(+(x28, 1), x26)), <=(+(x28, 1), x24)), >(+(x27, 1), 1)), <=(x27, x26)), <=(x27, x24)), >(+(x26, 1), 1)), >(+(x25, 1), 0)), >(+(x24, 1), 1))
f1002_0_isCyclic_FieldAccess(x30, x31, x32) → f834_0_isCyclic_NULL(x33, x34, x35) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x35, 1), 1), <=(x35, x32)), <=(x35, x31)), <=(x35, x30)), >(+(x34, 1), 0)), <=(+(x34, 1), x32)), <=(+(x34, 1), x31)), <=(+(x34, 1), x30)), >(+(x33, 1), 1)), <=(x33, x32)), <=(x33, x31)), <=(x33, x30)), >(+(x32, 1), 1)), >(+(x31, 1), 1)), >(+(x30, 1), 1))
f962_0_isCyclic_FieldAccess(x36, x37, x38) → f1002_0_isCyclic_FieldAccess(x39, x40, x41) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x41, 1), 1), <=(x41, x37)), >(+(x40, 1), 0)), <=(+(x40, 1), x38)), <=(+(x40, 1), x36)), >(+(x39, 1), 1)), <=(x39, x38)), <=(x39, x36)), >(+(x38, 1), 1)), >(+(x37, 1), 1)), >(+(x36, 1), 1))
f834_0_isCyclic_NULL(x42, x43, x44) → f962_0_isCyclic_FieldAccess(x45, x46, x47) | &&(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(x47, 1), 1), <=(+(x47, 2), x44)), <=(+(x47, 2), x42)), >(+(x46, 1), 0)), <=(x46, x43)), >(+(x45, 1), 3)), <=(x45, x44)), <=(x45, x42)), >(+(x44, 1), 3)), >(+(x43, 1), 0)), >(+(x42, 1), 3))

(14) YES