0 JBC
↳1 JBCToGraph (⇒, 240 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 0 ms)
↳4 AND
↳5 JBCTerminationSCC
↳6 SCCToIDPv1Proof (⇒, 810 ms)
↳7 IDP
↳8 IDPtoQDPProof (⇒, 30 ms)
↳9 QDP
↳10 QDPSizeChangeProof (⇔, 0 ms)
↳11 YES
↳12 JBCTerminationSCC
↳13 SCCToIDPv1Proof (⇒, 150 ms)
↳14 IDP
↳15 IDPNonInfProof (⇒, 70 ms)
↳16 AND
↳17 IDP
↳18 IDependencyGraphProof (⇔, 0 ms)
↳19 TRUE
↳20 IDP
↳21 IDependencyGraphProof (⇔, 0 ms)
↳22 TRUE
/**
* 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();
}
}
Generated 90 rules for P and 0 rules for R.
P rules:
746_0_duplicate_NULL(EOS(STATIC_746), java.lang.Object(o213sub), i58, java.lang.Object(o213sub)) → 748_0_duplicate_NULL(EOS(STATIC_748), java.lang.Object(o213sub), i58, java.lang.Object(o213sub))
748_0_duplicate_NULL(EOS(STATIC_748), java.lang.Object(o213sub), i58, java.lang.Object(o213sub)) → 750_0_duplicate_Load(EOS(STATIC_750), java.lang.Object(o213sub), i58)
750_0_duplicate_Load(EOS(STATIC_750), java.lang.Object(o213sub), i58) → 754_0_duplicate_EQ(EOS(STATIC_754), java.lang.Object(o213sub), i58, i58)
754_0_duplicate_EQ(EOS(STATIC_754), java.lang.Object(o213sub), matching1, matching2) → 757_0_duplicate_EQ(EOS(STATIC_757), java.lang.Object(o213sub), 1, 1) | &&(=(matching1, 1), =(matching2, 1))
754_0_duplicate_EQ(EOS(STATIC_754), java.lang.Object(o213sub), matching1, matching2) → 758_0_duplicate_EQ(EOS(STATIC_758), java.lang.Object(o213sub), 0, 0) | &&(=(matching1, 0), =(matching2, 0))
757_0_duplicate_EQ(EOS(STATIC_757), java.lang.Object(o213sub), matching1, matching2) → 762_0_duplicate_New(EOS(STATIC_762), java.lang.Object(o213sub), 1) | &&(&&(>(1, 0), =(matching1, 1)), =(matching2, 1))
762_0_duplicate_New(EOS(STATIC_762), java.lang.Object(o213sub), matching1) → 768_0_duplicate_Duplicate(EOS(STATIC_768), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
768_0_duplicate_Duplicate(EOS(STATIC_768), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 772_0_duplicate_Load(EOS(STATIC_772), java.lang.Object(o213sub), 1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(matching1, 1)
772_0_duplicate_Load(EOS(STATIC_772), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL))) → 777_0_duplicate_FieldAccess(EOS(STATIC_777), 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)
777_0_duplicate_FieldAccess(EOS(STATIC_777), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) → 783_0_duplicate_FieldAccess(EOS(STATIC_783), 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)
777_0_duplicate_FieldAccess(EOS(STATIC_777), java.lang.Object(o213sub), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(o213sub)) → 784_0_duplicate_FieldAccess(EOS(STATIC_784), 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)
783_0_duplicate_FieldAccess(EOS(STATIC_783), 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))) → 789_0_duplicate_FieldAccess(EOS(STATIC_789), 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)
789_0_duplicate_FieldAccess(EOS(STATIC_789), 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))) → 796_0_duplicate_Load(EOS(STATIC_796), 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)
796_0_duplicate_Load(EOS(STATIC_796), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227) → 803_0_duplicate_FieldAccess(EOS(STATIC_803), 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)
803_0_duplicate_FieldAccess(EOS(STATIC_803), 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))) → 810_0_duplicate_InvokeMethod(EOS(STATIC_810), 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)
810_0_duplicate_InvokeMethod(EOS(STATIC_810), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o227, o228) → 815_0_<init>_Load(EOS(STATIC_815), 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)
815_0_<init>_Load(EOS(STATIC_815), 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) → 823_0_<init>_InvokeMethod(EOS(STATIC_823), 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)
823_0_<init>_InvokeMethod(EOS(STATIC_823), 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))) → 833_0_<init>_Load(EOS(STATIC_833), 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)
833_0_<init>_Load(EOS(STATIC_833), 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) → 837_0_<init>_Load(EOS(STATIC_837), 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)
837_0_<init>_Load(EOS(STATIC_837), 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))) → 840_0_<init>_FieldAccess(EOS(STATIC_840), 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)
840_0_<init>_FieldAccess(EOS(STATIC_840), 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) → 845_0_<init>_Load(EOS(STATIC_845), 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)
845_0_<init>_Load(EOS(STATIC_845), 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) → 848_0_<init>_Load(EOS(STATIC_848), 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)
848_0_<init>_Load(EOS(STATIC_848), 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))) → 850_0_<init>_FieldAccess(EOS(STATIC_850), 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)
850_0_<init>_FieldAccess(EOS(STATIC_850), 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) → 854_0_<init>_Return(EOS(STATIC_854), 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)
854_0_<init>_Return(EOS(STATIC_854), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228)), o227, o228) → 859_0_duplicate_Store(EOS(STATIC_859), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
859_0_duplicate_Store(EOS(STATIC_859), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228))) → 863_0_duplicate_Load(EOS(STATIC_863), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
863_0_duplicate_Load(EOS(STATIC_863), 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)), 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)), java.lang.Object(ObjectList(EOC, o227, o228))) → 870_0_duplicate_FieldAccess(EOS(STATIC_870), java.lang.Object(ObjectList(EOC, o227, o228)), 1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
870_0_duplicate_FieldAccess(EOS(STATIC_870), java.lang.Object(ObjectList(EOC, o227, o228)), matching1, java.lang.Object(ObjectList(EOC, o227, o228)), java.lang.Object(ObjectList(EOC, o227, o228))) → 876_0_duplicate_Load(EOS(STATIC_876), java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228)))), 1) | =(matching1, 1)
876_0_duplicate_Load(EOS(STATIC_876), java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228)))), matching1) → 881_0_duplicate_FieldAccess(EOS(STATIC_881), 1, java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228))))) | =(matching1, 1)
881_0_duplicate_FieldAccess(EOS(STATIC_881), matching1, java.lang.Object(ObjectList(EOC, o227, java.lang.Object(ObjectList(EOC, o227, o228))))) → 886_0_duplicate_Store(EOS(STATIC_886), 1, java.lang.Object(ObjectList(EOC, o227, o228))) | =(matching1, 1)
886_0_duplicate_Store(EOS(STATIC_886), matching1, java.lang.Object(ObjectList(EOC, o227, o228))) → 890_0_duplicate_Load(EOS(STATIC_890), java.lang.Object(ObjectList(EOC, o227, o228)), 1) | =(matching1, 1)
890_0_duplicate_Load(EOS(STATIC_890), 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) → 896_0_duplicate_ConstantStackPush(EOS(STATIC_896), java.lang.Object(ObjectList(EOC, o227, o228))) | &&(>(1, 0), =(matching1, 1))
896_0_duplicate_ConstantStackPush(EOS(STATIC_896), java.lang.Object(ObjectList(EOC, o227, o228))) → 899_0_duplicate_Store(EOS(STATIC_899), java.lang.Object(ObjectList(EOC, o227, o228)), 0)
899_0_duplicate_Store(EOS(STATIC_899), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 903_0_duplicate_JMP(EOS(STATIC_903), java.lang.Object(ObjectList(EOC, o227, o228)), 0) | =(matching1, 0)
903_0_duplicate_JMP(EOS(STATIC_903), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 909_0_duplicate_Load(EOS(STATIC_909), java.lang.Object(ObjectList(EOC, o227, o228)), 0) | =(matching1, 0)
909_0_duplicate_Load(EOS(STATIC_909), java.lang.Object(ObjectList(EOC, o227, o228)), matching1) → 741_0_duplicate_Load(EOS(STATIC_741), java.lang.Object(ObjectList(EOC, o227, o228)), 0) | =(matching1, 0)
741_0_duplicate_Load(EOS(STATIC_741), o205, i58) → 746_0_duplicate_NULL(EOS(STATIC_746), o205, i58, o205)
784_0_duplicate_FieldAccess(EOS(STATIC_784), 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))) → 791_0_duplicate_FieldAccess(EOS(STATIC_791), 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)
791_0_duplicate_FieldAccess(EOS(STATIC_791), 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))) → 798_0_duplicate_Load(EOS(STATIC_798), 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)
798_0_duplicate_Load(EOS(STATIC_798), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, NULL, NULL)), java.lang.Object(ObjectList(EOC, NULL, NULL)), o230) → 804_0_duplicate_FieldAccess(EOS(STATIC_804), 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)
804_0_duplicate_FieldAccess(EOS(STATIC_804), 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))) → 811_0_duplicate_InvokeMethod(EOS(STATIC_811), 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)
811_0_duplicate_InvokeMethod(EOS(STATIC_811), 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) → 825_0_<init>_InvokeMethod(EOS(STATIC_825), 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)
825_0_<init>_InvokeMethod(EOS(STATIC_825), 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))) → 834_0_<init>_Load(EOS(STATIC_834), 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)
834_0_<init>_Load(EOS(STATIC_834), 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) → 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, java.lang.Object(ObjectList(EOC, NULL, NULL))) | =(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, java.lang.Object(ObjectList(EOC, NULL, NULL))) → 842_0_<init>_FieldAccess(EOS(STATIC_842), 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)
842_0_<init>_FieldAccess(EOS(STATIC_842), 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) → 849_0_<init>_Load(EOS(STATIC_849), 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)
849_0_<init>_Load(EOS(STATIC_849), 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))) → 851_0_<init>_FieldAccess(EOS(STATIC_851), 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)
851_0_<init>_FieldAccess(EOS(STATIC_851), 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) → 857_0_<init>_Return(EOS(STATIC_857), 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)
857_0_<init>_Return(EOS(STATIC_857), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231)), o230, o231) → 861_0_duplicate_Store(EOS(STATIC_861), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
861_0_duplicate_Store(EOS(STATIC_861), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231))) → 864_0_duplicate_Load(EOS(STATIC_864), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
864_0_duplicate_Load(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)), 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)), java.lang.Object(ObjectList(EOC, o230, o231))) → 872_0_duplicate_FieldAccess(EOS(STATIC_872), java.lang.Object(ObjectList(EOC, o230, o231)), 1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
872_0_duplicate_FieldAccess(EOS(STATIC_872), java.lang.Object(ObjectList(EOC, o230, o231)), matching1, java.lang.Object(ObjectList(EOC, o230, o231)), java.lang.Object(ObjectList(EOC, o230, o231))) → 879_0_duplicate_Load(EOS(STATIC_879), java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231)))), 1) | =(matching1, 1)
879_0_duplicate_Load(EOS(STATIC_879), java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231)))), matching1) → 883_0_duplicate_FieldAccess(EOS(STATIC_883), 1, java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231))))) | =(matching1, 1)
883_0_duplicate_FieldAccess(EOS(STATIC_883), matching1, java.lang.Object(ObjectList(EOC, o230, java.lang.Object(ObjectList(EOC, o230, o231))))) → 888_0_duplicate_Store(EOS(STATIC_888), 1, java.lang.Object(ObjectList(EOC, o230, o231))) | =(matching1, 1)
888_0_duplicate_Store(EOS(STATIC_888), matching1, java.lang.Object(ObjectList(EOC, o230, o231))) → 891_0_duplicate_Load(EOS(STATIC_891), java.lang.Object(ObjectList(EOC, o230, o231)), 1) | =(matching1, 1)
891_0_duplicate_Load(EOS(STATIC_891), 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) → 897_0_duplicate_ConstantStackPush(EOS(STATIC_897), java.lang.Object(ObjectList(EOC, o230, o231))) | &&(>(1, 0), =(matching1, 1))
897_0_duplicate_ConstantStackPush(EOS(STATIC_897), java.lang.Object(ObjectList(EOC, o230, o231))) → 901_0_duplicate_Store(EOS(STATIC_901), java.lang.Object(ObjectList(EOC, o230, o231)), 0)
901_0_duplicate_Store(EOS(STATIC_901), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 905_0_duplicate_JMP(EOS(STATIC_905), java.lang.Object(ObjectList(EOC, o230, o231)), 0) | =(matching1, 0)
905_0_duplicate_JMP(EOS(STATIC_905), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 912_0_duplicate_Load(EOS(STATIC_912), java.lang.Object(ObjectList(EOC, o230, o231)), 0) | =(matching1, 0)
912_0_duplicate_Load(EOS(STATIC_912), java.lang.Object(ObjectList(EOC, o230, o231)), matching1) → 741_0_duplicate_Load(EOS(STATIC_741), java.lang.Object(ObjectList(EOC, o230, o231)), 0) | =(matching1, 0)
758_0_duplicate_EQ(EOS(STATIC_758), java.lang.Object(o213sub), matching1, matching2) → 764_0_duplicate_Load(EOS(STATIC_764), java.lang.Object(o213sub), 0) | &&(=(matching1, 0), =(matching2, 0))
764_0_duplicate_Load(EOS(STATIC_764), java.lang.Object(o213sub), matching1) → 770_0_duplicate_FieldAccess(EOS(STATIC_770), 0, java.lang.Object(o213sub)) | =(matching1, 0)
770_0_duplicate_FieldAccess(EOS(STATIC_770), matching1, java.lang.Object(o213sub)) → 774_0_duplicate_FieldAccess(EOS(STATIC_774), 0, java.lang.Object(o213sub)) | =(matching1, 0)
770_0_duplicate_FieldAccess(EOS(STATIC_770), matching1, java.lang.Object(o213sub)) → 775_0_duplicate_FieldAccess(EOS(STATIC_775), 0, java.lang.Object(o213sub)) | =(matching1, 0)
774_0_duplicate_FieldAccess(EOS(STATIC_774), matching1, java.lang.Object(ObjectList(EOC, o219, o220))) → 779_0_duplicate_FieldAccess(EOS(STATIC_779), 0, java.lang.Object(ObjectList(EOC, o219, o220))) | =(matching1, 0)
779_0_duplicate_FieldAccess(EOS(STATIC_779), matching1, java.lang.Object(ObjectList(EOC, o219, o220))) → 786_0_duplicate_Store(EOS(STATIC_786), 0, o220) | =(matching1, 0)
786_0_duplicate_Store(EOS(STATIC_786), matching1, o220) → 793_0_duplicate_Load(EOS(STATIC_793), o220, 0) | =(matching1, 0)
793_0_duplicate_Load(EOS(STATIC_793), o220, matching1) → 799_0_duplicate_NE(EOS(STATIC_799), o220, 0) | =(matching1, 0)
799_0_duplicate_NE(EOS(STATIC_799), o220, matching1) → 806_0_duplicate_ConstantStackPush(EOS(STATIC_806), o220) | =(matching1, 0)
806_0_duplicate_ConstantStackPush(EOS(STATIC_806), o220) → 812_0_duplicate_JMP(EOS(STATIC_812), o220, 1)
812_0_duplicate_JMP(EOS(STATIC_812), o220, matching1) → 818_0_duplicate_Store(EOS(STATIC_818), o220, 1) | =(matching1, 1)
818_0_duplicate_Store(EOS(STATIC_818), o220, matching1) → 820_0_duplicate_JMP(EOS(STATIC_820), o220, 1) | =(matching1, 1)
820_0_duplicate_JMP(EOS(STATIC_820), o220, matching1) → 828_0_duplicate_Load(EOS(STATIC_828), o220, 1) | =(matching1, 1)
828_0_duplicate_Load(EOS(STATIC_828), o220, matching1) → 741_0_duplicate_Load(EOS(STATIC_741), o220, 1) | =(matching1, 1)
775_0_duplicate_FieldAccess(EOS(STATIC_775), matching1, java.lang.Object(ObjectList(EOC, o222, o223))) → 781_0_duplicate_FieldAccess(EOS(STATIC_781), 0, java.lang.Object(ObjectList(EOC, o222, o223))) | =(matching1, 0)
781_0_duplicate_FieldAccess(EOS(STATIC_781), matching1, java.lang.Object(ObjectList(EOC, o222, o223))) → 787_0_duplicate_Store(EOS(STATIC_787), 0, o223) | =(matching1, 0)
787_0_duplicate_Store(EOS(STATIC_787), matching1, o223) → 794_0_duplicate_Load(EOS(STATIC_794), o223, 0) | =(matching1, 0)
794_0_duplicate_Load(EOS(STATIC_794), o223, matching1) → 801_0_duplicate_NE(EOS(STATIC_801), o223, 0) | =(matching1, 0)
801_0_duplicate_NE(EOS(STATIC_801), o223, matching1) → 808_0_duplicate_ConstantStackPush(EOS(STATIC_808), o223) | =(matching1, 0)
808_0_duplicate_ConstantStackPush(EOS(STATIC_808), o223) → 813_0_duplicate_JMP(EOS(STATIC_813), o223, 1)
813_0_duplicate_JMP(EOS(STATIC_813), o223, matching1) → 819_0_duplicate_Store(EOS(STATIC_819), o223, 1) | =(matching1, 1)
819_0_duplicate_Store(EOS(STATIC_819), o223, matching1) → 821_0_duplicate_JMP(EOS(STATIC_821), o223, 1) | =(matching1, 1)
821_0_duplicate_JMP(EOS(STATIC_821), o223, matching1) → 831_0_duplicate_Load(EOS(STATIC_831), o223, 1) | =(matching1, 1)
831_0_duplicate_Load(EOS(STATIC_831), o223, matching1) → 741_0_duplicate_Load(EOS(STATIC_741), o223, 1) | =(matching1, 1)
R rules:
Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.
P rules:
746_0_duplicate_NULL(EOS(STATIC_746), java.lang.Object(ObjectList(EOC, x0, x1)), 1, java.lang.Object(ObjectList(EOC, x0, x1))) → 746_0_duplicate_NULL(EOS(STATIC_746), java.lang.Object(ObjectList(EOC, x0, x1)), 0, java.lang.Object(ObjectList(EOC, x0, x1)))
746_0_duplicate_NULL(EOS(STATIC_746), java.lang.Object(ObjectList(EOC, x0, x1)), 0, java.lang.Object(ObjectList(EOC, x0, x1))) → 746_0_duplicate_NULL(EOS(STATIC_746), x1, 1, x1)
R rules:
Filtered ground terms:
746_0_duplicate_NULL(x1, x2, x3, x4) → 746_0_duplicate_NULL(x2, x3, x4)
EOS(x1) → EOS
ObjectList(x1, x2, x3) → ObjectList(x2, x3)
Filtered duplicate args:
746_0_duplicate_NULL(x1, x2, x3) → 746_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:
746_0_duplicate_NULL(1, java.lang.Object(ObjectList(x1))) → 746_0_duplicate_NULL(0, java.lang.Object(ObjectList(x1)))
746_0_duplicate_NULL(0, java.lang.Object(ObjectList(x1))) → 746_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:
746_0_DUPLICATE_NULL(1, java.lang.Object(ObjectList(x1))) → 746_0_DUPLICATE_NULL(0, java.lang.Object(ObjectList(x1)))
746_0_DUPLICATE_NULL(0, java.lang.Object(ObjectList(x1))) → 746_0_DUPLICATE_NULL(1, x1)
R rules:
!= | ~ | 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 |
(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]')))
746_0_DUPLICATE_NULL(pos(s(01)), java.lang.Object(ObjectList(x1[0]))) → 746_0_DUPLICATE_NULL(pos(01), java.lang.Object(ObjectList(x1[0])))
746_0_DUPLICATE_NULL(pos(01), java.lang.Object(ObjectList(x1[1]))) → 746_0_DUPLICATE_NULL(pos(s(01)), x1[1])
From the DPs we obtained the following set of size-change graphs:
Generated 23 rules for P and 0 rules for R.
P rules:
357_0_createList_LE(EOS(STATIC_357), i39, i39) → 362_0_createList_LE(EOS(STATIC_362), i39, i39)
362_0_createList_LE(EOS(STATIC_362), i39, i39) → 366_0_createList_New(EOS(STATIC_366), i39) | >(i39, 0)
366_0_createList_New(EOS(STATIC_366), 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) → 426_0_<init>_FieldAccess(EOS(STATIC_426), i39)
426_0_<init>_FieldAccess(EOS(STATIC_426), i39) → 432_0_<init>_Return(EOS(STATIC_432), i39)
432_0_<init>_Return(EOS(STATIC_432), i39) → 437_0_createList_Store(EOS(STATIC_437), i39)
437_0_createList_Store(EOS(STATIC_437), i39) → 443_0_createList_Inc(EOS(STATIC_443), i39)
443_0_createList_Inc(EOS(STATIC_443), i39) → 449_0_createList_JMP(EOS(STATIC_449), +(i39, -1)) | >(i39, 0)
449_0_createList_JMP(EOS(STATIC_449), i45) → 459_0_createList_Load(EOS(STATIC_459), i45)
459_0_createList_Load(EOS(STATIC_459), i45) → 353_0_createList_Load(EOS(STATIC_353), i45)
353_0_createList_Load(EOS(STATIC_353), i36) → 357_0_createList_LE(EOS(STATIC_357), i36, i36)
R rules:
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
357_0_createList_LE(EOS(STATIC_357), x0, x0) → 357_0_createList_LE(EOS(STATIC_357), +(x0, -1), +(x0, -1)) | >(x0, 0)
R rules:
Filtered ground terms:
357_0_createList_LE(x1, x2, x3) → 357_0_createList_LE(x2, x3)
EOS(x1) → EOS
Cond_357_0_createList_LE(x1, x2, x3, x4) → Cond_357_0_createList_LE(x1, x3, x4)
Filtered duplicate args:
357_0_createList_LE(x1, x2) → 357_0_createList_LE(x2)
Cond_357_0_createList_LE(x1, x2, x3) → Cond_357_0_createList_LE(x1, x3)
Combined rules. Obtained 1 conditional rules for P and 0 conditional rules for R.
P rules:
357_0_createList_LE(x0) → 357_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:
357_0_CREATELIST_LE(x0) → COND_357_0_CREATELIST_LE(>(x0, 0), x0)
COND_357_0_CREATELIST_LE(TRUE, x0) → 357_0_CREATELIST_LE(+(x0, -1))
R rules:
!= | ~ | 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 |
Integer
(0) -> (1), if (x0[0] > 0 ∧x0[0] →* x0[1])
(1) -> (0), if (x0[1] + -1 →* x0[0])
(1) (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 357_0_CREATELIST_LE(x0[0])≥NonInfC∧357_0_CREATELIST_LE(x0[0])≥COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥))
(2) (>(x0[0], 0)=TRUE ⇒ 357_0_CREATELIST_LE(x0[0])≥NonInfC∧357_0_CREATELIST_LE(x0[0])≥COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])∧(UIncreasing(COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥))
(3) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(4) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(5) (x0[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
(6) (x0[0] ≥ 0 ⇒ (UIncreasing(COND_357_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)
(7) (COND_357_0_CREATELIST_LE(TRUE, x0[1])≥NonInfC∧COND_357_0_CREATELIST_LE(TRUE, x0[1])≥357_0_CREATELIST_LE(+(x0[1], -1))∧(UIncreasing(357_0_CREATELIST_LE(+(x0[1], -1))), ≥))
(8) ((UIncreasing(357_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(9) ((UIncreasing(357_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(10) ((UIncreasing(357_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)
(11) ((UIncreasing(357_0_CREATELIST_LE(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)
POL(TRUE) = 0
POL(FALSE) = 0
POL(357_0_CREATELIST_LE(x1)) = [2]x1
POL(COND_357_0_CREATELIST_LE(x1, x2)) = [2]x2
POL(>(x1, x2)) = [-1]
POL(0) = 0
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
COND_357_0_CREATELIST_LE(TRUE, x0[1]) → 357_0_CREATELIST_LE(+(x0[1], -1))
357_0_CREATELIST_LE(x0[0]) → COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])
357_0_CREATELIST_LE(x0[0]) → COND_357_0_CREATELIST_LE(>(x0[0], 0), x0[0])
!= | ~ | 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 |
Integer
!= | ~ | 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 |
Integer