Termination proof of /tmp/tmpIuebvk/CountMetaList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1220 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 130 ms)

        ↳7 IDP

        ↳8 IDPNonInfProof (⇒, 1200 ms)

        ↳9 IDP

        ↳10 IDependencyGraphProof (⇔, 0 ms)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇒, 130 ms)

        ↳13 IDP

        ↳14 IDependencyGraphProof (⇔, 0 ms)

        ↳15 TRUE

    ↳16 JBCTerminationSCC

        ↳17 SCCToIDPv1Proof (⇒, 1590 ms)

        ↳18 IDP

        ↳19 IDPtoQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 UsableRulesReductionPairsProof (⇔, 0 ms)

        ↳22 QDP

        ↳23 MRRProof (⇔, 0 ms)

        ↳24 QDP

        ↳25 PisEmptyProof (⇔, 0 ms)

        ↳26 YES

(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:
2358_0_createMetaList_Load(EOS(STATIC_2358), i77, i476, i476) → 2366_0_createMetaList_GE(EOS(STATIC_2366), i77, i476, i476, i77)
2366_0_createMetaList_GE(EOS(STATIC_2366), i77, i476, i476, i77) → 2373_0_createMetaList_GE(EOS(STATIC_2373), i77, i476, i476, i77)
2373_0_createMetaList_GE(EOS(STATIC_2373), i77, i476, i476, i77) → 2393_0_createMetaList_InvokeMethod(EOS(STATIC_2393), i77, i476) | <(i476, i77)
2393_0_createMetaList_InvokeMethod(EOS(STATIC_2393), i77, i476) → 2423_0_random_FieldAccess(EOS(STATIC_2423), i77, i476)
2423_0_random_FieldAccess(EOS(STATIC_2423), i77, i476) → 2449_0_random_FieldAccess(EOS(STATIC_2449), i77, i476)
2449_0_random_FieldAccess(EOS(STATIC_2449), i77, i476) → 2462_0_random_ArrayAccess(EOS(STATIC_2462), i77, i476)
2462_0_random_ArrayAccess(EOS(STATIC_2462), i77, i476) → 2469_0_random_ArrayAccess(EOS(STATIC_2469), i77, i476)
2469_0_random_ArrayAccess(EOS(STATIC_2469), i77, i476) → 2478_0_random_Store(EOS(STATIC_2478), i77, i476, o1984)
2478_0_random_Store(EOS(STATIC_2478), i77, i476, o1984) → 2488_0_random_FieldAccess(EOS(STATIC_2488), i77, i476, o1984)
2488_0_random_FieldAccess(EOS(STATIC_2488), i77, i476, o1984) → 2492_0_random_ConstantStackPush(EOS(STATIC_2492), i77, i476, o1984)
2492_0_random_ConstantStackPush(EOS(STATIC_2492), i77, i476, o1984) → 2497_0_random_IntArithmetic(EOS(STATIC_2497), i77, i476, o1984)
2497_0_random_IntArithmetic(EOS(STATIC_2497), i77, i476, o1984) → 2503_0_random_FieldAccess(EOS(STATIC_2503), i77, i476, o1984)
2503_0_random_FieldAccess(EOS(STATIC_2503), i77, i476, o1984) → 2507_0_random_Load(EOS(STATIC_2507), i77, i476, o1984)
2507_0_random_Load(EOS(STATIC_2507), i77, i476, o1984) → 2515_0_random_InvokeMethod(EOS(STATIC_2515), i77, i476, o1984)
2515_0_random_InvokeMethod(EOS(STATIC_2515), i77, i476, java.lang.Object(o2019sub)) → 2522_0_random_InvokeMethod(EOS(STATIC_2522), i77, i476, java.lang.Object(o2019sub))
2522_0_random_InvokeMethod(EOS(STATIC_2522), i77, i476, java.lang.Object(o2019sub)) → 2531_0_length_Load(EOS(STATIC_2531), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub))
2531_0_length_Load(EOS(STATIC_2531), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub)) → 2561_0_length_FieldAccess(EOS(STATIC_2561), i77, i476, java.lang.Object(o2019sub), java.lang.Object(o2019sub))
2561_0_length_FieldAccess(EOS(STATIC_2561), i77, i476, java.lang.Object(java.lang.String(o2109sub, i531)), java.lang.Object(java.lang.String(o2109sub, i531))) → 2585_0_length_FieldAccess(EOS(STATIC_2585), i77, i476, java.lang.Object(java.lang.String(o2109sub, i531)), java.lang.Object(java.lang.String(o2109sub, i531))) | &&(>=(i531, 0), >=(i532, 0))
2585_0_length_FieldAccess(EOS(STATIC_2585), i77, i476, java.lang.Object(java.lang.String(o2109sub, i531)), java.lang.Object(java.lang.String(o2109sub, i531))) → 2601_0_length_Return(EOS(STATIC_2601), i77, i476, java.lang.Object(java.lang.String(o2109sub, i531)), i531)
2601_0_length_Return(EOS(STATIC_2601), i77, i476, java.lang.Object(java.lang.String(o2109sub, i531)), i531) → 2617_0_random_Return(EOS(STATIC_2617), i77, i476, i531)
2617_0_random_Return(EOS(STATIC_2617), i77, i476, i531) → 2626_0_createMetaList_Store(EOS(STATIC_2626), i77, i476, i531)
2626_0_createMetaList_Store(EOS(STATIC_2626), i77, i476, i531) → 2638_0_createMetaList_ConstantStackPush(EOS(STATIC_2638), i77, i476, i531)
2638_0_createMetaList_ConstantStackPush(EOS(STATIC_2638), i77, i476, i531) → 2649_0_createMetaList_Store(EOS(STATIC_2649), i77, i476, i531)
2649_0_createMetaList_Store(EOS(STATIC_2649), i77, i476, i531) → 2660_0_createMetaList_Load(EOS(STATIC_2660), i77, i476, i531)
2660_0_createMetaList_Load(EOS(STATIC_2660), i77, i476, i531) → 2667_0_createMetaList_Store(EOS(STATIC_2667), i77, i476, i531)
2667_0_createMetaList_Store(EOS(STATIC_2667), i77, i476, i531) → 2676_0_createMetaList_Load(EOS(STATIC_2676), i77, i476, i531)
2676_0_createMetaList_Load(EOS(STATIC_2676), i77, i476, i531) → 2929_0_createMetaList_Load(EOS(STATIC_2929), i77, i476, i531)
2929_0_createMetaList_Load(EOS(STATIC_2929), i77, i476, i602) → 2935_0_createMetaList_LE(EOS(STATIC_2935), i77, i476, i602, i602)
2935_0_createMetaList_LE(EOS(STATIC_2935), i77, i476, matching1, matching2) → 2939_0_createMetaList_LE(EOS(STATIC_2939), i77, i476, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
2935_0_createMetaList_LE(EOS(STATIC_2935), i77, i476, i606, i606) → 2940_0_createMetaList_LE(EOS(STATIC_2940), i77, i476, i606, i606)
2939_0_createMetaList_LE(EOS(STATIC_2939), i77, i476, matching1, matching2) → 2945_0_createMetaList_New(EOS(STATIC_2945), i77, i476) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
2945_0_createMetaList_New(EOS(STATIC_2945), i77, i476) → 2948_0_createMetaList_Duplicate(EOS(STATIC_2948), i77, i476)
2948_0_createMetaList_Duplicate(EOS(STATIC_2948), i77, i476) → 2954_0_createMetaList_Load(EOS(STATIC_2954), i77, i476)
2954_0_createMetaList_Load(EOS(STATIC_2954), i77, i476) → 2961_0_createMetaList_Load(EOS(STATIC_2961), i77, i476)
2961_0_createMetaList_Load(EOS(STATIC_2961), i77, i476) → 2966_0_createMetaList_InvokeMethod(EOS(STATIC_2966), i77, i476)
2966_0_createMetaList_InvokeMethod(EOS(STATIC_2966), i77, i476) → 2972_0_<init>_Load(EOS(STATIC_2972), i77, i476)
2972_0_<init>_Load(EOS(STATIC_2972), i77, i476) → 2982_0_<init>_InvokeMethod(EOS(STATIC_2982), i77, i476)
2982_0_<init>_InvokeMethod(EOS(STATIC_2982), i77, i476) → 2988_0_<init>_Load(EOS(STATIC_2988), i77, i476)
2988_0_<init>_Load(EOS(STATIC_2988), i77, i476) → 2997_0_<init>_Load(EOS(STATIC_2997), i77, i476)
2997_0_<init>_Load(EOS(STATIC_2997), i77, i476) → 3003_0_<init>_FieldAccess(EOS(STATIC_3003), i77, i476)
3003_0_<init>_FieldAccess(EOS(STATIC_3003), i77, i476) → 3013_0_<init>_Load(EOS(STATIC_3013), i77, i476)
3013_0_<init>_Load(EOS(STATIC_3013), i77, i476) → 3023_0_<init>_Load(EOS(STATIC_3023), i77, i476)
3023_0_<init>_Load(EOS(STATIC_3023), i77, i476) → 3030_0_<init>_FieldAccess(EOS(STATIC_3030), i77, i476)
3030_0_<init>_FieldAccess(EOS(STATIC_3030), i77, i476) → 3038_0_<init>_Return(EOS(STATIC_3038), i77, i476)
3038_0_<init>_Return(EOS(STATIC_3038), i77, i476) → 3045_0_createMetaList_Store(EOS(STATIC_3045), i77, i476)
3045_0_createMetaList_Store(EOS(STATIC_3045), i77, i476) → 3056_0_createMetaList_Inc(EOS(STATIC_3056), i77, i476)
3056_0_createMetaList_Inc(EOS(STATIC_3056), i77, i476) → 3060_0_createMetaList_JMP(EOS(STATIC_3060), i77, +(i476, 1)) | >=(i476, 0)
3060_0_createMetaList_JMP(EOS(STATIC_3060), i77, i618) → 3066_0_createMetaList_Load(EOS(STATIC_3066), i77, i618)
3066_0_createMetaList_Load(EOS(STATIC_3066), i77, i618) → 2351_0_createMetaList_Load(EOS(STATIC_2351), i77, i618)
2351_0_createMetaList_Load(EOS(STATIC_2351), i77, i476) → 2358_0_createMetaList_Load(EOS(STATIC_2358), i77, i476, i476)
2940_0_createMetaList_LE(EOS(STATIC_2940), i77, i476, i606, i606) → 2946_0_createMetaList_New(EOS(STATIC_2946), i77, i476, i606) | >(i606, 0)
2946_0_createMetaList_New(EOS(STATIC_2946), i77, i476, i606) → 2949_0_createMetaList_Duplicate(EOS(STATIC_2949), i77, i476, i606)
2949_0_createMetaList_Duplicate(EOS(STATIC_2949), i77, i476, i606) → 2955_0_createMetaList_ConstantStackPush(EOS(STATIC_2955), i77, i476, i606)
2955_0_createMetaList_ConstantStackPush(EOS(STATIC_2955), i77, i476, i606) → 2962_0_createMetaList_Load(EOS(STATIC_2962), i77, i476, i606)
2962_0_createMetaList_Load(EOS(STATIC_2962), i77, i476, i606) → 2967_0_createMetaList_InvokeMethod(EOS(STATIC_2967), i77, i476, i606)
2967_0_createMetaList_InvokeMethod(EOS(STATIC_2967), i77, i476, i606) → 2973_0_<init>_Load(EOS(STATIC_2973), i77, i476, i606)
2973_0_<init>_Load(EOS(STATIC_2973), i77, i476, i606) → 2983_0_<init>_InvokeMethod(EOS(STATIC_2983), i77, i476, i606)
2983_0_<init>_InvokeMethod(EOS(STATIC_2983), i77, i476, i606) → 2990_0_<init>_Load(EOS(STATIC_2990), i77, i476, i606)
2990_0_<init>_Load(EOS(STATIC_2990), i77, i476, i606) → 2999_0_<init>_Load(EOS(STATIC_2999), i77, i476, i606)
2999_0_<init>_Load(EOS(STATIC_2999), i77, i476, i606) → 3005_0_<init>_FieldAccess(EOS(STATIC_3005), i77, i476, i606)
3005_0_<init>_FieldAccess(EOS(STATIC_3005), i77, i476, i606) → 3015_0_<init>_Load(EOS(STATIC_3015), i77, i476, i606)
3015_0_<init>_Load(EOS(STATIC_3015), i77, i476, i606) → 3024_0_<init>_Load(EOS(STATIC_3024), i77, i476, i606)
3024_0_<init>_Load(EOS(STATIC_3024), i77, i476, i606) → 3032_0_<init>_FieldAccess(EOS(STATIC_3032), i77, i476, i606)
3032_0_<init>_FieldAccess(EOS(STATIC_3032), i77, i476, i606) → 3040_0_<init>_Return(EOS(STATIC_3040), i77, i476, i606)
3040_0_<init>_Return(EOS(STATIC_3040), i77, i476, i606) → 3047_0_createMetaList_Store(EOS(STATIC_3047), i77, i476, i606)
3047_0_createMetaList_Store(EOS(STATIC_3047), i77, i476, i606) → 3057_0_createMetaList_Inc(EOS(STATIC_3057), i77, i476, i606)
3057_0_createMetaList_Inc(EOS(STATIC_3057), i77, i476, i606) → 3062_0_createMetaList_JMP(EOS(STATIC_3062), i77, i476, +(i606, -1)) | >(i606, 0)
3062_0_createMetaList_JMP(EOS(STATIC_3062), i77, i476, i619) → 3068_0_createMetaList_Load(EOS(STATIC_3068), i77, i476, i619)
3068_0_createMetaList_Load(EOS(STATIC_3068), i77, i476, i619) → 2929_0_createMetaList_Load(EOS(STATIC_2929), i77, i476, i619)
R rules:

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

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

Filtered ground terms:

2935_0_createMetaList_LE(x1, x2, x3, x4, x5) → 2935_0_createMetaList_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_2935_0_createMetaList_LE1(x1, x2, x3, x4, x5, x6) → Cond_2935_0_createMetaList_LE1(x1, x3, x4, x5, x6)
Cond_2935_0_createMetaList_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_2935_0_createMetaList_LE(x1, x3, x4, x7)

Filtered duplicate args:

2935_0_createMetaList_LE(x1, x2, x3, x4) → 2935_0_createMetaList_LE(x1, x2, x4)
Cond_2935_0_createMetaList_LE1(x1, x2, x3, x4, x5) → Cond_2935_0_createMetaList_LE1(x1, x2, x3, x5)

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

P rules:
2935_0_createMetaList_LE(x0, x1, 0) → 2935_0_createMetaList_LE(x0, +(x1, 1), x4) | &&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1)))
2935_0_createMetaList_LE(x0, x1, x2) → 2935_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:
2935_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
COND_2935_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2935_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
2935_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2935_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
COND_2935_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2935_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): 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(1): COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_0_CREATEMETALIST_LE(x0[1], x1[1] + 1, x4[1])
(2): 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(0) -> (1), if (x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1 ∧x0[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] > 0 ∧x0[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@2d35d6af 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 2935_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4) the following chains were created:

We consider the chain COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_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)))=TRUE∧x0[0]=x0[1]1∧x1[0]=x1[1]1∧x4[0]=x4[1]1 ⇒ 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2935_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)=TRUE ⇒ 2935_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(+(x1[1], 1), -1)), >(x0[0], +(+(x1[1], 1), 1))), x0[0], +(x1[1], 1), 0, x4[0])∧(U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2935_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∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2935_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_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_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)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1] ⇒ 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2935_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)=TRUE ⇒ 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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_2935_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2935_0_CREATEMETALIST_LE(x0, +(x1, 1), x4) the following chains were created:

We consider the chain 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_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)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1]∧x0[1]=x0[0]1∧+(x1[1], 1)=x1[0]1∧x4[1]=0 ⇒ COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2935_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2935_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)=TRUE ⇒ COND_2935_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥NonInfC∧COND_2935_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥2935_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), 0)∧(U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_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)))=TRUE∧x0[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_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2935_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2935_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)=TRUE ⇒ COND_2935_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥2935_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), x4[0])∧(U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 2935_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2935_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2) the following chains were created:

We consider the chain 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:
(27)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2935_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)=TRUE ⇒ 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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_2935_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2935_0_CREATEMETALIST_LE(x0, x1, +(x2, -1)) the following chains were created:

We consider the chain 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_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)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[0]∧x1[3]=x1[0]∧+(x2[3], -1)=0 ⇒ COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2935_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)=0 ⇒ COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2935_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(41)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[2]1∧x1[3]=x1[2]1∧+(x2[3], -1)=x2[2]1 ⇒ COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2935_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)=TRUE ⇒ COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2935_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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.

2935_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2935_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∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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_2935_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2935_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
- (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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)
2935_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2935_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2935_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_2935_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2935_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
- (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = [3]
POL(2935_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁
POL(0) = 0
POL(COND_2935_0_CREATEMETALIST_LE(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄ + [-1]x₃ + x₂ + [-1]x₁
POL(&&(x₁, x₂)) = 0
POL(>(x₁, x₂)) = 0
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_2935_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂

The following pairs are in P_>:

COND_2935_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2935_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P_bound:

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

The following pairs are in P_≥:

2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_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, TRUE)¹
FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(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): 2935_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2935_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(2): 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_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] > 0 ∧x0[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_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)
(2): 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_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] > 0 ∧x0[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@2d35d6af 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_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) the following chains were created:

We consider the chain 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(1)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[2]1∧x1[3]=x1[2]1∧+(x2[3], -1)=x2[2]1 ⇒ COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2935_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)=TRUE ⇒ COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2935_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 ⇒ (U^Increasing(2935_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 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) the following chains were created:

We consider the chain 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:
(8)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2935_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)=TRUE ⇒ 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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 ⇒ (U^Increasing(COND_2935_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_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
- (x2[2] ≥ 0 ⇒ (U^Increasing(2935_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)
2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2935_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)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_2935_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + x₄
POL(2935_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + x₃
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0

The following pairs are in P_>:

COND_2935_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2935_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

The following pairs are in P_bound:

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

The following pairs are in P_≥:

2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_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): 2935_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2935_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)) → 3352_0_countMetaList_NULL(EOS(STATIC_3352), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3352_0_countMetaList_NULL(EOS(STATIC_3352), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3354_0_countMetaList_Load(EOS(STATIC_3354), o3582, java.lang.Object(o3590sub))
3354_0_countMetaList_Load(EOS(STATIC_3354), o3582, java.lang.Object(o3590sub)) → 3357_0_countMetaList_FieldAccess(EOS(STATIC_3357), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3357_0_countMetaList_FieldAccess(EOS(STATIC_3357), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3360_0_countMetaList_FieldAccess(EOS(STATIC_3360), o3582, java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3357_0_countMetaList_FieldAccess(EOS(STATIC_3357), java.lang.Object(o3590sub), java.lang.Object(o3590sub), java.lang.Object(o3590sub)) → 3361_0_countMetaList_FieldAccess(EOS(STATIC_3361), java.lang.Object(o3590sub), java.lang.Object(o3590sub), java.lang.Object(o3590sub))
3360_0_countMetaList_FieldAccess(EOS(STATIC_3360), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593))) → 3364_0_countMetaList_FieldAccess(EOS(STATIC_3364), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593)))
3364_0_countMetaList_FieldAccess(EOS(STATIC_3364), o3582, java.lang.Object(List(EOC, o3592, o3593)), java.lang.Object(List(EOC, o3592, o3593))) → 3368_0_countMetaList_CheckCast(EOS(STATIC_3368), o3582, java.lang.Object(List(EOC, o3592, o3593)), o3592)
3368_0_countMetaList_CheckCast(EOS(STATIC_3368), 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))
3368_0_countMetaList_CheckCast(EOS(STATIC_3368), 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)) → 3381_0_countMetaList_CheckCast(EOS(STATIC_3381), 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) → 3408_0_countMetaList_Load(EOS(STATIC_3408), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) | &&(>(1, 0), =(matching1, 1))
3408_0_countMetaList_Load(EOS(STATIC_3408), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3419_0_countMetaList_FieldAccess(EOS(STATIC_3419), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)))
3419_0_countMetaList_FieldAccess(EOS(STATIC_3419), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593))) → 3430_0_countMetaList_CheckCast(EOS(STATIC_3430), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3430_0_countMetaList_CheckCast(EOS(STATIC_3430), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3439_0_countMetaList_Store(EOS(STATIC_3439), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3439_0_countMetaList_Store(EOS(STATIC_3439), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3446_0_countMetaList_Load(EOS(STATIC_3446), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub))
3446_0_countMetaList_Load(EOS(STATIC_3446), o3582, java.lang.Object(List(EOC, java.lang.Object(o3611sub), o3593)), java.lang.Object(o3611sub)) → 3452_0_countMetaList_Load(EOS(STATIC_3452), 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)))
3452_0_countMetaList_Load(EOS(STATIC_3452), 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))) → 3460_0_countMetaList_FieldAccess(EOS(STATIC_3460), 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))
3460_0_countMetaList_FieldAccess(EOS(STATIC_3460), 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)) → 3465_0_countMetaList_FieldAccess(EOS(STATIC_3465), 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))
3460_0_countMetaList_FieldAccess(EOS(STATIC_3460), 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)) → 3466_0_countMetaList_FieldAccess(EOS(STATIC_3466), 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))
3465_0_countMetaList_FieldAccess(EOS(STATIC_3465), 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))) → 3469_0_countMetaList_FieldAccess(EOS(STATIC_3469), 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)))
3469_0_countMetaList_FieldAccess(EOS(STATIC_3469), 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))) → 3475_0_countMetaList_FieldAccess(EOS(STATIC_3475), 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)
3475_0_countMetaList_FieldAccess(EOS(STATIC_3475), 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) → 3482_0_countMetaList_New(EOS(STATIC_3482), o3582put, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)))
3482_0_countMetaList_New(EOS(STATIC_3482), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797))) → 3489_0_countMetaList_Duplicate(EOS(STATIC_3489), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL)))
3489_0_countMetaList_Duplicate(EOS(STATIC_3489), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, o3796, o3797)), java.lang.Object(List(EOC, NULL, NULL))) → 3495_0_countMetaList_Load(EOS(STATIC_3495), 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)))
3495_0_countMetaList_Load(EOS(STATIC_3495), 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))) → 3502_0_countMetaList_FieldAccess(EOS(STATIC_3502), 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)))
3502_0_countMetaList_FieldAccess(EOS(STATIC_3502), 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))) → 3509_0_countMetaList_Load(EOS(STATIC_3509), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796)
3509_0_countMetaList_Load(EOS(STATIC_3509), o3582, java.lang.Object(List(EOC, o3797, o3593)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796) → 3516_0_countMetaList_InvokeMethod(EOS(STATIC_3516), o3582, java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o3796, java.lang.Object(List(EOC, o3797, o3593)))
3516_0_countMetaList_InvokeMethod(EOS(STATIC_3516), 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))))) → 3602_0_countMetaList_FieldAccess(EOS(STATIC_3602), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593)))))
3602_0_countMetaList_FieldAccess(EOS(STATIC_3602), o3582, java.lang.Object(List(EOC, o3796, java.lang.Object(List(EOC, o3797, o3593))))) → 3612_0_countMetaList_Store(EOS(STATIC_3612), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3612_0_countMetaList_Store(EOS(STATIC_3612), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3619_0_countMetaList_Inc(EOS(STATIC_3619), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3619_0_countMetaList_Inc(EOS(STATIC_3619), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3627_0_countMetaList_JMP(EOS(STATIC_3627), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3627_0_countMetaList_JMP(EOS(STATIC_3627), o3582, java.lang.Object(List(EOC, o3797, o3593))) → 3634_0_countMetaList_Load(EOS(STATIC_3634), o3582, java.lang.Object(List(EOC, o3797, o3593)))
3634_0_countMetaList_Load(EOS(STATIC_3634), 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)
3466_0_countMetaList_FieldAccess(EOS(STATIC_3466), 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))) → 3471_0_countMetaList_FieldAccess(EOS(STATIC_3471), 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)))
3471_0_countMetaList_FieldAccess(EOS(STATIC_3471), 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))) → 3477_0_countMetaList_FieldAccess(EOS(STATIC_3477), 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)
3477_0_countMetaList_FieldAccess(EOS(STATIC_3477), 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) → 3485_0_countMetaList_New(EOS(STATIC_3485), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800)))
3485_0_countMetaList_New(EOS(STATIC_3485), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)), java.lang.Object(List(EOC, o3799, o3800))) → 3492_0_countMetaList_Duplicate(EOS(STATIC_3492), 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)))
3492_0_countMetaList_Duplicate(EOS(STATIC_3492), 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))) → 3498_0_countMetaList_Load(EOS(STATIC_3498), 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)))
3498_0_countMetaList_Load(EOS(STATIC_3498), 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))) → 3505_0_countMetaList_FieldAccess(EOS(STATIC_3505), 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)))
3505_0_countMetaList_FieldAccess(EOS(STATIC_3505), 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))) → 3512_0_countMetaList_Load(EOS(STATIC_3512), 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)
3512_0_countMetaList_Load(EOS(STATIC_3512), 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) → 3518_0_countMetaList_InvokeMethod(EOS(STATIC_3518), 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)))
3518_0_countMetaList_InvokeMethod(EOS(STATIC_3518), 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))) → 3539_0_<init>_Load(EOS(STATIC_3539), 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)))
3539_0_<init>_Load(EOS(STATIC_3539), 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) → 3553_0_<init>_Load(EOS(STATIC_3553), 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)))
3553_0_<init>_Load(EOS(STATIC_3553), 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))))) → 3607_0_countMetaList_FieldAccess(EOS(STATIC_3607), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593)))))
3607_0_countMetaList_FieldAccess(EOS(STATIC_3607), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3799, java.lang.Object(List(EOC, o3800, o3593))))) → 3615_0_countMetaList_Store(EOS(STATIC_3615), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3615_0_countMetaList_Store(EOS(STATIC_3615), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3622_0_countMetaList_Inc(EOS(STATIC_3622), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3622_0_countMetaList_Inc(EOS(STATIC_3622), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3630_0_countMetaList_JMP(EOS(STATIC_3630), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3630_0_countMetaList_JMP(EOS(STATIC_3630), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593))) → 3637_0_countMetaList_Load(EOS(STATIC_3637), java.lang.Object(List(EOC, o3799, o3800)), java.lang.Object(List(EOC, o3800, o3593)))
3637_0_countMetaList_Load(EOS(STATIC_3637), 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)))
3381_0_countMetaList_CheckCast(EOS(STATIC_3381), 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) → 3410_0_countMetaList_Load(EOS(STATIC_3410), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) | =(matching1, 0)
3410_0_countMetaList_Load(EOS(STATIC_3410), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) → 3421_0_countMetaList_FieldAccess(EOS(STATIC_3421), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593)))
3421_0_countMetaList_FieldAccess(EOS(STATIC_3421), o3582, java.lang.Object(List(EOC, java.lang.Object(o3612sub), o3593))) → 3434_0_countMetaList_Store(EOS(STATIC_3434), o3582, o3593)
3434_0_countMetaList_Store(EOS(STATIC_3434), o3582, o3593) → 3440_0_countMetaList_Inc(EOS(STATIC_3440), o3582, o3593)
3440_0_countMetaList_Inc(EOS(STATIC_3440), o3582, o3593) → 3447_0_countMetaList_JMP(EOS(STATIC_3447), o3582, o3593)
3447_0_countMetaList_JMP(EOS(STATIC_3447), o3582, o3593) → 3454_0_countMetaList_Load(EOS(STATIC_3454), o3582, o3593)
3454_0_countMetaList_Load(EOS(STATIC_3454), 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))) → 3411_0_countMetaList_FieldAccess(EOS(STATIC_3411), o3582, java.lang.Object(List(EOC, NULL, o3593)))
3411_0_countMetaList_FieldAccess(EOS(STATIC_3411), o3582, java.lang.Object(List(EOC, NULL, o3593))) → 3422_0_countMetaList_Store(EOS(STATIC_3422), o3582, o3593)
3422_0_countMetaList_Store(EOS(STATIC_3422), o3582, o3593) → 3434_0_countMetaList_Store(EOS(STATIC_3434), o3582, o3593)
3361_0_countMetaList_FieldAccess(EOS(STATIC_3361), 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))) → 3371_0_countMetaList_CheckCast(EOS(STATIC_3371), java.lang.Object(List(EOC, o3595, o3596)), java.lang.Object(List(EOC, o3595, o3596)), o3595)
3371_0_countMetaList_CheckCast(EOS(STATIC_3371), 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))
3371_0_countMetaList_CheckCast(EOS(STATIC_3371), 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)) → 3385_0_countMetaList_CheckCast(EOS(STATIC_3385), 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))
3385_0_countMetaList_CheckCast(EOS(STATIC_3385), 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) → 3413_0_countMetaList_Load(EOS(STATIC_3413), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) | &&(>(1, 0), =(matching1, 1))
3413_0_countMetaList_Load(EOS(STATIC_3413), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596))) → 3424_0_countMetaList_FieldAccess(EOS(STATIC_3424), 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)))
3424_0_countMetaList_FieldAccess(EOS(STATIC_3424), 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))) → 3436_0_countMetaList_CheckCast(EOS(STATIC_3436), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3436_0_countMetaList_CheckCast(EOS(STATIC_3436), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3442_0_countMetaList_Store(EOS(STATIC_3442), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3442_0_countMetaList_Store(EOS(STATIC_3442), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3449_0_countMetaList_Load(EOS(STATIC_3449), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub))
3449_0_countMetaList_Load(EOS(STATIC_3449), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3613sub), o3596)), java.lang.Object(o3613sub)) → 3456_0_countMetaList_Load(EOS(STATIC_3456), 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)))
3456_0_countMetaList_Load(EOS(STATIC_3456), 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))) → 3463_0_countMetaList_FieldAccess(EOS(STATIC_3463), 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))
3463_0_countMetaList_FieldAccess(EOS(STATIC_3463), 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))) → 3468_0_countMetaList_FieldAccess(EOS(STATIC_3468), 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)))
3468_0_countMetaList_FieldAccess(EOS(STATIC_3468), 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))) → 3472_0_countMetaList_FieldAccess(EOS(STATIC_3472), 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)
3472_0_countMetaList_FieldAccess(EOS(STATIC_3472), 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) → 3479_0_countMetaList_New(EOS(STATIC_3479), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794)))
3479_0_countMetaList_New(EOS(STATIC_3479), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3793, o3794))) → 3487_0_countMetaList_Duplicate(EOS(STATIC_3487), 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)))
3487_0_countMetaList_Duplicate(EOS(STATIC_3487), 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))) → 3493_0_countMetaList_Load(EOS(STATIC_3493), 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)))
3493_0_countMetaList_Load(EOS(STATIC_3493), 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))) → 3499_0_countMetaList_FieldAccess(EOS(STATIC_3499), 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)))
3499_0_countMetaList_FieldAccess(EOS(STATIC_3499), 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))) → 3507_0_countMetaList_Load(EOS(STATIC_3507), 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)
3507_0_countMetaList_Load(EOS(STATIC_3507), 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) → 3513_0_countMetaList_InvokeMethod(EOS(STATIC_3513), 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)))
3513_0_countMetaList_InvokeMethod(EOS(STATIC_3513), 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))) → 3519_0_<init>_Load(EOS(STATIC_3519), 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)))
3519_0_<init>_Load(EOS(STATIC_3519), 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))) → 3529_0_<init>_Load(EOS(STATIC_3529), 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)))
3529_0_<init>_Load(EOS(STATIC_3529), 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))) → 3534_0_<init>_Load(EOS(STATIC_3534), 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)))
3534_0_<init>_Load(EOS(STATIC_3534), 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))) → 3540_0_<init>_FieldAccess(EOS(STATIC_3540), 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)
3540_0_<init>_FieldAccess(EOS(STATIC_3540), 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) → 3547_0_<init>_Load(EOS(STATIC_3547), 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)))
3547_0_<init>_Load(EOS(STATIC_3547), 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))))) → 3609_0_countMetaList_Store(EOS(STATIC_3609), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3609_0_countMetaList_Store(EOS(STATIC_3609), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3617_0_countMetaList_Inc(EOS(STATIC_3617), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3617_0_countMetaList_Inc(EOS(STATIC_3617), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3624_0_countMetaList_JMP(EOS(STATIC_3624), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3624_0_countMetaList_JMP(EOS(STATIC_3624), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596))) → 3632_0_countMetaList_Load(EOS(STATIC_3632), java.lang.Object(List(EOC, o3794, o3596)), java.lang.Object(List(EOC, o3794, o3596)))
3632_0_countMetaList_Load(EOS(STATIC_3632), 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)) → 3405_0_countMetaList_EQ(EOS(STATIC_3405), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), 0)
3405_0_countMetaList_EQ(EOS(STATIC_3405), 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))) → 3427_0_countMetaList_FieldAccess(EOS(STATIC_3427), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)))
3427_0_countMetaList_FieldAccess(EOS(STATIC_3427), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596))) → 3438_0_countMetaList_Store(EOS(STATIC_3438), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3438_0_countMetaList_Store(EOS(STATIC_3438), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3444_0_countMetaList_Inc(EOS(STATIC_3444), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3444_0_countMetaList_Inc(EOS(STATIC_3444), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3450_0_countMetaList_JMP(EOS(STATIC_3450), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3450_0_countMetaList_JMP(EOS(STATIC_3450), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596) → 3458_0_countMetaList_Load(EOS(STATIC_3458), java.lang.Object(List(EOC, java.lang.Object(o3614sub), o3596)), o3596)
3458_0_countMetaList_Load(EOS(STATIC_3458), 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))) → 3417_0_countMetaList_FieldAccess(EOS(STATIC_3417), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596)))
3417_0_countMetaList_FieldAccess(EOS(STATIC_3417), java.lang.Object(List(EOC, NULL, o3596)), java.lang.Object(List(EOC, NULL, o3596))) → 3429_0_countMetaList_Store(EOS(STATIC_3429), java.lang.Object(List(EOC, NULL, o3596)), o3596)
3429_0_countMetaList_Store(EOS(STATIC_3429), java.lang.Object(List(EOC, NULL, o3596)), o3596) → 3434_0_countMetaList_Store(EOS(STATIC_3434), 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.

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(x₁)) = 2·x₁
POL(List(x₁, x₂)) = x₁ + 2·x₂
POL(NULL) = 0
POL(java.lang.Object(x₁)) = 2·x₁

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

List₂ > java.lang.Object₁ > 3351_{0_{COUNTMETALIST_NULL₁}}

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.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPNonInfProof (SOUND transformation)

(9) Obligation:

(10) IDependencyGraphProof (EQUIVALENT transformation)

(11) Obligation:

(12) IDPNonInfProof (SOUND transformation)

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) SCCToIDPv1Proof (SOUND transformation)

(18) Obligation:

(19) IDPtoQDPProof (SOUND transformation)

(20) Obligation:

(21) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(22) Obligation:

(23) MRRProof (EQUIVALENT transformation)

(24) Obligation:

(25) PisEmptyProof (EQUIVALENT transformation)

(26) YES