Termination proof of /tmp/tmpbc6oLc/ListReverseAcyclicList.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 415 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 104 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 46 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 JBCTerminationSCC

        ↳13 SCCToIDPv1Proof (⇒, 118 ms)

        ↳14 IDP

        ↳15 IDPNonInfProof (⇒, 84 ms)

        ↳16 AND

            ↳17 IDP

                ↳18 IDependencyGraphProof (⇔, 0 ms)

                ↳19 TRUE

            ↳20 IDP

                ↳21 IDependencyGraphProof (⇔, 0 ms)

                ↳22 TRUE

(0) Obligation:

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

public class ListReverseAcyclicList {
	public static void main(String... args) {
		List x = List.createList(args[0].length(), null);
		List.reverse(x);
	}
}

class List {
	List n;

	public List(List next) {
		this.n = next;
	}

	public static void reverse(List x) {		
		List y = null;
		while (x != null) {
			List z = x;
			x = x.n;
			z.n = y;
			y = z;
		}
	}

	public static List createList(int l, List end) {
		while (--l > 0) {
			end = new List(end);
		}
		return end;
	}

	public static List createCycle(int l) {
		List last = new List(null);
		List first = createList(l - 1, last);
		last.n = first;
		return first;
	}

	public static List createPanhandleList(int pl, int cl) {
		return createList(pl, createCycle(cl));
	}

}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ListReverseAcyclicList.main([Ljava/lang/String;)V: Graph of 142 nodes with 2 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: ListReverseAcyclicList.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 28 rules for P and 0 rules for R.

P rules:
819_0_reverse_NULL(EOS(STATIC_819), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub)) → 820_0_reverse_NULL(EOS(STATIC_820), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub))
820_0_reverse_NULL(EOS(STATIC_820), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub)) → 823_0_reverse_Load(EOS(STATIC_823), o181, java.lang.Object(o261sub), o180)
823_0_reverse_Load(EOS(STATIC_823), o181, java.lang.Object(o261sub), o180) → 826_0_reverse_Store(EOS(STATIC_826), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub))
826_0_reverse_Store(EOS(STATIC_826), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub)) → 829_0_reverse_Load(EOS(STATIC_829), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub))
829_0_reverse_Load(EOS(STATIC_829), o181, java.lang.Object(o261sub), o180, java.lang.Object(o261sub)) → 833_0_reverse_FieldAccess(EOS(STATIC_833), o181, o180, java.lang.Object(o261sub), java.lang.Object(o261sub))
833_0_reverse_FieldAccess(EOS(STATIC_833), o181, o180, java.lang.Object(o261sub), java.lang.Object(o261sub)) → 835_0_reverse_FieldAccess(EOS(STATIC_835), o181, o180, java.lang.Object(o261sub), java.lang.Object(o261sub))
833_0_reverse_FieldAccess(EOS(STATIC_833), java.lang.Object(o261sub), o180, java.lang.Object(o261sub), java.lang.Object(o261sub)) → 836_0_reverse_FieldAccess(EOS(STATIC_836), java.lang.Object(o261sub), o180, java.lang.Object(o261sub), java.lang.Object(o261sub))
835_0_reverse_FieldAccess(EOS(STATIC_835), o181, o180, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263))) → 837_0_reverse_FieldAccess(EOS(STATIC_837), o181, o180, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263)))
837_0_reverse_FieldAccess(EOS(STATIC_837), o181, o180, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263))) → 840_0_reverse_Store(EOS(STATIC_840), o181, o180, java.lang.Object(List(EOC, o263)), o263)
840_0_reverse_Store(EOS(STATIC_840), o181, o180, java.lang.Object(List(EOC, o263)), o263) → 844_0_reverse_Load(EOS(STATIC_844), o181, o263, o180, java.lang.Object(List(EOC, o263)))
844_0_reverse_Load(EOS(STATIC_844), o181, o263, o180, java.lang.Object(List(EOC, o263))) → 847_0_reverse_Load(EOS(STATIC_847), o181, o263, o180, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263)))
847_0_reverse_Load(EOS(STATIC_847), o181, o263, o180, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263))) → 850_0_reverse_FieldAccess(EOS(STATIC_850), o181, o263, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263)), o180)
850_0_reverse_FieldAccess(EOS(STATIC_850), o181, o263, java.lang.Object(List(EOC, o263)), java.lang.Object(List(EOC, o263)), o180) → 855_0_reverse_Load(EOS(STATIC_855), o181, o263, java.lang.Object(List(EOC, o180)))
855_0_reverse_Load(EOS(STATIC_855), o181, o263, java.lang.Object(List(EOC, o180))) → 859_0_reverse_Store(EOS(STATIC_859), o181, o263, java.lang.Object(List(EOC, o180)))
859_0_reverse_Store(EOS(STATIC_859), o181, o263, java.lang.Object(List(EOC, o180))) → 863_0_reverse_JMP(EOS(STATIC_863), o181, o263, java.lang.Object(List(EOC, o180)))
863_0_reverse_JMP(EOS(STATIC_863), o181, o263, java.lang.Object(List(EOC, o180))) → 869_0_reverse_Load(EOS(STATIC_869), o181, o263, java.lang.Object(List(EOC, o180)))
869_0_reverse_Load(EOS(STATIC_869), o181, o263, java.lang.Object(List(EOC, o180))) → 753_0_reverse_Load(EOS(STATIC_753), o181, o263, java.lang.Object(List(EOC, o180)))
753_0_reverse_Load(EOS(STATIC_753), o181, o179, o180) → 819_0_reverse_NULL(EOS(STATIC_819), o181, o179, o180, o179)
836_0_reverse_FieldAccess(EOS(STATIC_836), java.lang.Object(List(EOC, o265)), o180, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265))) → 839_0_reverse_FieldAccess(EOS(STATIC_839), java.lang.Object(List(EOC, o265)), o180, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265)))
839_0_reverse_FieldAccess(EOS(STATIC_839), java.lang.Object(List(EOC, o265)), o180, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265))) → 842_0_reverse_Store(EOS(STATIC_842), java.lang.Object(List(EOC, o265)), o180, java.lang.Object(List(EOC, o265)), o265)
842_0_reverse_Store(EOS(STATIC_842), java.lang.Object(List(EOC, o265)), o180, java.lang.Object(List(EOC, o265)), o265) → 845_0_reverse_Load(EOS(STATIC_845), java.lang.Object(List(EOC, o265)), o265, o180, java.lang.Object(List(EOC, o265)))
845_0_reverse_Load(EOS(STATIC_845), java.lang.Object(List(EOC, o265)), o265, o180, java.lang.Object(List(EOC, o265))) → 849_0_reverse_Load(EOS(STATIC_849), java.lang.Object(List(EOC, o265)), o265, o180, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265)))
849_0_reverse_Load(EOS(STATIC_849), java.lang.Object(List(EOC, o265)), o265, o180, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265))) → 852_0_reverse_FieldAccess(EOS(STATIC_852), java.lang.Object(List(EOC, o265)), o265, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265)), o180)
852_0_reverse_FieldAccess(EOS(STATIC_852), java.lang.Object(List(EOC, o265)), o265, java.lang.Object(List(EOC, o265)), java.lang.Object(List(EOC, o265)), o180) → 858_0_reverse_Load(EOS(STATIC_858), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180)))
858_0_reverse_Load(EOS(STATIC_858), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180))) → 862_0_reverse_Store(EOS(STATIC_862), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180)))
862_0_reverse_Store(EOS(STATIC_862), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180))) → 865_0_reverse_JMP(EOS(STATIC_865), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180)))
865_0_reverse_JMP(EOS(STATIC_865), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180))) → 872_0_reverse_Load(EOS(STATIC_872), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180)))
872_0_reverse_Load(EOS(STATIC_872), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180))) → 753_0_reverse_Load(EOS(STATIC_753), java.lang.Object(List(EOC, o180)), o265, java.lang.Object(List(EOC, o180)))
R rules:

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

P rules:
819_0_reverse_NULL(EOS(STATIC_819), x0, java.lang.Object(List(EOC, x1)), x2, java.lang.Object(List(EOC, x1))) → 819_0_reverse_NULL(EOS(STATIC_819), x0, x1, java.lang.Object(List(EOC, x2)), x1)
819_0_reverse_NULL(EOS(STATIC_819), java.lang.Object(List(EOC, x0)), java.lang.Object(List(EOC, x0)), x1, java.lang.Object(List(EOC, x0))) → 819_0_reverse_NULL(EOS(STATIC_819), java.lang.Object(List(EOC, x1)), x0, java.lang.Object(List(EOC, x1)), x0)
R rules:

Filtered ground terms:

819_0_reverse_NULL(x1, x2, x3, x4, x5) → 819_0_reverse_NULL(x2, x3, x4, x5)
List(x1, x2) → List(x2)
EOS(x1) → EOS

Filtered duplicate args:

819_0_reverse_NULL(x1, x2, x3, x4) → 819_0_reverse_NULL(x1, x3, x4)

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

P rules:
819_0_reverse_NULL(x0, x2, java.lang.Object(List(x1))) → 819_0_reverse_NULL(x0, java.lang.Object(List(x2)), x1)
819_0_reverse_NULL(java.lang.Object(List(x0)), x1, java.lang.Object(List(x0))) → 819_0_reverse_NULL(java.lang.Object(List(x1)), java.lang.Object(List(x1)), x0)
R rules:

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

P rules:
819_0_REVERSE_NULL(x0, x2, java.lang.Object(List(x1))) → 819_0_REVERSE_NULL(x0, java.lang.Object(List(x2)), x1)
819_0_REVERSE_NULL(java.lang.Object(List(x0)), x1, java.lang.Object(List(x0))) → 819_0_REVERSE_NULL(java.lang.Object(List(x1)), java.lang.Object(List(x1)), x0)
R rules:

(7) Obligation:

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

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

The following domains are used:
none

R is empty.

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

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

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

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

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

The set Q is empty.

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

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

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

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

819_0_REVERSE_NULL(x0[0], x2[0], java.lang.Object(List(x1[0]))) → 819_0_REVERSE_NULL(x0[0], java.lang.Object(List(x2[0])), x1[0])
The graph contains the following edges 1 >= 1, 3 > 3
819_0_REVERSE_NULL(java.lang.Object(List(x0[1])), x1[1], java.lang.Object(List(x0[1]))) → 819_0_REVERSE_NULL(java.lang.Object(List(x1[1])), java.lang.Object(List(x1[1])), x0[1])
The graph contains the following edges 1 > 3, 3 > 3

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 17 rules for P and 0 rules for R.

P rules:
274_0_createList_Load(EOS(STATIC_274), i35) → 276_0_createList_LE(EOS(STATIC_276), i35, i35)
276_0_createList_LE(EOS(STATIC_276), i39, i39) → 280_0_createList_LE(EOS(STATIC_280), i39, i39)
280_0_createList_LE(EOS(STATIC_280), i39, i39) → 285_0_createList_New(EOS(STATIC_285), i39) | >(i39, 0)
285_0_createList_New(EOS(STATIC_285), i39) → 289_0_createList_Duplicate(EOS(STATIC_289), i39)
289_0_createList_Duplicate(EOS(STATIC_289), i39) → 293_0_createList_Load(EOS(STATIC_293), i39)
293_0_createList_Load(EOS(STATIC_293), i39) → 297_0_createList_InvokeMethod(EOS(STATIC_297), i39)
297_0_createList_InvokeMethod(EOS(STATIC_297), i39) → 301_0_<init>_Load(EOS(STATIC_301), i39)
301_0_<init>_Load(EOS(STATIC_301), i39) → 305_0_<init>_InvokeMethod(EOS(STATIC_305), i39)
305_0_<init>_InvokeMethod(EOS(STATIC_305), i39) → 308_0_<init>_Load(EOS(STATIC_308), i39)
308_0_<init>_Load(EOS(STATIC_308), i39) → 311_0_<init>_Load(EOS(STATIC_311), i39)
311_0_<init>_Load(EOS(STATIC_311), i39) → 316_0_<init>_FieldAccess(EOS(STATIC_316), i39)
316_0_<init>_FieldAccess(EOS(STATIC_316), i39) → 323_0_<init>_Return(EOS(STATIC_323), i39)
323_0_<init>_Return(EOS(STATIC_323), i39) → 329_0_createList_Store(EOS(STATIC_329), i39)
329_0_createList_Store(EOS(STATIC_329), i39) → 336_0_createList_JMP(EOS(STATIC_336), i39)
336_0_createList_JMP(EOS(STATIC_336), i39) → 359_0_createList_Inc(EOS(STATIC_359), i39)
359_0_createList_Inc(EOS(STATIC_359), i39) → 269_0_createList_Inc(EOS(STATIC_269), i39)
269_0_createList_Inc(EOS(STATIC_269), i31) → 274_0_createList_Load(EOS(STATIC_274), +(i31, -1)) | >=(i31, 0)
R rules:

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

P rules:
274_0_createList_Load(EOS(STATIC_274), x0) → 274_0_createList_Load(EOS(STATIC_274), +(x0, -1)) | >(x0, 0)
R rules:

Filtered ground terms:

274_0_createList_Load(x1, x2) → 274_0_createList_Load(x2)
EOS(x1) → EOS
Cond_274_0_createList_Load(x1, x2, x3) → Cond_274_0_createList_Load(x1, x3)

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

P rules:
274_0_createList_Load(x0) → 274_0_createList_Load(+(x0, -1)) | >(x0, 0)
R rules:

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

P rules:
274_0_CREATELIST_LOAD(x0) → COND_274_0_CREATELIST_LOAD(>(x0, 0), x0)
COND_274_0_CREATELIST_LOAD(TRUE, x0) → 274_0_CREATELIST_LOAD(+(x0, -1))
R rules:

(14) 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): 274_0_CREATELIST_LOAD(x0[0]) → COND_274_0_CREATELIST_LOAD(x0[0] > 0, x0[0])
(1): COND_274_0_CREATELIST_LOAD(TRUE, x0[1]) → 274_0_CREATELIST_LOAD(x0[1] + -1)

(0) -> (1), if (x0[0] > 0 ∧x0[0] →^* x0[1])

(1) -> (0), if (x0[1] + -1 →^* x0[0])

The set Q is empty.

(15) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@2aec4bcb Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 274_0_CREATELIST_LOAD(x0) → COND_274_0_CREATELIST_LOAD(>(x0, 0), x0) the following chains were created:

We consider the chain 274_0_CREATELIST_LOAD(x0[0]) → COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0]), COND_274_0_CREATELIST_LOAD(TRUE, x0[1]) → 274_0_CREATELIST_LOAD(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 274_0_CREATELIST_LOAD(x0[0])≥NonInfC∧274_0_CREATELIST_LOAD(x0[0])≥COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])∧(U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 274_0_CREATELIST_LOAD(x0[0])≥NonInfC∧274_0_CREATELIST_LOAD(x0[0])≥COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])∧(U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_274_0_CREATELIST_LOAD(TRUE, x0) → 274_0_CREATELIST_LOAD(+(x0, -1)) the following chains were created:

We consider the chain COND_274_0_CREATELIST_LOAD(TRUE, x0[1]) → 274_0_CREATELIST_LOAD(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_274_0_CREATELIST_LOAD(TRUE, x0[1])≥NonInfC∧COND_274_0_CREATELIST_LOAD(TRUE, x0[1])≥274_0_CREATELIST_LOAD(+(x0[1], -1))∧(U^Increasing(274_0_CREATELIST_LOAD(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(274_0_CREATELIST_LOAD(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(274_0_CREATELIST_LOAD(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(274_0_CREATELIST_LOAD(+(x0[1], -1))), ≥)∧[bni_10] = 0∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(274_0_CREATELIST_LOAD(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

274_0_CREATELIST_LOAD(x0) → COND_274_0_CREATELIST_LOAD(>(x0, 0), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
COND_274_0_CREATELIST_LOAD(TRUE, x0) → 274_0_CREATELIST_LOAD(+(x0, -1))
- ((U^Increasing(274_0_CREATELIST_LOAD(+(x0[1], -1))), ≥)∧[bni_10] = 0∧0 = 0∧[2 + (-1)bso_11] ≥ 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(274_0_CREATELIST_LOAD(x₁)) = [2]x₁
POL(COND_274_0_CREATELIST_LOAD(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

COND_274_0_CREATELIST_LOAD(TRUE, x0[1]) → 274_0_CREATELIST_LOAD(+(x0[1], -1))

The following pairs are in P_bound:

274_0_CREATELIST_LOAD(x0[0]) → COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

274_0_CREATELIST_LOAD(x0[0]) → COND_274_0_CREATELIST_LOAD(>(x0[0], 0), x0[0])

There are no usable rules.

(16) Complex Obligation (AND)

(17) 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): 274_0_CREATELIST_LOAD(x0[0]) → COND_274_0_CREATELIST_LOAD(x0[0] > 0, x0[0])

The set Q is empty.

(18) IDependencyGraphProof (EQUIVALENT transformation)

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

(19) TRUE

(20) 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:
(1): COND_274_0_CREATELIST_LOAD(TRUE, x0[1]) → 274_0_CREATELIST_LOAD(x0[1] + -1)

The set Q is empty.

(21) 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) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) SCCToIDPv1Proof (SOUND transformation)

(14) Obligation:

(15) IDPNonInfProof (SOUND transformation)

(16) Complex Obligation (AND)

(17) Obligation:

(18) IDependencyGraphProof (EQUIVALENT transformation)

(19) TRUE

(20) Obligation:

(21) IDependencyGraphProof (EQUIVALENT transformation)

(22) TRUE