Termination proof of /tmp/tmpEVX8z9/CountMetaListRec.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1180 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 950 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 0 ms)

        ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 UsableRulesReductionPairsProof (⇔, 20 ms)

        ↳15 QDP

        ↳16 MRRProof (⇔, 0 ms)

        ↳17 QDP

        ↳18 PisEmptyProof (⇔, 0 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIDPv1Proof (⇒, 300 ms)

        ↳22 IDP

        ↳23 IDPNonInfProof (⇒, 940 ms)

        ↳24 IDP

        ↳25 IDependencyGraphProof (⇔, 0 ms)

        ↳26 IDP

        ↳27 IDPNonInfProof (⇒, 190 ms)

        ↳28 IDP

        ↳29 IDependencyGraphProof (⇔, 0 ms)

        ↳30 TRUE

(0) Obligation:

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

public class CountMetaListRec {
	public static void main(String[] args) {
		Random.args = args;
		List l = createMetaList();

		int count = countMetaList(l);
	}

	public static int countMetaList(List cur) {
		if (cur == null) {
			return 0;
		} else {
			if (cur.value instanceof List) {
				List inner = (List) cur.value;
				cur.value = inner.next;
				cur = new List(inner.value, cur);
			}
			return 1 + countMetaList(cur.next);
		}
	}

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

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

CountMetaListRec.countMetaList(LList;)I: Graph of 88 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

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

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 59 rules for P and 33 rules for R.

P rules:
1638_0_countMetaList_NONNULL(EOS(STATIC_1638), java.lang.Object(o1488sub), java.lang.Object(o1488sub)) → 1644_0_countMetaList_NONNULL(EOS(STATIC_1644), java.lang.Object(o1488sub), java.lang.Object(o1488sub))
1644_0_countMetaList_NONNULL(EOS(STATIC_1644), java.lang.Object(o1488sub), java.lang.Object(o1488sub)) → 1649_0_countMetaList_Load(EOS(STATIC_1649), java.lang.Object(o1488sub))
1649_0_countMetaList_Load(EOS(STATIC_1649), java.lang.Object(o1488sub)) → 1656_0_countMetaList_FieldAccess(EOS(STATIC_1656), java.lang.Object(o1488sub), java.lang.Object(o1488sub))
1656_0_countMetaList_FieldAccess(EOS(STATIC_1656), java.lang.Object(List(EOC, o1498, o1499)), java.lang.Object(List(EOC, o1498, o1499))) → 1662_0_countMetaList_FieldAccess(EOS(STATIC_1662), java.lang.Object(List(EOC, o1498, o1499)), java.lang.Object(List(EOC, o1498, o1499)))
1662_0_countMetaList_FieldAccess(EOS(STATIC_1662), java.lang.Object(List(EOC, o1498, o1499)), java.lang.Object(List(EOC, o1498, o1499))) → 1667_0_countMetaList_CheckCast(EOS(STATIC_1667), java.lang.Object(List(EOC, o1498, o1499)), o1498)
1667_0_countMetaList_CheckCast(EOS(STATIC_1667), java.lang.Object(List(EOC, java.lang.Object(o1511sub), o1499)), java.lang.Object(o1511sub)) → 1674_0_countMetaList_CheckCast(EOS(STATIC_1674), java.lang.Object(List(EOC, java.lang.Object(o1511sub), o1499)), java.lang.Object(o1511sub))
1667_0_countMetaList_CheckCast(EOS(STATIC_1667), java.lang.Object(List(EOC, NULL, o1499)), NULL) → 1675_0_countMetaList_CheckCast(EOS(STATIC_1675), java.lang.Object(List(EOC, NULL, o1499)), NULL)
1674_0_countMetaList_CheckCast(EOS(STATIC_1674), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub)) → 1684_0_countMetaList_CheckCast(EOS(STATIC_1684), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub))
1674_0_countMetaList_CheckCast(EOS(STATIC_1674), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), java.lang.Object(o1514sub)) → 1686_0_countMetaList_CheckCast(EOS(STATIC_1686), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), java.lang.Object(o1514sub))
1684_0_countMetaList_CheckCast(EOS(STATIC_1684), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub)) → 1691_0_countMetaList_EQ(EOS(STATIC_1691), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), 1)
1691_0_countMetaList_EQ(EOS(STATIC_1691), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), matching1) → 1704_0_countMetaList_Load(EOS(STATIC_1704), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499))) | &&(>(1, 0), =(matching1, 1))
1704_0_countMetaList_Load(EOS(STATIC_1704), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499))) → 1714_0_countMetaList_FieldAccess(EOS(STATIC_1714), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)))
1714_0_countMetaList_FieldAccess(EOS(STATIC_1714), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499))) → 1721_0_countMetaList_CheckCast(EOS(STATIC_1721), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub))
1721_0_countMetaList_CheckCast(EOS(STATIC_1721), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub)) → 1730_0_countMetaList_Store(EOS(STATIC_1730), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub))
1730_0_countMetaList_Store(EOS(STATIC_1730), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub)) → 1740_0_countMetaList_Load(EOS(STATIC_1740), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub))
1740_0_countMetaList_Load(EOS(STATIC_1740), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub)) → 1747_0_countMetaList_Load(EOS(STATIC_1747), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)))
1747_0_countMetaList_Load(EOS(STATIC_1747), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499))) → 1756_0_countMetaList_FieldAccess(EOS(STATIC_1756), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1499)), java.lang.Object(o1513sub))
1756_0_countMetaList_FieldAccess(EOS(STATIC_1756), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577))) → 1767_0_countMetaList_FieldAccess(EOS(STATIC_1767), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577)))
1767_0_countMetaList_FieldAccess(EOS(STATIC_1767), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577))) → 1779_0_countMetaList_FieldAccess(EOS(STATIC_1779), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), o1577)
1779_0_countMetaList_FieldAccess(EOS(STATIC_1779), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1499)), o1577) → 1790_0_countMetaList_New(EOS(STATIC_1790), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, o1577)))
1790_0_countMetaList_New(EOS(STATIC_1790), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, o1577))) → 1801_0_countMetaList_Duplicate(EOS(STATIC_1801), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL)))
1801_0_countMetaList_Duplicate(EOS(STATIC_1801), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL))) → 1810_0_countMetaList_Load(EOS(STATIC_1810), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
1810_0_countMetaList_Load(EOS(STATIC_1810), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 1825_0_countMetaList_FieldAccess(EOS(STATIC_1825), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1576, o1577)))
1825_0_countMetaList_FieldAccess(EOS(STATIC_1825), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1576, o1577))) → 1842_0_countMetaList_Load(EOS(STATIC_1842), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576)
1842_0_countMetaList_Load(EOS(STATIC_1842), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576) → 1867_0_countMetaList_InvokeMethod(EOS(STATIC_1867), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)))
1867_0_countMetaList_InvokeMethod(EOS(STATIC_1867), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499))) → 1881_0_<init>_Load(EOS(STATIC_1881), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)))
1881_0_<init>_Load(EOS(STATIC_1881), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499))) → 1917_0_<init>_InvokeMethod(EOS(STATIC_1917), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)))
1917_0_<init>_InvokeMethod(EOS(STATIC_1917), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL))) → 1940_0_<init>_Load(EOS(STATIC_1940), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)))
1940_0_<init>_Load(EOS(STATIC_1940), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499))) → 1979_0_<init>_Load(EOS(STATIC_1979), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)))
1979_0_<init>_Load(EOS(STATIC_1979), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL))) → 1990_0_<init>_FieldAccess(EOS(STATIC_1990), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576)
1990_0_<init>_FieldAccess(EOS(STATIC_1990), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, NULL, NULL)), o1576) → 2009_0_<init>_Load(EOS(STATIC_2009), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1499)))
2009_0_<init>_Load(EOS(STATIC_2009), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1499))) → 2021_0_<init>_Load(EOS(STATIC_2021), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, NULL)))
2021_0_<init>_Load(EOS(STATIC_2021), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, NULL))) → 2043_0_<init>_FieldAccess(EOS(STATIC_2043), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1499)))
2043_0_<init>_FieldAccess(EOS(STATIC_2043), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1499)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1499))) → 2085_0_<init>_Return(EOS(STATIC_2085), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))), o1576, java.lang.Object(List(EOC, o1577, o1499)))
2085_0_<init>_Return(EOS(STATIC_2085), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))), o1576, java.lang.Object(List(EOC, o1577, o1499))) → 2095_0_countMetaList_Store(EOS(STATIC_2095), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))))
2095_0_countMetaList_Store(EOS(STATIC_2095), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499))))) → 2114_0_countMetaList_ConstantStackPush(EOS(STATIC_2114), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))))
2114_0_countMetaList_ConstantStackPush(EOS(STATIC_2114), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499))))) → 2123_0_countMetaList_Load(EOS(STATIC_2123), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))), 1)
2123_0_countMetaList_Load(EOS(STATIC_2123), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499)))), matching1) → 2144_0_countMetaList_FieldAccess(EOS(STATIC_2144), 1, java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499))))) | =(matching1, 1)
2144_0_countMetaList_FieldAccess(EOS(STATIC_2144), matching1, java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1499))))) → 2189_0_countMetaList_InvokeMethod(EOS(STATIC_2189), 1, java.lang.Object(List(EOC, o1577, o1499))) | =(matching1, 1)
2189_0_countMetaList_InvokeMethod(EOS(STATIC_2189), matching1, java.lang.Object(List(EOC, o1577, o1499))) → 2200_1_countMetaList_InvokeMethod(2200_0_countMetaList_Load(EOS(STATIC_2200), java.lang.Object(List(EOC, o1577, o1499))), 1, java.lang.Object(List(EOC, o1577, o1499))) | =(matching1, 1)
2200_0_countMetaList_Load(EOS(STATIC_2200), java.lang.Object(List(EOC, o1577, o1499))) → 2215_0_countMetaList_Load(EOS(STATIC_2215), java.lang.Object(List(EOC, o1577, o1499)))
2215_0_countMetaList_Load(EOS(STATIC_2215), java.lang.Object(List(EOC, o1577, o1499))) → 1633_0_countMetaList_Load(EOS(STATIC_1633), java.lang.Object(List(EOC, o1577, o1499)))
1633_0_countMetaList_Load(EOS(STATIC_1633), o1471) → 1638_0_countMetaList_NONNULL(EOS(STATIC_1638), o1471, o1471)
1686_0_countMetaList_CheckCast(EOS(STATIC_1686), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), java.lang.Object(o1514sub)) → 1696_0_countMetaList_EQ(EOS(STATIC_1696), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), 0)
1696_0_countMetaList_EQ(EOS(STATIC_1696), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), matching1) → 1706_0_countMetaList_ConstantStackPush(EOS(STATIC_1706), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499))) | =(matching1, 0)
1706_0_countMetaList_ConstantStackPush(EOS(STATIC_1706), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499))) → 1715_0_countMetaList_Load(EOS(STATIC_1715), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), 1)
1715_0_countMetaList_Load(EOS(STATIC_1715), java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499)), matching1) → 1723_0_countMetaList_FieldAccess(EOS(STATIC_1723), 1, java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499))) | =(matching1, 1)
1723_0_countMetaList_FieldAccess(EOS(STATIC_1723), matching1, java.lang.Object(List(EOC, java.lang.Object(o1514sub), o1499))) → 1732_0_countMetaList_InvokeMethod(EOS(STATIC_1732), 1, o1499) | =(matching1, 1)
1732_0_countMetaList_InvokeMethod(EOS(STATIC_1732), matching1, o1499) → 1741_1_countMetaList_InvokeMethod(1741_0_countMetaList_Load(EOS(STATIC_1741), o1499), 1, o1499) | =(matching1, 1)
1741_0_countMetaList_Load(EOS(STATIC_1741), o1499) → 1749_0_countMetaList_Load(EOS(STATIC_1749), o1499)
1749_0_countMetaList_Load(EOS(STATIC_1749), o1499) → 1633_0_countMetaList_Load(EOS(STATIC_1633), o1499)
1675_0_countMetaList_CheckCast(EOS(STATIC_1675), java.lang.Object(List(EOC, NULL, o1499)), NULL) → 1687_0_countMetaList_EQ(EOS(STATIC_1687), java.lang.Object(List(EOC, NULL, o1499)), 0)
1687_0_countMetaList_EQ(EOS(STATIC_1687), java.lang.Object(List(EOC, NULL, o1499)), matching1) → 1697_0_countMetaList_ConstantStackPush(EOS(STATIC_1697), java.lang.Object(List(EOC, NULL, o1499))) | =(matching1, 0)
1697_0_countMetaList_ConstantStackPush(EOS(STATIC_1697), java.lang.Object(List(EOC, NULL, o1499))) → 1707_0_countMetaList_Load(EOS(STATIC_1707), java.lang.Object(List(EOC, NULL, o1499)), 1)
1707_0_countMetaList_Load(EOS(STATIC_1707), java.lang.Object(List(EOC, NULL, o1499)), matching1) → 1717_0_countMetaList_FieldAccess(EOS(STATIC_1717), 1, java.lang.Object(List(EOC, NULL, o1499))) | =(matching1, 1)
1717_0_countMetaList_FieldAccess(EOS(STATIC_1717), matching1, java.lang.Object(List(EOC, NULL, o1499))) → 1724_0_countMetaList_InvokeMethod(EOS(STATIC_1724), 1, o1499) | =(matching1, 1)
1724_0_countMetaList_InvokeMethod(EOS(STATIC_1724), matching1, o1499) → 1733_1_countMetaList_InvokeMethod(1733_0_countMetaList_Load(EOS(STATIC_1733), o1499), 1, o1499) | =(matching1, 1)
1733_0_countMetaList_Load(EOS(STATIC_1733), o1499) → 1743_0_countMetaList_Load(EOS(STATIC_1743), o1499)
1743_0_countMetaList_Load(EOS(STATIC_1743), o1499) → 1633_0_countMetaList_Load(EOS(STATIC_1633), o1499)
R rules:
1638_0_countMetaList_NONNULL(EOS(STATIC_1638), NULL, NULL) → 1646_0_countMetaList_NONNULL(EOS(STATIC_1646), NULL, NULL)
1646_0_countMetaList_NONNULL(EOS(STATIC_1646), NULL, NULL) → 1650_0_countMetaList_ConstantStackPush(EOS(STATIC_1650), NULL)
1650_0_countMetaList_ConstantStackPush(EOS(STATIC_1650), NULL) → 1658_0_countMetaList_Return(EOS(STATIC_1658), NULL, 0)
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return(EOS(STATIC_1658), NULL, matching1), matching2, NULL) → 1771_0_countMetaList_Return(EOS(STATIC_1771), 1, NULL, NULL, 0) | &&(=(matching1, 0), =(matching2, 1))
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(EOS(STATIC_2529), i1143), matching1, o1499) → 2550_0_countMetaList_Return(EOS(STATIC_2550), 1, java.lang.Object(List(EOC, o2860, o2859)), i1143) | =(matching1, 1)
1741_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return(EOS(STATIC_1658), NULL, matching1), matching2, NULL) → 1780_0_countMetaList_Return(EOS(STATIC_1780), 1, NULL, NULL, 0) | &&(=(matching1, 0), =(matching2, 1))
1741_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(EOS(STATIC_2529), i1143), matching1, o1499) → 2552_0_countMetaList_Return(EOS(STATIC_2552), 1, java.lang.Object(List(EOC, o2860, o2859)), i1143) | =(matching1, 1)
1771_0_countMetaList_Return(EOS(STATIC_1771), matching1, NULL, NULL, matching2) → 1781_0_countMetaList_IntArithmetic(EOS(STATIC_1781), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1780_0_countMetaList_Return(EOS(STATIC_1780), matching1, NULL, NULL, matching2) → 1791_0_countMetaList_IntArithmetic(EOS(STATIC_1791), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1781_0_countMetaList_IntArithmetic(EOS(STATIC_1781), matching1, matching2) → 2523_0_countMetaList_IntArithmetic(EOS(STATIC_2523), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1791_0_countMetaList_IntArithmetic(EOS(STATIC_1791), matching1, matching2) → 2523_0_countMetaList_IntArithmetic(EOS(STATIC_2523), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1853_0_countMetaList_Return(EOS(STATIC_1853), matching1, java.lang.Object(List(EOC, o1649, NULL)), matching2) → 1955_0_countMetaList_Return(EOS(STATIC_1955), 1, java.lang.Object(List(EOC, o1649, NULL)), 1) | &&(=(matching1, 1), =(matching2, 1))
1859_0_countMetaList_Return(EOS(STATIC_1859), matching1, java.lang.Object(List(EOC, o1660, NULL)), matching2) → 1964_0_countMetaList_Return(EOS(STATIC_1964), 1, java.lang.Object(List(EOC, o1660, NULL)), 1) | &&(=(matching1, 1), =(matching2, 1))
1955_0_countMetaList_Return(EOS(STATIC_1955), matching1, java.lang.Object(List(EOC, o1802, o1801)), i703) → 2060_0_countMetaList_Return(EOS(STATIC_2060), 1, java.lang.Object(List(EOC, o1802, o1801)), i703) | =(matching1, 1)
1964_0_countMetaList_Return(EOS(STATIC_1964), matching1, java.lang.Object(List(EOC, o1834, o1833)), i711) → 2070_0_countMetaList_Return(EOS(STATIC_2070), 1, java.lang.Object(List(EOC, o1834, o1833)), i711) | =(matching1, 1)
2060_0_countMetaList_Return(EOS(STATIC_2060), matching1, java.lang.Object(List(EOC, o1995, o1994)), i765) → 2162_0_countMetaList_Return(EOS(STATIC_2162), 1, java.lang.Object(List(EOC, o1995, o1994)), i765) | =(matching1, 1)
2070_0_countMetaList_Return(EOS(STATIC_2070), matching1, java.lang.Object(List(EOC, o2030, o2029)), i775) → 2173_0_countMetaList_Return(EOS(STATIC_2173), 1, java.lang.Object(List(EOC, o2030, o2029)), i775) | =(matching1, 1)
2162_0_countMetaList_Return(EOS(STATIC_2162), matching1, java.lang.Object(List(EOC, o2198, o2197)), i839) → 2272_0_countMetaList_Return(EOS(STATIC_2272), 1, java.lang.Object(List(EOC, o2198, o2197)), i839) | =(matching1, 1)
2173_0_countMetaList_Return(EOS(STATIC_2173), matching1, java.lang.Object(List(EOC, o2232, o2231)), i849) → 2283_0_countMetaList_Return(EOS(STATIC_2283), 1, java.lang.Object(List(EOC, o2232, o2231)), i849) | =(matching1, 1)
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(EOS(STATIC_2529), i1143), matching1, java.lang.Object(List(EOC, o1577, o1499))) → 2555_0_countMetaList_Return(EOS(STATIC_2555), 1, java.lang.Object(List(EOC, o2860, o2859)), i1143) | =(matching1, 1)
2272_0_countMetaList_Return(EOS(STATIC_2272), matching1, java.lang.Object(List(EOC, o2399, o2398)), i909) → 2387_0_countMetaList_Return(EOS(STATIC_2387), 1, java.lang.Object(List(EOC, o2399, o2398)), i909) | =(matching1, 1)
2283_0_countMetaList_Return(EOS(STATIC_2283), matching1, java.lang.Object(List(EOC, o2434, o2433)), i919) → 2396_0_countMetaList_Return(EOS(STATIC_2396), 1, java.lang.Object(List(EOC, o2434, o2433)), i919) | =(matching1, 1)
2310_0_countMetaList_Return(EOS(STATIC_2310), matching1, java.lang.Object(List(EOC, NULL, o2497)), i944) → 2488_0_countMetaList_Return(EOS(STATIC_2488), 1, java.lang.Object(List(EOC, NULL, o2497)), i944) | =(matching1, 1)
2387_0_countMetaList_Return(EOS(STATIC_2387), matching1, java.lang.Object(List(EOC, o2634, o2633)), i986) → 2402_0_countMetaList_IntArithmetic(EOS(STATIC_2402), 1, i986) | =(matching1, 1)
2396_0_countMetaList_Return(EOS(STATIC_2396), matching1, java.lang.Object(List(EOC, o2662, o2661)), i992) → 2403_0_countMetaList_IntArithmetic(EOS(STATIC_2403), 1, i992) | =(matching1, 1)
2402_0_countMetaList_IntArithmetic(EOS(STATIC_2402), matching1, i986) → 2523_0_countMetaList_IntArithmetic(EOS(STATIC_2523), 1, i986) | =(matching1, 1)
2403_0_countMetaList_IntArithmetic(EOS(STATIC_2403), matching1, i992) → 2523_0_countMetaList_IntArithmetic(EOS(STATIC_2523), 1, i992) | =(matching1, 1)
2488_0_countMetaList_Return(EOS(STATIC_2488), matching1, java.lang.Object(List(EOC, NULL, o2813)), i1068) → 2507_0_countMetaList_Return(EOS(STATIC_2507), 1, java.lang.Object(List(EOC, NULL, o2813)), i1068) | =(matching1, 1)
2507_0_countMetaList_Return(EOS(STATIC_2507), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1094) → 2523_0_countMetaList_IntArithmetic(EOS(STATIC_2523), 1, i1094) | =(matching1, 1)
2523_0_countMetaList_IntArithmetic(EOS(STATIC_2523), matching1, i1094) → 2529_0_countMetaList_Return(EOS(STATIC_2529), +(1, i1094)) | =(matching1, 1)
2550_0_countMetaList_Return(EOS(STATIC_2550), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1143) → 2387_0_countMetaList_Return(EOS(STATIC_2387), 1, java.lang.Object(List(EOC, o2860, o2859)), i1143) | =(matching1, 1)
2552_0_countMetaList_Return(EOS(STATIC_2552), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1143) → 2396_0_countMetaList_Return(EOS(STATIC_2396), 1, java.lang.Object(List(EOC, o2860, o2859)), i1143) | =(matching1, 1)
2555_0_countMetaList_Return(EOS(STATIC_2555), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1143) → 2507_0_countMetaList_Return(EOS(STATIC_2507), 1, java.lang.Object(List(EOC, o2860, o2859)), i1143) | =(matching1, 1)

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

P rules:
1638_0_countMetaList_NONNULL(EOS(STATIC_1638), 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))) → 2200_1_countMetaList_InvokeMethod(1638_0_countMetaList_NONNULL(EOS(STATIC_1638), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2))), 1, java.lang.Object(List(EOC, x1, x2)))
1638_0_countMetaList_NONNULL(EOS(STATIC_1638), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), java.lang.Object(List(EOC, java.lang.Object(x0), x1))) → 1741_1_countMetaList_InvokeMethod(1638_0_countMetaList_NONNULL(EOS(STATIC_1638), x1, x1), 1, x1)
1638_0_countMetaList_NONNULL(EOS(STATIC_1638), java.lang.Object(List(EOC, NULL, x0)), java.lang.Object(List(EOC, NULL, x0))) → 1733_1_countMetaList_InvokeMethod(1638_0_countMetaList_NONNULL(EOS(STATIC_1638), x0, x0), 1, x0)
R rules:
1638_0_countMetaList_NONNULL(EOS(STATIC_1638), NULL, NULL) → 1658_0_countMetaList_Return(EOS(STATIC_1658), NULL, 0)
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return(EOS(STATIC_1658), NULL, 0), 1, NULL) → 2529_0_countMetaList_Return(EOS(STATIC_2529), 1)
1741_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return(EOS(STATIC_1658), NULL, 0), 1, NULL) → 2529_0_countMetaList_Return(EOS(STATIC_2529), 1)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(EOS(STATIC_2529), x0), 1, x2) → 2529_0_countMetaList_Return(EOS(STATIC_2529), +(1, x0))
1741_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(EOS(STATIC_2529), x0), 1, x2) → 2529_0_countMetaList_Return(EOS(STATIC_2529), +(1, x0))
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(EOS(STATIC_2529), x0), 1, java.lang.Object(List(EOC, x2, x3))) → 2529_0_countMetaList_Return(EOS(STATIC_2529), +(1, x0))

Filtered ground terms:

1733_1_countMetaList_InvokeMethod(x1, x2, x3) → 1733_1_countMetaList_InvokeMethod(x1, x3)
1638_0_countMetaList_NONNULL(x1, x2, x3) → 1638_0_countMetaList_NONNULL(x2, x3)
List(x1, x2, x3) → List(x2, x3)
1741_1_countMetaList_InvokeMethod(x1, x2, x3) → 1741_1_countMetaList_InvokeMethod(x1, x3)
2200_1_countMetaList_InvokeMethod(x1, x2, x3) → 2200_1_countMetaList_InvokeMethod(x1, x3)
2529_0_countMetaList_Return(x1, x2) → 2529_0_countMetaList_Return(x2)
1658_0_countMetaList_Return(x1, x2, x3) → 1658_0_countMetaList_Return

Filtered duplicate args:

1638_0_countMetaList_NONNULL(x1, x2) → 1638_0_countMetaList_NONNULL(x2)

Filtered unneeded arguments:

2200_1_countMetaList_InvokeMethod(x1, x2) → 2200_1_countMetaList_InvokeMethod(x1)

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

P rules:
1638_0_countMetaList_NONNULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 2200_1_countMetaList_InvokeMethod(1638_0_countMetaList_NONNULL(java.lang.Object(List(x1, x2))))
1638_0_countMetaList_NONNULL(java.lang.Object(List(java.lang.Object(x0), x1))) → 1741_1_countMetaList_InvokeMethod(1638_0_countMetaList_NONNULL(x1), x1)
1638_0_countMetaList_NONNULL(java.lang.Object(List(NULL, x0))) → 1733_1_countMetaList_InvokeMethod(1638_0_countMetaList_NONNULL(x0), x0)
R rules:
1638_0_countMetaList_NONNULL(NULL) → 1658_0_countMetaList_Return
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL) → 2529_0_countMetaList_Return(1)
1741_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL) → 2529_0_countMetaList_Return(1)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x2) → 2529_0_countMetaList_Return(+(1, x0))
1741_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x2) → 2529_0_countMetaList_Return(+(1, x0))
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0)) → 2529_0_countMetaList_Return(+(1, x0))

Performed bisimulation on rules. Used the following equivalence classes: {[1733_1_countMetaList_InvokeMethod_2, 1741_1_countMetaList_InvokeMethod_2]=1733_1_countMetaList_InvokeMethod_2}

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

P rules:
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1, x2)))
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0), x1))) → 1638_0_COUNTMETALIST_NONNULL(x1)
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0))) → 1638_0_COUNTMETALIST_NONNULL(x0)
R rules:
1638_0_countMetaList_NONNULL(NULL) → 1658_0_countMetaList_Return
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL) → 2529_0_countMetaList_Return(1)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x2) → 2529_0_countMetaList_Return(+(1, x0))
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0)) → 2529_0_countMetaList_Return(+(1, x0))

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

Integer

The ITRS R consists of the following rules:
1638_0_countMetaList_NONNULL(NULL) → 1658_0_countMetaList_Return
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL) → 2529_0_countMetaList_Return(1)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x2) → 2529_0_countMetaList_Return(1 + x0)
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0)) → 2529_0_countMetaList_Return(1 + x0)

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

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

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

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

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

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

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

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

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

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

The set Q consists of the following terms:
1638_0_countMetaList_NONNULL(NULL)
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x1)
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0))

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

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

1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1638_0_COUNTMETALIST_NONNULL(x1[1])
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1638_0_COUNTMETALIST_NONNULL(x0[2])

The TRS R consists of the following rules:

1638_0_countMetaList_NONNULL(NULL) → 1658_0_countMetaList_Return
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL) → 2529_0_countMetaList_Return(pos(s(0)))
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x2) → 2529_0_countMetaList_Return(plus_int(pos(s(0)), x0))
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0)) → 2529_0_countMetaList_Return(plus_int(pos(s(0)), x0))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

1638_0_countMetaList_NONNULL(NULL)
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x1)
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

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

(10) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(11) Obligation:

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

1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1638_0_COUNTMETALIST_NONNULL(x1[1])
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1638_0_COUNTMETALIST_NONNULL(x0[2])

R is empty.
The set Q consists of the following terms:

1638_0_countMetaList_NONNULL(NULL)
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x1)
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

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

(12) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

1638_0_countMetaList_NONNULL(NULL)
1733_1_countMetaList_InvokeMethod(1658_0_countMetaList_Return, NULL)
1733_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0), x1)
2200_1_countMetaList_InvokeMethod(2529_0_countMetaList_Return(x0))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

(13) Obligation:

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

1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1638_0_COUNTMETALIST_NONNULL(x1[1])
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1638_0_COUNTMETALIST_NONNULL(x0[2])

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

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

1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1638_0_COUNTMETALIST_NONNULL(x0[2])

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(1638_0_COUNTMETALIST_NONNULL(x₁)) = 2·x₁
POL(List(x₁, x₂)) = x₁ + 2·x₂
POL(NULL) = 0
POL(java.lang.Object(x₁)) = 2·x₁

(15) Obligation:

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

1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1638_0_COUNTMETALIST_NONNULL(x1[1])

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

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

1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1638_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1638_0_COUNTMETALIST_NONNULL(x1[1])

Used ordering: Polynomial interpretation [POLO]:

POL(1638_0_COUNTMETALIST_NONNULL(x₁)) = 2·x₁
POL(List(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(java.lang.Object(x₁)) = 2 + 2·x₁

(17) Obligation:

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

(18) PisEmptyProof (EQUIVALENT transformation)

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

(19) YES

(20) Obligation:

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

(21) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 69 rules for P and 0 rules for R.

P rules:
2706_0_createMetaList_Load(EOS(STATIC_2706), i79, i1246, i1246) → 2708_0_createMetaList_GE(EOS(STATIC_2708), i79, i1246, i1246, i79)
2708_0_createMetaList_GE(EOS(STATIC_2708), i79, i1246, i1246, i79) → 2710_0_createMetaList_GE(EOS(STATIC_2710), i79, i1246, i1246, i79)
2710_0_createMetaList_GE(EOS(STATIC_2710), i79, i1246, i1246, i79) → 2713_0_createMetaList_InvokeMethod(EOS(STATIC_2713), i79, i1246) | <(i1246, i79)
2713_0_createMetaList_InvokeMethod(EOS(STATIC_2713), i79, i1246) → 2715_0_random_FieldAccess(EOS(STATIC_2715), i79, i1246)
2715_0_random_FieldAccess(EOS(STATIC_2715), i79, i1246) → 2719_0_random_FieldAccess(EOS(STATIC_2719), i79, i1246)
2719_0_random_FieldAccess(EOS(STATIC_2719), i79, i1246) → 2723_0_random_ArrayAccess(EOS(STATIC_2723), i79, i1246)
2723_0_random_ArrayAccess(EOS(STATIC_2723), i79, i1246) → 2724_0_random_ArrayAccess(EOS(STATIC_2724), i79, i1246)
2724_0_random_ArrayAccess(EOS(STATIC_2724), i79, i1246) → 2727_0_random_Store(EOS(STATIC_2727), i79, i1246, o3114)
2727_0_random_Store(EOS(STATIC_2727), i79, i1246, o3114) → 2730_0_random_FieldAccess(EOS(STATIC_2730), i79, i1246, o3114)
2730_0_random_FieldAccess(EOS(STATIC_2730), i79, i1246, o3114) → 2731_0_random_ConstantStackPush(EOS(STATIC_2731), i79, i1246, o3114)
2731_0_random_ConstantStackPush(EOS(STATIC_2731), i79, i1246, o3114) → 2734_0_random_IntArithmetic(EOS(STATIC_2734), i79, i1246, o3114)
2734_0_random_IntArithmetic(EOS(STATIC_2734), i79, i1246, o3114) → 2737_0_random_FieldAccess(EOS(STATIC_2737), i79, i1246, o3114)
2737_0_random_FieldAccess(EOS(STATIC_2737), i79, i1246, o3114) → 2739_0_random_Load(EOS(STATIC_2739), i79, i1246, o3114)
2739_0_random_Load(EOS(STATIC_2739), i79, i1246, o3114) → 2743_0_random_InvokeMethod(EOS(STATIC_2743), i79, i1246, o3114)
2743_0_random_InvokeMethod(EOS(STATIC_2743), i79, i1246, java.lang.Object(o3132sub)) → 2746_0_random_InvokeMethod(EOS(STATIC_2746), i79, i1246, java.lang.Object(o3132sub))
2746_0_random_InvokeMethod(EOS(STATIC_2746), i79, i1246, java.lang.Object(o3132sub)) → 2749_0_length_Load(EOS(STATIC_2749), i79, i1246, java.lang.Object(o3132sub), java.lang.Object(o3132sub))
2749_0_length_Load(EOS(STATIC_2749), i79, i1246, java.lang.Object(o3132sub), java.lang.Object(o3132sub)) → 2757_0_length_FieldAccess(EOS(STATIC_2757), i79, i1246, java.lang.Object(o3132sub), java.lang.Object(o3132sub))
2757_0_length_FieldAccess(EOS(STATIC_2757), i79, i1246, java.lang.Object(java.lang.String(o3142sub, i1278)), java.lang.Object(java.lang.String(o3142sub, i1278))) → 2758_0_length_FieldAccess(EOS(STATIC_2758), i79, i1246, java.lang.Object(java.lang.String(o3142sub, i1278)), java.lang.Object(java.lang.String(o3142sub, i1278))) | &&(>=(i1278, 0), >=(i1279, 0))
2758_0_length_FieldAccess(EOS(STATIC_2758), i79, i1246, java.lang.Object(java.lang.String(o3142sub, i1278)), java.lang.Object(java.lang.String(o3142sub, i1278))) → 2763_0_length_Return(EOS(STATIC_2763), i79, i1246, java.lang.Object(java.lang.String(o3142sub, i1278)), i1278)
2763_0_length_Return(EOS(STATIC_2763), i79, i1246, java.lang.Object(java.lang.String(o3142sub, i1278)), i1278) → 2768_0_random_Return(EOS(STATIC_2768), i79, i1246, i1278)
2768_0_random_Return(EOS(STATIC_2768), i79, i1246, i1278) → 2769_0_createMetaList_Store(EOS(STATIC_2769), i79, i1246, i1278)
2769_0_createMetaList_Store(EOS(STATIC_2769), i79, i1246, i1278) → 2774_0_createMetaList_ConstantStackPush(EOS(STATIC_2774), i79, i1246, i1278)
2774_0_createMetaList_ConstantStackPush(EOS(STATIC_2774), i79, i1246, i1278) → 2778_0_createMetaList_Store(EOS(STATIC_2778), i79, i1246, i1278)
2778_0_createMetaList_Store(EOS(STATIC_2778), i79, i1246, i1278) → 2781_0_createMetaList_Load(EOS(STATIC_2781), i79, i1246, i1278)
2781_0_createMetaList_Load(EOS(STATIC_2781), i79, i1246, i1278) → 2786_0_createMetaList_Store(EOS(STATIC_2786), i79, i1246, i1278)
2786_0_createMetaList_Store(EOS(STATIC_2786), i79, i1246, i1278) → 2792_0_createMetaList_Load(EOS(STATIC_2792), i79, i1246, i1278)
2792_0_createMetaList_Load(EOS(STATIC_2792), i79, i1246, i1278) → 2899_0_createMetaList_Load(EOS(STATIC_2899), i79, i1246, i1278)
2899_0_createMetaList_Load(EOS(STATIC_2899), i79, i1246, i1339) → 2902_0_createMetaList_LE(EOS(STATIC_2902), i79, i1246, i1339, i1339)
2902_0_createMetaList_LE(EOS(STATIC_2902), i79, i1246, matching1, matching2) → 2903_0_createMetaList_LE(EOS(STATIC_2903), i79, i1246, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
2902_0_createMetaList_LE(EOS(STATIC_2902), i79, i1246, i1342, i1342) → 2904_0_createMetaList_LE(EOS(STATIC_2904), i79, i1246, i1342, i1342)
2903_0_createMetaList_LE(EOS(STATIC_2903), i79, i1246, matching1, matching2) → 2905_0_createMetaList_New(EOS(STATIC_2905), i79, i1246) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
2905_0_createMetaList_New(EOS(STATIC_2905), i79, i1246) → 2908_0_createMetaList_Duplicate(EOS(STATIC_2908), i79, i1246)
2908_0_createMetaList_Duplicate(EOS(STATIC_2908), i79, i1246) → 2910_0_createMetaList_Load(EOS(STATIC_2910), i79, i1246)
2910_0_createMetaList_Load(EOS(STATIC_2910), i79, i1246) → 2913_0_createMetaList_Load(EOS(STATIC_2913), i79, i1246)
2913_0_createMetaList_Load(EOS(STATIC_2913), i79, i1246) → 2916_0_createMetaList_InvokeMethod(EOS(STATIC_2916), i79, i1246)
2916_0_createMetaList_InvokeMethod(EOS(STATIC_2916), i79, i1246) → 2918_0_<init>_Load(EOS(STATIC_2918), i79, i1246)
2918_0_<init>_Load(EOS(STATIC_2918), i79, i1246) → 2921_0_<init>_InvokeMethod(EOS(STATIC_2921), i79, i1246)
2921_0_<init>_InvokeMethod(EOS(STATIC_2921), i79, i1246) → 2924_0_<init>_Load(EOS(STATIC_2924), i79, i1246)
2924_0_<init>_Load(EOS(STATIC_2924), i79, i1246) → 2927_0_<init>_Load(EOS(STATIC_2927), i79, i1246)
2927_0_<init>_Load(EOS(STATIC_2927), i79, i1246) → 2929_0_<init>_FieldAccess(EOS(STATIC_2929), i79, i1246)
2929_0_<init>_FieldAccess(EOS(STATIC_2929), i79, i1246) → 2933_0_<init>_Load(EOS(STATIC_2933), i79, i1246)
2933_0_<init>_Load(EOS(STATIC_2933), i79, i1246) → 2936_0_<init>_Load(EOS(STATIC_2936), i79, i1246)
2936_0_<init>_Load(EOS(STATIC_2936), i79, i1246) → 2939_0_<init>_FieldAccess(EOS(STATIC_2939), i79, i1246)
2939_0_<init>_FieldAccess(EOS(STATIC_2939), i79, i1246) → 2942_0_<init>_Return(EOS(STATIC_2942), i79, i1246)
2942_0_<init>_Return(EOS(STATIC_2942), i79, i1246) → 2946_0_createMetaList_Store(EOS(STATIC_2946), i79, i1246)
2946_0_createMetaList_Store(EOS(STATIC_2946), i79, i1246) → 2948_0_createMetaList_Inc(EOS(STATIC_2948), i79, i1246)
2948_0_createMetaList_Inc(EOS(STATIC_2948), i79, i1246) → 2951_0_createMetaList_JMP(EOS(STATIC_2951), i79, +(i1246, 1)) | >=(i1246, 0)
2951_0_createMetaList_JMP(EOS(STATIC_2951), i79, i1348) → 2953_0_createMetaList_Load(EOS(STATIC_2953), i79, i1348)
2953_0_createMetaList_Load(EOS(STATIC_2953), i79, i1348) → 2704_0_createMetaList_Load(EOS(STATIC_2704), i79, i1348)
2704_0_createMetaList_Load(EOS(STATIC_2704), i79, i1246) → 2706_0_createMetaList_Load(EOS(STATIC_2706), i79, i1246, i1246)
2904_0_createMetaList_LE(EOS(STATIC_2904), i79, i1246, i1342, i1342) → 2907_0_createMetaList_New(EOS(STATIC_2907), i79, i1246, i1342) | >(i1342, 0)
2907_0_createMetaList_New(EOS(STATIC_2907), i79, i1246, i1342) → 2909_0_createMetaList_Duplicate(EOS(STATIC_2909), i79, i1246, i1342)
2909_0_createMetaList_Duplicate(EOS(STATIC_2909), i79, i1246, i1342) → 2912_0_createMetaList_ConstantStackPush(EOS(STATIC_2912), i79, i1246, i1342)
2912_0_createMetaList_ConstantStackPush(EOS(STATIC_2912), i79, i1246, i1342) → 2914_0_createMetaList_Load(EOS(STATIC_2914), i79, i1246, i1342)
2914_0_createMetaList_Load(EOS(STATIC_2914), i79, i1246, i1342) → 2917_0_createMetaList_InvokeMethod(EOS(STATIC_2917), i79, i1246, i1342)
2917_0_createMetaList_InvokeMethod(EOS(STATIC_2917), i79, i1246, i1342) → 2919_0_<init>_Load(EOS(STATIC_2919), i79, i1246, i1342)
2919_0_<init>_Load(EOS(STATIC_2919), i79, i1246, i1342) → 2923_0_<init>_InvokeMethod(EOS(STATIC_2923), i79, i1246, i1342)
2923_0_<init>_InvokeMethod(EOS(STATIC_2923), i79, i1246, i1342) → 2925_0_<init>_Load(EOS(STATIC_2925), i79, i1246, i1342)
2925_0_<init>_Load(EOS(STATIC_2925), i79, i1246, i1342) → 2928_0_<init>_Load(EOS(STATIC_2928), i79, i1246, i1342)
2928_0_<init>_Load(EOS(STATIC_2928), i79, i1246, i1342) → 2931_0_<init>_FieldAccess(EOS(STATIC_2931), i79, i1246, i1342)
2931_0_<init>_FieldAccess(EOS(STATIC_2931), i79, i1246, i1342) → 2935_0_<init>_Load(EOS(STATIC_2935), i79, i1246, i1342)
2935_0_<init>_Load(EOS(STATIC_2935), i79, i1246, i1342) → 2937_0_<init>_Load(EOS(STATIC_2937), i79, i1246, i1342)
2937_0_<init>_Load(EOS(STATIC_2937), i79, i1246, i1342) → 2940_0_<init>_FieldAccess(EOS(STATIC_2940), i79, i1246, i1342)
2940_0_<init>_FieldAccess(EOS(STATIC_2940), i79, i1246, i1342) → 2944_0_<init>_Return(EOS(STATIC_2944), i79, i1246, i1342)
2944_0_<init>_Return(EOS(STATIC_2944), i79, i1246, i1342) → 2947_0_createMetaList_Store(EOS(STATIC_2947), i79, i1246, i1342)
2947_0_createMetaList_Store(EOS(STATIC_2947), i79, i1246, i1342) → 2949_0_createMetaList_Inc(EOS(STATIC_2949), i79, i1246, i1342)
2949_0_createMetaList_Inc(EOS(STATIC_2949), i79, i1246, i1342) → 2952_0_createMetaList_JMP(EOS(STATIC_2952), i79, i1246, +(i1342, -1)) | >(i1342, 0)
2952_0_createMetaList_JMP(EOS(STATIC_2952), i79, i1246, i1349) → 2955_0_createMetaList_Load(EOS(STATIC_2955), i79, i1246, i1349)
2955_0_createMetaList_Load(EOS(STATIC_2955), i79, i1246, i1349) → 2899_0_createMetaList_Load(EOS(STATIC_2899), i79, i1246, i1349)
R rules:

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

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

Filtered ground terms:

2902_0_createMetaList_LE(x1, x2, x3, x4, x5) → 2902_0_createMetaList_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_2902_0_createMetaList_LE1(x1, x2, x3, x4, x5, x6) → Cond_2902_0_createMetaList_LE1(x1, x3, x4, x5, x6)
Cond_2902_0_createMetaList_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_2902_0_createMetaList_LE(x1, x3, x4, x7)

Filtered duplicate args:

2902_0_createMetaList_LE(x1, x2, x3, x4) → 2902_0_createMetaList_LE(x1, x2, x4)
Cond_2902_0_createMetaList_LE1(x1, x2, x3, x4, x5) → Cond_2902_0_createMetaList_LE1(x1, x2, x3, x5)

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

P rules:
2902_0_createMetaList_LE(x0, x1, 0) → 2902_0_createMetaList_LE(x0, +(x1, 1), x4) | &&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1)))
2902_0_createMetaList_LE(x0, x1, x2) → 2902_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:
2902_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
COND_2902_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2902_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
2902_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2902_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
COND_2902_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2902_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
R rules:

(22) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(1): COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_0_CREATEMETALIST_LE(x0[1], x1[1] + 1, x4[1])
(2): 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_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.

(23) 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@36735db5 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 2902_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4) the following chains were created:

We consider the chain COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_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 ⇒ 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2902_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 ⇒ 2902_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥COND_2902_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_2902_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_2902_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_2902_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_2902_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_2902_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_2902_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_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_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] ⇒ 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2902_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 ⇒ 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2902_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_2902_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_2902_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_2902_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_2902_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_2902_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2902_0_CREATEMETALIST_LE(x0, +(x1, 1), x4) the following chains were created:

We consider the chain 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_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_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2902_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2902_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_2902_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥NonInfC∧COND_2902_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥2902_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), 0)∧(U^Increasing(2902_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(2902_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(2902_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(2902_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(2902_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 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_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_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2902_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2902_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_2902_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥2902_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), x4[0])∧(U^Increasing(2902_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(2902_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(2902_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(2902_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(2902_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 2902_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2902_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2) the following chains were created:

We consider the chain 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_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] ⇒ 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2902_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 ⇒ 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2902_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_2902_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_2902_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_2902_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_2902_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_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2902_0_CREATEMETALIST_LE(x0, x1, +(x2, -1)) the following chains were created:

We consider the chain 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2902_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2902_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(2902_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(2902_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(2902_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(2902_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(2902_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 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2902_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2902_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(2902_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(2902_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(2902_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(2902_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(2902_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.

2902_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2902_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_2902_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_2902_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_2902_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_2902_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2902_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
- (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2902_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(2902_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)
2902_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2902_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2902_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
- (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(2902_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(2902_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) = 0
POL(2902_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁
POL(0) = 0
POL(COND_2902_0_CREATEMETALIST_LE(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄ + [-1]x₃ + x₂ + [-1]x₁
POL(&&(x₁, x₂)) = 0
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_2902_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂

The following pairs are in P_>:

COND_2902_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2902_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P_bound:

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

The following pairs are in P_≥:

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

(24) 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): 2902_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2902_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(2): 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_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.

(25) IDependencyGraphProof (EQUIVALENT transformation)

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

(26) 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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)
(2): 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_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.

(27) 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@36735db5 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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) the following chains were created:

We consider the chain 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2902_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2902_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(2902_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(2902_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(2902_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(2902_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(2902_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 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) the following chains were created:

We consider the chain 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_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] ⇒ 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2902_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 ⇒ 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2902_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_2902_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_2902_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_2902_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_2902_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_2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
- (x2[2] ≥ 0 ⇒ (U^Increasing(2902_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)
2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2902_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_2902_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + x₄
POL(2902_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_2902_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2902_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

The following pairs are in P_bound:

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

The following pairs are in P_≥:

2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

There are no usable rules.

(28) 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): 2902_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2902_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])

The set Q is empty.

(29) IDependencyGraphProof (EQUIVALENT transformation)

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

(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) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) QReductionProof (EQUIVALENT transformation)

(13) Obligation:

(14) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(15) Obligation:

(16) MRRProof (EQUIVALENT transformation)

(17) Obligation:

(18) PisEmptyProof (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIDPv1Proof (SOUND transformation)

(22) Obligation:

(23) IDPNonInfProof (SOUND transformation)

(24) Obligation:

(25) IDependencyGraphProof (EQUIVALENT transformation)

(26) Obligation:

(27) IDPNonInfProof (SOUND transformation)

(28) Obligation:

(29) IDependencyGraphProof (EQUIVALENT transformation)

(30) TRUE