(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: CountMetaList
public class CountMetaList {
public static void main(String[] args) {
Random.args = args;
List l = createMetaList();

int count = countMetaList(l);
}

public static int countMetaList(List cur) {
int res = 0;
while (cur != null) {
if (cur.value instanceof List) {
List inner = (List) cur.value;
cur.value = inner.next;
cur = new List(inner.value, cur);
}
cur = cur.next;
res++;
}

return res;
}

public static List createMetaList() {
int count = Random.random();
List cur = null;
for (int i = 0; i < count; i++) {
int innerCount = Random.random();
List innerList = null;
for (int j = innerCount; j > 0; j--) {
innerList = new List(null, innerList);
}
cur = new List(innerList, cur);
}

return cur;
}
}

class List {
Object value;
List next;

public List(Object v, List n) {
this.value = v;
this.next = n;
}
}


public class Random {
static String[] args;
static int index = 0;

public static int random() {
String string = args[index];
index++;
return string.length();
}
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CountMetaList.main([Ljava/lang/String;)V: Graph of 201 nodes with 1 SCC.

CountMetaList.createMetaList()LList;: Graph of 195 nodes with 1 SCC.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountMetaList.createMetaList()LList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 69 rules for P and 0 rules for R.


P rules:
2361_0_createMetaList_Load(EOS(STATIC_2361), i77, i476, i476) → 2369_0_createMetaList_GE(EOS(STATIC_2369), i77, i476, i476, i77)
2369_0_createMetaList_GE(EOS(STATIC_2369), i77, i476, i476, i77) → 2377_0_createMetaList_GE(EOS(STATIC_2377), i77, i476, i476, i77)
2377_0_createMetaList_GE(EOS(STATIC_2377), i77, i476, i476, i77) → 2396_0_createMetaList_InvokeMethod(EOS(STATIC_2396), i77, i476) | <(i476, i77)
2396_0_createMetaList_InvokeMethod(EOS(STATIC_2396), i77, i476) → 2426_0_random_FieldAccess(EOS(STATIC_2426), i77, i476)
2426_0_random_FieldAccess(EOS(STATIC_2426), i77, i476) → 2453_0_random_FieldAccess(EOS(STATIC_2453), i77, i476)
2453_0_random_FieldAccess(EOS(STATIC_2453), i77, i476) → 2467_0_random_ArrayAccess(EOS(STATIC_2467), i77, i476)
2467_0_random_ArrayAccess(EOS(STATIC_2467), i77, i476) → 2476_0_random_ArrayAccess(EOS(STATIC_2476), i77, i476)
2476_0_random_ArrayAccess(EOS(STATIC_2476), i77, i476) → 2485_0_random_Store(EOS(STATIC_2485), i77, i476, o1984)
2485_0_random_Store(EOS(STATIC_2485), i77, i476, o1984) → 2496_0_random_FieldAccess(EOS(STATIC_2496), i77, i476, o1984)
2496_0_random_FieldAccess(EOS(STATIC_2496), i77, i476, o1984) → 2499_0_random_ConstantStackPush(EOS(STATIC_2499), i77, i476, o1984)
2499_0_random_ConstantStackPush(EOS(STATIC_2499), i77, i476, o1984) → 2505_0_random_IntArithmetic(EOS(STATIC_2505), i77, i476, o1984)
2505_0_random_IntArithmetic(EOS(STATIC_2505), i77, i476, o1984) → 2511_0_random_FieldAccess(EOS(STATIC_2511), i77, i476, o1984)
2511_0_random_FieldAccess(EOS(STATIC_2511), i77, i476, o1984) → 2516_0_random_Load(EOS(STATIC_2516), i77, i476, o1984)
2516_0_random_Load(EOS(STATIC_2516), i77, i476, o1984) → 2526_0_random_InvokeMethod(EOS(STATIC_2526), i77, i476, o1984)
2526_0_random_InvokeMethod(EOS(STATIC_2526), i77, i476, java.lang.Object(o2019sub)) → 2533_0_random_InvokeMethod(EOS(STATIC_2533), i77, i476, java.lang.Object(o2019sub))
2533_0_random_InvokeMethod(EOS(STATIC_2533), i77, i476, java.lang.Object(o2019sub)) → 2541_0_length_Load(EOS(STATIC_2541), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub))
2541_0_length_Load(EOS(STATIC_2541), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub)) → 2567_0_length_FieldAccess(EOS(STATIC_2567), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub))
2567_0_length_FieldAccess(EOS(STATIC_2567), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), java.lang.Object(java.lang.String(o2111sub, i531))) → 2587_0_length_FieldAccess(EOS(STATIC_2587), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), java.lang.Object(java.lang.String(o2111sub, i531))) | &&(>=(i531, 0), >=(i532, 0))
2587_0_length_FieldAccess(EOS(STATIC_2587), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), java.lang.Object(java.lang.String(o2111sub, i531))) → 2603_0_length_Return(EOS(STATIC_2603), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), i531)
2603_0_length_Return(EOS(STATIC_2603), i77, i476, java.lang.Object(java.lang.String(o2111sub, i531)), i531) → 2618_0_random_Return(EOS(STATIC_2618), i77, i476, i531)
2618_0_random_Return(EOS(STATIC_2618), i77, i476, i531) → 2629_0_createMetaList_Store(EOS(STATIC_2629), i77, i476, i531)
2629_0_createMetaList_Store(EOS(STATIC_2629), i77, i476, i531) → 2640_0_createMetaList_ConstantStackPush(EOS(STATIC_2640), i77, i476, i531)
2640_0_createMetaList_ConstantStackPush(EOS(STATIC_2640), i77, i476, i531) → 2650_0_createMetaList_Store(EOS(STATIC_2650), i77, i476, i531)
2650_0_createMetaList_Store(EOS(STATIC_2650), i77, i476, i531) → 2662_0_createMetaList_Load(EOS(STATIC_2662), i77, i476, i531)
2662_0_createMetaList_Load(EOS(STATIC_2662), i77, i476, i531) → 2669_0_createMetaList_Store(EOS(STATIC_2669), i77, i476, i531)
2669_0_createMetaList_Store(EOS(STATIC_2669), i77, i476, i531) → 2678_0_createMetaList_Load(EOS(STATIC_2678), i77, i476, i531)
2678_0_createMetaList_Load(EOS(STATIC_2678), i77, i476, i531) → 2935_0_createMetaList_Load(EOS(STATIC_2935), i77, i476, i531)
2935_0_createMetaList_Load(EOS(STATIC_2935), i77, i476, i603) → 2941_0_createMetaList_LE(EOS(STATIC_2941), i77, i476, i603, i603)
2941_0_createMetaList_LE(EOS(STATIC_2941), i77, i476, matching1, matching2) → 2946_0_createMetaList_LE(EOS(STATIC_2946), i77, i476, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
2941_0_createMetaList_LE(EOS(STATIC_2941), i77, i476, i608, i608) → 2947_0_createMetaList_LE(EOS(STATIC_2947), i77, i476, i608, i608)
2946_0_createMetaList_LE(EOS(STATIC_2946), i77, i476, matching1, matching2) → 2951_0_createMetaList_New(EOS(STATIC_2951), i77, i476) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
2951_0_createMetaList_New(EOS(STATIC_2951), i77, i476) → 2954_0_createMetaList_Duplicate(EOS(STATIC_2954), i77, i476)
2954_0_createMetaList_Duplicate(EOS(STATIC_2954), i77, i476) → 2959_0_createMetaList_Load(EOS(STATIC_2959), i77, i476)
2959_0_createMetaList_Load(EOS(STATIC_2959), i77, i476) → 2965_0_createMetaList_Load(EOS(STATIC_2965), i77, i476)
2965_0_createMetaList_Load(EOS(STATIC_2965), i77, i476) → 2972_0_createMetaList_InvokeMethod(EOS(STATIC_2972), i77, i476)
2972_0_createMetaList_InvokeMethod(EOS(STATIC_2972), i77, i476) → 2976_0_<init>_Load(EOS(STATIC_2976), i77, i476)
2976_0_<init>_Load(EOS(STATIC_2976), i77, i476) → 2988_0_<init>_InvokeMethod(EOS(STATIC_2988), i77, i476)
2988_0_<init>_InvokeMethod(EOS(STATIC_2988), i77, i476) → 2995_0_<init>_Load(EOS(STATIC_2995), i77, i476)
2995_0_<init>_Load(EOS(STATIC_2995), i77, i476) → 3002_0_<init>_Load(EOS(STATIC_3002), i77, i476)
3002_0_<init>_Load(EOS(STATIC_3002), i77, i476) → 3009_0_<init>_FieldAccess(EOS(STATIC_3009), i77, i476)
3009_0_<init>_FieldAccess(EOS(STATIC_3009), i77, i476) → 3019_0_<init>_Load(EOS(STATIC_3019), i77, i476)
3019_0_<init>_Load(EOS(STATIC_3019), i77, i476) → 3028_0_<init>_Load(EOS(STATIC_3028), i77, i476)
3028_0_<init>_Load(EOS(STATIC_3028), i77, i476) → 3036_0_<init>_FieldAccess(EOS(STATIC_3036), i77, i476)
3036_0_<init>_FieldAccess(EOS(STATIC_3036), i77, i476) → 3044_0_<init>_Return(EOS(STATIC_3044), i77, i476)
3044_0_<init>_Return(EOS(STATIC_3044), i77, i476) → 3052_0_createMetaList_Store(EOS(STATIC_3052), i77, i476)
3052_0_createMetaList_Store(EOS(STATIC_3052), i77, i476) → 3062_0_createMetaList_Inc(EOS(STATIC_3062), i77, i476)
3062_0_createMetaList_Inc(EOS(STATIC_3062), i77, i476) → 3066_0_createMetaList_JMP(EOS(STATIC_3066), i77, +(i476, 1)) | >=(i476, 0)
3066_0_createMetaList_JMP(EOS(STATIC_3066), i77, i618) → 3072_0_createMetaList_Load(EOS(STATIC_3072), i77, i618)
3072_0_createMetaList_Load(EOS(STATIC_3072), i77, i618) → 2354_0_createMetaList_Load(EOS(STATIC_2354), i77, i618)
2354_0_createMetaList_Load(EOS(STATIC_2354), i77, i476) → 2361_0_createMetaList_Load(EOS(STATIC_2361), i77, i476, i476)
2947_0_createMetaList_LE(EOS(STATIC_2947), i77, i476, i608, i608) → 2952_0_createMetaList_New(EOS(STATIC_2952), i77, i476, i608) | >(i608, 0)
2952_0_createMetaList_New(EOS(STATIC_2952), i77, i476, i608) → 2955_0_createMetaList_Duplicate(EOS(STATIC_2955), i77, i476, i608)
2955_0_createMetaList_Duplicate(EOS(STATIC_2955), i77, i476, i608) → 2961_0_createMetaList_ConstantStackPush(EOS(STATIC_2961), i77, i476, i608)
2961_0_createMetaList_ConstantStackPush(EOS(STATIC_2961), i77, i476, i608) → 2967_0_createMetaList_Load(EOS(STATIC_2967), i77, i476, i608)
2967_0_createMetaList_Load(EOS(STATIC_2967), i77, i476, i608) → 2973_0_createMetaList_InvokeMethod(EOS(STATIC_2973), i77, i476, i608)
2973_0_createMetaList_InvokeMethod(EOS(STATIC_2973), i77, i476, i608) → 2978_0_<init>_Load(EOS(STATIC_2978), i77, i476, i608)
2978_0_<init>_Load(EOS(STATIC_2978), i77, i476, i608) → 2990_0_<init>_InvokeMethod(EOS(STATIC_2990), i77, i476, i608)
2990_0_<init>_InvokeMethod(EOS(STATIC_2990), i77, i476, i608) → 2996_0_<init>_Load(EOS(STATIC_2996), i77, i476, i608)
2996_0_<init>_Load(EOS(STATIC_2996), i77, i476, i608) → 3004_0_<init>_Load(EOS(STATIC_3004), i77, i476, i608)
3004_0_<init>_Load(EOS(STATIC_3004), i77, i476, i608) → 3011_0_<init>_FieldAccess(EOS(STATIC_3011), i77, i476, i608)
3011_0_<init>_FieldAccess(EOS(STATIC_3011), i77, i476, i608) → 3021_0_<init>_Load(EOS(STATIC_3021), i77, i476, i608)
3021_0_<init>_Load(EOS(STATIC_3021), i77, i476, i608) → 3030_0_<init>_Load(EOS(STATIC_3030), i77, i476, i608)
3030_0_<init>_Load(EOS(STATIC_3030), i77, i476, i608) → 3037_0_<init>_FieldAccess(EOS(STATIC_3037), i77, i476, i608)
3037_0_<init>_FieldAccess(EOS(STATIC_3037), i77, i476, i608) → 3046_0_<init>_Return(EOS(STATIC_3046), i77, i476, i608)
3046_0_<init>_Return(EOS(STATIC_3046), i77, i476, i608) → 3053_0_createMetaList_Store(EOS(STATIC_3053), i77, i476, i608)
3053_0_createMetaList_Store(EOS(STATIC_3053), i77, i476, i608) → 3064_0_createMetaList_Inc(EOS(STATIC_3064), i77, i476, i608)
3064_0_createMetaList_Inc(EOS(STATIC_3064), i77, i476, i608) → 3068_0_createMetaList_JMP(EOS(STATIC_3068), i77, i476, +(i608, -1)) | >(i608, 0)
3068_0_createMetaList_JMP(EOS(STATIC_3068), i77, i476, i619) → 3074_0_createMetaList_Load(EOS(STATIC_3074), i77, i476, i619)
3074_0_createMetaList_Load(EOS(STATIC_3074), i77, i476, i619) → 2935_0_createMetaList_Load(EOS(STATIC_2935), i77, i476, i619)
R rules:

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


P rules:
2941_0_createMetaList_LE(EOS(STATIC_2941), x0, x1, 0, 0) → 2941_0_createMetaList_LE(EOS(STATIC_2941), x0, +(x1, 1), x4, x4) | &&(&&(>(+(x4, 1), 0), >(+(x1, 1), 0)), >(x0, +(x1, 1)))
2941_0_createMetaList_LE(EOS(STATIC_2941), x0, x1, x2, x2) → 2941_0_createMetaList_LE(EOS(STATIC_2941), x0, x1, +(x2, -1), +(x2, -1)) | >(x2, 0)
R rules:

Filtered ground terms:



2941_0_createMetaList_LE(x1, x2, x3, x4, x5) → 2941_0_createMetaList_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_2941_0_createMetaList_LE1(x1, x2, x3, x4, x5, x6) → Cond_2941_0_createMetaList_LE1(x1, x3, x4, x5, x6)
Cond_2941_0_createMetaList_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_2941_0_createMetaList_LE(x1, x3, x4, x7)

Filtered duplicate args:



2941_0_createMetaList_LE(x1, x2, x3, x4) → 2941_0_createMetaList_LE(x1, x2, x4)
Cond_2941_0_createMetaList_LE1(x1, x2, x3, x4, x5) → Cond_2941_0_createMetaList_LE1(x1, x2, x3, x5)

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


P rules:
2941_0_createMetaList_LE(x0, x1, 0) → 2941_0_createMetaList_LE(x0, +(x1, 1), x4) | &&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1)))
2941_0_createMetaList_LE(x0, x1, x2) → 2941_0_createMetaList_LE(x0, x1, +(x2, -1)) | >(x2, 0)
R rules:

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


P rules:
2941_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
COND_2941_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2941_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
2941_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2941_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
COND_2941_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2941_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
R rules:

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(1): COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], x1[1] + 1, x4[1])
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(0) -> (1), if (x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1x0[0]* x0[1]x1[0]* x1[1]x4[0]* x4[1])


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


(1) -> (2), if (x0[1]* x0[2]x1[1] + 1* x1[2]x4[1]* x2[2])


(2) -> (3), if (x2[2] > 0x0[2]* x0[3]x1[2]* x1[3]x2[2]* x2[3])


(3) -> (0), if (x0[3]* x0[0]x1[3]* x1[0]x2[3] + -1* 0)


(3) -> (2), if (x0[3]* x0[2]x1[3]* x1[2]x2[3] + -1* x2[2])



The set Q is empty.

(8) 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.IdpDefaultShapeHeuristic@1bec079e 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 2941_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4) the following chains were created:
  • We consider the chain COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]) which results in the following constraint:

    (1)    (x0[1]=x0[0]+(x1[1], 1)=x1[0]x4[1]=0&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUEx0[0]=x0[1]1x1[0]=x1[1]1x4[0]=x4[1]12941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))



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

    (2)    (>(x0[0], +(+(x1[1], 1), 1))=TRUE>(x4[0], -1)=TRUE>(+(x1[1], 1), -1)=TRUE2941_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(+(x1[1], 1), -1)), >(x0[0], +(+(x1[1], 1), 1))), x0[0], +(x1[1], 1), 0, x4[0])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))



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

    (3)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



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

    (4)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



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

    (5)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (6)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



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

    (7)    (x0[0] ≥ 0∧x4[0] ≥ 0∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)


    (8)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



  • We consider the chain COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]) which results in the following constraint:

    (9)    (x0[3]=x0[0]x1[3]=x1[0]+(x2[3], -1)=0&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUEx0[0]=x0[1]x1[0]=x1[1]x4[0]=x4[1]2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))



    We simplified constraint (9) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (10)    (+(x2[3], -1)=0>(x0[0], +(x1[0], 1))=TRUE>(x4[0], -1)=TRUE>(x1[0], -1)=TRUE2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))



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

    (11)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



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

    (12)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



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

    (13)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (x2[3] + [-1] ≥ 0∧x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)







For Pair COND_2941_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2941_0_CREATEMETALIST_LE(x0, +(x1, 1), x4) the following chains were created:
  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]) which results in the following constraint:

    (15)    (&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUEx0[0]=x0[1]x1[0]=x1[1]x4[0]=x4[1]x0[1]=x0[0]1+(x1[1], 1)=x1[0]1x4[1]=0COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))



    We simplified constraint (15) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:

    (16)    (>(x0[0], +(x1[0], 1))=TRUE>(x1[0], -1)=TRUECOND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥2941_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), 0)∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))



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

    (17)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



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

    (18)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



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

    (19)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (20)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:

    (21)    (&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUEx0[0]=x0[1]x1[0]=x1[1]x4[0]=x4[1]x0[1]=x0[2]+(x1[1], 1)=x1[2]x4[1]=x2[2]COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))



    We simplified constraint (21) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (22)    (>(x0[0], +(x1[0], 1))=TRUE>(x4[0], -1)=TRUE>(x1[0], -1)=TRUECOND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥2941_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), x4[0])∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))



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

    (23)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



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

    (24)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



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

    (25)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)



    We simplified constraint (25) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (26)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)







For Pair 2941_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2941_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2) the following chains were created:
  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:

    (27)    (>(x2[2], 0)=TRUEx0[2]=x0[3]x1[2]=x1[3]x2[2]=x2[3]2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))



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

    (28)    (>(x2[2], 0)=TRUE2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))



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

    (29)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)



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

    (30)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)



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

    (31)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)



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

    (32)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)



    We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (33)    (x2[2] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)







For Pair COND_2941_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2941_0_CREATEMETALIST_LE(x0, x1, +(x2, -1)) the following chains were created:
  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]) which results in the following constraint:

    (34)    (>(x2[2], 0)=TRUEx0[2]=x0[3]x1[2]=x1[3]x2[2]=x2[3]x0[3]=x0[0]x1[3]=x1[0]+(x2[3], -1)=0COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))



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

    (35)    (>(x2[2], 0)=TRUE+(x2[2], -1)=0COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2941_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))



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

    (36)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)



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

    (37)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)



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

    (38)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)



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

    (39)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)



    We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (40)    (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)



  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:

    (41)    (>(x2[2], 0)=TRUEx0[2]=x0[3]x1[2]=x1[3]x2[2]=x2[3]x0[3]=x0[2]1x1[3]=x1[2]1+(x2[3], -1)=x2[2]1COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))



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

    (42)    (>(x2[2], 0)=TRUECOND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2941_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))



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

    (43)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)



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

    (44)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)



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

    (45)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)



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

    (46)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)



    We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (47)    (x2[2] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • 2941_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
    • (x0[0] ≥ 0∧x4[0] ≥ 0∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
    • (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
    • (x2[3] + [-1] ≥ 0∧x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

  • COND_2941_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2941_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
    • (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
    • (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

  • 2941_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2941_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
    • (x2[2] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

  • COND_2941_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2941_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
    • (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
    • (x2[2] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 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(2941_0_CREATEMETALIST_LE(x1, x2, x3)) = [-1] + [-1]x2 + x1   
POL(0) = 0   
POL(COND_2941_0_CREATEMETALIST_LE(x1, x2, x3, x4, x5)) = [-1] + [-1]x4 + [-1]x3 + x2 + [-1]x1   
POL(&&(x1, x2)) = 0   
POL(>(x1, x2)) = [-1]   
POL(-1) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(COND_2941_0_CREATEMETALIST_LE1(x1, x2, x3, x4)) = [-1] + [-1]x3 + x2   

The following pairs are in P>:

COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in Pbound:

2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
COND_2941_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2941_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P:

2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

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

&&(TRUE, TRUE)1TRUE1
&&(TRUE, FALSE)1FALSE1
&&(FALSE, TRUE)1FALSE1
&&(FALSE, FALSE)1FALSE1

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

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 2941_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2941_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(3) -> (0), if (x0[3]* x0[0]x1[3]* x1[0]x2[3] + -1* 0)


(3) -> (2), if (x0[3]* x0[2]x1[3]* x1[2]x2[3] + -1* x2[2])


(2) -> (3), if (x2[2] > 0x0[2]* x0[3]x1[2]* x1[3]x2[2]* x2[3])



The set Q is empty.

(10) IDependencyGraphProof (EQUIVALENT transformation)

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

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])

(3) -> (2), if (x0[3]* x0[2]x1[3]* x1[2]x2[3] + -1* x2[2])


(2) -> (3), if (x2[2] > 0x0[2]* x0[3]x1[2]* x1[3]x2[2]* x2[3])



The set Q is empty.

(12) 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.IdpDefaultShapeHeuristic@1bec079e 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 COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) the following chains were created:
  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:

    (1)    (>(x2[2], 0)=TRUEx0[2]=x0[3]x1[2]=x1[3]x2[2]=x2[3]x0[3]=x0[2]1x1[3]=x1[2]1+(x2[3], -1)=x2[2]1COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))



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

    (2)    (>(x2[2], 0)=TRUECOND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2941_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))



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

    (3)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)



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

    (4)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)



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

    (5)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)



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

    (6)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)



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

    (7)    (x2[2] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)







For Pair 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) the following chains were created:
  • We consider the chain 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:

    (8)    (>(x2[2], 0)=TRUEx0[2]=x0[3]x1[2]=x1[3]x2[2]=x2[3]2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))



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

    (9)    (>(x2[2], 0)=TRUE2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))



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

    (10)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)



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

    (11)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)



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

    (12)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)



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

    (13)    (x2[2] + [-1] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    (x2[2] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)







To summarize, we get the following constraints P for the following pairs.
  • COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
    • (x2[2] ≥ 0 ⇒ (UIncreasing(2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

  • 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
    • (x2[2] ≥ 0 ⇒ (UIncreasing(COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 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(COND_2941_0_CREATEMETALIST_LE1(x1, x2, x3, x4)) = [-1] + x4   
POL(2941_0_CREATEMETALIST_LE(x1, x2, x3)) = [-1] + x3   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   

The following pairs are in P>:

COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

The following pairs are in Pbound:

COND_2941_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2941_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

The following pairs are in P:

2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

There are no usable rules.

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Integer


R is empty.

The integer pair graph contains the following rules and edges:
(2): 2941_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2941_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])


The set Q is empty.

(14) IDependencyGraphProof (EQUIVALENT transformation)

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

(15) TRUE

(16) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountMetaList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(17) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 137 rules for P and 0 rules for R.


P rules:
3351_0_countMetaList_NULL(EOS(STATIC_3351), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3353_0_countMetaList_NULL(EOS(STATIC_3353), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3353_0_countMetaList_NULL(EOS(STATIC_3353), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3355_0_countMetaList_Load(EOS(STATIC_3355), o3582, java.lang.Object(o3590sub))
3355_0_countMetaList_Load(EOS(STATIC_3355), o3582, java.lang.Object(o3590sub)) → 3358_0_countMetaList_FieldAccess(EOS(STATIC_3358), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3358_0_countMetaList_FieldAccess(EOS(STATIC_3358), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3361_0_countMetaList_FieldAccess(EOS(STATIC_3361), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3358_0_countMetaList_FieldAccess(EOS(STATIC_3358), java.lang.Object(o3590sub), java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3362_0_countMetaList_FieldAccess(EOS(STATIC_3362), java.lang.Object(o3590sub), java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3361_0_countMetaList_FieldAccess(EOS(STATIC_3361), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593))) → 3365_0_countMetaList_FieldAccess(EOS(STATIC_3365), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593)))
3365_0_countMetaList_FieldAccess(EOS(STATIC_3365), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593))) → 3369_0_countMetaList_CheckCast(EOS(STATIC_3369), o3582, java.lang.Object(List(EOC, o3592, o3593)), o3592)
3369_0_countMetaList_CheckCast(EOS(STATIC_3369), o3582, java.lang.Object(List(EOC, java.lang.Object(o3609sub), o3593)), java.lang.Object(o3609sub)) → 3374_0_countMetaList_CheckCast(EOS(STATIC_3374), o3582, java.lang.Object(List(EOC, java.lang.Object(o3609sub), o3593)), java.lang.Object(o3609sub))
3369_0_countMetaList_CheckCast(EOS(STATIC_3369), o3582, java.lang.Object(List(EOC, NULL, o3593)), NULL) → 3375_0_countMetaList_CheckCast(EOS(STATIC_3375), o3582, java.lang.Object(List(EOC, NULL, o3593)), NULL)
3374_0_countMetaList_CheckCast(EOS(STATIC_3374), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3380_0_countMetaList_CheckCast(EOS(STATIC_3380), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3374_0_countMetaList_CheckCast(EOS(STATIC_3374), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), java.lang.Object(o3612sub)) → 3382_0_countMetaList_CheckCast(EOS(STATIC_3382), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), java.lang.Object(o3612sub))
3380_0_countMetaList_CheckCast(EOS(STATIC_3380), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3390_0_countMetaList_EQ(EOS(STATIC_3390), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), 1)
3390_0_countMetaList_EQ(EOS(STATIC_3390), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), matching1) → 3407_0_countMetaList_Load(EOS(STATIC_3407), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) | &&(>(1, 0), =(matching1, 1))
3407_0_countMetaList_Load(EOS(STATIC_3407), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3417_0_countMetaList_FieldAccess(EOS(STATIC_3417), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)))
3417_0_countMetaList_FieldAccess(EOS(STATIC_3417), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3429_0_countMetaList_CheckCast(EOS(STATIC_3429), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3429_0_countMetaList_CheckCast(EOS(STATIC_3429), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3438_0_countMetaList_Store(EOS(STATIC_3438), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3438_0_countMetaList_Store(EOS(STATIC_3438), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3444_0_countMetaList_Load(EOS(STATIC_3444), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3444_0_countMetaList_Load(EOS(STATIC_3444), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3450_0_countMetaList_Load(EOS(STATIC_3450), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)))
3450_0_countMetaList_Load(EOS(STATIC_3450), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3459_0_countMetaList_FieldAccess(EOS(STATIC_3459), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3459_0_countMetaList_FieldAccess(EOS(STATIC_3459), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3463_0_countMetaList_FieldAccess(EOS(STATIC_3463), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3459_0_countMetaList_FieldAccess(EOS(STATIC_3459), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3464_0_countMetaList_FieldAccess(EOS(STATIC_3464), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3463_0_countMetaList_FieldAccess(EOS(STATIC_3463), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3467_0_countMetaList_FieldAccess(EOS(STATIC_3467), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)))
3467_0_countMetaList_FieldAccess(EOS(STATIC_3467), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3473_0_countMetaList_FieldAccess(EOS(STATIC_3473), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), o3797)
3473_0_countMetaList_FieldAccess(EOS(STATIC_3473), o3582, java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3796, o3797)), o3593)), o3797) → 3480_0_countMetaList_New(EOS(STATIC_3480), o3582put, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)))
3480_0_countMetaList_New(EOS(STATIC_3480), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3487_0_countMetaList_Duplicate(EOS(STATIC_3487), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)))
3487_0_countMetaList_Duplicate(EOS(STATIC_3487), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL))) → 3493_0_countMetaList_Load(EOS(STATIC_3493), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
3493_0_countMetaList_Load(EOS(STATIC_3493), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 3501_0_countMetaList_FieldAccess(EOS(STATIC_3501), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3796, o3797)))
3501_0_countMetaList_FieldAccess(EOS(STATIC_3501), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3796, o3797))) → 3508_0_countMetaList_Load(EOS(STATIC_3508), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796)
3508_0_countMetaList_Load(EOS(STATIC_3508), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796) → 3515_0_countMetaList_InvokeMethod(EOS(STATIC_3515), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3515_0_countMetaList_InvokeMethod(EOS(STATIC_3515), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3520_0_<init>_Load(EOS(STATIC_3520), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3520_0_<init>_Load(EOS(STATIC_3520), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3525_0_<init>_InvokeMethod(EOS(STATIC_3525), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3525_0_<init>_InvokeMethod(EOS(STATIC_3525), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3531_0_<init>_Load(EOS(STATIC_3531), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3531_0_<init>_Load(EOS(STATIC_3531), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3537_0_<init>_Load(EOS(STATIC_3537), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3537_0_<init>_Load(EOS(STATIC_3537), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3543_0_<init>_FieldAccess(EOS(STATIC_3543), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796)
3543_0_<init>_FieldAccess(EOS(STATIC_3543), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3796) → 3550_0_<init>_Load(EOS(STATIC_3550), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593)))
3550_0_<init>_Load(EOS(STATIC_3550), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593))) → 3557_0_<init>_Load(EOS(STATIC_3557), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)))
3557_0_<init>_Load(EOS(STATIC_3557), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL))) → 3563_0_<init>_FieldAccess(EOS(STATIC_3563), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593)))
3563_0_<init>_FieldAccess(EOS(STATIC_3563), o3582, java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3796, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, NULL)), java.lang.Object(List(EOC, o3797, o3593))) → 3571_0_<init>_Return(EOS(STATIC_3571), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3571_0_<init>_Return(EOS(STATIC_3571), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))), o3796, java.lang.Object(List(EOC, o3797, o3593))) → 3579_0_countMetaList_Store(EOS(STATIC_3579), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3579_0_countMetaList_Store(EOS(STATIC_3579), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3589_0_countMetaList_Load(EOS(STATIC_3589), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3589_0_countMetaList_Load(EOS(STATIC_3589), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3601_0_countMetaList_FieldAccess(EOS(STATIC_3601), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3601_0_countMetaList_FieldAccess(EOS(STATIC_3601), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3610_0_countMetaList_Store(EOS(STATIC_3610), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3610_0_countMetaList_Store(EOS(STATIC_3610), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3617_0_countMetaList_Inc(EOS(STATIC_3617), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3617_0_countMetaList_Inc(EOS(STATIC_3617), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3625_0_countMetaList_JMP(EOS(STATIC_3625), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3625_0_countMetaList_JMP(EOS(STATIC_3625), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3633_0_countMetaList_Load(EOS(STATIC_3633), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3633_0_countMetaList_Load(EOS(STATIC_3633), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3348_0_countMetaList_Load(EOS(STATIC_3348), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3348_0_countMetaList_Load(EOS(STATIC_3348), o3582, o3581) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), o3582, o3581, o3581)
3464_0_countMetaList_FieldAccess(EOS(STATIC_3464), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3469_0_countMetaList_FieldAccess(EOS(STATIC_3469), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)))
3469_0_countMetaList_FieldAccess(EOS(STATIC_3469), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3476_0_countMetaList_FieldAccess(EOS(STATIC_3476), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), o3800)
3476_0_countMetaList_FieldAccess(EOS(STATIC_3476), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3799, o3800)), o3593)), o3800) → 3483_0_countMetaList_New(EOS(STATIC_3483), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)))
3483_0_countMetaList_New(EOS(STATIC_3483), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3490_0_countMetaList_Duplicate(EOS(STATIC_3490), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)))
3490_0_countMetaList_Duplicate(EOS(STATIC_3490), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL))) → 3497_0_countMetaList_Load(EOS(STATIC_3497), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
3497_0_countMetaList_Load(EOS(STATIC_3497), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 3504_0_countMetaList_FieldAccess(EOS(STATIC_3504), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3799, o3800)))
3504_0_countMetaList_FieldAccess(EOS(STATIC_3504), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3799, o3800))) → 3511_0_countMetaList_Load(EOS(STATIC_3511), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799)
3511_0_countMetaList_Load(EOS(STATIC_3511), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799) → 3517_0_countMetaList_InvokeMethod(EOS(STATIC_3517), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3517_0_countMetaList_InvokeMethod(EOS(STATIC_3517), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3521_0_<init>_Load(EOS(STATIC_3521), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3521_0_<init>_Load(EOS(STATIC_3521), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3528_0_<init>_InvokeMethod(EOS(STATIC_3528), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3528_0_<init>_InvokeMethod(EOS(STATIC_3528), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3533_0_<init>_Load(EOS(STATIC_3533), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3533_0_<init>_Load(EOS(STATIC_3533), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3540_0_<init>_Load(EOS(STATIC_3540), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)))
3540_0_<init>_Load(EOS(STATIC_3540), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL))) → 3546_0_<init>_FieldAccess(EOS(STATIC_3546), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799)
3546_0_<init>_FieldAccess(EOS(STATIC_3546), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, NULL, NULL)), o3799) → 3554_0_<init>_Load(EOS(STATIC_3554), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593)))
3554_0_<init>_Load(EOS(STATIC_3554), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593))) → 3559_0_<init>_Load(EOS(STATIC_3559), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)))
3559_0_<init>_Load(EOS(STATIC_3559), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL))) → 3565_0_<init>_FieldAccess(EOS(STATIC_3565), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593)))
3565_0_<init>_FieldAccess(EOS(STATIC_3565), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3799, NULL)), o3799, java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, NULL)), java.lang.Object(List(EOC, o3800, o3593))) → 3575_0_<init>_Return(EOS(STATIC_3575), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), o3799, java.lang.Object(List(EOC, o3800, o3593)))
3575_0_<init>_Return(EOS(STATIC_3575), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))), o3799, java.lang.Object(List(EOC, o3800, o3593))) → 3582_0_countMetaList_Store(EOS(STATIC_3582), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3582_0_countMetaList_Store(EOS(STATIC_3582), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3594_0_countMetaList_Load(EOS(STATIC_3594), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3594_0_countMetaList_Load(EOS(STATIC_3594), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3606_0_countMetaList_FieldAccess(EOS(STATIC_3606), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3606_0_countMetaList_FieldAccess(EOS(STATIC_3606), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3613_0_countMetaList_Store(EOS(STATIC_3613), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3613_0_countMetaList_Store(EOS(STATIC_3613), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3620_0_countMetaList_Inc(EOS(STATIC_3620), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3620_0_countMetaList_Inc(EOS(STATIC_3620), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3627_0_countMetaList_JMP(EOS(STATIC_3627), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3627_0_countMetaList_JMP(EOS(STATIC_3627), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3635_0_countMetaList_Load(EOS(STATIC_3635), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3635_0_countMetaList_Load(EOS(STATIC_3635), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3348_0_countMetaList_Load(EOS(STATIC_3348), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3382_0_countMetaList_CheckCast(EOS(STATIC_3382), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), java.lang.Object(o3612sub)) → 3395_0_countMetaList_EQ(EOS(STATIC_3395), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), 0)
3395_0_countMetaList_EQ(EOS(STATIC_3395), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)), matching1) → 3409_0_countMetaList_Load(EOS(STATIC_3409), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) | =(matching1, 0)
3409_0_countMetaList_Load(EOS(STATIC_3409), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) → 3420_0_countMetaList_FieldAccess(EOS(STATIC_3420), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)))
3420_0_countMetaList_FieldAccess(EOS(STATIC_3420), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) → 3432_0_countMetaList_Store(EOS(STATIC_3432), o3582, o3593)
3432_0_countMetaList_Store(EOS(STATIC_3432), o3582, o3593) → 3439_0_countMetaList_Inc(EOS(STATIC_3439), o3582, o3593)
3439_0_countMetaList_Inc(EOS(STATIC_3439), o3582, o3593) → 3445_0_countMetaList_JMP(EOS(STATIC_3445), o3582, o3593)
3445_0_countMetaList_JMP(EOS(STATIC_3445), o3582, o3593) → 3453_0_countMetaList_Load(EOS(STATIC_3453), o3582, o3593)
3453_0_countMetaList_Load(EOS(STATIC_3453), o3582, o3593) → 3348_0_countMetaList_Load(EOS(STATIC_3348), o3582, o3593)
3375_0_countMetaList_CheckCast(EOS(STATIC_3375), o3582, java.lang.Object(List(EOC, NULL, o3593)), NULL) → 3383_0_countMetaList_EQ(EOS(STATIC_3383), o3582, java.lang.Object(List(EOC, NULL, o3593)), 0)
3383_0_countMetaList_EQ(EOS(STATIC_3383), o3582, java.lang.Object(List(EOC, NULL, o3593)), matching1) → 3396_0_countMetaList_Load(EOS(STATIC_3396), o3582, java.lang.Object(List(EOC, NULL, o3593))) | =(matching1, 0)
3396_0_countMetaList_Load(EOS(STATIC_3396), o3582, java.lang.Object(List(EOC, NULL, o3593))) → 3410_0_countMetaList_FieldAccess(EOS(STATIC_3410), o3582, java.lang.Object(List(EOC, NULL, o3593)))
3410_0_countMetaList_FieldAccess(EOS(STATIC_3410), o3582, java.lang.Object(List(EOC, NULL, o3593))) → 3421_0_countMetaList_Store(EOS(STATIC_3421), o3582, o3593)
3421_0_countMetaList_Store(EOS(STATIC_3421), o3582, o3593) → 3432_0_countMetaList_Store(EOS(STATIC_3432), o3582, o3593)
3362_0_countMetaList_FieldAccess(EOS(STATIC_3362), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596))) → 3366_0_countMetaList_FieldAccess(EOS(STATIC_3366), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)))
3366_0_countMetaList_FieldAccess(EOS(STATIC_3366), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596))) → 3372_0_countMetaList_CheckCast(EOS(STATIC_3372), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), o3595)
3372_0_countMetaList_CheckCast(EOS(STATIC_3372), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(o3610sub)) → 3377_0_countMetaList_CheckCast(EOS(STATIC_3377), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3610sub), o3596)), java.lang.Object(o3610sub))
3372_0_countMetaList_CheckCast(EOS(STATIC_3372), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), NULL) → 3378_0_countMetaList_CheckCast(EOS(STATIC_3378), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), NULL)
3377_0_countMetaList_CheckCast(EOS(STATIC_3377), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3386_0_countMetaList_CheckCast(EOS(STATIC_3386), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3377_0_countMetaList_CheckCast(EOS(STATIC_3377), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(o3614sub)) → 3387_0_countMetaList_CheckCast(EOS(STATIC_3387), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(o3614sub))
3386_0_countMetaList_CheckCast(EOS(STATIC_3386), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3399_0_countMetaList_EQ(EOS(STATIC_3399), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), 1)
3399_0_countMetaList_EQ(EOS(STATIC_3399), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), matching1) → 3412_0_countMetaList_Load(EOS(STATIC_3412), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) | &&(>(1, 0), =(matching1, 1))
3412_0_countMetaList_Load(EOS(STATIC_3412), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3423_0_countMetaList_FieldAccess(EOS(STATIC_3423), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)))
3423_0_countMetaList_FieldAccess(EOS(STATIC_3423), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3435_0_countMetaList_CheckCast(EOS(STATIC_3435), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3435_0_countMetaList_CheckCast(EOS(STATIC_3435), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3441_0_countMetaList_Store(EOS(STATIC_3441), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3441_0_countMetaList_Store(EOS(STATIC_3441), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3447_0_countMetaList_Load(EOS(STATIC_3447), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3447_0_countMetaList_Load(EOS(STATIC_3447), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3455_0_countMetaList_Load(EOS(STATIC_3455), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)))
3455_0_countMetaList_Load(EOS(STATIC_3455), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3462_0_countMetaList_FieldAccess(EOS(STATIC_3462), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3462_0_countMetaList_FieldAccess(EOS(STATIC_3462), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3466_0_countMetaList_FieldAccess(EOS(STATIC_3466), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)))
3466_0_countMetaList_FieldAccess(EOS(STATIC_3466), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3470_0_countMetaList_FieldAccess(EOS(STATIC_3470), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), o3794)
3470_0_countMetaList_FieldAccess(EOS(STATIC_3470), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o3793, o3794)), o3596)), o3794) → 3477_0_countMetaList_New(EOS(STATIC_3477), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)))
3477_0_countMetaList_New(EOS(STATIC_3477), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3485_0_countMetaList_Duplicate(EOS(STATIC_3485), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL)))
3485_0_countMetaList_Duplicate(EOS(STATIC_3485), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL))) → 3491_0_countMetaList_Load(EOS(STATIC_3491), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
3491_0_countMetaList_Load(EOS(STATIC_3491), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 3498_0_countMetaList_FieldAccess(EOS(STATIC_3498), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3793, o3794)))
3498_0_countMetaList_FieldAccess(EOS(STATIC_3498), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3793, o3794))) → 3505_0_countMetaList_Load(EOS(STATIC_3505), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793)
3505_0_countMetaList_Load(EOS(STATIC_3505), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793) → 3512_0_countMetaList_InvokeMethod(EOS(STATIC_3512), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3512_0_countMetaList_InvokeMethod(EOS(STATIC_3512), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3518_0_<init>_Load(EOS(STATIC_3518), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3518_0_<init>_Load(EOS(STATIC_3518), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3523_0_<init>_InvokeMethod(EOS(STATIC_3523), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)))
3523_0_<init>_InvokeMethod(EOS(STATIC_3523), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL))) → 3530_0_<init>_Load(EOS(STATIC_3530), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3530_0_<init>_Load(EOS(STATIC_3530), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3535_0_<init>_Load(EOS(STATIC_3535), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)))
3535_0_<init>_Load(EOS(STATIC_3535), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL))) → 3541_0_<init>_FieldAccess(EOS(STATIC_3541), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793)
3541_0_<init>_FieldAccess(EOS(STATIC_3541), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, NULL, NULL)), o3793) → 3548_0_<init>_Load(EOS(STATIC_3548), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596)))
3548_0_<init>_Load(EOS(STATIC_3548), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596))) → 3555_0_<init>_Load(EOS(STATIC_3555), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)))
3555_0_<init>_Load(EOS(STATIC_3555), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL))) → 3561_0_<init>_FieldAccess(EOS(STATIC_3561), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596)))
3561_0_<init>_FieldAccess(EOS(STATIC_3561), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3793, NULL)), o3793, java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, NULL)), java.lang.Object(List(EOC, o3794, o3596))) → 3568_0_<init>_Return(EOS(STATIC_3568), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), o3793, java.lang.Object(List(EOC, o3794, o3596)))
3568_0_<init>_Return(EOS(STATIC_3568), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))), o3793, java.lang.Object(List(EOC, o3794, o3596))) → 3576_0_countMetaList_Store(EOS(STATIC_3576), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))))
3576_0_countMetaList_Store(EOS(STATIC_3576), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596))))) → 3585_0_countMetaList_Load(EOS(STATIC_3585), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))))
3585_0_countMetaList_Load(EOS(STATIC_3585), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596))))) → 3597_0_countMetaList_FieldAccess(EOS(STATIC_3597), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596)))))
3597_0_countMetaList_FieldAccess(EOS(STATIC_3597), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, java.lang.Object(List(EOC, o3794, o3596))))) → 3608_0_countMetaList_Store(EOS(STATIC_3608), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3608_0_countMetaList_Store(EOS(STATIC_3608), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3615_0_countMetaList_Inc(EOS(STATIC_3615), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3615_0_countMetaList_Inc(EOS(STATIC_3615), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3622_0_countMetaList_JMP(EOS(STATIC_3622), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3622_0_countMetaList_JMP(EOS(STATIC_3622), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3630_0_countMetaList_Load(EOS(STATIC_3630), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3630_0_countMetaList_Load(EOS(STATIC_3630), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3348_0_countMetaList_Load(EOS(STATIC_3348), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3387_0_countMetaList_CheckCast(EOS(STATIC_3387), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(o3614sub)) → 3404_0_countMetaList_EQ(EOS(STATIC_3404), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), 0)
3404_0_countMetaList_EQ(EOS(STATIC_3404), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), matching1) → 3415_0_countMetaList_Load(EOS(STATIC_3415), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) | =(matching1, 0)
3415_0_countMetaList_Load(EOS(STATIC_3415), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) → 3426_0_countMetaList_FieldAccess(EOS(STATIC_3426), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)))
3426_0_countMetaList_FieldAccess(EOS(STATIC_3426), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) → 3437_0_countMetaList_Store(EOS(STATIC_3437), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3437_0_countMetaList_Store(EOS(STATIC_3437), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3442_0_countMetaList_Inc(EOS(STATIC_3442), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3442_0_countMetaList_Inc(EOS(STATIC_3442), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3449_0_countMetaList_JMP(EOS(STATIC_3449), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3449_0_countMetaList_JMP(EOS(STATIC_3449), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3457_0_countMetaList_Load(EOS(STATIC_3457), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3457_0_countMetaList_Load(EOS(STATIC_3457), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3348_0_countMetaList_Load(EOS(STATIC_3348), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3378_0_countMetaList_CheckCast(EOS(STATIC_3378), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), NULL) → 3388_0_countMetaList_EQ(EOS(STATIC_3388), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), 0)
3388_0_countMetaList_EQ(EOS(STATIC_3388), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)), matching1) → 3406_0_countMetaList_Load(EOS(STATIC_3406), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) | =(matching1, 0)
3406_0_countMetaList_Load(EOS(STATIC_3406), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) → 3416_0_countMetaList_FieldAccess(EOS(STATIC_3416), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)))
3416_0_countMetaList_FieldAccess(EOS(STATIC_3416), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) → 3427_0_countMetaList_Store(EOS(STATIC_3427), java.lang.Object(List(EOC, NULL, o3596)), o3596)
3427_0_countMetaList_Store(EOS(STATIC_3427), java.lang.Object(List(EOC, NULL, o3596)), o3596) → 3432_0_countMetaList_Store(EOS(STATIC_3432), java.lang.Object(List(EOC, NULL, o3596)), o3596)
R rules:

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


P rules:
3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x1, x2)), x3))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), x4, java.lang.Object(List(EOC, x2, x3)), java.lang.Object(List(EOC, x2, x3)))
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, x0, x1)), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2)))
3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, java.lang.Object(List(EOC, java.lang.Object(x1), x2)), java.lang.Object(List(EOC, java.lang.Object(x1), x2))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, x2, x2)
3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, java.lang.Object(List(EOC, NULL, x1)), java.lang.Object(List(EOC, NULL, x1))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), x0, x1, x1)
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2)))
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), java.lang.Object(List(EOC, java.lang.Object(x0), x1))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), x1, x1)
3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, NULL, x0)), java.lang.Object(List(EOC, NULL, x0)), java.lang.Object(List(EOC, NULL, x0))) → 3351_0_countMetaList_NULL(EOS(STATIC_3351), java.lang.Object(List(EOC, NULL, x0)), x0, x0)
R rules:

Filtered ground terms:



3351_0_countMetaList_NULL(x1, x2, x3, x4) → 3351_0_countMetaList_NULL(x2, x3, x4)
List(x1, x2, x3) → List(x2, x3)
EOS(x1) → EOS

Filtered duplicate args:



3351_0_countMetaList_NULL(x1, x2, x3) → 3351_0_countMetaList_NULL(x1, x3)

Filtered all free variables in P and R:



3351_0_countMetaList_NULL(x1, x2) → 3351_0_countMetaList_NULL(x2)

Current set of rules:


P rules:
3351_0_countMetaList_NULL(java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → 3351_0_countMetaList_NULL(java.lang.Object(List(x2, x3)))
3351_0_countMetaList_NULL(java.lang.Object(List(java.lang.Object(x1), x2))) → 3351_0_countMetaList_NULL(x2)
3351_0_countMetaList_NULL(java.lang.Object(List(NULL, x1))) → 3351_0_countMetaList_NULL(x1)
R rules:

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


P rules:
3351_0_countMetaList_NULL(java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → 3351_0_countMetaList_NULL(java.lang.Object(List(x2, x3)))
3351_0_countMetaList_NULL(java.lang.Object(List(java.lang.Object(x1), x2))) → 3351_0_countMetaList_NULL(x2)
3351_0_countMetaList_NULL(java.lang.Object(List(NULL, x1))) → 3351_0_countMetaList_NULL(x1)
R rules:

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


P rules:
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1, x2)), x3))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2, x3)))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1), x2))) → 3351_0_COUNTMETALIST_NULL(x2)
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1))) → 3351_0_COUNTMETALIST_NULL(x1)
R rules:

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph contains the following rules and edges:
(0): 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
(1): 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])
(2): 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1[2]))) → 3351_0_COUNTMETALIST_NULL(x1[2])

(0) -> (0), if (java.lang.Object(List(x2[0], x3[0])) →* java.lang.Object(List(java.lang.Object(List(x1[0]', x2[0]')), x3[0]')))


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


(0) -> (2), if (java.lang.Object(List(x2[0], x3[0])) →* java.lang.Object(List(NULL, x1[2])))


(1) -> (0), if (x2[1]* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))


(1) -> (1), if (x2[1]* java.lang.Object(List(java.lang.Object(x1[1]'), x2[1]')))


(1) -> (2), if (x2[1]* java.lang.Object(List(NULL, x1[2])))


(2) -> (0), if (x1[2]* java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0])))


(2) -> (1), if (x1[2]* java.lang.Object(List(java.lang.Object(x1[1]), x2[1])))


(2) -> (2), if (x1[2]* java.lang.Object(List(NULL, x1[2]')))



The set Q is empty.

(19) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(20) Obligation:

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

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1[2]))) → 3351_0_COUNTMETALIST_NULL(x1[2])

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

(21) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(NULL, x1[2]))) → 3351_0_COUNTMETALIST_NULL(x1[2])
No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(3351_0_COUNTMETALIST_NULL(x1)) = 2·x1   
POL(List(x1, x2)) = x1 + 2·x2   
POL(NULL) = 0   
POL(java.lang.Object(x1)) = 2·x1   

(22) Obligation:

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

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])

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

(23) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(List(x1[0], x2[0])), x3[0]))) → 3351_0_COUNTMETALIST_NULL(java.lang.Object(List(x2[0], x3[0])))
3351_0_COUNTMETALIST_NULL(java.lang.Object(List(java.lang.Object(x1[1]), x2[1]))) → 3351_0_COUNTMETALIST_NULL(x2[1])


Used ordering: Knuth-Bendix order [KBO] with precedence:
List2 > java.lang.Object1 > 33510COUNTMETALISTNULL1

and weight map:

3351_0_COUNTMETALIST_NULL_1=1
java.lang.Object_1=1
List_2=0

The variable weight is 1

(24) Obligation:

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

(25) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(26) YES