(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_22 (Sun Microsystems Inc.) Main-Class: IntListDupRec/IntListDupRec
package IntListDupRec;

public class IntListDupRec {
public static void main(String[] args) {
Random.args = args;
List l = List.createList(Random.random());

l.dupList();
}
}

class List {
boolean dupped;
List next;

public List(boolean d, List n) {
this.dupped = d;
this.next = n;
}

public void dupList() {
if (this.next == null) {
new List(false, this);
} else if (this.dupped == false) {
List next = this.next;
this.next = new List(true, next);
}
this.next.dupList();
this.dupped = false;
}

public static List createList(int l) {
if (l < 0) {
return null;
} else {
return new List(false, createList(l - 1));
}
}
}

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:
IntListDupRec.IntListDupRec.main([Ljava/lang/String;)V: Graph of 115 nodes with 0 SCCs.

IntListDupRec.List.createList(I)LIntListDupRec/List;: Graph of 44 nodes with 0 SCCs.

IntListDupRec.List.dupList()V: Graph of 94 nodes with 0 SCCs.


(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: IntListDupRec.List.dupList()V
SCC calls the following helper methods: IntListDupRec.List.dupList()V
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 40 rules for P and 55 rules for R.


P rules:
677_0_dupList_FieldAccess(EOS(STATIC_677), java.lang.Object(IntListDupRec.List(EOC, o161, i93)), java.lang.Object(IntListDupRec.List(EOC, o161, i93))) → 679_0_dupList_FieldAccess(EOS(STATIC_679), java.lang.Object(IntListDupRec.List(EOC, o161, i93)), java.lang.Object(IntListDupRec.List(EOC, o161, i93)))
679_0_dupList_FieldAccess(EOS(STATIC_679), java.lang.Object(IntListDupRec.List(EOC, o161, i93)), java.lang.Object(IntListDupRec.List(EOC, o161, i93))) → 682_0_dupList_NONNULL(EOS(STATIC_682), java.lang.Object(IntListDupRec.List(EOC, o161, i93)), o161)
682_0_dupList_NONNULL(EOS(STATIC_682), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)), java.lang.Object(o163sub)) → 684_0_dupList_NONNULL(EOS(STATIC_684), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)), java.lang.Object(o163sub))
684_0_dupList_NONNULL(EOS(STATIC_684), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)), java.lang.Object(o163sub)) → 687_0_dupList_Load(EOS(STATIC_687), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)))
687_0_dupList_Load(EOS(STATIC_687), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93))) → 689_0_dupList_FieldAccess(EOS(STATIC_689), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)))
689_0_dupList_FieldAccess(EOS(STATIC_689), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93))) → 692_0_dupList_NE(EOS(STATIC_692), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i93)), i93)
692_0_dupList_NE(EOS(STATIC_692), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), i95) → 696_0_dupList_NE(EOS(STATIC_696), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), i95)
692_0_dupList_NE(EOS(STATIC_692), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2) → 697_0_dupList_NE(EOS(STATIC_697), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), 0) | &&(=(matching1, 0), =(matching2, 0))
696_0_dupList_NE(EOS(STATIC_696), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), i95) → 701_0_dupList_Load(EOS(STATIC_701), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95))) | !(=(i95, 0))
701_0_dupList_Load(EOS(STATIC_701), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95))) → 706_0_dupList_FieldAccess(EOS(STATIC_706), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)))
706_0_dupList_FieldAccess(EOS(STATIC_706), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95))) → 711_0_dupList_InvokeMethod(EOS(STATIC_711), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub))
711_0_dupList_InvokeMethod(EOS(STATIC_711), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub)) → 714_1_dupList_InvokeMethod(714_0_dupList_Load(EOS(STATIC_714), java.lang.Object(o163sub)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub))
714_0_dupList_Load(EOS(STATIC_714), java.lang.Object(o163sub)) → 718_0_dupList_Load(EOS(STATIC_718), java.lang.Object(o163sub))
718_0_dupList_Load(EOS(STATIC_718), java.lang.Object(o163sub)) → 675_0_dupList_Load(EOS(STATIC_675), java.lang.Object(o163sub))
675_0_dupList_Load(EOS(STATIC_675), java.lang.Object(o156sub)) → 677_0_dupList_FieldAccess(EOS(STATIC_677), java.lang.Object(o156sub), java.lang.Object(o156sub))
697_0_dupList_NE(EOS(STATIC_697), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2) → 702_0_dupList_Load(EOS(STATIC_702), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0))) | &&(=(matching1, 0), =(matching2, 0))
702_0_dupList_Load(EOS(STATIC_702), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1))) → 707_0_dupList_FieldAccess(EOS(STATIC_707), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0))) | =(matching1, 0)
707_0_dupList_FieldAccess(EOS(STATIC_707), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2))) → 713_0_dupList_Store(EOS(STATIC_713), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub)) | &&(=(matching1, 0), =(matching2, 0))
713_0_dupList_Store(EOS(STATIC_713), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub)) → 715_0_dupList_Load(EOS(STATIC_715), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub)) | =(matching1, 0)
715_0_dupList_Load(EOS(STATIC_715), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub)) → 720_0_dupList_New(EOS(STATIC_720), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0))) | =(matching1, 0)
720_0_dupList_New(EOS(STATIC_720), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2))) → 724_0_dupList_Duplicate(EOS(STATIC_724), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(=(matching1, 0), =(matching2, 0))
724_0_dupList_Duplicate(EOS(STATIC_724), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3))) → 728_0_dupList_ConstantStackPush(EOS(STATIC_728), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
728_0_dupList_ConstantStackPush(EOS(STATIC_728), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4))) → 731_0_dupList_Load(EOS(STATIC_731), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
731_0_dupList_Load(EOS(STATIC_731), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5) → 735_0_dupList_InvokeMethod(EOS(STATIC_735), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub)) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1))
735_0_dupList_InvokeMethod(EOS(STATIC_735), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub)) → 738_0_<init>_Load(EOS(STATIC_738), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub)) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1))
738_0_<init>_Load(EOS(STATIC_738), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), matching7, java.lang.Object(o163sub)) → 746_0_<init>_InvokeMethod(EOS(STATIC_746), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1)), =(matching6, 0)), =(matching7, 1))
746_0_<init>_InvokeMethod(EOS(STATIC_746), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), matching7, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching8))) → 749_0_<init>_Load(EOS(STATIC_749), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub)) | &&(&&(&&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1)), =(matching6, 0)), =(matching7, 1)), =(matching8, 0))
749_0_<init>_Load(EOS(STATIC_749), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), matching7, java.lang.Object(o163sub)) → 753_0_<init>_Load(EOS(STATIC_753), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1)), =(matching6, 0)), =(matching7, 1))
753_0_<init>_Load(EOS(STATIC_753), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), matching7, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching8))) → 757_0_<init>_FieldAccess(EOS(STATIC_757), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 1) | &&(&&(&&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1)), =(matching6, 0)), =(matching7, 1)), =(matching8, 0))
757_0_<init>_FieldAccess(EOS(STATIC_757), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching7)), matching8) → 762_0_<init>_Load(EOS(STATIC_762), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), java.lang.Object(o163sub)) | &&(&&(&&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 1)), =(matching6, 0)), =(matching7, 0)), =(matching8, 1))
762_0_<init>_Load(EOS(STATIC_762), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), java.lang.Object(o163sub)) → 767_0_<init>_Load(EOS(STATIC_767), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), 1, java.lang.Object(o163sub), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 1))) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 1)), =(matching5, 1)), =(matching6, 1))
767_0_<init>_Load(EOS(STATIC_767), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6))) → 770_0_<init>_FieldAccess(EOS(STATIC_770), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), 1, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, 1)), java.lang.Object(o163sub)) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 1)), =(matching5, 1)), =(matching6, 1))
770_0_<init>_FieldAccess(EOS(STATIC_770), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(o163sub), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6)), java.lang.Object(o163sub)) → 776_0_<init>_Return(EOS(STATIC_776), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 1, java.lang.Object(o163sub)) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 1)), =(matching5, 1)), =(matching6, 1))
776_0_<init>_Return(EOS(STATIC_776), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching3)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching4)), matching5, java.lang.Object(o163sub)) → 778_0_dupList_FieldAccess(EOS(STATIC_778), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1)), =(matching4, 1)), =(matching5, 1))
778_0_dupList_FieldAccess(EOS(STATIC_778), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching3))) → 784_0_dupList_Load(EOS(STATIC_784), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
784_0_dupList_Load(EOS(STATIC_784), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2))) → 788_0_dupList_FieldAccess(EOS(STATIC_788), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 0))) | &&(=(matching1, 1), =(matching2, 0))
788_0_dupList_FieldAccess(EOS(STATIC_788), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching3)), matching4))) → 791_0_dupList_InvokeMethod(EOS(STATIC_791), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1)), =(matching4, 0))
791_0_dupList_InvokeMethod(EOS(STATIC_791), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching3))) → 794_1_dupList_InvokeMethod(794_0_dupList_Load(EOS(STATIC_794), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
794_0_dupList_Load(EOS(STATIC_794), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1))) → 798_0_dupList_Load(EOS(STATIC_798), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | =(matching1, 1)
798_0_dupList_Load(EOS(STATIC_798), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1))) → 675_0_dupList_Load(EOS(STATIC_675), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | =(matching1, 1)
R rules:
682_0_dupList_NONNULL(EOS(STATIC_682), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL) → 685_0_dupList_NONNULL(EOS(STATIC_685), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL)
685_0_dupList_NONNULL(EOS(STATIC_685), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL) → 688_0_dupList_New(EOS(STATIC_688), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)))
688_0_dupList_New(EOS(STATIC_688), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 690_0_dupList_Duplicate(EOS(STATIC_690), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)))
690_0_dupList_Duplicate(EOS(STATIC_690), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1))) → 694_0_dupList_ConstantStackPush(EOS(STATIC_694), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | =(matching1, 0)
694_0_dupList_ConstantStackPush(EOS(STATIC_694), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2))) → 699_0_dupList_Load(EOS(STATIC_699), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0) | &&(=(matching1, 0), =(matching2, 0))
699_0_dupList_Load(EOS(STATIC_699), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3) → 704_0_dupList_InvokeMethod(EOS(STATIC_704), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
704_0_dupList_InvokeMethod(EOS(STATIC_704), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 709_0_<init>_Load(EOS(STATIC_709), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
709_0_<init>_Load(EOS(STATIC_709), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 716_0_<init>_InvokeMethod(EOS(STATIC_716), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(EOS(STATIC_832), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), NULL), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), i95)), java.lang.Object(IntListDupRec.List(EOC, NULL, i105))) → 847_0_dupList_InvokeMethod(EOS(STATIC_847), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), i95)), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), NULL)
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), java.lang.Object(IntListDupRec.List(EOC, o303, i140))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub)) → 1063_0_dupList_InvokeMethod(EOS(STATIC_1063), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub)) → 1151_0_dupList_InvokeMethod(EOS(STATIC_1151), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0))) | =(matching1, 0)
716_0_<init>_InvokeMethod(EOS(STATIC_716), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6))) → 722_0_<init>_Load(EOS(STATIC_722), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0)), =(matching6, 0))
722_0_<init>_Load(EOS(STATIC_722), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 726_0_<init>_Load(EOS(STATIC_726), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
726_0_<init>_Load(EOS(STATIC_726), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6))) → 729_0_<init>_FieldAccess(EOS(STATIC_729), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0)), =(matching6, 0))
729_0_<init>_FieldAccess(EOS(STATIC_729), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching5)), matching6) → 733_0_<init>_Load(EOS(STATIC_733), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0)), =(matching6, 0))
733_0_<init>_Load(EOS(STATIC_733), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 736_0_<init>_Load(EOS(STATIC_736), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
736_0_<init>_Load(EOS(STATIC_736), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4))) → 740_0_<init>_FieldAccess(EOS(STATIC_740), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
740_0_<init>_FieldAccess(EOS(STATIC_740), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 744_0_<init>_Return(EOS(STATIC_744), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
744_0_<init>_Return(EOS(STATIC_744), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 747_0_dupList_StackPop(EOS(STATIC_747), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
747_0_dupList_StackPop(EOS(STATIC_747), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), matching1))) → 751_0_dupList_JMP(EOS(STATIC_751), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) | =(matching1, 0)
751_0_dupList_JMP(EOS(STATIC_751), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 755_0_dupList_Load(EOS(STATIC_755), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)))
755_0_dupList_Load(EOS(STATIC_755), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 759_0_dupList_FieldAccess(EOS(STATIC_759), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)))
759_0_dupList_FieldAccess(EOS(STATIC_759), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), java.lang.Object(IntListDupRec.List(EOC, NULL, i93))) → 765_0_dupList_InvokeMethod(EOS(STATIC_765), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL)
765_0_dupList_InvokeMethod(EOS(STATIC_765), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL) → 768_0_dupList_InvokeMethod(EOS(STATIC_768), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL)
768_0_dupList_InvokeMethod(EOS(STATIC_768), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL) → 772_0_<init>_Load(EOS(STATIC_772), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
772_0_<init>_Load(EOS(STATIC_772), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 780_0_<init>_InvokeMethod(EOS(STATIC_780), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
780_0_<init>_InvokeMethod(EOS(STATIC_780), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 786_0_<init>_Load(EOS(STATIC_786), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
786_0_<init>_Load(EOS(STATIC_786), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 792_0_<init>_InvokeMethod(EOS(STATIC_792), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
792_0_<init>_InvokeMethod(EOS(STATIC_792), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 796_0_<init>_Load(EOS(STATIC_796), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(IntListDupRec.List(EOC, o303, i140))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching3))) → 1083_0_dupList_InvokeMethod(EOS(STATIC_1083), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(IntListDupRec.List(EOC, o303, i140))) | &&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2)), matching3)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching4))) → 1159_0_dupList_InvokeMethod(EOS(STATIC_1159), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171))) | &&(&&(&&(=(matching1, 0), =(matching2, 1)), =(matching3, 0)), =(matching4, 1))
796_0_<init>_Load(EOS(STATIC_796), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 800_0_<init>_InvokeMethod(EOS(STATIC_800), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
800_0_<init>_InvokeMethod(EOS(STATIC_800), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 804_0_<init>_Load(EOS(STATIC_804), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
804_0_<init>_Load(EOS(STATIC_804), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 806_0_<init>_InvokeMethod(EOS(STATIC_806), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
806_0_<init>_InvokeMethod(EOS(STATIC_806), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 808_0_<init>_Load(EOS(STATIC_808), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
808_0_<init>_Load(EOS(STATIC_808), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 810_0_<init>_Load(EOS(STATIC_810), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
810_0_<init>_Load(EOS(STATIC_810), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 812_0_<init>_FieldAccess(EOS(STATIC_812), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
812_0_<init>_FieldAccess(EOS(STATIC_812), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 817_0_<init>_Load(EOS(STATIC_817), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
817_0_<init>_Load(EOS(STATIC_817), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 819_0_<init>_InvokeMethod(EOS(STATIC_819), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
819_0_<init>_InvokeMethod(EOS(STATIC_819), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 822_0_<init>_StackPop(EOS(STATIC_822), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
822_0_<init>_StackPop(EOS(STATIC_822), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 824_0_<init>_Return(EOS(STATIC_824), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
824_0_<init>_Return(EOS(STATIC_824), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 826_0_<init>_Return(EOS(STATIC_826), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
826_0_<init>_Return(EOS(STATIC_826), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 827_0_<init>_Return(EOS(STATIC_827), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
827_0_<init>_Return(EOS(STATIC_827), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 829_0_<init>_Return(EOS(STATIC_829), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL)
829_0_<init>_Return(EOS(STATIC_829), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL) → 832_0_dupList_InvokeMethod(EOS(STATIC_832), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i93)), NULL)
847_0_dupList_InvokeMethod(EOS(STATIC_847), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), i95)), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), NULL) → 879_0_dupList_InvokeMethod(EOS(STATIC_879), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), i95)), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i105)))
879_0_dupList_InvokeMethod(EOS(STATIC_879), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o224, i115)), i95)), java.lang.Object(IntListDupRec.List(EOC, o224, i115)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, o224, i115))) → 967_0_dupList_InvokeMethod(EOS(STATIC_967), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o224, i115)), i95)), java.lang.Object(IntListDupRec.List(EOC, o224, i115)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, o224, i115)))
943_0_dupList_InvokeMethod(EOS(STATIC_943), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o274, i133)), matching1)), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o274, i133)), matching3)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o274, i133)), matching4)), java.lang.Object(IntListDupRec.List(EOC, o274, i133))) → 994_0_dupList_InvokeMethod(EOS(STATIC_994), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o274, i133)), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o274, i133)), 1)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o274, i133)), 1)), java.lang.Object(IntListDupRec.List(EOC, o274, i133))) | &&(&&(&&(=(matching1, 1), =(matching2, 0)), =(matching3, 1)), =(matching4, 1))
967_0_dupList_InvokeMethod(EOS(STATIC_967), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(IntListDupRec.List(EOC, o303, i140)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, o303, i140))) → 1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(IntListDupRec.List(EOC, o303, i140)))
994_0_dupList_InvokeMethod(EOS(STATIC_994), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o323, i147)), i146)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o323, i147)), i146)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o323, i147)), i146)), java.lang.Object(IntListDupRec.List(EOC, o323, i147))) → 1084_0_dupList_InvokeMethod(EOS(STATIC_1084), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o323, i147)), i146)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o323, i147)), i146)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o323, i147)), i146)), java.lang.Object(IntListDupRec.List(EOC, o323, i147))) | =(matching1, 0)
1063_0_dupList_InvokeMethod(EOS(STATIC_1063), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157))) → 967_0_dupList_InvokeMethod(EOS(STATIC_967), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i157)))
1083_0_dupList_InvokeMethod(EOS(STATIC_1083), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(IntListDupRec.List(EOC, o303, i140))) → 1084_0_dupList_InvokeMethod(EOS(STATIC_1084), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o303, i140)), i95)), java.lang.Object(IntListDupRec.List(EOC, o303, i140))) | =(matching1, 0)
1084_0_dupList_InvokeMethod(EOS(STATIC_1084), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), java.lang.Object(IntListDupRec.List(EOC, o396, i172))) → 1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171))) | =(matching1, 0)
1151_0_dupList_InvokeMethod(EOS(STATIC_1151), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching1)), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching2)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching3))) → 967_0_dupList_InvokeMethod(EOS(STATIC_967), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
1159_0_dupList_InvokeMethod(EOS(STATIC_1159), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching1)), matching2)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching3)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), matching4)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171))) → 1084_0_dupList_InvokeMethod(EOS(STATIC_1084), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, o396, i172)), i171))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))

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


P rules:
677_0_dupList_FieldAccess(EOS(STATIC_677), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), x1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), x1))) → 714_1_dupList_InvokeMethod(677_0_dupList_FieldAccess(EOS(STATIC_677), java.lang.Object(x0), java.lang.Object(x0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), x1)), java.lang.Object(x0)) | !(=(x1, 0))
677_0_dupList_FieldAccess(EOS(STATIC_677), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 0))) → 794_1_dupList_InvokeMethod(677_0_dupList_FieldAccess(EOS(STATIC_677), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 1))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 1)))
R rules:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListDupRec.List(EOC, x0, x1))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x3), x4)), java.lang.Object(x3)) → 1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), x4)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x4), x5)), java.lang.Object(x4)) → 1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)), x5)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(EOS(STATIC_832), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, x0)), NULL), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, x0)), x1)), java.lang.Object(IntListDupRec.List(EOC, NULL, x0))) → 1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, x0)), x1)), java.lang.Object(IntListDupRec.List(EOC, NULL, x0)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(EOS(STATIC_1003), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), java.lang.Object(IntListDupRec.List(EOC, x0, x1))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x3), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x3), 1))) → 1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x4), 1)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x4), 1))) → 1122_0_dupList_InvokeMethod(EOS(STATIC_1122), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, x0, x1)), x2)), 0)))

Filtered ground terms:



IntListDupRec.List(x1, x2, x3) → IntListDupRec.List(x2, x3)
677_0_dupList_FieldAccess(x1, x2, x3) → 677_0_dupList_FieldAccess(x2, x3)
Cond_677_0_dupList_FieldAccess(x1, x2, x3, x4) → Cond_677_0_dupList_FieldAccess(x1, x3, x4)
1122_0_dupList_InvokeMethod(x1, x2, x3, x4) → 1122_0_dupList_InvokeMethod(x3, x4)
java.lang.NullPointerException(x1) → java.lang.NullPointerException
java.lang.RuntimeException(x1) → java.lang.RuntimeException
java.lang.Exception(x1) → java.lang.Exception
java.lang.Throwable(x1) → java.lang.Throwable
1003_0_dupList_InvokeMethod(x1, x2, x3, x4) → 1003_0_dupList_InvokeMethod(x3, x4)
832_0_dupList_InvokeMethod(x1, x2, x3, x4) → 832_0_dupList_InvokeMethod(x3)

Filtered duplicate args:



677_0_dupList_FieldAccess(x1, x2) → 677_0_dupList_FieldAccess(x2)
Cond_677_0_dupList_FieldAccess(x1, x2, x3) → Cond_677_0_dupList_FieldAccess(x1, x3)
714_1_dupList_InvokeMethod(x1, x2, x3) → 714_1_dupList_InvokeMethod(x1, x2)
794_1_dupList_InvokeMethod(x1, x2, x3) → 794_1_dupList_InvokeMethod(x1, x2)
1003_0_dupList_InvokeMethod(x1, x2) → 1003_0_dupList_InvokeMethod(x1)
1122_0_dupList_InvokeMethod(x1, x2) → 1122_0_dupList_InvokeMethod(x1)

Filtered unneeded arguments:



794_1_dupList_InvokeMethod(x1, x2) → 794_1_dupList_InvokeMethod(x1)

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


P rules:
677_0_dupList_FieldAccess(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 714_1_dupList_InvokeMethod(677_0_dupList_FieldAccess(java.lang.Object(x0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) | !(=(x1, 0))
677_0_dupList_FieldAccess(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 794_1_dupList_InvokeMethod(677_0_dupList_FieldAccess(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1))))
R rules:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))), java.lang.Object(IntListDupRec.List(java.lang.Object(x4), x5))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), x5)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), 0)))

Finished conversion. Obtained 3 rules for P and 5 rules for R. System has predefined symbols.


P rules:
677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1, 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1)))
COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0))
677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1)))
R rules:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))), java.lang.Object(IntListDupRec.List(java.lang.Object(x4), x5))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), x5)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), 0)))

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

Boolean, Integer


The ITRS R consists of the following rules:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))), java.lang.Object(IntListDupRec.List(java.lang.Object(x4), x5))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), x5)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), 0)))

The integer pair graph contains the following rules and edges:
(0): 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(x1[0] = 0), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))
(1): COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))
(2): 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))

(0) -> (1), if (!(x1[0] = 0) ∧java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])) →* java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))


(1) -> (0), if (java.lang.Object(x0[1]) →* java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))


(1) -> (2), if (java.lang.Object(x0[1]) →* java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))


(2) -> (0), if (java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)) →* java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))


(2) -> (2), if (java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)) →* java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]'), 0)))



The set Q consists of the following terms:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))))

(8) IDPNonInfProof (SOUND transformation)

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

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 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1, 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) the following chains were created:
  • We consider the chain 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))), COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])) which results in the following constraint:

    (1)    (!(=(x1[0], 0))=TRUEjava.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])) ⇒ 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))∧(UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥))



    We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:

    (2)    (!(=(x1[0], 0))=TRUE677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))∧(UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (0 ≥ 0 ⇒ (UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥)∧[(5)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[4 + (-1)bso_24] + [8]x0[0] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (0 ≥ 0 ⇒ (UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥)∧[(5)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[4 + (-1)bso_24] + [8]x0[0] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (0 ≥ 0 ⇒ (UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥)∧[(5)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[4 + (-1)bso_24] + [8]x0[0] ≥ 0)



    We simplified constraint (5) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

    (6)    (0 ≥ 0 ⇒ (UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥)∧0 ≥ 0∧[(16)bni_23] ≥ 0∧[(5)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧[4 + (-1)bso_24] ≥ 0∧[1] ≥ 0)







For Pair COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0)) the following chains were created:
  • We consider the chain 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))), COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) which results in the following constraint:

    (7)    (!(=(x1[0], 0))=TRUEjava.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))∧java.lang.Object(x0[1])=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]1), x1[0]1)) ⇒ COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥NonInfC∧COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥))



    We simplified constraint (7) using rules (I), (II), (III) which results in the following new constraint:

    (8)    (!(=(x1[0], 0))=TRUECOND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]1), x1[0]1)), x1[0])))≥NonInfC∧COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]1), x1[0]1)), x1[0])))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]1), x1[0]1)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥))



    We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (9)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧[(9)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x0[0]1 ≥ 0∧[4 + (-1)bso_26] + [16]x0[0]1 ≥ 0)



    We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (10)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧[(9)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x0[0]1 ≥ 0∧[4 + (-1)bso_26] + [16]x0[0]1 ≥ 0)



    We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (11)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧[(9)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x0[0]1 ≥ 0∧[4 + (-1)bso_26] + [16]x0[0]1 ≥ 0)



    We simplified constraint (11) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

    (12)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_25] ≥ 0∧[(9)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_26] ≥ 0∧[1] ≥ 0)



  • We consider the chain 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))), COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))) which results in the following constraint:

    (13)    (!(=(x1[0], 0))=TRUEjava.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))∧java.lang.Object(x0[1])=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)) ⇒ COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥NonInfC∧COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥))



    We simplified constraint (13) using rules (I), (II), (III) which results in the following new constraint:

    (14)    (!(=(x1[0], 0))=TRUECOND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)), x1[0])))≥NonInfC∧COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)), x1[0])))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥))



    We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (15)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧[(9)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x0[2] ≥ 0∧[4 + (-1)bso_26] + [16]x0[2] ≥ 0)



    We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (16)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧[(9)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x0[2] ≥ 0∧[4 + (-1)bso_26] + [16]x0[2] ≥ 0)



    We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (17)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧[(9)bni_25 + (-1)Bound*bni_25] + [(32)bni_25]x0[2] ≥ 0∧[4 + (-1)bso_26] + [16]x0[2] ≥ 0)



    We simplified constraint (17) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:

    (18)    (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧0 ≥ 0∧[(32)bni_25] ≥ 0∧[(9)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧[4 + (-1)bso_26] ≥ 0∧[1] ≥ 0)







For Pair 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1))) the following chains were created:
  • We consider the chain COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) which results in the following constraint:

    (19)    (java.lang.Object(x0[1])=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))∧java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])) ⇒ 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥))



    We simplified constraint (19) using rules (I), (II), (III), (IV) which results in the following new constraint:

    (20)    (677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥))



    We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (21)    ((UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥)∧[bni_27] = 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (22)    ((UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥)∧[bni_27] = 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (23)    ((UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥)∧[bni_27] = 0∧[(-1)bso_28] ≥ 0)



    We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (24)    ((UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥)∧[bni_27] = 0∧0 ≥ 0∧[(-1)bso_28] ≥ 0)



  • We consider the chain 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) which results in the following constraint:

    (25)    (java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0))∧java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])) ⇒ 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1)))), ≥))



    We solved constraint (25) using rules (I), (II).
  • We consider the chain COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))) which results in the following constraint:

    (26)    (java.lang.Object(x0[1])=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))∧java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)) ⇒ 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥))



    We solved constraint (26) using rules (I), (II).
  • We consider the chain 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))) which results in the following constraint:

    (27)    (java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0))∧java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1))=java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]2), 0)) ⇒ 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥NonInfC∧677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1)))∧(UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1)))), ≥))



    We solved constraint (27) using rules (I), (II).




To summarize, we get the following constraints P for the following pairs.
  • 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1, 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1)))
    • (0 ≥ 0 ⇒ (UIncreasing(COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))), ≥)∧0 ≥ 0∧[(16)bni_23] ≥ 0∧[(5)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧[4 + (-1)bso_24] ≥ 0∧[1] ≥ 0)

  • COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0))
    • (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(32)bni_25] ≥ 0∧[(9)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧[4 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
    • (0 ≥ 0 ⇒ (UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))), ≥)∧0 ≥ 0∧[(32)bni_25] ≥ 0∧[(9)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧[4 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

  • 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1)))
    • ((UIncreasing(677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))), ≥)∧[bni_27] = 0∧0 ≥ 0∧[(-1)bso_28] ≥ 0)




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(714_1_dupList_InvokeMethod(x1, x2)) = 0   
POL(1003_0_dupList_InvokeMethod(x1)) = 0   
POL(java.lang.Object(x1)) = [2]x1   
POL(IntListDupRec.List(x1, x2)) = [1] + [2]x1   
POL(1122_0_dupList_InvokeMethod(x1)) = 0   
POL(0) = 0   
POL(832_0_dupList_InvokeMethod(x1)) = 0   
POL(NULL) = 0   
POL(794_1_dupList_InvokeMethod(x1)) = 0   
POL(677_0_DUPLIST_FIELDACCESS(x1)) = [1] + [2]x1   
POL(COND_677_0_DUPLIST_FIELDACCESS(x1, x2)) = [-1] + x2 + x1   
POL(!(x1)) = 0   
POL(=(x1, x2)) = 0   
POL(1) = 0   

The following pairs are in P>:

677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))
COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))

The following pairs are in Pbound:

677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_677_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))
COND_677_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))

The following pairs are in P:

677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))

At least the following rules have been oriented under context sensitive arithmetic replacement:

!(TRUE)1FALSE1
!(FALSE)1TRUE1

(9) 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


The ITRS R consists of the following rules:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))), java.lang.Object(IntListDupRec.List(java.lang.Object(x4), x5))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), x5)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0)), 0)))

The integer pair graph contains the following rules and edges:
(2): 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))

(2) -> (2), if (java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)) →* java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]'), 0)))



The set Q consists of the following terms:
714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), 0))))

(10) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(11) Obligation:

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

677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), pos(01)))) → 677_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), pos(s(01)))))

The TRS R consists of the following rules:

714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01)))), java.lang.Object(IntListDupRec.List(java.lang.Object(x4), x5))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01))), x5)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01))))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01))))) → 1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01))), pos(01))))

The set Q consists of the following terms:

714_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4)))
714_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01)))), java.lang.Object(IntListDupRec.List(java.lang.Object(x3), x4)))
714_1_dupList_InvokeMethod(832_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
794_1_dupList_InvokeMethod(1003_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))))
794_1_dupList_InvokeMethod(1122_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), pos(01)))))

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

(12) DependencyGraphProof (EQUIVALENT transformation)

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

(13) TRUE

(14) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: IntListDupRec.List.createList(I)LIntListDupRec/List;
SCC calls the following helper methods: IntListDupRec.List.createList(I)LIntListDupRec/List;
Performed SCC analyses: UsedFieldsAnalysis

(15) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 12 rules for P and 30 rules for R.


P rules:
234_0_createList_GE(EOS(STATIC_234), i26, i26) → 240_0_createList_GE(EOS(STATIC_240), i26, i26)
240_0_createList_GE(EOS(STATIC_240), i26, i26) → 245_0_createList_New(EOS(STATIC_245), i26) | >=(i26, 0)
245_0_createList_New(EOS(STATIC_245), i26) → 249_0_createList_Duplicate(EOS(STATIC_249), i26)
249_0_createList_Duplicate(EOS(STATIC_249), i26) → 254_0_createList_ConstantStackPush(EOS(STATIC_254), i26)
254_0_createList_ConstantStackPush(EOS(STATIC_254), i26) → 261_0_createList_Load(EOS(STATIC_261), i26)
261_0_createList_Load(EOS(STATIC_261), i26) → 264_0_createList_ConstantStackPush(EOS(STATIC_264), i26)
264_0_createList_ConstantStackPush(EOS(STATIC_264), i26) → 266_0_createList_IntArithmetic(EOS(STATIC_266), i26, 1)
266_0_createList_IntArithmetic(EOS(STATIC_266), i26, matching1) → 268_0_createList_InvokeMethod(EOS(STATIC_268), -(i26, 1)) | &&(>=(i26, 0), =(matching1, 1))
268_0_createList_InvokeMethod(EOS(STATIC_268), i29) → 270_1_createList_InvokeMethod(270_0_createList_Load(EOS(STATIC_270), i29), i29)
270_0_createList_Load(EOS(STATIC_270), i29) → 272_0_createList_Load(EOS(STATIC_272), i29)
272_0_createList_Load(EOS(STATIC_272), i29) → 228_0_createList_Load(EOS(STATIC_228), i29)
228_0_createList_Load(EOS(STATIC_228), i23) → 234_0_createList_GE(EOS(STATIC_234), i23, i23)
R rules:
234_0_createList_GE(EOS(STATIC_234), matching1, matching2) → 239_0_createList_GE(EOS(STATIC_239), -1, -1) | &&(=(matching1, -1), =(matching2, -1))
239_0_createList_GE(EOS(STATIC_239), matching1, matching2) → 244_0_createList_ConstantStackPush(EOS(STATIC_244), -1) | &&(&&(<(-1, 0), =(matching1, -1)), =(matching2, -1))
244_0_createList_ConstantStackPush(EOS(STATIC_244), matching1) → 247_0_createList_Return(EOS(STATIC_247), -1) | =(matching1, -1)
270_1_createList_InvokeMethod(247_0_createList_Return(EOS(STATIC_247), matching1), matching2) → 278_0_createList_Return(EOS(STATIC_278), -1, -1) | &&(=(matching1, -1), =(matching2, -1))
270_1_createList_InvokeMethod(299_0_createList_Return(EOS(STATIC_299)), i38) → 313_0_createList_Return(EOS(STATIC_313), i38)
270_1_createList_InvokeMethod(480_0_createList_Return(EOS(STATIC_480)), i81) → 511_0_createList_Return(EOS(STATIC_511), i81)
278_0_createList_Return(EOS(STATIC_278), matching1, matching2) → 280_0_createList_InvokeMethod(EOS(STATIC_280)) | &&(=(matching1, -1), =(matching2, -1))
280_0_createList_InvokeMethod(EOS(STATIC_280)) → 281_0_<init>_Load(EOS(STATIC_281))
281_0_<init>_Load(EOS(STATIC_281)) → 283_0_<init>_InvokeMethod(EOS(STATIC_283))
283_0_<init>_InvokeMethod(EOS(STATIC_283)) → 285_0_<init>_Load(EOS(STATIC_285))
285_0_<init>_Load(EOS(STATIC_285)) → 287_0_<init>_Load(EOS(STATIC_287))
287_0_<init>_Load(EOS(STATIC_287)) → 289_0_<init>_FieldAccess(EOS(STATIC_289))
289_0_<init>_FieldAccess(EOS(STATIC_289)) → 291_0_<init>_Load(EOS(STATIC_291))
291_0_<init>_Load(EOS(STATIC_291)) → 293_0_<init>_Load(EOS(STATIC_293))
293_0_<init>_Load(EOS(STATIC_293)) → 295_0_<init>_FieldAccess(EOS(STATIC_295))
295_0_<init>_FieldAccess(EOS(STATIC_295)) → 297_0_<init>_Return(EOS(STATIC_297))
297_0_<init>_Return(EOS(STATIC_297)) → 299_0_createList_Return(EOS(STATIC_299))
313_0_createList_Return(EOS(STATIC_313), i38) → 403_0_createList_Return(EOS(STATIC_403), i38)
403_0_createList_Return(EOS(STATIC_403), i61) → 409_0_createList_InvokeMethod(EOS(STATIC_409))
409_0_createList_InvokeMethod(EOS(STATIC_409)) → 414_0_<init>_Load(EOS(STATIC_414))
414_0_<init>_Load(EOS(STATIC_414)) → 425_0_<init>_InvokeMethod(EOS(STATIC_425))
425_0_<init>_InvokeMethod(EOS(STATIC_425)) → 432_0_<init>_Load(EOS(STATIC_432))
432_0_<init>_Load(EOS(STATIC_432)) → 438_0_<init>_Load(EOS(STATIC_438))
438_0_<init>_Load(EOS(STATIC_438)) → 448_0_<init>_FieldAccess(EOS(STATIC_448))
448_0_<init>_FieldAccess(EOS(STATIC_448)) → 454_0_<init>_Load(EOS(STATIC_454))
454_0_<init>_Load(EOS(STATIC_454)) → 459_0_<init>_Load(EOS(STATIC_459))
459_0_<init>_Load(EOS(STATIC_459)) → 465_0_<init>_FieldAccess(EOS(STATIC_465))
465_0_<init>_FieldAccess(EOS(STATIC_465)) → 472_0_<init>_Return(EOS(STATIC_472))
472_0_<init>_Return(EOS(STATIC_472)) → 480_0_createList_Return(EOS(STATIC_480))
511_0_createList_Return(EOS(STATIC_511), i81) → 403_0_createList_Return(EOS(STATIC_403), i81)

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


P rules:
234_0_createList_GE(EOS(STATIC_234), x0, x0) → 270_1_createList_InvokeMethod(234_0_createList_GE(EOS(STATIC_234), -(x0, 1), -(x0, 1)), -(x0, 1)) | >(+(x0, 1), 0)
R rules:
234_0_createList_GE(EOS(STATIC_234), -1, -1) → 247_0_createList_Return(EOS(STATIC_247), -1)
270_1_createList_InvokeMethod(247_0_createList_Return(EOS(STATIC_247), -1), -1) → 299_0_createList_Return(EOS(STATIC_299))
270_1_createList_InvokeMethod(299_0_createList_Return(EOS(STATIC_299)), x0) → 480_0_createList_Return(EOS(STATIC_480))
270_1_createList_InvokeMethod(480_0_createList_Return(EOS(STATIC_480)), x0) → 480_0_createList_Return(EOS(STATIC_480))

Filtered ground terms:



234_0_createList_GE(x1, x2, x3) → 234_0_createList_GE(x2, x3)
Cond_234_0_createList_GE(x1, x2, x3, x4) → Cond_234_0_createList_GE(x1, x3, x4)
480_0_createList_Return(x1) → 480_0_createList_Return
299_0_createList_Return(x1) → 299_0_createList_Return
247_0_createList_Return(x1, x2) → 247_0_createList_Return

Filtered duplicate args:



234_0_createList_GE(x1, x2) → 234_0_createList_GE(x2)
Cond_234_0_createList_GE(x1, x2, x3) → Cond_234_0_createList_GE(x1, x3)

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


P rules:
234_0_createList_GE(x0) → 270_1_createList_InvokeMethod(234_0_createList_GE(-(x0, 1)), -(x0, 1)) | >(x0, -1)
R rules:
234_0_createList_GE(-1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, -1) → 299_0_createList_Return
270_1_createList_InvokeMethod(299_0_createList_Return, x0) → 480_0_createList_Return
270_1_createList_InvokeMethod(480_0_createList_Return, x0) → 480_0_createList_Return

Performed bisimulation on rules. Used the following equivalence classes: {[247_0_createList_Return, 299_0_createList_Return, 480_0_createList_Return]=247_0_createList_Return}


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


P rules:
234_0_CREATELIST_GE(x0) → COND_234_0_CREATELIST_GE(>(x0, -1), x0)
COND_234_0_CREATELIST_GE(TRUE, x0) → 234_0_CREATELIST_GE(-(x0, 1))
R rules:
234_0_createList_GE(-1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, -1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, x0) → 247_0_createList_Return

(16) 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


The ITRS R consists of the following rules:
234_0_createList_GE(-1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, -1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, x0) → 247_0_createList_Return

The integer pair graph contains the following rules and edges:
(0): 234_0_CREATELIST_GE(x0[0]) → COND_234_0_CREATELIST_GE(x0[0] > -1, x0[0])
(1): COND_234_0_CREATELIST_GE(TRUE, x0[1]) → 234_0_CREATELIST_GE(x0[1] - 1)

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


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



The set Q consists of the following terms:
234_0_createList_GE(-1)
270_1_createList_InvokeMethod(247_0_createList_Return, x0)

(17) 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@75411b99 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 234_0_CREATELIST_GE(x0) → COND_234_0_CREATELIST_GE(>(x0, -1), x0) the following chains were created:
  • We consider the chain 234_0_CREATELIST_GE(x0[0]) → COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0]), COND_234_0_CREATELIST_GE(TRUE, x0[1]) → 234_0_CREATELIST_GE(-(x0[1], 1)) which results in the following constraint:

    (1)    (>(x0[0], -1)=TRUEx0[0]=x0[1]234_0_CREATELIST_GE(x0[0])≥NonInfC∧234_0_CREATELIST_GE(x0[0])≥COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])∧(UIncreasing(COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (>(x0[0], -1)=TRUE234_0_CREATELIST_GE(x0[0])≥NonInfC∧234_0_CREATELIST_GE(x0[0])≥COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])∧(UIncreasing(COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    (x0[0] ≥ 0 ⇒ (UIncreasing(COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)







For Pair COND_234_0_CREATELIST_GE(TRUE, x0) → 234_0_CREATELIST_GE(-(x0, 1)) the following chains were created:
  • We consider the chain COND_234_0_CREATELIST_GE(TRUE, x0[1]) → 234_0_CREATELIST_GE(-(x0[1], 1)) which results in the following constraint:

    (6)    (COND_234_0_CREATELIST_GE(TRUE, x0[1])≥NonInfC∧COND_234_0_CREATELIST_GE(TRUE, x0[1])≥234_0_CREATELIST_GE(-(x0[1], 1))∧(UIncreasing(234_0_CREATELIST_GE(-(x0[1], 1))), ≥))



    We simplified constraint (6) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (7)    ((UIncreasing(234_0_CREATELIST_GE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧[2 + (-1)bso_14] ≥ 0)



    We simplified constraint (7) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (8)    ((UIncreasing(234_0_CREATELIST_GE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧[2 + (-1)bso_14] ≥ 0)



    We simplified constraint (8) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (9)    ((UIncreasing(234_0_CREATELIST_GE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧[2 + (-1)bso_14] ≥ 0)



    We simplified constraint (9) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (10)    ((UIncreasing(234_0_CREATELIST_GE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧0 = 0∧[2 + (-1)bso_14] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • 234_0_CREATELIST_GE(x0) → COND_234_0_CREATELIST_GE(>(x0, -1), x0)
    • (x0[0] ≥ 0 ⇒ (UIncreasing(COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)

  • COND_234_0_CREATELIST_GE(TRUE, x0) → 234_0_CREATELIST_GE(-(x0, 1))
    • ((UIncreasing(234_0_CREATELIST_GE(-(x0[1], 1))), ≥)∧[bni_13] = 0∧0 = 0∧[2 + (-1)bso_14] ≥ 0)




The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = 0   
POL(234_0_createList_GE(x1)) = [-1]   
POL(-1) = [-1]   
POL(247_0_createList_Return) = [-1]   
POL(270_1_createList_InvokeMethod(x1, x2)) = [-1]   
POL(234_0_CREATELIST_GE(x1)) = [2]x1   
POL(COND_234_0_CREATELIST_GE(x1, x2)) = [2]x2   
POL(>(x1, x2)) = [-1]   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(1) = [1]   

The following pairs are in P>:

COND_234_0_CREATELIST_GE(TRUE, x0[1]) → 234_0_CREATELIST_GE(-(x0[1], 1))

The following pairs are in Pbound:

234_0_CREATELIST_GE(x0[0]) → COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])

The following pairs are in P:

234_0_CREATELIST_GE(x0[0]) → COND_234_0_CREATELIST_GE(>(x0[0], -1), x0[0])

There are no usable rules.

(18) Complex Obligation (AND)

(19) 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


The ITRS R consists of the following rules:
234_0_createList_GE(-1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, -1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, x0) → 247_0_createList_Return

The integer pair graph contains the following rules and edges:
(0): 234_0_CREATELIST_GE(x0[0]) → COND_234_0_CREATELIST_GE(x0[0] > -1, x0[0])


The set Q consists of the following terms:
234_0_createList_GE(-1)
270_1_createList_InvokeMethod(247_0_createList_Return, x0)

(20) IDependencyGraphProof (EQUIVALENT transformation)

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

(21) TRUE

(22) 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


The ITRS R consists of the following rules:
234_0_createList_GE(-1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, -1) → 247_0_createList_Return
270_1_createList_InvokeMethod(247_0_createList_Return, x0) → 247_0_createList_Return

The integer pair graph contains the following rules and edges:
(1): COND_234_0_CREATELIST_GE(TRUE, x0[1]) → 234_0_CREATELIST_GE(x0[1] - 1)


The set Q consists of the following terms:
234_0_createList_GE(-1)
270_1_createList_InvokeMethod(247_0_createList_Return, x0)

(23) IDependencyGraphProof (EQUIVALENT transformation)

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

(24) TRUE