(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:
671_0_dupList_FieldAccess(EOS(STATIC_671), java.lang.Object(IntListDupRec.List(EOC, o161, i92)), java.lang.Object(IntListDupRec.List(EOC, o161, i92))) → 673_0_dupList_FieldAccess(EOS(STATIC_673), java.lang.Object(IntListDupRec.List(EOC, o161, i92)), java.lang.Object(IntListDupRec.List(EOC, o161, i92)))
673_0_dupList_FieldAccess(EOS(STATIC_673), java.lang.Object(IntListDupRec.List(EOC, o161, i92)), java.lang.Object(IntListDupRec.List(EOC, o161, i92))) → 674_0_dupList_NONNULL(EOS(STATIC_674), java.lang.Object(IntListDupRec.List(EOC, o161, i92)), o161)
674_0_dupList_NONNULL(EOS(STATIC_674), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)), java.lang.Object(o163sub)) → 677_0_dupList_NONNULL(EOS(STATIC_677), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)), java.lang.Object(o163sub))
677_0_dupList_NONNULL(EOS(STATIC_677), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)), java.lang.Object(o163sub)) → 680_0_dupList_Load(EOS(STATIC_680), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)))
680_0_dupList_Load(EOS(STATIC_680), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92))) → 683_0_dupList_FieldAccess(EOS(STATIC_683), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)))
683_0_dupList_FieldAccess(EOS(STATIC_683), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92))) → 688_0_dupList_NE(EOS(STATIC_688), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i92)), i92)
688_0_dupList_NE(EOS(STATIC_688), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), i95) → 691_0_dupList_NE(EOS(STATIC_691), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), i95)
688_0_dupList_NE(EOS(STATIC_688), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2) → 692_0_dupList_NE(EOS(STATIC_692), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), 0) | &&(=(matching1, 0), =(matching2, 0))
691_0_dupList_NE(EOS(STATIC_691), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), i95) → 696_0_dupList_Load(EOS(STATIC_696), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95))) | !(=(i95, 0))
696_0_dupList_Load(EOS(STATIC_696), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95))) → 699_0_dupList_FieldAccess(EOS(STATIC_699), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)))
699_0_dupList_FieldAccess(EOS(STATIC_699), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95))) → 705_0_dupList_InvokeMethod(EOS(STATIC_705), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub))
705_0_dupList_InvokeMethod(EOS(STATIC_705), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub)) → 708_1_dupList_InvokeMethod(708_0_dupList_Load(EOS(STATIC_708), java.lang.Object(o163sub)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), i95)), java.lang.Object(o163sub))
708_0_dupList_Load(EOS(STATIC_708), java.lang.Object(o163sub)) → 713_0_dupList_Load(EOS(STATIC_713), java.lang.Object(o163sub))
713_0_dupList_Load(EOS(STATIC_713), java.lang.Object(o163sub)) → 669_0_dupList_Load(EOS(STATIC_669), java.lang.Object(o163sub))
669_0_dupList_Load(EOS(STATIC_669), java.lang.Object(o156sub)) → 671_0_dupList_FieldAccess(EOS(STATIC_671), java.lang.Object(o156sub), java.lang.Object(o156sub))
692_0_dupList_NE(EOS(STATIC_692), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2) → 697_0_dupList_Load(EOS(STATIC_697), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0))) | &&(=(matching1, 0), =(matching2, 0))
697_0_dupList_Load(EOS(STATIC_697), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1))) → 701_0_dupList_FieldAccess(EOS(STATIC_701), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0))) | =(matching1, 0)
701_0_dupList_FieldAccess(EOS(STATIC_701), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching2))) → 706_0_dupList_Store(EOS(STATIC_706), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub)) | &&(=(matching1, 0), =(matching2, 0))
706_0_dupList_Store(EOS(STATIC_706), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub)) → 710_0_dupList_Load(EOS(STATIC_710), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 0)), java.lang.Object(o163sub)) | =(matching1, 0)
710_0_dupList_Load(EOS(STATIC_710), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), java.lang.Object(o163sub)) → 715_0_dupList_New(EOS(STATIC_715), 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)
715_0_dupList_New(EOS(STATIC_715), 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))) → 720_0_dupList_Duplicate(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)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(=(matching1, 0), =(matching2, 0))
720_0_dupList_Duplicate(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)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching3))) → 723_0_dupList_ConstantStackPush(EOS(STATIC_723), 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))
723_0_dupList_ConstantStackPush(EOS(STATIC_723), 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))) → 726_0_dupList_Load(EOS(STATIC_726), 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))
726_0_dupList_Load(EOS(STATIC_726), 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) → 730_0_dupList_InvokeMethod(EOS(STATIC_730), 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))
730_0_dupList_InvokeMethod(EOS(STATIC_730), 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)) → 733_0_<init>_Load(EOS(STATIC_733), 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))
733_0_<init>_Load(EOS(STATIC_733), 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)) → 739_0_<init>_InvokeMethod(EOS(STATIC_739), 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))
739_0_<init>_InvokeMethod(EOS(STATIC_739), 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))) → 743_0_<init>_Load(EOS(STATIC_743), 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))
743_0_<init>_Load(EOS(STATIC_743), 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)) → 747_0_<init>_Load(EOS(STATIC_747), 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))
747_0_<init>_Load(EOS(STATIC_747), 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))) → 751_0_<init>_FieldAccess(EOS(STATIC_751), 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))
751_0_<init>_FieldAccess(EOS(STATIC_751), 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) → 756_0_<init>_Load(EOS(STATIC_756), 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))
756_0_<init>_Load(EOS(STATIC_756), 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)) → 761_0_<init>_Load(EOS(STATIC_761), 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))
761_0_<init>_Load(EOS(STATIC_761), 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))) → 765_0_<init>_FieldAccess(EOS(STATIC_765), 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))
765_0_<init>_FieldAccess(EOS(STATIC_765), 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)) → 771_0_<init>_Return(EOS(STATIC_771), 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))
771_0_<init>_Return(EOS(STATIC_771), 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)) → 772_0_dupList_FieldAccess(EOS(STATIC_772), 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))
772_0_dupList_FieldAccess(EOS(STATIC_772), 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))) → 778_0_dupList_Load(EOS(STATIC_778), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1)), 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 1))
778_0_dupList_Load(EOS(STATIC_778), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1)), matching2))) → 782_0_dupList_FieldAccess(EOS(STATIC_782), 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))
782_0_dupList_FieldAccess(EOS(STATIC_782), 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))) → 784_0_dupList_InvokeMethod(EOS(STATIC_784), 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))
784_0_dupList_InvokeMethod(EOS(STATIC_784), 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))) → 788_1_dupList_InvokeMethod(788_0_dupList_Load(EOS(STATIC_788), 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))
788_0_dupList_Load(EOS(STATIC_788), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1))) → 792_0_dupList_Load(EOS(STATIC_792), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | =(matching1, 1)
792_0_dupList_Load(EOS(STATIC_792), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), matching1))) → 669_0_dupList_Load(EOS(STATIC_669), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(o163sub), 1))) | =(matching1, 1)
R rules:
674_0_dupList_NONNULL(EOS(STATIC_674), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL) → 678_0_dupList_NONNULL(EOS(STATIC_678), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL)
678_0_dupList_NONNULL(EOS(STATIC_678), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL) → 681_0_dupList_New(EOS(STATIC_681), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)))
681_0_dupList_New(EOS(STATIC_681), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 685_0_dupList_Duplicate(EOS(STATIC_685), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)))
685_0_dupList_Duplicate(EOS(STATIC_685), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1))) → 689_0_dupList_ConstantStackPush(EOS(STATIC_689), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | =(matching1, 0)
689_0_dupList_ConstantStackPush(EOS(STATIC_689), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2))) → 694_0_dupList_Load(EOS(STATIC_694), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0) | &&(=(matching1, 0), =(matching2, 0))
694_0_dupList_Load(EOS(STATIC_694), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3) → 698_0_dupList_InvokeMethod(EOS(STATIC_698), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
698_0_dupList_InvokeMethod(EOS(STATIC_698), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 702_0_<init>_Load(EOS(STATIC_702), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
702_0_<init>_Load(EOS(STATIC_702), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 712_0_<init>_InvokeMethod(EOS(STATIC_712), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(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, 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))) → 843_0_dupList_InvokeMethod(EOS(STATIC_843), 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)
708_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)) → 1061_0_dupList_InvokeMethod(EOS(STATIC_1061), 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)))
708_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)) → 1152_0_dupList_InvokeMethod(EOS(STATIC_1152), 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)
712_0_<init>_InvokeMethod(EOS(STATIC_712), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6))) → 718_0_<init>_Load(EOS(STATIC_718), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0)), =(matching6, 0))
718_0_<init>_Load(EOS(STATIC_718), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 721_0_<init>_Load(EOS(STATIC_721), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0))
721_0_<init>_Load(EOS(STATIC_721), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), matching5, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching6))) → 725_0_<init>_FieldAccess(EOS(STATIC_725), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0)), =(matching6, 0))
725_0_<init>_FieldAccess(EOS(STATIC_725), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching5)), matching6) → 728_0_<init>_Load(EOS(STATIC_728), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | &&(&&(&&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0)), =(matching5, 0)), =(matching6, 0))
728_0_<init>_Load(EOS(STATIC_728), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 732_0_<init>_Load(EOS(STATIC_732), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
732_0_<init>_Load(EOS(STATIC_732), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4))) → 735_0_<init>_FieldAccess(EOS(STATIC_735), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, 0)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
735_0_<init>_FieldAccess(EOS(STATIC_735), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching1)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, matching4)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 737_0_<init>_Return(EOS(STATIC_737), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 0)), 0, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | &&(&&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0)), =(matching4, 0))
737_0_<init>_Return(EOS(STATIC_737), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), matching1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), matching2)), matching3, java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 741_0_dupList_StackPop(EOS(STATIC_741), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 0))) | &&(&&(=(matching1, 0), =(matching2, 0)), =(matching3, 0))
741_0_dupList_StackPop(EOS(STATIC_741), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), matching1))) → 745_0_dupList_JMP(EOS(STATIC_745), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) | =(matching1, 0)
745_0_dupList_JMP(EOS(STATIC_745), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 749_0_dupList_Load(EOS(STATIC_749), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)))
749_0_dupList_Load(EOS(STATIC_749), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 753_0_dupList_FieldAccess(EOS(STATIC_753), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)))
753_0_dupList_FieldAccess(EOS(STATIC_753), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), java.lang.Object(IntListDupRec.List(EOC, NULL, i92))) → 759_0_dupList_InvokeMethod(EOS(STATIC_759), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL)
759_0_dupList_InvokeMethod(EOS(STATIC_759), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL) → 763_0_dupList_InvokeMethod(EOS(STATIC_763), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL)
763_0_dupList_InvokeMethod(EOS(STATIC_763), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL) → 766_0_<init>_Load(EOS(STATIC_766), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
766_0_<init>_Load(EOS(STATIC_766), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 774_0_<init>_InvokeMethod(EOS(STATIC_774), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
774_0_<init>_InvokeMethod(EOS(STATIC_774), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC)))))) → 779_0_<init>_Load(EOS(STATIC_779), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
779_0_<init>_Load(EOS(STATIC_779), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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>_InvokeMethod(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, i92)), 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>_InvokeMethod(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, i92)), 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)))))) → 790_0_<init>_Load(EOS(STATIC_790), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
788_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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))
788_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))
790_0_<init>_Load(EOS(STATIC_790), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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)))))) → 795_0_<init>_InvokeMethod(EOS(STATIC_795), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
795_0_<init>_InvokeMethod(EOS(STATIC_795), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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)))))) → 798_0_<init>_Load(EOS(STATIC_798), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
798_0_<init>_Load(EOS(STATIC_798), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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)))))) → 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, i92)), 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))))))
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, i92)), 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)))))) → 803_0_<init>_Load(EOS(STATIC_803), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
803_0_<init>_Load(EOS(STATIC_803), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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, i92)), 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))))))
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, i92)), 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>_FieldAccess(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, i92)), 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))))))
806_0_<init>_FieldAccess(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, i92)), 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>_Load(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, i92)), 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))))))
812_0_<init>_Load(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, i92)), 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)))))) → 814_0_<init>_InvokeMethod(EOS(STATIC_814), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
814_0_<init>_InvokeMethod(EOS(STATIC_814), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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)))))) → 816_0_<init>_StackPop(EOS(STATIC_816), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
816_0_<init>_StackPop(EOS(STATIC_816), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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)))))) → 818_0_<init>_Return(EOS(STATIC_818), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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))))))
818_0_<init>_Return(EOS(STATIC_818), java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))), java.lang.Object(IntListDupRec.List(EOC, NULL, i92)), 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)))))) → 819_0_<init>_Return(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, i92)), 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))))))
819_0_<init>_Return(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, i92)), 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)))))) → 822_0_<init>_Return(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, i92)), NULL, java.lang.Object(java.lang.Throwable(java.lang.Exception(java.lang.RuntimeException(java.lang.NullPointerException(EOC))))))
822_0_<init>_Return(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, i92)), NULL, 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, i92)), NULL)
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, i92)), NULL) → 827_0_dupList_InvokeMethod(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, i92)), NULL)
843_0_dupList_InvokeMethod(EOS(STATIC_843), 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) → 874_0_dupList_InvokeMethod(EOS(STATIC_874), 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)))
874_0_dupList_InvokeMethod(EOS(STATIC_874), 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))) → 965_0_dupList_InvokeMethod(EOS(STATIC_965), 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)))
939_0_dupList_InvokeMethod(EOS(STATIC_939), 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))) → 991_0_dupList_InvokeMethod(EOS(STATIC_991), 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))
965_0_dupList_InvokeMethod(EOS(STATIC_965), 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))) → 1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)))
991_0_dupList_InvokeMethod(EOS(STATIC_991), 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)
1061_0_dupList_InvokeMethod(EOS(STATIC_1061), 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))) → 965_0_dupList_InvokeMethod(EOS(STATIC_965), 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)
1152_0_dupList_InvokeMethod(EOS(STATIC_1152), 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))) → 965_0_dupList_InvokeMethod(EOS(STATIC_965), 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:
671_0_dupList_FieldAccess(EOS(STATIC_671), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), x1)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), x1))) → 708_1_dupList_InvokeMethod(671_0_dupList_FieldAccess(EOS(STATIC_671), 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))
671_0_dupList_FieldAccess(EOS(STATIC_671), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 0)), java.lang.Object(IntListDupRec.List(EOC, java.lang.Object(x0), 0))) → 788_1_dupList_InvokeMethod(671_0_dupList_FieldAccess(EOS(STATIC_671), 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:
708_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)) → 1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)))
708_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)) → 1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(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, 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))) → 1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)))
788_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(EOS(STATIC_1001), 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)))
788_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)
671_0_dupList_FieldAccess(x1, x2, x3) → 671_0_dupList_FieldAccess(x2, x3)
Cond_671_0_dupList_FieldAccess(x1, x2, x3, x4) → Cond_671_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
1001_0_dupList_InvokeMethod(x1, x2, x3, x4) → 1001_0_dupList_InvokeMethod(x3, x4)
827_0_dupList_InvokeMethod(x1, x2, x3, x4) → 827_0_dupList_InvokeMethod(x3)

Filtered duplicate args:



671_0_dupList_FieldAccess(x1, x2) → 671_0_dupList_FieldAccess(x2)
Cond_671_0_dupList_FieldAccess(x1, x2, x3) → Cond_671_0_dupList_FieldAccess(x1, x3)
708_1_dupList_InvokeMethod(x1, x2, x3) → 708_1_dupList_InvokeMethod(x1, x2)
788_1_dupList_InvokeMethod(x1, x2, x3) → 788_1_dupList_InvokeMethod(x1, x2)
1001_0_dupList_InvokeMethod(x1, x2) → 1001_0_dupList_InvokeMethod(x1)
1122_0_dupList_InvokeMethod(x1, x2) → 1122_0_dupList_InvokeMethod(x1)

Filtered unneeded arguments:



788_1_dupList_InvokeMethod(x1, x2) → 788_1_dupList_InvokeMethod(x1)

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


P rules:
671_0_dupList_FieldAccess(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 708_1_dupList_InvokeMethod(671_0_dupList_FieldAccess(java.lang.Object(x0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) | !(=(x1, 0))
671_0_dupList_FieldAccess(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 788_1_dupList_InvokeMethod(671_0_dupList_FieldAccess(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1))))
R rules:
708_1_dupList_InvokeMethod(1001_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))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
708_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))) → 1001_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_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)))
788_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:
671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → COND_671_0_DUPLIST_FIELDACCESS(!(=(x1, 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1)))
COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0))
671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1)))
R rules:
708_1_dupList_InvokeMethod(1001_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))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
708_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))) → 1001_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_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)))
788_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:
708_1_dupList_InvokeMethod(1001_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))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
708_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))) → 1001_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_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)))
788_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): 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_0_DUPLIST_FIELDACCESS(!(x1[0] = 0), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))
(1): COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))
(2): 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_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:
708_1_dupList_InvokeMethod(1001_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)))
708_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))))
788_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@20cb6d74 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 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → COND_671_0_DUPLIST_FIELDACCESS(!(=(x1, 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) the following chains were created:
  • We consider the chain 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))), COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 671_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])) ⇒ 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥COND_671_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))∧(UIncreasing(COND_671_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))=TRUE671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))≥COND_671_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0])))∧(UIncreasing(COND_671_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_671_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_671_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_671_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_671_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_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0)) the following chains were created:
  • We consider the chain 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))), COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_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_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥NonInfC∧COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))∧(UIncreasing(671_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_671_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_671_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])))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]1), x1[0]1)))∧(UIncreasing(671_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(671_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(671_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(671_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(671_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 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_0_DUPLIST_FIELDACCESS(!(=(x1[0], 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))), COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_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_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥NonInfC∧COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1])))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1]))∧(UIncreasing(671_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_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)), x1[0])))≥NonInfC∧COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)), x1[0])))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))∧(UIncreasing(671_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(671_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(671_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(671_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(671_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 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1))) the following chains were created:
  • We consider the chain COND_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_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])) ⇒ 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))∧(UIncreasing(671_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)    (671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))∧(UIncreasing(671_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(671_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(671_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(671_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(671_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 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[0]), x1[0]))) → COND_671_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])) ⇒ 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1)))∧(UIncreasing(671_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_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0[1]), x1[1]))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0[1])), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_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)) ⇒ 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0)))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1)))∧(UIncreasing(671_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 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 1))), 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_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)) ⇒ 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥NonInfC∧671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 0)))≥671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]1), 1)))∧(UIncreasing(671_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.
  • 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → COND_671_0_DUPLIST_FIELDACCESS(!(=(x1, 0)), java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1)))
    • (0 ≥ 0 ⇒ (UIncreasing(COND_671_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_671_0_DUPLIST_FIELDACCESS(TRUE, java.lang.Object(IntListDupRec.List(java.lang.Object(x0), x1))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(x0))
    • (0 ≥ 0 ⇒ (UIncreasing(671_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(671_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)

  • 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 0))) → 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0), 1)))
    • ((UIncreasing(671_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(708_1_dupList_InvokeMethod(x1, x2)) = 0   
POL(1001_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(827_0_dupList_InvokeMethod(x1)) = 0   
POL(NULL) = 0   
POL(788_1_dupList_InvokeMethod(x1)) = 0   
POL(671_0_DUPLIST_FIELDACCESS(x1)) = [1] + [2]x1   
POL(COND_671_0_DUPLIST_FIELDACCESS(x1, x2)) = [-1] + x2 + x1   
POL(!(x1)) = 0   
POL(=(x1, x2)) = 0   
POL(1) = 0   

The following pairs are in P>:

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

The following pairs are in Pbound:

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

The following pairs are in P:

671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_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:
708_1_dupList_InvokeMethod(1001_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))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
708_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))) → 1001_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_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)))
788_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): 671_0_DUPLIST_FIELDACCESS(java.lang.Object(IntListDupRec.List(java.lang.Object(x0[2]), 0))) → 671_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:
708_1_dupList_InvokeMethod(1001_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)))
708_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))))
788_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:

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

The TRS R consists of the following rules:

708_1_dupList_InvokeMethod(1001_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))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2)), x4)))
708_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))) → 1001_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1))) → 1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_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))))
788_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:

708_1_dupList_InvokeMethod(1001_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)))
708_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)))
708_1_dupList_InvokeMethod(827_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(NULL, x0))), java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(NULL, x0)), x1)))
788_1_dupList_InvokeMethod(1001_0_dupList_InvokeMethod(java.lang.Object(IntListDupRec.List(java.lang.Object(IntListDupRec.List(x0, x1)), x2))))
788_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:
236_0_createList_GE(EOS(STATIC_236), i26, i26) → 242_0_createList_GE(EOS(STATIC_242), i26, i26)
242_0_createList_GE(EOS(STATIC_242), i26, i26) → 247_0_createList_New(EOS(STATIC_247), i26) | >=(i26, 0)
247_0_createList_New(EOS(STATIC_247), i26) → 252_0_createList_Duplicate(EOS(STATIC_252), i26)
252_0_createList_Duplicate(EOS(STATIC_252), i26) → 257_0_createList_ConstantStackPush(EOS(STATIC_257), i26)
257_0_createList_ConstantStackPush(EOS(STATIC_257), i26) → 263_0_createList_Load(EOS(STATIC_263), i26)
263_0_createList_Load(EOS(STATIC_263), i26) → 266_0_createList_ConstantStackPush(EOS(STATIC_266), i26)
266_0_createList_ConstantStackPush(EOS(STATIC_266), i26) → 268_0_createList_IntArithmetic(EOS(STATIC_268), i26, 1)
268_0_createList_IntArithmetic(EOS(STATIC_268), i26, matching1) → 270_0_createList_InvokeMethod(EOS(STATIC_270), -(i26, 1)) | &&(>=(i26, 0), =(matching1, 1))
270_0_createList_InvokeMethod(EOS(STATIC_270), i29) → 272_1_createList_InvokeMethod(272_0_createList_Load(EOS(STATIC_272), i29), i29)
272_0_createList_Load(EOS(STATIC_272), i29) → 274_0_createList_Load(EOS(STATIC_274), i29)
274_0_createList_Load(EOS(STATIC_274), i29) → 231_0_createList_Load(EOS(STATIC_231), i29)
231_0_createList_Load(EOS(STATIC_231), i23) → 236_0_createList_GE(EOS(STATIC_236), i23, i23)
R rules:
236_0_createList_GE(EOS(STATIC_236), matching1, matching2) → 241_0_createList_GE(EOS(STATIC_241), -1, -1) | &&(=(matching1, -1), =(matching2, -1))
241_0_createList_GE(EOS(STATIC_241), matching1, matching2) → 246_0_createList_ConstantStackPush(EOS(STATIC_246), -1) | &&(&&(<(-1, 0), =(matching1, -1)), =(matching2, -1))
246_0_createList_ConstantStackPush(EOS(STATIC_246), matching1) → 250_0_createList_Return(EOS(STATIC_250), -1) | =(matching1, -1)
272_1_createList_InvokeMethod(250_0_createList_Return(EOS(STATIC_250), matching1), matching2) → 280_0_createList_Return(EOS(STATIC_280), -1, -1) | &&(=(matching1, -1), =(matching2, -1))
272_1_createList_InvokeMethod(301_0_createList_Return(EOS(STATIC_301)), i38) → 316_0_createList_Return(EOS(STATIC_316), i38)
272_1_createList_InvokeMethod(487_0_createList_Return(EOS(STATIC_487)), i82) → 520_0_createList_Return(EOS(STATIC_520), i82)
280_0_createList_Return(EOS(STATIC_280), matching1, matching2) → 282_0_createList_InvokeMethod(EOS(STATIC_282)) | &&(=(matching1, -1), =(matching2, -1))
282_0_createList_InvokeMethod(EOS(STATIC_282)) → 283_0_<init>_Load(EOS(STATIC_283))
283_0_<init>_Load(EOS(STATIC_283)) → 285_0_<init>_InvokeMethod(EOS(STATIC_285))
285_0_<init>_InvokeMethod(EOS(STATIC_285)) → 288_0_<init>_Load(EOS(STATIC_288))
288_0_<init>_Load(EOS(STATIC_288)) → 290_0_<init>_Load(EOS(STATIC_290))
290_0_<init>_Load(EOS(STATIC_290)) → 292_0_<init>_FieldAccess(EOS(STATIC_292))
292_0_<init>_FieldAccess(EOS(STATIC_292)) → 294_0_<init>_Load(EOS(STATIC_294))
294_0_<init>_Load(EOS(STATIC_294)) → 296_0_<init>_Load(EOS(STATIC_296))
296_0_<init>_Load(EOS(STATIC_296)) → 298_0_<init>_FieldAccess(EOS(STATIC_298))
298_0_<init>_FieldAccess(EOS(STATIC_298)) → 300_0_<init>_Return(EOS(STATIC_300))
300_0_<init>_Return(EOS(STATIC_300)) → 301_0_createList_Return(EOS(STATIC_301))
316_0_createList_Return(EOS(STATIC_316), i38) → 409_0_createList_Return(EOS(STATIC_409), i38)
409_0_createList_Return(EOS(STATIC_409), i61) → 414_0_createList_InvokeMethod(EOS(STATIC_414))
414_0_createList_InvokeMethod(EOS(STATIC_414)) → 420_0_<init>_Load(EOS(STATIC_420))
420_0_<init>_Load(EOS(STATIC_420)) → 431_0_<init>_InvokeMethod(EOS(STATIC_431))
431_0_<init>_InvokeMethod(EOS(STATIC_431)) → 439_0_<init>_Load(EOS(STATIC_439))
439_0_<init>_Load(EOS(STATIC_439)) → 445_0_<init>_Load(EOS(STATIC_445))
445_0_<init>_Load(EOS(STATIC_445)) → 456_0_<init>_FieldAccess(EOS(STATIC_456))
456_0_<init>_FieldAccess(EOS(STATIC_456)) → 461_0_<init>_Load(EOS(STATIC_461))
461_0_<init>_Load(EOS(STATIC_461)) → 464_0_<init>_Load(EOS(STATIC_464))
464_0_<init>_Load(EOS(STATIC_464)) → 471_0_<init>_FieldAccess(EOS(STATIC_471))
471_0_<init>_FieldAccess(EOS(STATIC_471)) → 480_0_<init>_Return(EOS(STATIC_480))
480_0_<init>_Return(EOS(STATIC_480)) → 487_0_createList_Return(EOS(STATIC_487))
520_0_createList_Return(EOS(STATIC_520), i82) → 409_0_createList_Return(EOS(STATIC_409), i82)

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


P rules:
236_0_createList_GE(EOS(STATIC_236), x0, x0) → 272_1_createList_InvokeMethod(236_0_createList_GE(EOS(STATIC_236), -(x0, 1), -(x0, 1)), -(x0, 1)) | >(+(x0, 1), 0)
R rules:
236_0_createList_GE(EOS(STATIC_236), -1, -1) → 250_0_createList_Return(EOS(STATIC_250), -1)
272_1_createList_InvokeMethod(250_0_createList_Return(EOS(STATIC_250), -1), -1) → 301_0_createList_Return(EOS(STATIC_301))
272_1_createList_InvokeMethod(301_0_createList_Return(EOS(STATIC_301)), x0) → 487_0_createList_Return(EOS(STATIC_487))
272_1_createList_InvokeMethod(487_0_createList_Return(EOS(STATIC_487)), x0) → 487_0_createList_Return(EOS(STATIC_487))

Filtered ground terms:



236_0_createList_GE(x1, x2, x3) → 236_0_createList_GE(x2, x3)
Cond_236_0_createList_GE(x1, x2, x3, x4) → Cond_236_0_createList_GE(x1, x3, x4)
487_0_createList_Return(x1) → 487_0_createList_Return
301_0_createList_Return(x1) → 301_0_createList_Return
250_0_createList_Return(x1, x2) → 250_0_createList_Return

Filtered duplicate args:



236_0_createList_GE(x1, x2) → 236_0_createList_GE(x2)
Cond_236_0_createList_GE(x1, x2, x3) → Cond_236_0_createList_GE(x1, x3)

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


P rules:
236_0_createList_GE(x0) → 272_1_createList_InvokeMethod(236_0_createList_GE(-(x0, 1)), -(x0, 1)) | >(x0, -1)
R rules:
236_0_createList_GE(-1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, -1) → 301_0_createList_Return
272_1_createList_InvokeMethod(301_0_createList_Return, x0) → 487_0_createList_Return
272_1_createList_InvokeMethod(487_0_createList_Return, x0) → 487_0_createList_Return

Performed bisimulation on rules. Used the following equivalence classes: {[250_0_createList_Return, 301_0_createList_Return, 487_0_createList_Return]=250_0_createList_Return}


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


P rules:
236_0_CREATELIST_GE(x0) → COND_236_0_CREATELIST_GE(>(x0, -1), x0)
COND_236_0_CREATELIST_GE(TRUE, x0) → 236_0_CREATELIST_GE(-(x0, 1))
R rules:
236_0_createList_GE(-1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, -1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, x0) → 250_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:
236_0_createList_GE(-1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, -1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, x0) → 250_0_createList_Return

The integer pair graph contains the following rules and edges:
(0): 236_0_CREATELIST_GE(x0[0]) → COND_236_0_CREATELIST_GE(x0[0] > -1, x0[0])
(1): COND_236_0_CREATELIST_GE(TRUE, x0[1]) → 236_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:
236_0_createList_GE(-1)
272_1_createList_InvokeMethod(250_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@3996a317 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 236_0_CREATELIST_GE(x0) → COND_236_0_CREATELIST_GE(>(x0, -1), x0) the following chains were created:
  • We consider the chain 236_0_CREATELIST_GE(x0[0]) → COND_236_0_CREATELIST_GE(>(x0[0], -1), x0[0]), COND_236_0_CREATELIST_GE(TRUE, x0[1]) → 236_0_CREATELIST_GE(-(x0[1], 1)) which results in the following constraint:

    (1)    (>(x0[0], -1)=TRUEx0[0]=x0[1]236_0_CREATELIST_GE(x0[0])≥NonInfC∧236_0_CREATELIST_GE(x0[0])≥COND_236_0_CREATELIST_GE(>(x0[0], -1), x0[0])∧(UIncreasing(COND_236_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)=TRUE236_0_CREATELIST_GE(x0[0])≥NonInfC∧236_0_CREATELIST_GE(x0[0])≥COND_236_0_CREATELIST_GE(>(x0[0], -1), x0[0])∧(UIncreasing(COND_236_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_236_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_236_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_236_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_236_0_CREATELIST_GE(TRUE, x0) → 236_0_CREATELIST_GE(-(x0, 1)) the following chains were created:
  • We consider the chain COND_236_0_CREATELIST_GE(TRUE, x0[1]) → 236_0_CREATELIST_GE(-(x0[1], 1)) which results in the following constraint:

    (6)    (COND_236_0_CREATELIST_GE(TRUE, x0[1])≥NonInfC∧COND_236_0_CREATELIST_GE(TRUE, x0[1])≥236_0_CREATELIST_GE(-(x0[1], 1))∧(UIncreasing(236_0_CREATELIST_GE(-(x0[1], 1))), ≥))



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

    (7)    ((UIncreasing(236_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(236_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(236_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(236_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.
  • 236_0_CREATELIST_GE(x0) → COND_236_0_CREATELIST_GE(>(x0, -1), x0)
    • (x0[0] ≥ 0 ⇒ (UIncreasing(COND_236_0_CREATELIST_GE(>(x0[0], -1), x0[0])), ≥)∧[(-1)Bound*bni_11] + [(2)bni_11]x0[0] ≥ 0∧[(-1)bso_12] ≥ 0)

  • COND_236_0_CREATELIST_GE(TRUE, x0) → 236_0_CREATELIST_GE(-(x0, 1))
    • ((UIncreasing(236_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(236_0_createList_GE(x1)) = [-1]   
POL(-1) = [-1]   
POL(250_0_createList_Return) = [-1]   
POL(272_1_createList_InvokeMethod(x1, x2)) = [-1]   
POL(236_0_CREATELIST_GE(x1)) = [2]x1   
POL(COND_236_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_236_0_CREATELIST_GE(TRUE, x0[1]) → 236_0_CREATELIST_GE(-(x0[1], 1))

The following pairs are in Pbound:

236_0_CREATELIST_GE(x0[0]) → COND_236_0_CREATELIST_GE(>(x0[0], -1), x0[0])

The following pairs are in P:

236_0_CREATELIST_GE(x0[0]) → COND_236_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:
236_0_createList_GE(-1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, -1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, x0) → 250_0_createList_Return

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


The set Q consists of the following terms:
236_0_createList_GE(-1)
272_1_createList_InvokeMethod(250_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:
236_0_createList_GE(-1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, -1) → 250_0_createList_Return
272_1_createList_InvokeMethod(250_0_createList_Return, x0) → 250_0_createList_Return

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


The set Q consists of the following terms:
236_0_createList_GE(-1)
272_1_createList_InvokeMethod(250_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