Termination proof of /tmp/tmph0WVgL/ListDuplicate.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 220 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 840 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 0 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 70 ms)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇒, 140 ms)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔, 0 ms)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔, 0 ms)

                ↳22 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: ListDuplicate

/**
 * 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 96 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: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 90 rules for P and 0 rules for R.

P rules:
747_0_duplicate_NULL(EOS(STATIC_747), java.lang.Object(o213sub), i58, java.lang.Object(o213sub)) → 749_0_duplicate_NULL(EOS(STATIC_749), java.lang.Object(o213sub), i58, java.lang.Object(o213sub))
749_0_duplicate_NULL(EOS(STATIC_749), java.lang.Object(o213sub), i58, java.lang.Object(o213sub)) → 751_0_duplicate_Load(EOS(STATIC_751), java.lang.Object(o213sub), i58)
751_0_duplicate_Load(EOS(STATIC_751), java.lang.Object(o213sub), i58) → 755_0_duplicate_EQ(EOS(STATIC_755), java.lang.Object(o213sub), i58, i58)
755_0_duplicate_EQ(EOS(STATIC_755), java.lang.Object(o213sub), matching1, matching2) → 758_0_duplicate_EQ(EOS(STATIC_758), java.lang.Object(o213sub), 1, 1) | &&(=(matching1, 1), =(matching2, 1))
755_0_duplicate_EQ(EOS(STATIC_755), java.lang.Object(o213sub), matching1, matching2) → 759_0_duplicate_EQ(EOS(STATIC_759), java.lang.Object(o213sub), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
758_0_duplicate_EQ(EOS(STATIC_758), java.lang.Object(o213sub), matching1, matching2) → 763_0_duplicate_New(EOS(STATIC_763), java.lang.Object(o213sub), 1) | &&(&&(>(1, 0), =(matching1, 1)), =(matching2, 1))
763_0_duplicate_New(EOS(STATIC_763), java.lang.Object(o213sub), matching1) → 769_0_duplicate_Duplicate(EOS(STATIC_769), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
769_0_duplicate_Duplicate(EOS(STATIC_769), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 773_0_duplicate_Load(EOS(STATIC_773), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
773_0_duplicate_Load(EOS(STATIC_773), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL))) → 779_0_duplicate_FieldAccess(EOS(STATIC_779), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) | =(matching1, 1)
779_0_duplicate_FieldAccess(EOS(STATIC_779), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) → 785_0_duplicate_FieldAccess(EOS(STATIC_785), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) | =(matching1, 1)
779_0_duplicate_FieldAccess(EOS(STATIC_779), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) → 786_0_duplicate_FieldAccess(EOS(STATIC_786), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) | =(matching1, 1)
785_0_duplicate_FieldAccess(EOS(STATIC_785), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o227, o228))) → 791_0_duplicate_FieldAccess(EOS(STATIC_791), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
791_0_duplicate_FieldAccess(EOS(STATIC_791), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o227, o228))) → 798_0_duplicate_Load(EOS(STATIC_798), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227) | =(matching1, 1)
798_0_duplicate_Load(EOS(STATIC_798), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227) → 805_0_duplicate_FieldAccess(EOS(STATIC_805), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
805_0_duplicate_FieldAccess(EOS(STATIC_805), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, java.lang.Object(ObjectList(EOC, o227, o228))) → 811_0_duplicate_InvokeMethod(EOS(STATIC_811), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) | =(matching1, 1)
811_0_duplicate_InvokeMethod(EOS(STATIC_811), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) → 816_0_<init>_Load(EOS(STATIC_816), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) | =(matching1, 1)
816_0_<init>_Load(EOS(STATIC_816), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) → 826_0_<init>_InvokeMethod(EOS(STATIC_826), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
826_0_<init>_InvokeMethod(EOS(STATIC_826), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 836_0_<init>_Load(EOS(STATIC_836), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) | =(matching1, 1)
836_0_<init>_Load(EOS(STATIC_836), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) → 839_0_<init>_Load(EOS(STATIC_839), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
839_0_<init>_Load(EOS(STATIC_839), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 843_0_<init>_FieldAccess(EOS(STATIC_843), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227) | =(matching1, 1)
843_0_<init>_FieldAccess(EOS(STATIC_843), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o228, java.lang.Object(ObjectList(EOC, NULL, NULL)), o227) → 846_0_<init>_Load(EOS(STATIC_846), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, NULL)), java.lang.Object(ObjectList(EOC, o227, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, o227, NULL)), o228) | =(matching1, 1)
846_0_<init>_Load(EOS(STATIC_846), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, NULL)), java.lang.Object(ObjectList(EOC, o227, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, o227, NULL)), o228) → 849_0_<init>_Load(EOS(STATIC_849), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, NULL)), java.lang.Object(ObjectList(EOC, o227, NULL)), o227, o228, o228, java.lang.Object(ObjectList(EOC, o227, NULL))) | =(matching1, 1)
849_0_<init>_Load(EOS(STATIC_849), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, NULL)), java.lang.Object(ObjectList(EOC, o227, NULL)), o227, o228, o228, java.lang.Object(ObjectList(EOC, o227, NULL))) → 852_0_<init>_FieldAccess(EOS(STATIC_852), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, NULL)), java.lang.Object(ObjectList(EOC, o227, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, o227, NULL)), o228) | =(matching1, 1)
852_0_<init>_FieldAccess(EOS(STATIC_852), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, NULL)), java.lang.Object(ObjectList(EOC, o227, NULL)), o227, o228, java.lang.Object(ObjectList(EOC, o227, NULL)), o228) → 857_0_<init>_Return(EOS(STATIC_857), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228)), o227, o228) | =(matching1, 1)
857_0_<init>_Return(EOS(STATIC_857), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228)), o227, o228) → 862_0_duplicate_Store(EOS(STATIC_862), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
862_0_duplicate_Store(EOS(STATIC_862), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228))) → 866_0_duplicate_Load(EOS(STATIC_866), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
866_0_duplicate_Load(EOS(STATIC_866), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228))) → 869_0_duplicate_Load(EOS(STATIC_869), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
869_0_duplicate_Load(EOS(STATIC_869), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228))) → 873_0_duplicate_FieldAccess(EOS(STATIC_873), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
873_0_duplicate_FieldAccess(EOS(STATIC_873), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228))) → 879_0_duplicate_Load(EOS(STATIC_879), java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228)))), 1) | =(matching1, 1)
879_0_duplicate_Load(EOS(STATIC_879), java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228)))), matching1) → 885_0_duplicate_FieldAccess(EOS(STATIC_885), 1, java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228))))) | =(matching1, 1)
885_0_duplicate_FieldAccess(EOS(STATIC_885), matching1, java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228))))) → 888_0_duplicate_Store(EOS(STATIC_888), 1, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
888_0_duplicate_Store(EOS(STATIC_888), matching1, java.lang.Object(ObjectList(EOC, o227, o228))) → 892_0_duplicate_Load(EOS(STATIC_892), java.lang.Object(ObjectList(EOC, o227, o228)), 1) | =(matching1, 1)
892_0_duplicate_Load(EOS(STATIC_892), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 894_0_duplicate_NE(EOS(STATIC_894), java.lang.Object(ObjectList(EOC, o227, o228)), 1) | =(matching1, 1)
894_0_duplicate_NE(EOS(STATIC_894), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 898_0_duplicate_ConstantStackPush(EOS(STATIC_898), java.lang.Object(ObjectList(EOC, o227, o228))) | &&(>(1, 0), =(matching1, 1))
898_0_duplicate_ConstantStackPush(EOS(STATIC_898), java.lang.Object(ObjectList(EOC, o227, o228))) → 902_0_duplicate_Store(EOS(STATIC_902), java.lang.Object(ObjectList(EOC, o227, o228)), 0)
902_0_duplicate_Store(EOS(STATIC_902), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 907_0_duplicate_JMP(EOS(STATIC_907), java.lang.Object(ObjectList(EOC, o227, o228)), 0) | =(matching1, 0)
907_0_duplicate_JMP(EOS(STATIC_907), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 911_0_duplicate_Load(EOS(STATIC_911), java.lang.Object(ObjectList(EOC, o227, o228)), 0) | =(matching1, 0)
911_0_duplicate_Load(EOS(STATIC_911), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 742_0_duplicate_Load(EOS(STATIC_742), java.lang.Object(ObjectList(EOC, o227, o228)), 0) | =(matching1, 0)
742_0_duplicate_Load(EOS(STATIC_742), o205, i58) → 747_0_duplicate_NULL(EOS(STATIC_747), o205, i58, o205)
786_0_duplicate_FieldAccess(EOS(STATIC_786), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o230, o231))) → 793_0_duplicate_FieldAccess(EOS(STATIC_793), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
793_0_duplicate_FieldAccess(EOS(STATIC_793), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, o230, o231))) → 800_0_duplicate_Load(EOS(STATIC_800), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230) | =(matching1, 1)
800_0_duplicate_Load(EOS(STATIC_800), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230) → 807_0_duplicate_FieldAccess(EOS(STATIC_807), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
807_0_duplicate_FieldAccess(EOS(STATIC_807), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, java.lang.Object(ObjectList(EOC, o230, o231))) → 812_0_duplicate_InvokeMethod(EOS(STATIC_812), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231) | =(matching1, 1)
812_0_duplicate_InvokeMethod(EOS(STATIC_812), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231) → 817_0_<init>_Load(EOS(STATIC_817), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231) | =(matching1, 1)
817_0_<init>_Load(EOS(STATIC_817), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231) → 828_0_<init>_InvokeMethod(EOS(STATIC_828), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
828_0_<init>_InvokeMethod(EOS(STATIC_828), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 838_0_<init>_Load(EOS(STATIC_838), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231) | =(matching1, 1)
838_0_<init>_Load(EOS(STATIC_838), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231) → 841_0_<init>_Load(EOS(STATIC_841), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
841_0_<init>_Load(EOS(STATIC_841), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 845_0_<init>_FieldAccess(EOS(STATIC_845), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230) | =(matching1, 1)
845_0_<init>_FieldAccess(EOS(STATIC_845), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o231, java.lang.Object(ObjectList(EOC, NULL, NULL)), o230) → 847_0_<init>_Load(EOS(STATIC_847), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, NULL)), java.lang.Object(ObjectList(EOC, o230, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, o230, NULL)), o231) | =(matching1, 1)
847_0_<init>_Load(EOS(STATIC_847), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, NULL)), java.lang.Object(ObjectList(EOC, o230, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, o230, NULL)), o231) → 850_0_<init>_Load(EOS(STATIC_850), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, NULL)), java.lang.Object(ObjectList(EOC, o230, NULL)), o230, o231, o231, java.lang.Object(ObjectList(EOC, o230, NULL))) | =(matching1, 1)
850_0_<init>_Load(EOS(STATIC_850), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, NULL)), java.lang.Object(ObjectList(EOC, o230, NULL)), o230, o231, o231, java.lang.Object(ObjectList(EOC, o230, NULL))) → 854_0_<init>_FieldAccess(EOS(STATIC_854), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, NULL)), java.lang.Object(ObjectList(EOC, o230, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, o230, NULL)), o231) | =(matching1, 1)
854_0_<init>_FieldAccess(EOS(STATIC_854), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, NULL)), java.lang.Object(ObjectList(EOC, o230, NULL)), o230, o231, java.lang.Object(ObjectList(EOC, o230, NULL)), o231) → 860_0_<init>_Return(EOS(STATIC_860), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231)), o230, o231) | =(matching1, 1)
860_0_<init>_Return(EOS(STATIC_860), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231)), o230, o231) → 864_0_duplicate_Store(EOS(STATIC_864), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
864_0_duplicate_Store(EOS(STATIC_864), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231))) → 868_0_duplicate_Load(EOS(STATIC_868), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
868_0_duplicate_Load(EOS(STATIC_868), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231))) → 871_0_duplicate_Load(EOS(STATIC_871), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
871_0_duplicate_Load(EOS(STATIC_871), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231))) → 875_0_duplicate_FieldAccess(EOS(STATIC_875), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
875_0_duplicate_FieldAccess(EOS(STATIC_875), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231))) → 882_0_duplicate_Load(EOS(STATIC_882), java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231)))), 1) | =(matching1, 1)
882_0_duplicate_Load(EOS(STATIC_882), java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231)))), matching1) → 886_0_duplicate_FieldAccess(EOS(STATIC_886), 1, java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231))))) | =(matching1, 1)
886_0_duplicate_FieldAccess(EOS(STATIC_886), matching1, java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231))))) → 890_0_duplicate_Store(EOS(STATIC_890), 1, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
890_0_duplicate_Store(EOS(STATIC_890), matching1, java.lang.Object(ObjectList(EOC, o230, o231))) → 893_0_duplicate_Load(EOS(STATIC_893), java.lang.Object(ObjectList(EOC, o230, o231)), 1) | =(matching1, 1)
893_0_duplicate_Load(EOS(STATIC_893), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 895_0_duplicate_NE(EOS(STATIC_895), java.lang.Object(ObjectList(EOC, o230, o231)), 1) | =(matching1, 1)
895_0_duplicate_NE(EOS(STATIC_895), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 899_0_duplicate_ConstantStackPush(EOS(STATIC_899), java.lang.Object(ObjectList(EOC, o230, o231))) | &&(>(1, 0), =(matching1, 1))
899_0_duplicate_ConstantStackPush(EOS(STATIC_899), java.lang.Object(ObjectList(EOC, o230, o231))) → 904_0_duplicate_Store(EOS(STATIC_904), java.lang.Object(ObjectList(EOC, o230, o231)), 0)
904_0_duplicate_Store(EOS(STATIC_904), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 908_0_duplicate_JMP(EOS(STATIC_908), java.lang.Object(ObjectList(EOC, o230, o231)), 0) | =(matching1, 0)
908_0_duplicate_JMP(EOS(STATIC_908), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 915_0_duplicate_Load(EOS(STATIC_915), java.lang.Object(ObjectList(EOC, o230, o231)), 0) | =(matching1, 0)
915_0_duplicate_Load(EOS(STATIC_915), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 742_0_duplicate_Load(EOS(STATIC_742), java.lang.Object(ObjectList(EOC, o230, o231)), 0) | =(matching1, 0)
759_0_duplicate_EQ(EOS(STATIC_759), java.lang.Object(o213sub), matching1, matching2) → 765_0_duplicate_Load(EOS(STATIC_765), java.lang.Object(o213sub), 0) | &&(=(matching1, 0), =(matching2, 0))
765_0_duplicate_Load(EOS(STATIC_765), java.lang.Object(o213sub), matching1) → 771_0_duplicate_FieldAccess(EOS(STATIC_771), 0, java.lang.Object(o213sub)) | =(matching1, 0)
771_0_duplicate_FieldAccess(EOS(STATIC_771), matching1, java.lang.Object(o213sub)) → 775_0_duplicate_FieldAccess(EOS(STATIC_775), 0, java.lang.Object(o213sub)) | =(matching1, 0)
771_0_duplicate_FieldAccess(EOS(STATIC_771), matching1, java.lang.Object(o213sub)) → 776_0_duplicate_FieldAccess(EOS(STATIC_776), 0, java.lang.Object(o213sub)) | =(matching1, 0)
775_0_duplicate_FieldAccess(EOS(STATIC_775), matching1, java.lang.Object(ObjectList(EOC, o219, o220))) → 781_0_duplicate_FieldAccess(EOS(STATIC_781), 0, java.lang.Object(ObjectList(EOC, o219, o220))) | =(matching1, 0)
781_0_duplicate_FieldAccess(EOS(STATIC_781), matching1, java.lang.Object(ObjectList(EOC, o219, o220))) → 788_0_duplicate_Store(EOS(STATIC_788), 0, o220) | =(matching1, 0)
788_0_duplicate_Store(EOS(STATIC_788), matching1, o220) → 795_0_duplicate_Load(EOS(STATIC_795), o220, 0) | =(matching1, 0)
795_0_duplicate_Load(EOS(STATIC_795), o220, matching1) → 802_0_duplicate_NE(EOS(STATIC_802), o220, 0) | =(matching1, 0)
802_0_duplicate_NE(EOS(STATIC_802), o220, matching1) → 808_0_duplicate_ConstantStackPush(EOS(STATIC_808), o220) | =(matching1, 0)
808_0_duplicate_ConstantStackPush(EOS(STATIC_808), o220) → 814_0_duplicate_JMP(EOS(STATIC_814), o220, 1)
814_0_duplicate_JMP(EOS(STATIC_814), o220, matching1) → 818_0_duplicate_Store(EOS(STATIC_818), o220, 1) | =(matching1, 1)
818_0_duplicate_Store(EOS(STATIC_818), o220, matching1) → 822_0_duplicate_JMP(EOS(STATIC_822), o220, 1) | =(matching1, 1)
822_0_duplicate_JMP(EOS(STATIC_822), o220, matching1) → 831_0_duplicate_Load(EOS(STATIC_831), o220, 1) | =(matching1, 1)
831_0_duplicate_Load(EOS(STATIC_831), o220, matching1) → 742_0_duplicate_Load(EOS(STATIC_742), o220, 1) | =(matching1, 1)
776_0_duplicate_FieldAccess(EOS(STATIC_776), matching1, java.lang.Object(ObjectList(EOC, o222, o223))) → 782_0_duplicate_FieldAccess(EOS(STATIC_782), 0, java.lang.Object(ObjectList(EOC, o222, o223))) | =(matching1, 0)
782_0_duplicate_FieldAccess(EOS(STATIC_782), matching1, java.lang.Object(ObjectList(EOC, o222, o223))) → 789_0_duplicate_Store(EOS(STATIC_789), 0, o223) | =(matching1, 0)
789_0_duplicate_Store(EOS(STATIC_789), matching1, o223) → 796_0_duplicate_Load(EOS(STATIC_796), o223, 0) | =(matching1, 0)
796_0_duplicate_Load(EOS(STATIC_796), o223, matching1) → 803_0_duplicate_NE(EOS(STATIC_803), o223, 0) | =(matching1, 0)
803_0_duplicate_NE(EOS(STATIC_803), o223, matching1) → 809_0_duplicate_ConstantStackPush(EOS(STATIC_809), o223) | =(matching1, 0)
809_0_duplicate_ConstantStackPush(EOS(STATIC_809), o223) → 815_0_duplicate_JMP(EOS(STATIC_815), o223, 1)
815_0_duplicate_JMP(EOS(STATIC_815), o223, matching1) → 820_0_duplicate_Store(EOS(STATIC_820), o223, 1) | =(matching1, 1)
820_0_duplicate_Store(EOS(STATIC_820), o223, matching1) → 824_0_duplicate_JMP(EOS(STATIC_824), o223, 1) | =(matching1, 1)
824_0_duplicate_JMP(EOS(STATIC_824), o223, matching1) → 834_0_duplicate_Load(EOS(STATIC_834), o223, 1) | =(matching1, 1)
834_0_duplicate_Load(EOS(STATIC_834), o223, matching1) → 742_0_duplicate_Load(EOS(STATIC_742), o223, 1) | =(matching1, 1)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
747_0_duplicate_NULL(EOS(STATIC_747), java.lang.Object(ObjectList(EOC, x0, x1)), 1, java.lang.Object(ObjectList(EOC, x0, x1))) → 747_0_duplicate_NULL(EOS(STATIC_747), java.lang.Object(ObjectList(EOC, x0, x1)), 0, java.lang.Object(ObjectList(EOC, x0, x1)))
747_0_duplicate_NULL(EOS(STATIC_747), java.lang.Object(ObjectList(EOC, x0, x1)), 0, java.lang.Object(ObjectList(EOC, x0, x1))) → 747_0_duplicate_NULL(EOS(STATIC_747), x1, 1, x1)
R rules:

Filtered ground terms:

747_0_duplicate_NULL(x1, x2, x3, x4) → 747_0_duplicate_NULL(x2, x3, x4)
EOS(x1) → EOS
ObjectList(x1, x2, x3) → ObjectList(x2, x3)

Filtered duplicate args:

747_0_duplicate_NULL(x1, x2, x3) → 747_0_duplicate_NULL(x2, x3)

Filtered unneeded arguments:

ObjectList(x1, x2) → ObjectList(x2)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
747_0_duplicate_NULL(1, java.lang.Object(ObjectList(x1))) → 747_0_duplicate_NULL(0, java.lang.Object(ObjectList(x1)))
747_0_duplicate_NULL(0, java.lang.Object(ObjectList(x1))) → 747_0_duplicate_NULL(1, x1)
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has no predefined symbols.

P rules:
747_0_DUPLICATE_NULL(1, java.lang.Object(ObjectList(x1))) → 747_0_DUPLICATE_NULL(0, java.lang.Object(ObjectList(x1)))
747_0_DUPLICATE_NULL(0, java.lang.Object(ObjectList(x1))) → 747_0_DUPLICATE_NULL(1, x1)
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): 747_0_DUPLICATE_NULL(1, java.lang.Object(ObjectList(x1[0]))) → 747_0_DUPLICATE_NULL(0, java.lang.Object(ObjectList(x1[0])))
(1): 747_0_DUPLICATE_NULL(0, java.lang.Object(ObjectList(x1[1]))) → 747_0_DUPLICATE_NULL(1, x1[1])

(0) -> (0), if (0 →^* 1∧java.lang.Object(ObjectList(x1[0])) →^* java.lang.Object(ObjectList(x1[0]')))

(0) -> (1), if java.lang.Object(ObjectList(x1[0])) →^* java.lang.Object(ObjectList(x1[1]))

(1) -> (0), if x1[1] →^* java.lang.Object(ObjectList(x1[0]))

(1) -> (1), if (1 →^* 0∧x1[1] →^* java.lang.Object(ObjectList(x1[1]')))

The set Q is empty.

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

747_0_DUPLICATE_NULL(pos(s(01)), java.lang.Object(ObjectList(x1[0]))) → 747_0_DUPLICATE_NULL(pos(01), java.lang.Object(ObjectList(x1[0])))
747_0_DUPLICATE_NULL(pos(01), java.lang.Object(ObjectList(x1[1]))) → 747_0_DUPLICATE_NULL(pos(s(01)), x1[1])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

747_0_DUPLICATE_NULL(pos(01), java.lang.Object(ObjectList(x1[1]))) → 747_0_DUPLICATE_NULL(pos(s(01)), x1[1])
The graph contains the following edges 2 > 2
747_0_DUPLICATE_NULL(pos(s(01)), java.lang.Object(ObjectList(x1[0]))) → 747_0_DUPLICATE_NULL(pos(01), java.lang.Object(ObjectList(x1[0])))
The graph contains the following edges 2 >= 2

(11) YES

(12) 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: UsedFieldsAnalysis

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 23 rules for P and 0 rules for R.

P rules:
358_0_createList_LE(EOS(STATIC_358), i39, i39) → 363_0_createList_LE(EOS(STATIC_363), i39, i39)
363_0_createList_LE(EOS(STATIC_363), i39, i39) → 367_0_createList_New(EOS(STATIC_367), i39) | >(i39, 0)
367_0_createList_New(EOS(STATIC_367), i39) → 370_0_createList_Duplicate(EOS(STATIC_370), i39)
370_0_createList_Duplicate(EOS(STATIC_370), i39) → 374_0_createList_New(EOS(STATIC_374), i39)
374_0_createList_New(EOS(STATIC_374), i39) → 380_0_createList_Duplicate(EOS(STATIC_380), i39)
380_0_createList_Duplicate(EOS(STATIC_380), i39) → 390_0_createList_InvokeMethod(EOS(STATIC_390), i39)
390_0_createList_InvokeMethod(EOS(STATIC_390), i39) → 392_0_createList_Load(EOS(STATIC_392), i39)
392_0_createList_Load(EOS(STATIC_392), i39) → 395_0_createList_InvokeMethod(EOS(STATIC_395), i39)
395_0_createList_InvokeMethod(EOS(STATIC_395), i39) → 399_0_<init>_Load(EOS(STATIC_399), i39)
399_0_<init>_Load(EOS(STATIC_399), i39) → 404_0_<init>_InvokeMethod(EOS(STATIC_404), i39)
404_0_<init>_InvokeMethod(EOS(STATIC_404), i39) → 406_0_<init>_Load(EOS(STATIC_406), i39)
406_0_<init>_Load(EOS(STATIC_406), i39) → 412_0_<init>_Load(EOS(STATIC_412), i39)
412_0_<init>_Load(EOS(STATIC_412), i39) → 415_0_<init>_FieldAccess(EOS(STATIC_415), i39)
415_0_<init>_FieldAccess(EOS(STATIC_415), i39) → 420_0_<init>_Load(EOS(STATIC_420), i39)
420_0_<init>_Load(EOS(STATIC_420), i39) → 422_0_<init>_Load(EOS(STATIC_422), i39)
422_0_<init>_Load(EOS(STATIC_422), i39) → 425_0_<init>_FieldAccess(EOS(STATIC_425), i39)
425_0_<init>_FieldAccess(EOS(STATIC_425), i39) → 431_0_<init>_Return(EOS(STATIC_431), i39)
431_0_<init>_Return(EOS(STATIC_431), i39) → 436_0_createList_Store(EOS(STATIC_436), i39)
436_0_createList_Store(EOS(STATIC_436), i39) → 442_0_createList_Inc(EOS(STATIC_442), i39)
442_0_createList_Inc(EOS(STATIC_442), i39) → 448_0_createList_JMP(EOS(STATIC_448), +(i39, -1)) | >(i39, 0)
448_0_createList_JMP(EOS(STATIC_448), i45) → 458_0_createList_Load(EOS(STATIC_458), i45)
458_0_createList_Load(EOS(STATIC_458), i45) → 353_0_createList_Load(EOS(STATIC_353), i45)
353_0_createList_Load(EOS(STATIC_353), i36) → 358_0_createList_LE(EOS(STATIC_358), i36, i36)
R rules:

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
358_0_createList_LE(EOS(STATIC_358), x0, x0) → 358_0_createList_LE(EOS(STATIC_358), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:

Filtered ground terms:

358_0_createList_LE(x1, x2, x3) → 358_0_createList_LE(x2, x3)
EOS(x1) → EOS
Cond_358_0_createList_LE(x1, x2, x3, x4) → Cond_358_0_createList_LE(x1, x3, x4)

Filtered duplicate args:

358_0_createList_LE(x1, x2) → 358_0_createList_LE(x2)
Cond_358_0_createList_LE(x1, x2, x3) → Cond_358_0_createList_LE(x1, x3)

Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.

P rules:
358_0_createList_LE(x0) → 358_0_createList_LE(+(x0, -1)) | >(x0, 0)
R rules:

Finished conversion. Obtained 2 rules for P and 0 rules for R. System has predefined symbols.

P rules:
358_0_CREATELIST_LE(x0) → COND_358_0_CREATELIST_LE(>(x0, 0), x0)
COND_358_0_CREATELIST_LE(TRUE, x0) → 358_0_CREATELIST_LE(+(x0, -1))
R rules:

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 358_0_CREATELIST_LE(x0[0]) → COND_358_0_CREATELIST_LE(x0[0] > 0, x0[0])
(1): COND_358_0_CREATELIST_LE(TRUE, x0[1]) → 358_0_CREATELIST_LE(x0[1] + -1)

(0) -> (1), if (x0[0] > 0 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] + -1 →^* x0[0])

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@27743073 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 358_0_CREATELIST_LE(x0) → COND_358_0_CREATELIST_LE(>(x0, 0), x0) the following chains were created:

We consider the chain 358_0_CREATELIST_LE(x0[0]) → COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0]), COND_358_0_CREATELIST_LE(TRUE, x0[1]) → 358_0_CREATELIST_LE(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 358_0_CREATELIST_LE(x0[0])≥NonInfC∧358_0_CREATELIST_LE(x0[0])≥COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 358_0_CREATELIST_LE(x0[0])≥NonInfC∧358_0_CREATELIST_LE(x0[0])≥COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])∧(U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_358_0_CREATELIST_LE(TRUE, x0) → 358_0_CREATELIST_LE(+(x0, -1)) the following chains were created:

We consider the chain COND_358_0_CREATELIST_LE(TRUE, x0[1]) → 358_0_CREATELIST_LE(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_358_0_CREATELIST_LE(TRUE, x0[1])≥NonInfC∧COND_358_0_CREATELIST_LE(TRUE, x0[1])≥358_0_CREATELIST_LE(+(x0[1], -1))∧(U^Increasing(358_0_CREATELIST_LE(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(358_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(358_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(358_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(358_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

358_0_CREATELIST_LE(x0) → COND_358_0_CREATELIST_LE(>(x0, 0), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
COND_358_0_CREATELIST_LE(TRUE, x0) → 358_0_CREATELIST_LE(+(x0, -1))
- ((U^Increasing(358_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(358_0_CREATELIST_LE(x₁)) = [2]x₁
POL(COND_358_0_CREATELIST_LE(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

COND_358_0_CREATELIST_LE(TRUE, x0[1]) → 358_0_CREATELIST_LE(+(x0[1], -1))

The following pairs are in P_bound:

358_0_CREATELIST_LE(x0[0]) → COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

358_0_CREATELIST_LE(x0[0]) → COND_358_0_CREATELIST_LE(>(x0[0], 0), x0[0])

There are no usable rules.

(16) Complex Obligation (AND)

(17) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 358_0_CREATELIST_LE(x0[0]) → COND_358_0_CREATELIST_LE(x0[0] > 0, x0[0])

The set Q is empty.

(18) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(19) TRUE

(20) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_358_0_CREATELIST_LE(TRUE, x0[1]) → 358_0_CREATELIST_LE(x0[1] + -1)

The set Q is empty.

(21) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Complex Obligation (AND)

(17) Obligation:

(18) IDependencyGraphProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE