Termination of the given JBC could be proven:

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

(0) Obligation:

JBC Problem based on JBC Program:
/**
 * This class represents a list, where the function duplicate() can be used to
 * duplicate all elements in the list.
 * @author cotto
 */
public class ListDuplicate {
  /**
   * Walk through the list and, for each original element, copy it and append
   * this copy after the original. This transforms abc to aabbcc.
   */
  public static void duplicate(ObjectList list) {
    ObjectList current = list;
    boolean even = true;
    while (current != null) {
      // only copy the original elements!
      if (even) {
        final ObjectList copy =
          new ObjectList(current.value, current.next);
        current.next = copy;
      }
      current = current.next;
      even = !even;
    }
  }

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


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();
  }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ListDuplicate.main([Ljava/lang/String;)V: Graph of 50 nodes with 0 SCCs.

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

ListDuplicate.duplicate(LObjectList;)V: Graph of 95 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: ListDuplicate.duplicate(LObjectList;)V
SCC calls the following helper methods:
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
    • ObjectList: [value, next]
  • Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 90 IRules

P rules:
f589_0_duplicate_NULL(EOS, o95, java.lang.Object(o104sub), i58, java.lang.Object(o104sub)) → f592_0_duplicate_NULL(EOS, o95, java.lang.Object(o104sub), i58, java.lang.Object(o104sub))
f592_0_duplicate_NULL(EOS, o95, java.lang.Object(o104sub), i58, java.lang.Object(o104sub)) → f595_0_duplicate_Load(EOS, o95, java.lang.Object(o104sub), i58)
f595_0_duplicate_Load(EOS, o95, java.lang.Object(o104sub), i58) → f599_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), i58, i58)
f599_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), matching1, matching2) → f603_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), 1, 1) | &&(=(matching1, 1), =(matching2, 1))
f599_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), matching1, matching2) → f604_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f603_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), matching1, matching2) → f613_0_duplicate_New(EOS, o95, java.lang.Object(o104sub), 1) | &&(&&(>(1, 0), =(matching1, 1)), =(matching2, 1))
f613_0_duplicate_New(EOS, o95, java.lang.Object(o104sub), matching1) → f627_0_duplicate_Duplicate(EOS, o95, java.lang.Object(o104sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
f627_0_duplicate_Duplicate(EOS, o95, java.lang.Object(o104sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL))) → f633_0_duplicate_Load(EOS, o95, java.lang.Object(o104sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
f633_0_duplicate_Load(EOS, o95, java.lang.Object(o104sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL))) → f644_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(o104sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o104sub)) | =(matching1, 1)
f644_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(o104sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o104sub)) → f660_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(o104sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o104sub)) | =(matching1, 1)
f644_0_duplicate_FieldAccess(EOS, java.lang.Object(o126sub), java.lang.Object(o126sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o126sub)) → f661_0_duplicate_FieldAccess(EOS, java.lang.Object(o126sub), java.lang.Object(o126sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o126sub)) | =(matching1, 1)
f660_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o131, o132))) → f665_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f665_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o131, o132))) → f674_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131) | =(matching1, 1)
f674_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131) → f684_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f684_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, java.lang.Object(ObjectList(EOC, o131, o132))) → f694_0_duplicate_InvokeMethod(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132) | =(matching1, 1)
f694_0_duplicate_InvokeMethod(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132) → f704_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132) | =(matching1, 1)
f704_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132) → f717_0__init__InvokeMethod(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
f717_0__init__InvokeMethod(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL))) → f734_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132) | =(matching1, 1)
f734_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132) → f738_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
f738_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL))) → f741_0__init__FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131) | =(matching1, 1)
f741_0__init__FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o132, java.lang.Object(ObjectList(EOC, NULL, NULL)), o131) → f749_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, NULL)), java.lang.Object(ObjectList(EOC, o131, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, o131, NULL)), o132) | =(matching1, 1)
f749_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, NULL)), java.lang.Object(ObjectList(EOC, o131, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, o131, NULL)), o132) → f757_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, NULL)), java.lang.Object(ObjectList(EOC, o131, NULL)), o131, o132, o132, java.lang.Object(ObjectList(EOC, o131, NULL))) | =(matching1, 1)
f757_0__init__Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, NULL)), java.lang.Object(ObjectList(EOC, o131, NULL)), o131, o132, o132, java.lang.Object(ObjectList(EOC, o131, NULL))) → f760_0__init__FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, NULL)), java.lang.Object(ObjectList(EOC, o131, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, o131, NULL)), o132) | =(matching1, 1)
f760_0__init__FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, NULL)), java.lang.Object(ObjectList(EOC, o131, NULL)), o131, o132, java.lang.Object(ObjectList(EOC, o131, NULL)), o132) → f767_0__init__Return(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, o132)), java.lang.Object(ObjectList(EOC, o131, o132)), o131, o132) | =(matching1, 1)
f767_0__init__Return(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, o132)), java.lang.Object(ObjectList(EOC, o131, o132)), o131, o132) → f774_0_duplicate_Store(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f774_0_duplicate_Store(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, o132))) → f779_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f779_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, o132))) → f784_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, o132)), java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f784_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, o132)), java.lang.Object(ObjectList(EOC, o131, o132))) → f789_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1, java.lang.Object(ObjectList(EOC, o131, o132)), java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f789_0_duplicate_FieldAccess(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1, java.lang.Object(ObjectList(EOC, o131, o132)), java.lang.Object(ObjectList(EOC, o131, o132))) → f796_0_duplicate_Load(EOS, o95put, java.lang.Object(ObjectList(EOC, o131, java.lang.Object(ObjectList(EOC, o131, o132)))), 1) | =(matching1, 1)
f796_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, java.lang.Object(ObjectList(EOC, o131, o132)))), matching1) → f801_0_duplicate_FieldAccess(EOS, o95, 1, java.lang.Object(ObjectList(EOC, o131, java.lang.Object(ObjectList(EOC, o131, o132))))) | =(matching1, 1)
f801_0_duplicate_FieldAccess(EOS, o95, matching1, java.lang.Object(ObjectList(EOC, o131, java.lang.Object(ObjectList(EOC, o131, o132))))) → f807_0_duplicate_Store(EOS, o95, 1, java.lang.Object(ObjectList(EOC, o131, o132))) | =(matching1, 1)
f807_0_duplicate_Store(EOS, o95, matching1, java.lang.Object(ObjectList(EOC, o131, o132))) → f814_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1) | =(matching1, 1)
f814_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1) → f823_0_duplicate_NE(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 1) | =(matching1, 1)
f823_0_duplicate_NE(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1) → f828_0_duplicate_ConstantStackPush(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132))) | &&(>(1, 0), =(matching1, 1))
f828_0_duplicate_ConstantStackPush(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132))) → f832_0_duplicate_Store(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 0)
f832_0_duplicate_Store(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1) → f841_0_duplicate_JMP(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 0) | =(matching1, 0)
f841_0_duplicate_JMP(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1) → f851_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 0) | =(matching1, 0)
f851_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), matching1) → f584_0_duplicate_Load(EOS, o95, java.lang.Object(ObjectList(EOC, o131, o132)), 0) | =(matching1, 0)
f584_0_duplicate_Load(EOS, o95, o96, i58) → f589_0_duplicate_NULL(EOS, o95, o96, i58, o96)
f661_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o134, o135))) → f667_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f667_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o134, o135))) → f677_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134) | =(matching1, 1)
f677_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134) → f687_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f687_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, java.lang.Object(ObjectList(EOC, o134, o135))) → f697_0_duplicate_InvokeMethod(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135) | =(matching1, 1)
f697_0_duplicate_InvokeMethod(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135) → f706_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135) | =(matching1, 1)
f706_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135) → f720_0__init__InvokeMethod(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
f720_0__init__InvokeMethod(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL))) → f736_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135) | =(matching1, 1)
f736_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135) → f739_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
f739_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL))) → f744_0__init__FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134) | =(matching1, 1)
f744_0__init__FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o135, java.lang.Object(ObjectList(EOC, NULL, NULL)), o134) → f754_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, NULL)), java.lang.Object(ObjectList(EOC, o134, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, o134, NULL)), o135) | =(matching1, 1)
f754_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, NULL)), java.lang.Object(ObjectList(EOC, o134, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, o134, NULL)), o135) → f759_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, NULL)), java.lang.Object(ObjectList(EOC, o134, NULL)), o134, o135, o135, java.lang.Object(ObjectList(EOC, o134, NULL))) | =(matching1, 1)
f759_0__init__Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, NULL)), java.lang.Object(ObjectList(EOC, o134, NULL)), o134, o135, o135, java.lang.Object(ObjectList(EOC, o134, NULL))) → f761_0__init__FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, NULL)), java.lang.Object(ObjectList(EOC, o134, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, o134, NULL)), o135) | =(matching1, 1)
f761_0__init__FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, NULL)), java.lang.Object(ObjectList(EOC, o134, NULL)), o134, o135, java.lang.Object(ObjectList(EOC, o134, NULL)), o135) → f771_0__init__Return(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), o134, o135) | =(matching1, 1)
f771_0__init__Return(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), o134, o135) → f776_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f776_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, o135))) → f782_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f782_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, o135))) → f787_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f787_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135))) → f792_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), 1, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f792_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135)), matching1, java.lang.Object(ObjectList(EOC, o134, o135)), java.lang.Object(ObjectList(EOC, o134, o135))) → f797_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), 1) | =(matching1, 1)
f797_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), matching1) → f804_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), 1, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135))))) | =(matching1, 1)
f804_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), matching1, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135))))) → f810_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), 1, java.lang.Object(ObjectList(EOC, o134, o135))) | =(matching1, 1)
f810_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), matching1, java.lang.Object(ObjectList(EOC, o134, o135))) → f819_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), 1) | =(matching1, 1)
f819_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), matching1) → f827_0_duplicate_NE(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), 1) | =(matching1, 1)
f827_0_duplicate_NE(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), matching1) → f829_0_duplicate_ConstantStackPush(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135))) | &&(>(1, 0), =(matching1, 1))
f829_0_duplicate_ConstantStackPush(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135))) → f837_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), 0)
f837_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), matching1) → f845_0_duplicate_JMP(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), 0) | =(matching1, 0)
f845_0_duplicate_JMP(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), matching1) → f858_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), 0) | =(matching1, 0)
f858_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), matching1) → f584_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o134, java.lang.Object(ObjectList(EOC, o134, o135)))), java.lang.Object(ObjectList(EOC, o134, o135)), 0) | =(matching1, 0)
f604_0_duplicate_EQ(EOS, o95, java.lang.Object(o104sub), matching1, matching2) → f624_0_duplicate_Load(EOS, o95, java.lang.Object(o104sub), 0) | &&(=(matching1, 0), =(matching2, 0))
f624_0_duplicate_Load(EOS, o95, java.lang.Object(o104sub), matching1) → f631_0_duplicate_FieldAccess(EOS, o95, 0, java.lang.Object(o104sub)) | =(matching1, 0)
f631_0_duplicate_FieldAccess(EOS, o95, matching1, java.lang.Object(o104sub)) → f641_0_duplicate_FieldAccess(EOS, o95, 0, java.lang.Object(o104sub)) | =(matching1, 0)
f631_0_duplicate_FieldAccess(EOS, java.lang.Object(o116sub), matching1, java.lang.Object(o116sub)) → f642_0_duplicate_FieldAccess(EOS, java.lang.Object(o116sub), 0, java.lang.Object(o116sub)) | =(matching1, 0)
f641_0_duplicate_FieldAccess(EOS, o95, matching1, java.lang.Object(ObjectList(EOC, o118, o119))) → f646_0_duplicate_FieldAccess(EOS, o95, 0, java.lang.Object(ObjectList(EOC, o118, o119))) | =(matching1, 0)
f646_0_duplicate_FieldAccess(EOS, o95, matching1, java.lang.Object(ObjectList(EOC, o118, o119))) → f662_0_duplicate_Store(EOS, o95, 0, o119) | =(matching1, 0)
f662_0_duplicate_Store(EOS, o95, matching1, o119) → f669_0_duplicate_Load(EOS, o95, o119, 0) | =(matching1, 0)
f669_0_duplicate_Load(EOS, o95, o119, matching1) → f679_0_duplicate_NE(EOS, o95, o119, 0) | =(matching1, 0)
f679_0_duplicate_NE(EOS, o95, o119, matching1) → f689_0_duplicate_ConstantStackPush(EOS, o95, o119) | =(matching1, 0)
f689_0_duplicate_ConstantStackPush(EOS, o95, o119) → f699_0_duplicate_JMP(EOS, o95, o119, 1)
f699_0_duplicate_JMP(EOS, o95, o119, matching1) → f708_0_duplicate_Store(EOS, o95, o119, 1) | =(matching1, 1)
f708_0_duplicate_Store(EOS, o95, o119, matching1) → f713_0_duplicate_JMP(EOS, o95, o119, 1) | =(matching1, 1)
f713_0_duplicate_JMP(EOS, o95, o119, matching1) → f726_0_duplicate_Load(EOS, o95, o119, 1) | =(matching1, 1)
f726_0_duplicate_Load(EOS, o95, o119, matching1) → f584_0_duplicate_Load(EOS, o95, o119, 1) | =(matching1, 1)
f642_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), matching1, java.lang.Object(ObjectList(EOC, o121, o122))) → f649_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), 0, java.lang.Object(ObjectList(EOC, o121, o122))) | =(matching1, 0)
f649_0_duplicate_FieldAccess(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), matching1, java.lang.Object(ObjectList(EOC, o121, o122))) → f663_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), 0, o122) | =(matching1, 0)
f663_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), matching1, o122) → f672_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 0) | =(matching1, 0)
f672_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, matching1) → f682_0_duplicate_NE(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 0) | =(matching1, 0)
f682_0_duplicate_NE(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, matching1) → f692_0_duplicate_ConstantStackPush(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122) | =(matching1, 0)
f692_0_duplicate_ConstantStackPush(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122) → f701_0_duplicate_JMP(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 1)
f701_0_duplicate_JMP(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, matching1) → f711_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 1) | =(matching1, 1)
f711_0_duplicate_Store(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, matching1) → f715_0_duplicate_JMP(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 1) | =(matching1, 1)
f715_0_duplicate_JMP(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, matching1) → f732_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 1) | =(matching1, 1)
f732_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, matching1) → f584_0_duplicate_Load(EOS, java.lang.Object(ObjectList(EOC, o121, o122)), o122, 1) | =(matching1, 1)

Combined rules. Obtained 4 IRules

P rules:
f589_0_duplicate_NULL(EOS, x0, java.lang.Object(ObjectList(EOC, x1, x2)), 1, java.lang.Object(ObjectList(EOC, x1, x2))) → f589_0_duplicate_NULL(EOS, x4, java.lang.Object(ObjectList(EOC, x1, x2)), 0, java.lang.Object(ObjectList(EOC, x1, x2)))
f589_0_duplicate_NULL(EOS, java.lang.Object(ObjectList(EOC, x0, x1)), java.lang.Object(ObjectList(EOC, x0, x1)), 1, java.lang.Object(ObjectList(EOC, x0, x1))) → f589_0_duplicate_NULL(EOS, java.lang.Object(ObjectList(EOC, x0, java.lang.Object(ObjectList(EOC, x0, x1)))), java.lang.Object(ObjectList(EOC, x0, x1)), 0, java.lang.Object(ObjectList(EOC, x0, x1)))
f589_0_duplicate_NULL(EOS, x0, java.lang.Object(ObjectList(EOC, x1, x2)), 0, java.lang.Object(ObjectList(EOC, x1, x2))) → f589_0_duplicate_NULL(EOS, x0, x2, 1, x2)
f589_0_duplicate_NULL(EOS, java.lang.Object(ObjectList(EOC, x0, x1)), java.lang.Object(ObjectList(EOC, x0, x1)), 0, java.lang.Object(ObjectList(EOC, x0, x1))) → f589_0_duplicate_NULL(EOS, java.lang.Object(ObjectList(EOC, x0, x1)), x1, 1, x1)

Filtered ground terms:


f589_0_duplicate_NULL(x1, x2, x3, x4, x5) → f589_0_duplicate_NULL(x2, x3, x4, x5)
ObjectList(x1, x2, x3) → ObjectList(x2, x3)

Filtered duplicate terms:


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

Filtered unneeded terms:


ObjectList(x1, x2) → ObjectList(x2)

Prepared 4 rules for path length conversion:

P rules:
f589_0_duplicate_NULL(x0, 1, java.lang.Object(ObjectList(x2))) → f589_0_duplicate_NULL(x4, 0, java.lang.Object(ObjectList(x2)))
f589_0_duplicate_NULL(java.lang.Object(ObjectList(x1)), 1, java.lang.Object(ObjectList(x1))) → f589_0_duplicate_NULL(java.lang.Object(ObjectList(java.lang.Object(ObjectList(x1)))), 0, java.lang.Object(ObjectList(x1)))
f589_0_duplicate_NULL(x0, 0, java.lang.Object(ObjectList(x2))) → f589_0_duplicate_NULL(x0, 1, x2)
f589_0_duplicate_NULL(java.lang.Object(ObjectList(x1)), 0, java.lang.Object(ObjectList(x1))) → f589_0_duplicate_NULL(java.lang.Object(ObjectList(x1)), 1, x1)

Finished conversion. Obtained 4 rules.

P rules:
f589_0_duplicate_NULL(v10, c1, v11) → f589_0_duplicate_NULL(v12, 0, v13) | &&(&&(&&(&&(&&(>(+(v13, 1), 1), <=(v13, v11)), >(+(v12, 1), 0)), >(+(v11, 1), 1)), >(+(v10, 1), 0)), =(1, c1))
f589_0_duplicate_NULL(v14, c1, v15) → f589_0_duplicate_NULL(v16, 0, v17) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v17, 1), 1), <=(v17, v15)), <=(v17, v14)), >(+(v16, 1), 3)), <=(-(v16, 2), v15)), <=(-(v16, 2), v14)), >(+(v15, 1), 1)), >(+(v14, 1), 1)), =(1, c1))
f589_0_duplicate_NULL(v18, c0, v19) → f589_0_duplicate_NULL(v20, 1, v21) | &&(&&(&&(&&(&&(&&(>(+(v21, 1), 0), <=(+(v21, 1), v19)), >(+(v20, 1), 0)), <=(v20, v18)), >(+(v19, 1), 1)), >(+(v18, 1), 0)), =(0, c0))
f589_0_duplicate_NULL(v22, c0, v23) → f589_0_duplicate_NULL(v24, 1, v25) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v25, 1), 0), <=(+(v25, 1), v23)), <=(+(v25, 1), v22)), >(+(v24, 1), 1)), <=(v24, v23)), <=(v24, v22)), >(+(v23, 1), 1)), >(+(v22, 1), 1)), =(0, c0))

(7) Obligation:

Rules:
f589_0_duplicate_NULL(v10, c1, v11) → f589_0_duplicate_NULL(v12, 0, v13) | &&(&&(&&(&&(&&(>(+(v13, 1), 1), <=(v13, v11)), >(+(v12, 1), 0)), >(+(v11, 1), 1)), >(+(v10, 1), 0)), =(1, c1))
f589_0_duplicate_NULL(v14, c1, v15) → f589_0_duplicate_NULL(v16, 0, v17) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v17, 1), 1), <=(v17, v15)), <=(v17, v14)), >(+(v16, 1), 3)), <=(-(v16, 2), v15)), <=(-(v16, 2), v14)), >(+(v15, 1), 1)), >(+(v14, 1), 1)), =(1, c1))
f589_0_duplicate_NULL(v18, c0, v19) → f589_0_duplicate_NULL(v20, 1, v21) | &&(&&(&&(&&(&&(&&(>(+(v21, 1), 0), <=(+(v21, 1), v19)), >(+(v20, 1), 0)), <=(v20, v18)), >(+(v19, 1), 1)), >(+(v18, 1), 0)), =(0, c0))
f589_0_duplicate_NULL(v22, c0, v23) → f589_0_duplicate_NULL(v24, 1, v25) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(v25, 1), 0), <=(+(v25, 1), v23)), <=(+(v25, 1), v22)), >(+(v24, 1), 1)), <=(v24, v23)), <=(v24, v22)), >(+(v23, 1), 1)), >(+(v22, 1), 1)), =(0, c0))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:


[f589_0_duplicate_NULL(x)] = 1·x2 + 2·x3

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



Therefore the following rule(s) have been dropped:


f589_0_duplicate_NULL(x0, x1, x2) → f589_0_duplicate_NULL(x3, 0, x4) | &&(&&(&&(&&(&&(>(+(x4, 1), 1), <=(x4, x2)), >(+(x3, 1), 0)), >(+(x2, 1), 1)), >(+(x0, 1), 0)), =(1, x1))
f589_0_duplicate_NULL(x5, x6, x7) → f589_0_duplicate_NULL(x8, 0, x9) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x9, 1), 1), <=(x9, x7)), <=(x9, x5)), >(+(x8, 1), 3)), <=(-(x8, 2), x7)), <=(-(x8, 2), x5)), >(+(x7, 1), 1)), >(+(x5, 1), 1)), =(1, x6))
f589_0_duplicate_NULL(x10, x11, x12) → f589_0_duplicate_NULL(x13, 1, x14) | &&(&&(&&(&&(&&(&&(>(+(x14, 1), 0), <=(+(x14, 1), x12)), >(+(x13, 1), 0)), <=(x13, x10)), >(+(x12, 1), 1)), >(+(x10, 1), 0)), =(0, x11))
f589_0_duplicate_NULL(x15, x16, x17) → f589_0_duplicate_NULL(x18, 1, x19) | &&(&&(&&(&&(&&(&&(&&(&&(>(+(x19, 1), 0), <=(+(x19, 1), x17)), <=(+(x19, 1), x15)), >(+(x18, 1), 1)), <=(x18, x17)), <=(x18, x15)), >(+(x17, 1), 1)), >(+(x15, 1), 1)), =(0, x16))

(9) YES

(10) 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:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f387_0_createList_LE(EOS, i42, i42) → f391_0_createList_LE(EOS, i42, i42)
f391_0_createList_LE(EOS, i42, i42) → f394_0_createList_New(EOS, i42) | >(i42, 0)
f394_0_createList_New(EOS, i42) → f398_0_createList_Duplicate(EOS, i42)
f398_0_createList_Duplicate(EOS, i42) → f400_0_createList_New(EOS, i42)
f400_0_createList_New(EOS, i42) → f412_0_createList_Duplicate(EOS, i42)
f412_0_createList_Duplicate(EOS, i42) → f424_0_createList_InvokeMethod(EOS, i42)
f424_0_createList_InvokeMethod(EOS, i42) → f428_0_createList_Load(EOS, i42)
f428_0_createList_Load(EOS, i42) → f432_0_createList_InvokeMethod(EOS, i42)
f432_0_createList_InvokeMethod(EOS, i42) → f435_0__init__Load(EOS, i42)
f435_0__init__Load(EOS, i42) → f442_0__init__InvokeMethod(EOS, i42)
f442_0__init__InvokeMethod(EOS, i42) → f444_0__init__Load(EOS, i42)
f444_0__init__Load(EOS, i42) → f452_0__init__Load(EOS, i42)
f452_0__init__Load(EOS, i42) → f454_0__init__FieldAccess(EOS, i42)
f454_0__init__FieldAccess(EOS, i42) → f459_0__init__Load(EOS, i42)
f459_0__init__Load(EOS, i42) → f463_0__init__Load(EOS, i42)
f463_0__init__Load(EOS, i42) → f467_0__init__FieldAccess(EOS, i42)
f467_0__init__FieldAccess(EOS, i42) → f473_0__init__Return(EOS, i42)
f473_0__init__Return(EOS, i42) → f476_0_createList_Store(EOS, i42)
f476_0_createList_Store(EOS, i42) → f479_0_createList_Inc(EOS, i42)
f479_0_createList_Inc(EOS, i42) → f483_0_createList_JMP(EOS, +(i42, -1)) | >(i42, 0)
f483_0_createList_JMP(EOS, i51) → f491_0_createList_Load(EOS, i51)
f491_0_createList_Load(EOS, i51) → f383_0_createList_Load(EOS, i51)
f383_0_createList_Load(EOS, i39) → f387_0_createList_LE(EOS, i39, i39)

Combined rules. Obtained 1 IRules

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

Filtered ground terms:


f387_0_createList_LE(x1, x2, x3) → f387_0_createList_LE(x2, x3)
Cond_f387_0_createList_LE(x1, x2, x3, x4) → Cond_f387_0_createList_LE(x1, x3, x4)

Filtered duplicate terms:


f387_0_createList_LE(x1, x2) → f387_0_createList_LE(x2)
Cond_f387_0_createList_LE(x1, x2, x3) → Cond_f387_0_createList_LE(x1, x3)

Prepared 1 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(12) Obligation:

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

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f387_0_createList_LE(x2)] = x2

Therefore the following rule(s) have been dropped:


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

(14) YES