Termination proof of /tmp/tmpIpUhTC/CountMetaList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 ITRStoIDPProof (⇔)

        ↳7 IDP

        ↳8 UsableRulesProof (⇔)

        ↳9 IDP

        ↳10 ItpfGraphProof (⇔)

        ↳11 IDP

        ↳12 IDPNonInfProof (⇐)

        ↳13 AND

            ↳14 IDP

                ↳15 IDependencyGraphProof (⇔)

                ↳16 TRUE

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔)

                ↳19 TRUE

    ↳20 ITRS

        ↳21 ITRSFilterProcessorProof (⇐)

        ↳22 ITRS

        ↳23 ITRStoIDPProof (⇔)

        ↳24 IDP

        ↳25 UsableRulesProof (⇔)

        ↳26 IDP

        ↳27 ItpfGraphProof (⇔)

        ↳28 IDP

        ↳29 IDPNonInfProof (⇐)

        ↳30 AND

            ↳31 IDP

                ↳32 IDependencyGraphProof (⇔)

                ↳33 IDP

                ↳34 IDPNonInfProof (⇐)

                ↳35 AND

                    ↳36 IDP

                        ↳37 IDependencyGraphProof (⇔)

                        ↳38 TRUE

                    ↳39 IDP

                        ↳40 IDependencyGraphProof (⇔)

                        ↳41 TRUE

            ↳42 IDP

                ↳43 IDependencyGraphProof (⇔)

                ↳44 IDP

                ↳45 IDPNonInfProof (⇐)

                ↳46 AND

                    ↳47 IDP

                        ↳48 IDependencyGraphProof (⇔)

                        ↳49 TRUE

                    ↳50 IDP

                        ↳51 IDependencyGraphProof (⇔)

                        ↳52 TRUE

(0) Obligation:

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

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

		int count = countMetaList(l);
	}

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

		return res;
	}

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

		return cur;
	}
}

class List {
	Object value;
	List next;

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


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

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

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 355 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS 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 TRS R consists of the following rules:
Load2486(o2217, java.lang.Object(List(java.lang.Object(List(o4531, o4532)), o2493)), i128) → Inc4194(o2217new, java.lang.Object(List(o4532, o2493)), i128)
Load2486(o2217, java.lang.Object(List(java.lang.Object(o2641Sub1234), o2493)), i128) → Inc4194(o2217, o2493, i128)
Load2486(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), i128) → Inc4194(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), o2498, i128)
Load2486(java.lang.Object(List(NULL, o2498)), java.lang.Object(List(NULL, o2498)), i128) → Inc4194(java.lang.Object(List(NULL, o2498)), o2498, i128)
Inc4194(o2217, o2493, i128) → Load2486(o2217, o2493, i128 + 1)
Load2486(o2217, java.lang.Object(List(NULL, o2493)), i128) → Load2486(o2217, o2493, i128 + 1)
Load2486(java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), i128) → Load2486(java.lang.Object(List(o4550, o2498)), java.lang.Object(List(o4550, o2498)), i128 + 1)
The set Q consists of the following terms:
Load2486(x0, java.lang.Object(List(java.lang.Object(x1), x2)), x3)
Inc4194(x0, x1, x2)
Load2486(x0, java.lang.Object(List(NULL, x1)), x2)

(6) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(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:
Load2486(o2217, java.lang.Object(List(java.lang.Object(List(o4531, o4532)), o2493)), i128) → Inc4194(o2217new, java.lang.Object(List(o4532, o2493)), i128)
Load2486(o2217, java.lang.Object(List(java.lang.Object(o2641Sub1234), o2493)), i128) → Inc4194(o2217, o2493, i128)
Load2486(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), i128) → Inc4194(java.lang.Object(List(java.lang.Object(o2824Sub1234), o2498)), o2498, i128)
Load2486(java.lang.Object(List(NULL, o2498)), java.lang.Object(List(NULL, o2498)), i128) → Inc4194(java.lang.Object(List(NULL, o2498)), o2498, i128)
Inc4194(o2217, o2493, i128) → Load2486(o2217, o2493, i128 + 1)
Load2486(o2217, java.lang.Object(List(NULL, o2493)), i128) → Load2486(o2217, o2493, i128 + 1)
Load2486(java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), java.lang.Object(List(java.lang.Object(List(o4549, o4550)), o2498)), i128) → Load2486(java.lang.Object(List(o4550, o2498)), java.lang.Object(List(o4550, o2498)), i128 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
(1): LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
(2): LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
(3): LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
(4): INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], i128[4] + 1)
(5): LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], i128[5] + 1)
(6): LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), i128[6] + 1)

(0) -> (4), if ((java.lang.Object(List(o4532[0], o2493[0])) →^* o2493[4])∧(i128[0] →^* i128[4])∧(o2217new[0] →^* o2217[4]))

(1) -> (4), if ((o2493[1] →^* o2493[4])∧(i128[1] →^* i128[4])∧(o2217[1] →^* o2217[4]))

(2) -> (4), if ((java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])) →^* o2217[4])∧(i128[2] →^* i128[4])∧(o2498[2] →^* o2493[4]))

(3) -> (4), if ((o2498[3] →^* o2493[4])∧(i128[3] →^* i128[4])∧(java.lang.Object(List(NULL, o2498[3])) →^* o2217[4]))

(4) -> (0), if ((i128[4] + 1 →^* i128[0])∧(o2493[4] →^* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[4] →^* o2217[0]))

(4) -> (1), if ((o2217[4] →^* o2217[1])∧(i128[4] + 1 →^* i128[1])∧(o2493[4] →^* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1]))))

(4) -> (2), if ((o2493[4] →^* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[4] + 1 →^* i128[2])∧(o2217[4] →^* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2]))))

(4) -> (3), if ((i128[4] + 1 →^* i128[3])∧(o2217[4] →^* java.lang.Object(List(NULL, o2498[3])))∧(o2493[4] →^* java.lang.Object(List(NULL, o2498[3]))))

(4) -> (5), if ((o2493[4] →^* java.lang.Object(List(NULL, o2493[5])))∧(i128[4] + 1 →^* i128[5])∧(o2217[4] →^* o2217[5]))

(4) -> (6), if ((i128[4] + 1 →^* i128[6])∧(o2493[4] →^* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(o2217[4] →^* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(5) -> (0), if ((o2493[5] →^* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(o2217[5] →^* o2217[0])∧(i128[5] + 1 →^* i128[0]))

(5) -> (1), if ((o2493[5] →^* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(o2217[5] →^* o2217[1])∧(i128[5] + 1 →^* i128[1]))

(5) -> (2), if ((o2493[5] →^* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(o2217[5] →^* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[5] + 1 →^* i128[2]))

(5) -> (3), if ((o2493[5] →^* java.lang.Object(List(NULL, o2498[3])))∧(o2217[5] →^* java.lang.Object(List(NULL, o2498[3])))∧(i128[5] + 1 →^* i128[3]))

(5) -> (5), if ((i128[5] + 1 →^* i128[5]')∧(o2493[5] →^* java.lang.Object(List(NULL, o2493[5]')))∧(o2217[5] →^* o2217[5]'))

(5) -> (6), if ((o2217[5] →^* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])))∧(i128[5] + 1 →^* i128[6])∧(o2493[5] →^* java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6]))))

(6) -> (0), if ((java.lang.Object(List(o4550[6], o2498[6])) →^* java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])))∧(i128[6] + 1 →^* i128[0])∧(java.lang.Object(List(o4550[6], o2498[6])) →^* o2217[0]))

(6) -> (1), if ((java.lang.Object(List(o4550[6], o2498[6])) →^* java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])))∧(i128[6] + 1 →^* i128[1])∧(java.lang.Object(List(o4550[6], o2498[6])) →^* o2217[1]))

(6) -> (2), if ((java.lang.Object(List(o4550[6], o2498[6])) →^* java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])))∧(i128[6] + 1 →^* i128[2]))

(6) -> (3), if ((java.lang.Object(List(o4550[6], o2498[6])) →^* java.lang.Object(List(NULL, o2498[3])))∧(i128[6] + 1 →^* i128[3]))

(6) -> (5), if ((i128[6] + 1 →^* i128[5])∧(java.lang.Object(List(o4550[6], o2498[6])) →^* java.lang.Object(List(NULL, o2493[5])))∧(java.lang.Object(List(o4550[6], o2498[6])) →^* o2217[5]))

(6) -> (6), if ((java.lang.Object(List(o4550[6], o2498[6])) →^* java.lang.Object(List(java.lang.Object(List(o4549[6]', o4550[6]')), o2498[6]')))∧(i128[6] + 1 →^* i128[6]'))

The set Q consists of the following terms:
Load2486(x0, java.lang.Object(List(java.lang.Object(x1), x2)), x3)
Inc4194(x0, x1, x2)
Load2486(x0, java.lang.Object(List(NULL, x1)), x2)

(8) 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.

(9) Obligation:

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

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

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2486(o2217[0], java.lang.Object(List(java.lang.Object(List(o4531[0], o4532[0])), o2493[0])), i128[0]) → INC4194(o2217new[0], java.lang.Object(List(o4532[0], o2493[0])), i128[0])
(1): LOAD2486(o2217[1], java.lang.Object(List(java.lang.Object(o2641Sub1234[1]), o2493[1])), i128[1]) → INC4194(o2217[1], o2493[1], i128[1])
(2): LOAD2486(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), i128[2]) → INC4194(java.lang.Object(List(java.lang.Object(o2824Sub1234[2]), o2498[2])), o2498[2], i128[2])
(3): LOAD2486(java.lang.Object(List(NULL, o2498[3])), java.lang.Object(List(NULL, o2498[3])), i128[3]) → INC4194(java.lang.Object(List(NULL, o2498[3])), o2498[3], i128[3])
(4): INC4194(o2217[4], o2493[4], i128[4]) → LOAD2486(o2217[4], o2493[4], i128[4] + 1)
(5): LOAD2486(o2217[5], java.lang.Object(List(NULL, o2493[5])), i128[5]) → LOAD2486(o2217[5], o2493[5], i128[5] + 1)
(6): LOAD2486(java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), java.lang.Object(List(java.lang.Object(List(o4549[6], o4550[6])), o2498[6])), i128[6]) → LOAD2486(java.lang.Object(List(o4550[6], o2498[6])), java.lang.Object(List(o4550[6], o2498[6])), i128[6] + 1)