time complexity proof of /tmp/tmpYdlhWu/ListReverseAcyclicList.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 167 + 84 * |#0|).

0 JBC problem

↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 462 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(15)), 21 ms)

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 137 ms)

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 39 ms)

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳10 WeightedIntTrs

        ↳11 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳12 WeightedIntTrs

        ↳13 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳14 WeightedIntTrs

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 150 ms)

    ↳16 WeightedIntTrs

        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 45 ms)

        ↳18 WeightedIntTrs

        ↳19 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳20 WeightedIntTrs

        ↳21 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳22 WeightedIntTrs

        ↳23 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳24 WeightedIntTrs

↳25 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(15)), 22 ms)

↳26 JBCComplexityEdges

    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 192 ms)

    ↳28 WeightedIntTrs

    ↳29 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 32 ms)

    ↳30 WeightedIntTrs

    ↳31 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 47 ms)

    ↳32 WeightedIntTrs

    ↳33 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳34 WeightedIntTrs

    ↳35 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳36 WeightedIntTrs

    ↳37 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 143 ms)

    ↳40 BOUNDS(CONSTANT, 152 + 84 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class ListReverseAcyclicList {
	public static void main(int i) {
		List x = List.createList(i, 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 (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ListReverseAcyclicList.main(I)V: Graph of 102 nodes with 2 SCCs.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(15)) transformation)

Extracted set of 88 edges for the analysis of TIME complexity. Kept leaves.

(4) Obligation:

Set of 88 edges based on JBC Program.
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [n]

Considered paths: nonterm paths and paths from start to sinks

(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 88 jbc graph edges to a weighted ITS with 88 rules.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 88 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_InvokeMethod_53(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_53(i2, NULL, env, static) -{0,0}> main_InvokeMethod_54(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_54(i2, NULL, env, static) -{1,1}> createList_Inc_56(i2, NULL, env, static) :|: NULL = 0
createList_Inc_56(i2, NULL, env, static) -{1,1}> createList_Load_59(i4, NULL, i2, env, static) :|: NULL = 0 && i2 + -1 = i4
createList_Load_59(i4, NULL, i2, env, static) -{1,1}> createList_LE_62(i4, NULL, i2, env, static) :|: NULL = 0
createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, NULL, i2, env, static) :|: NULL = 0 && i14 <= 0
createList_LE_62(i15, NULL, i16, env, static) -{0,0}> createList_LE_65(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16
createList_LE_65(i15, NULL, i16, env, static) -{1,1}> createList_New_69(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16 && 0 < i15
createList_New_69(i15, NULL, i16, env, static) -{1,1}> createList_Duplicate_74(o4, i15, NULL, i16, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Duplicate_74(o4, i15, NULL, i16, env, static) -{1,1}> createList_Load_79(o4, i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Load_79(o4, i15, NULL, i16, env, static) -{1,1}> createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Return_105(o4', i15, i16, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 1 <= i15 && 0 < o4 && o4' <= o4 + NULL && 2 <= i16 && 0 < o4'
langle_init_rangle_Return_105(o4, i15, i16, NULL, env, static) -{1,1}> createList_Store_113(o4, i15, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Store_113(o4, i15, i16, NULL, env, static) -{1,1}> createList_JMP_134(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_JMP_134(i15, o4, i16, NULL, env, static) -{0,0}> createList_JMP_726(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 0 <= NULL && 2 <= i16
createList_JMP_726(i88, o191, i16, o192, env, static) -{1,1}> createList_Inc_729(i88, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i88 && 0 < o191 && 2 <= i16
createList_Inc_729(i88, o191, i16, o192, env, static) -{1,1}> createList_Load_733(i91, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i88 && i88 + -1 = i91 && 0 < o191 && 0 <= i91 && 2 <= i16
createList_Load_733(i91, o191, i16, o192, env, static) -{1,1}> createList_LE_740(i91, o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 0 <= i91 && 2 <= i16
createList_LE_740(iconst_0, o191, i16, o192, env, static) -{0,0}> createList_LE_742(iconst_0, o191, i16, o192, env, static) :|: 0 <= o192 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o191 && 2 <= i16
createList_LE_740(i96, o191, i16, o192, env, static) -{0,0}> createList_LE_743(i96, o191, i16, o192, env, static) :|: 0 <= o192 && 0 <= i96 && 1 <= i96 && 0 < o191 && 2 <= i16
createList_LE_742(iconst_0, o191, i16, o192, env, static) -{1,1}> createList_Load_746(o191, i16, o192, env, static) :|: 0 <= o192 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o191 && 2 <= i16
createList_LE_743(i96, o191, i16, o192, env, static) -{1,1}> createList_New_749(i96, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 0 < i96 && 2 <= i16
createList_Load_746(o191, i16, o192, env, static) -{1,1}> createList_Return_752(o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_New_749(i96, o191, i16, o192, env, static) -{1,1}> createList_Duplicate_755(o212, i96, o191, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && o212 = 1 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Return_752(o191, i16, o192, env, static) -{1,1}> main_Store_758(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_Duplicate_755(o212, i96, o191, i16, NULL, o192, env, static) -{1,1}> createList_Load_759(o212, i96, o191, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
main_Store_758(i16, o191, o192, env, static) -{1,1}> main_Load_761(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_Load_759(o212, i96, o191, i16, NULL, o192, env, static) -{1,1}> createList_InvokeMethod_763(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
main_Load_761(i16, o191, o192, env, static) -{1,1}> main_InvokeMethod_765(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_InvokeMethod_763(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_766(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
main_InvokeMethod_765(i16, o191, o192, env, static) -{1,1}> reverse_ConstantStackPush_767(o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
langle_init_rangle_Load_766(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_InvokeMethod_768(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
reverse_ConstantStackPush_767(o191, i16, o192, env, static) -{1,1}> reverse_Store_769(NULL, o191, i16, o192, env, static) :|: NULL = 0 && 0 <= o192 && 0 < o191 && 2 <= i16
langle_init_rangle_InvokeMethod_768(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_770(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
reverse_Store_769(NULL, o191, i16, o192, env, static) -{1,1}> reverse_Load_772(o191, NULL, i16, o192, env, static) :|: NULL = 0 && 0 <= o192 && 0 < o191 && 2 <= i16
langle_init_rangle_Load_770(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_774(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
reverse_Load_772(o191, NULL, i16, o192, env, static) -{0,0}> reverse_Load_865(o191, NULL, i16, env, static) :|: NULL = 0 && 0 <= o192 && 0 <= NULL && 0 < o191 && 2 <= i16 && 0 <= o191
langle_init_rangle_Load_774(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_FieldAccess_778(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_FieldAccess_778(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Return_792(o212', i96, i16, o191, o192, env, static) :|: NULL = 0 && 0 <= o192 && o212' = o212 + o191 && 0 < o212' && o212' <= o212 + o191 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_Return_792(o212, i96, i16, o191, o192, env, static) -{1,1}> createList_Store_796(o212, i96, i16, o191, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Store_796(o212, i96, i16, o191, o192, env, static) -{1,1}> createList_JMP_810(i96, o212, i16, o191, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_JMP_810(i96, o212, i16, o191, o192, env, static) -{0,0}> createList_JMP_726(i96, o212, i16, o191, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212 && 0 <= o191
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16
reverse_NULL_886(o269, o257, i16, env, static) -{0,0}> reverse_NULL_891(o269, o257, i16, env, static) :|: 0 <= o257 && 0 < o269 && 0 <= o269 && 2 <= i16
reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(NULL, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16
reverse_NULL_891(o269, o257, i16, env, static) -{1,1}> reverse_Load_895(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Load_895(o269, o257, i16, env, static) -{1,1}> reverse_Store_899(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Store_899(o272, o257, i16, env, static) -{0,0}> reverse_Store_908(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 1 + o273 = o272 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_908(o272, o257, i16, o273, env, static) -{1,1}> reverse_Load_912(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_912(o272, o257, i16, o273, env, static) -{1,1}> reverse_FieldAccess_914(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_914(o272, o257, i16, o273, env, static) -{1,1}> reverse_Store_916(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_916(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_917(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_917(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_919(o272, o273, o257, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_919(o272, o273, o257, i16, env, static) -{1,1}> reverse_FieldAccess_921(o272, o257, o273, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_921(o272, o257, o273, i16, env, static) -{1,1}> reverse_Load_923(o273, o272', i16, o257, env, static) :|: 0 <= o257 && 0 < o272' && 0 <= o273 && o272' <= o272 + o257 && 2 <= i16 && o272' = o272 + o257 + -1 * o273 && 0 < o272
reverse_Load_923(o273, o272, i16, o257, env, static) -{1,1}> reverse_Store_924(o272, o273, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_924(o272, o273, i16, o257, env, static) -{1,1}> reverse_JMP_925(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_JMP_925(o273, o272, i16, o257, env, static) -{1,1}> reverse_Load_929(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_929(o273, o272, i16, o257, env, static) -{0,0}> reverse_Load_865(o273, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 0 <= o272 && 2 <= i16 && 0 < o272

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i4', 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
by chaining
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_InvokeMethod_53(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_53(i2, NULL, env, static) -{0,0}> main_InvokeMethod_54(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_54(i2, NULL, env, static) -{1,1}> createList_Inc_56(i2, NULL, env, static) :|: NULL = 0
createList_Inc_56(i2, NULL, env, static) -{1,1}> createList_Load_59(i4, NULL, i2, env, static) :|: NULL = 0 && i2 + -1 = i4
createList_Load_59(i4, NULL, i2, env, static) -{1,1}> createList_LE_62(i4, NULL, i2, env, static) :|: NULL = 0

obtained
createList_LE_62(i15, 0, i16, env, static) -{12,12}> createList_JMP_726(i15, o4''', i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15
by chaining
createList_LE_62(i15, NULL, i16, env, static) -{0,0}> createList_LE_65(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16
createList_LE_65(i15, NULL, i16, env, static) -{1,1}> createList_New_69(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16 && 0 < i15
createList_New_69(i15, NULL, i16, env, static) -{1,1}> createList_Duplicate_74(o4, i15, NULL, i16, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Duplicate_74(o4, i15, NULL, i16, env, static) -{1,1}> createList_Load_79(o4, i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Load_79(o4, i15, NULL, i16, env, static) -{1,1}> createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Return_105(o4', i15, i16, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 1 <= i15 && 0 < o4 && o4' <= o4 + NULL && 2 <= i16 && 0 < o4'
langle_init_rangle_Return_105(o4, i15, i16, NULL, env, static) -{1,1}> createList_Store_113(o4, i15, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Store_113(o4, i15, i16, NULL, env, static) -{1,1}> createList_JMP_134(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_JMP_134(i15, o4, i16, NULL, env, static) -{0,0}> createList_JMP_726(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 0 <= NULL && 2 <= i16

obtained
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i91', o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
by chaining
createList_JMP_726(i88, o191, i16, o192, env, static) -{1,1}> createList_Inc_729(i88, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i88 && 0 < o191 && 2 <= i16
createList_Inc_729(i88, o191, i16, o192, env, static) -{1,1}> createList_Load_733(i91, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i88 && i88 + -1 = i91 && 0 < o191 && 0 <= i91 && 2 <= i16
createList_Load_733(i91, o191, i16, o192, env, static) -{1,1}> createList_LE_740(i91, o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 0 <= i91 && 2 <= i16

obtained
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, o212''', i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
by chaining
createList_LE_740(i96, o191, i16, o192, env, static) -{0,0}> createList_LE_743(i96, o191, i16, o192, env, static) :|: 0 <= o192 && 0 <= i96 && 1 <= i96 && 0 < o191 && 2 <= i16
createList_LE_743(i96, o191, i16, o192, env, static) -{1,1}> createList_New_749(i96, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 0 < i96 && 2 <= i16
createList_New_749(i96, o191, i16, o192, env, static) -{1,1}> createList_Duplicate_755(o212, i96, o191, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && o212 = 1 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Duplicate_755(o212, i96, o191, i16, NULL, o192, env, static) -{1,1}> createList_Load_759(o212, i96, o191, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Load_759(o212, i96, o191, i16, NULL, o192, env, static) -{1,1}> createList_InvokeMethod_763(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_InvokeMethod_763(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_766(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_Load_766(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_InvokeMethod_768(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_InvokeMethod_768(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_770(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_Load_770(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_774(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_Load_774(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_FieldAccess_778(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_FieldAccess_778(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Return_792(o212', i96, i16, o191, o192, env, static) :|: NULL = 0 && 0 <= o192 && o212' = o212 + o191 && 0 < o212' && o212' <= o212 + o191 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_Return_792(o212, i96, i16, o191, o192, env, static) -{1,1}> createList_Store_796(o212, i96, i16, o191, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Store_796(o212, i96, i16, o191, o192, env, static) -{1,1}> createList_JMP_810(i96, o212, i16, o191, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_JMP_810(i96, o212, i16, o191, o192, env, static) -{0,0}> createList_JMP_726(i96, o212, i16, o191, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212 && 0 <= o191

obtained
createList_LE_740(0, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0
by chaining
createList_LE_740(iconst_0, o191, i16, o192, env, static) -{0,0}> createList_LE_742(iconst_0, o191, i16, o192, env, static) :|: 0 <= o192 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o191 && 2 <= i16
createList_LE_742(iconst_0, o191, i16, o192, env, static) -{1,1}> createList_Load_746(o191, i16, o192, env, static) :|: 0 <= o192 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o191 && 2 <= i16
createList_Load_746(o191, i16, o192, env, static) -{1,1}> createList_Return_752(o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_Return_752(o191, i16, o192, env, static) -{1,1}> main_Store_758(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
main_Store_758(i16, o191, o192, env, static) -{1,1}> main_Load_761(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
main_Load_761(i16, o191, o192, env, static) -{1,1}> main_InvokeMethod_765(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
main_InvokeMethod_765(i16, o191, o192, env, static) -{1,1}> reverse_ConstantStackPush_767(o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
reverse_ConstantStackPush_767(o191, i16, o192, env, static) -{1,1}> reverse_Store_769(NULL, o191, i16, o192, env, static) :|: NULL = 0 && 0 <= o192 && 0 < o191 && 2 <= i16
reverse_Store_769(NULL, o191, i16, o192, env, static) -{1,1}> reverse_Load_772(o191, NULL, i16, o192, env, static) :|: NULL = 0 && 0 <= o192 && 0 < o191 && 2 <= i16
reverse_Load_772(o191, NULL, i16, o192, env, static) -{0,0}> reverse_Load_865(o191, NULL, i16, env, static) :|: NULL = 0 && 0 <= o192 && 0 <= NULL && 0 < o191 && 2 <= i16 && 0 <= o191

obtained
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', o272''', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269
by chaining
reverse_NULL_886(o269, o257, i16, env, static) -{0,0}> reverse_NULL_891(o269, o257, i16, env, static) :|: 0 <= o257 && 0 < o269 && 0 <= o269 && 2 <= i16
reverse_NULL_891(o269, o257, i16, env, static) -{1,1}> reverse_Load_895(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Load_895(o269, o257, i16, env, static) -{1,1}> reverse_Store_899(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Store_899(o272, o257, i16, env, static) -{0,0}> reverse_Store_908(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 1 + o273 = o272 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_908(o272, o257, i16, o273, env, static) -{1,1}> reverse_Load_912(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_912(o272, o257, i16, o273, env, static) -{1,1}> reverse_FieldAccess_914(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_914(o272, o257, i16, o273, env, static) -{1,1}> reverse_Store_916(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_916(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_917(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_917(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_919(o272, o273, o257, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_919(o272, o273, o257, i16, env, static) -{1,1}> reverse_FieldAccess_921(o272, o257, o273, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_921(o272, o257, o273, i16, env, static) -{1,1}> reverse_Load_923(o273, o272', i16, o257, env, static) :|: 0 <= o257 && 0 < o272' && 0 <= o273 && o272' <= o272 + o257 && 2 <= i16 && o272' = o272 + o257 + -1 * o273 && 0 < o272
reverse_Load_923(o273, o272, i16, o257, env, static) -{1,1}> reverse_Store_924(o272, o273, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_924(o272, o273, i16, o257, env, static) -{1,1}> reverse_JMP_925(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_JMP_925(o273, o272, i16, o257, env, static) -{1,1}> reverse_Load_929(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_929(o273, o272, i16, o257, env, static) -{0,0}> reverse_Load_865(o273, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 0 <= o272 && 2 <= i16 && 0 < o272

(8) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i4', 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, NULL, i2, env, static) :|: NULL = 0 && i14 <= 0
createList_LE_62(i15, 0, i16, env, static) -{12,12}> createList_JMP_726(i15, o4''', i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i91', o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, o212''', i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
createList_LE_740(0, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16
reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(NULL, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', o272''', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269

(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

createList_LE_740(0, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0
was transformed to
createList_LE_740(x, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0

createList_LE_62(i15, 0, i16, env, static) -{12,12}> createList_JMP_726(i15, o4''', i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15
was transformed to
createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, o4''', i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0

(10) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
createList_LE_740(x, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', o272''', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i91', o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(NULL, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i4', 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, o212''', i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, NULL, i2, env, static) :|: NULL = 0 && i14 <= 0
createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, o4''', i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16

(11) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, o4''', i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0
was transformed to
createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, 1 + 0, i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0

createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i91', o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
was transformed to
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i88 + -1, o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191

reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', o272''', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269
was transformed to
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', 1 + o273' + o257 + -1 * o273', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269

reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(NULL, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16
was transformed to
reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(0, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16

main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i4', 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
was transformed to
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i2 + -1, 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'

createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, NULL, i2, env, static) :|: NULL = 0 && i14 <= 0
was transformed to
createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, 0, i2, env, static) :|: NULL = 0 && i14 <= 0

createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, o212''', i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
was transformed to
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1

(12) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, 1 + 0, i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i88 + -1, o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', 1 + o273' + o257 + -1 * o273', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269
reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(0, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i2 + -1, 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, 0, i2, env, static) :|: NULL = 0 && i14 <= 0
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16
createList_LE_740(x, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0

(13) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i2 + -1, 0, i2, env, static'1) :|: 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
was transformed to
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i2 - 1, 0, i2, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i2 - 1 = i4'

createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
was transformed to
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191, env, static) :|: o212''' = 1 + o191 && 0 < i96 && 0 < o212''' && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96

reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', 1 + o273' + o257 + -1 * o273', i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257 && 0 <= o269
was transformed to
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', 1 + o257, i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257

createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i88 + -1, o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
was transformed to
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i88 - 1, o191, i16, o192, env, static) :|: i88 - 1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191

createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, 1 + 0, i16, 0, env, static) :|: o4''' = 1 + 0 && 2 <= i16 && o4''' <= 1 + 0 && 0 <= 0 && 0 < 1 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0
was transformed to
createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, 1, i16, 0, env, static) :|: o4''' = 1 && 2 <= i16 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0

createList_LE_740(x, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0
was transformed to
createList_LE_740(x, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o192 && 2 <= i16 && x = 0

(14) Obligation:

IntTrs with 9 rules
Start term: main_Load_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
reverse_NULL_886(o269, o257, i16, env, static) -{12,12}> reverse_Load_865(o273', 1 + o257, i16, env, static) :|: 0 < o269 && 0 < o272''' && 1 + o273' = o269 && 2 <= i16 && o272''' = o269 + o257 + -1 * o273' && 0 <= o257 && 0 <= o273' && o272''' <= o269 + o257
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191, env, static) :|: o212''' = 1 + o191 && 0 < i96 && 0 < o212''' && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96
createList_LE_740(x, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o192 && 2 <= i16 && x = 0
reverse_NULL_886(NULL, o257, i16, env, static) -{0,0}> reverse_NULL_893(0, o257, i16, env, static) :|: NULL = 0 && 0 <= o257 && 0 <= NULL && 2 <= i16
createList_LE_62(i15, x, i16, env, static) -{12,12}> createList_JMP_726(i15, 1, i16, 0, env, static) :|: o4''' = 1 && 2 <= i16 && 0 < o4''' && 1 <= i15 && 0 < i15 && x = 0
main_Load_1(i2, env, static) -{20,20}> createList_LE_62(i2 - 1, 0, i2, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i2 - 1 = i4'
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i88 - 1, o191, i16, o192, env, static) :|: i88 - 1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
createList_LE_62(i14, NULL, i2, env, static) -{0,0}> createList_LE_64(i14, 0, i2, env, static) :|: NULL = 0 && i14 <= 0
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16

(15) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 88 jbc graph edges to a weighted ITS with 88 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Did no encode lower bounds for putfield and astore.

(16) Obligation:

(17) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

(20) Obligation:

(21) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

(22) Obligation:

(23) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

(24) Obligation:

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(15)) transformation)

Extracted set of 86 edges for the analysis of TIME complexity. Dropped leaves.

(26) Obligation:

Set of 86 edges based on JBC Program.
Performed SCC analyses:

Used field analysis yielded the following read fields:
- List: [n]

Considered paths: all paths from start

(27) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

Transformed 86 jbc graph edges to a weighted ITS with 86 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(28) Obligation:

IntTrs with 86 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_InvokeMethod_53(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_53(i2, NULL, env, static) -{0,0}> main_InvokeMethod_54(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_54(i2, NULL, env, static) -{1,1}> createList_Inc_56(i2, NULL, env, static) :|: NULL = 0
createList_Inc_56(i2, NULL, env, static) -{1,1}> createList_Load_59(i4, NULL, i2, env, static) :|: NULL = 0 && i2 + -1 = i4
createList_Load_59(i4, NULL, i2, env, static) -{1,1}> createList_LE_62(i4, NULL, i2, env, static) :|: NULL = 0
createList_LE_62(i15, NULL, i16, env, static) -{0,0}> createList_LE_65(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16
createList_LE_65(i15, NULL, i16, env, static) -{1,1}> createList_New_69(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16 && 0 < i15
createList_New_69(i15, NULL, i16, env, static) -{1,1}> createList_Duplicate_74(o4, i15, NULL, i16, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Duplicate_74(o4, i15, NULL, i16, env, static) -{1,1}> createList_Load_79(o4, i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Load_79(o4, i15, NULL, i16, env, static) -{1,1}> createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Return_105(o4', i15, i16, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 1 <= i15 && 0 < o4 && o4' <= o4 + NULL && 2 <= i16 && 0 < o4'
langle_init_rangle_Return_105(o4, i15, i16, NULL, env, static) -{1,1}> createList_Store_113(o4, i15, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Store_113(o4, i15, i16, NULL, env, static) -{1,1}> createList_JMP_134(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_JMP_134(i15, o4, i16, NULL, env, static) -{0,0}> createList_JMP_726(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 0 <= NULL && 2 <= i16
createList_JMP_726(i88, o191, i16, o192, env, static) -{1,1}> createList_Inc_729(i88, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i88 && 0 < o191 && 2 <= i16
createList_Inc_729(i88, o191, i16, o192, env, static) -{1,1}> createList_Load_733(i91, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i88 && i88 + -1 = i91 && 0 < o191 && 0 <= i91 && 2 <= i16
createList_Load_733(i91, o191, i16, o192, env, static) -{1,1}> createList_LE_740(i91, o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 0 <= i91 && 2 <= i16
createList_LE_740(iconst_0, o191, i16, o192, env, static) -{0,0}> createList_LE_742(iconst_0, o191, i16, o192, env, static) :|: 0 <= o192 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o191 && 2 <= i16
createList_LE_740(i96, o191, i16, o192, env, static) -{0,0}> createList_LE_743(i96, o191, i16, o192, env, static) :|: 0 <= o192 && 0 <= i96 && 1 <= i96 && 0 < o191 && 2 <= i16
createList_LE_742(iconst_0, o191, i16, o192, env, static) -{1,1}> createList_Load_746(o191, i16, o192, env, static) :|: 0 <= o192 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o191 && 2 <= i16
createList_LE_743(i96, o191, i16, o192, env, static) -{1,1}> createList_New_749(i96, o191, i16, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 0 < i96 && 2 <= i16
createList_Load_746(o191, i16, o192, env, static) -{1,1}> createList_Return_752(o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_New_749(i96, o191, i16, o192, env, static) -{1,1}> createList_Duplicate_755(o212, i96, o191, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && o212 = 1 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Return_752(o191, i16, o192, env, static) -{1,1}> main_Store_758(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_Duplicate_755(o212, i96, o191, i16, NULL, o192, env, static) -{1,1}> createList_Load_759(o212, i96, o191, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
main_Store_758(i16, o191, o192, env, static) -{1,1}> main_Load_761(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_Load_759(o212, i96, o191, i16, NULL, o192, env, static) -{1,1}> createList_InvokeMethod_763(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
main_Load_761(i16, o191, o192, env, static) -{1,1}> main_InvokeMethod_765(i16, o191, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
createList_InvokeMethod_763(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_766(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
main_InvokeMethod_765(i16, o191, o192, env, static) -{1,1}> reverse_ConstantStackPush_767(o191, i16, o192, env, static) :|: 0 <= o192 && 0 < o191 && 2 <= i16
langle_init_rangle_Load_766(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_InvokeMethod_768(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
reverse_ConstantStackPush_767(o191, i16, o192, env, static) -{1,1}> reverse_Store_769(NULL, o191, i16, o192, env, static) :|: NULL = 0 && 0 <= o192 && 0 < o191 && 2 <= i16
langle_init_rangle_InvokeMethod_768(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_770(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
reverse_Store_769(NULL, o191, i16, o192, env, static) -{1,1}> reverse_Load_772(o191, NULL, i16, o192, env, static) :|: NULL = 0 && 0 <= o192 && 0 < o191 && 2 <= i16
langle_init_rangle_Load_770(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Load_774(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
reverse_Load_772(o191, NULL, i16, o192, env, static) -{0,0}> reverse_Load_865(o191, NULL, i16, env, static) :|: NULL = 0 && 0 <= o192 && 0 <= NULL && 0 < o191 && 2 <= i16 && 0 <= o191
langle_init_rangle_Load_774(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_FieldAccess_778(o212, o191, i96, i16, NULL, o192, env, static) :|: NULL = 0 && 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_FieldAccess_778(o212, o191, i96, i16, NULL, o192, env, static) -{1,1}> langle_init_rangle_Return_792(o212', i96, i16, o191, o192, env, static) :|: NULL = 0 && 0 <= o192 && o212' = o212 + o191 && 0 < o212' && o212' <= o212 + o191 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
langle_init_rangle_Return_792(o212, i96, i16, o191, o192, env, static) -{1,1}> createList_Store_796(o212, i96, i16, o191, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_Store_796(o212, i96, i16, o191, o192, env, static) -{1,1}> createList_JMP_810(i96, o212, i16, o191, o192, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212
createList_JMP_810(i96, o212, i16, o191, o192, env, static) -{0,0}> createList_JMP_726(i96, o212, i16, o191, env, static) :|: 0 <= o192 && 1 <= i96 && 0 < o191 && 2 <= i16 && 0 < o212 && 0 <= o191
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16
reverse_NULL_886(o269, o257, i16, env, static) -{0,0}> reverse_NULL_891(o269, o257, i16, env, static) :|: 0 <= o257 && 0 < o269 && 0 <= o269 && 2 <= i16
reverse_NULL_891(o269, o257, i16, env, static) -{1,1}> reverse_Load_895(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Load_895(o269, o257, i16, env, static) -{1,1}> reverse_Store_899(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Store_899(o272, o257, i16, env, static) -{0,0}> reverse_Store_908(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 1 + o273 = o272 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_908(o272, o257, i16, o273, env, static) -{1,1}> reverse_Load_912(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_912(o272, o257, i16, o273, env, static) -{1,1}> reverse_FieldAccess_914(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_914(o272, o257, i16, o273, env, static) -{1,1}> reverse_Store_916(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_916(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_917(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_917(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_919(o272, o273, o257, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_919(o272, o273, o257, i16, env, static) -{1,1}> reverse_FieldAccess_921(o272, o257, o273, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_921(o272, o257, o273, i16, env, static) -{1,1}> reverse_Load_923(o273, o272', i16, o257, env, static) :|: 0 <= o257 && 0 < o272' && 0 <= o273 && o272' <= o272 + o257 && 2 <= i16 && o272' = o272 + o257 + -1 * o273 && 0 < o272
reverse_Load_923(o273, o272, i16, o257, env, static) -{1,1}> reverse_Store_924(o272, o273, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_924(o272, o273, i16, o257, env, static) -{1,1}> reverse_JMP_925(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_JMP_925(o273, o272, i16, o257, env, static) -{1,1}> reverse_Load_929(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_929(o273, o272, i16, o257, env, static) -{0,0}> reverse_Load_865(o273, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 0 <= o272 && 2 <= i16 && 0 < o272

(29) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

obtained
main_Load_1(i2, env, static) -{32,32}> createList_JMP_726(i4', o4''', i2, 0, env, static'1) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
by chaining
main_Load_1(i2, env, static) -{0,0}> main_Load_3(i2, env, static) :|: 0 >= 0
main_Load_3(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_29(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_31(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_31(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_39(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i2, env, static) -{1,1}> main_Load_41(i2, env, static) :|: 0 >= 0
main_Load_41(i2, env, static) -{0,0}> main_Load_42(i2, env, static) :|: 0 >= 0
main_Load_42(i2, env, static) -{0,0}> main_Load_44(i2, env, static) :|: 0 <= static
main_Load_44(i2, env, static) -{0,0}> main_Load_46(i2, env, static) :|: 0 >= 0
main_Load_46(i2, env, static) -{0,0}> main_Load_48(i2, env, static) :|: 0 >= 0
main_Load_48(i2, env, static) -{1,1}> main_ConstantStackPush_50(i2, env, static) :|: 0 >= 0
main_ConstantStackPush_50(i2, env, static) -{1,1}> main_InvokeMethod_53(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_53(i2, NULL, env, static) -{0,0}> main_InvokeMethod_54(i2, NULL, env, static) :|: NULL = 0
main_InvokeMethod_54(i2, NULL, env, static) -{1,1}> createList_Inc_56(i2, NULL, env, static) :|: NULL = 0
createList_Inc_56(i2, NULL, env, static) -{1,1}> createList_Load_59(i4, NULL, i2, env, static) :|: NULL = 0 && i2 + -1 = i4
createList_Load_59(i4, NULL, i2, env, static) -{1,1}> createList_LE_62(i4, NULL, i2, env, static) :|: NULL = 0
createList_LE_62(i15, NULL, i16, env, static) -{0,0}> createList_LE_65(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16
createList_LE_65(i15, NULL, i16, env, static) -{1,1}> createList_New_69(i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 2 <= i16 && 0 < i15
createList_New_69(i15, NULL, i16, env, static) -{1,1}> createList_Duplicate_74(o4, i15, NULL, i16, env, static) :|: NULL = 0 && o4 = 1 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Duplicate_74(o4, i15, NULL, i16, env, static) -{1,1}> createList_Load_79(o4, i15, NULL, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Load_79(o4, i15, NULL, i16, env, static) -{1,1}> createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_InvokeMethod_83(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_87(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_InvokeMethod_91(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_96(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_Load_99(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
langle_init_rangle_FieldAccess_101(o4, NULL, i15, i16, env, static) -{1,1}> langle_init_rangle_Return_105(o4', i15, i16, NULL, env, static) :|: NULL = 0 && o4' = o4 + NULL && 1 <= i15 && 0 < o4 && o4' <= o4 + NULL && 2 <= i16 && 0 < o4'
langle_init_rangle_Return_105(o4, i15, i16, NULL, env, static) -{1,1}> createList_Store_113(o4, i15, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_Store_113(o4, i15, i16, NULL, env, static) -{1,1}> createList_JMP_134(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 2 <= i16
createList_JMP_134(i15, o4, i16, NULL, env, static) -{0,0}> createList_JMP_726(i15, o4, i16, NULL, env, static) :|: NULL = 0 && 1 <= i15 && 0 < o4 && 0 <= NULL && 2 <= i16

obtained
reverse_Load_865(o256, o257, i16, env, static) -{13,13}> reverse_Load_865(o273', o272''', i16, env, static) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256
by chaining
reverse_Load_865(o256, o257, i16, env, static) -{1,1}> reverse_NULL_886(o256, o257, i16, env, static) :|: 0 <= o257 && 0 <= o256 && 2 <= i16
reverse_NULL_886(o269, o257, i16, env, static) -{0,0}> reverse_NULL_891(o269, o257, i16, env, static) :|: 0 <= o257 && 0 < o269 && 0 <= o269 && 2 <= i16
reverse_NULL_891(o269, o257, i16, env, static) -{1,1}> reverse_Load_895(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Load_895(o269, o257, i16, env, static) -{1,1}> reverse_Store_899(o269, o257, i16, env, static) :|: 0 < o269 && 0 <= o257 && 2 <= i16
reverse_Store_899(o272, o257, i16, env, static) -{0,0}> reverse_Store_908(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 1 + o273 = o272 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_908(o272, o257, i16, o273, env, static) -{1,1}> reverse_Load_912(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_912(o272, o257, i16, o273, env, static) -{1,1}> reverse_FieldAccess_914(o272, o257, i16, o273, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_914(o272, o257, i16, o273, env, static) -{1,1}> reverse_Store_916(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_916(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_917(o273, o257, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_917(o273, o257, o272, i16, env, static) -{1,1}> reverse_Load_919(o272, o273, o257, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_919(o272, o273, o257, i16, env, static) -{1,1}> reverse_FieldAccess_921(o272, o257, o273, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_FieldAccess_921(o272, o257, o273, i16, env, static) -{1,1}> reverse_Load_923(o273, o272', i16, o257, env, static) :|: 0 <= o257 && 0 < o272' && 0 <= o273 && o272' <= o272 + o257 && 2 <= i16 && o272' = o272 + o257 + -1 * o273 && 0 < o272
reverse_Load_923(o273, o272, i16, o257, env, static) -{1,1}> reverse_Store_924(o272, o273, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Store_924(o272, o273, i16, o257, env, static) -{1,1}> reverse_JMP_925(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_JMP_925(o273, o272, i16, o257, env, static) -{1,1}> reverse_Load_929(o273, o272, i16, o257, env, static) :|: 0 <= o257 && 0 <= o273 && 2 <= i16 && 0 < o272
reverse_Load_929(o273, o272, i16, o257, env, static) -{0,0}> reverse_Load_865(o273, o272, i16, env, static) :|: 0 <= o257 && 0 <= o273 && 0 <= o272 && 2 <= i16 && 0 < o272

(30) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, env, static) -{32,32}> createList_JMP_726(i4', o4''', i2, 0, env, static'1) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_JMP_726(i88, o191, i16, o192, env, static) -{3,3}> createList_LE_740(i91', o191, i16, o192, env, static) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
createList_LE_740(i96, o191, i16, o192, env, static) -{12,12}> createList_JMP_726(i96, o212''', i16, o191, env, static) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
createList_LE_740(0, o191, i16, o192, env, static) -{8,8}> reverse_Load_865(o191, 0, i16, env, static) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0
reverse_Load_865(o256, o257, i16, env, static) -{13,13}> reverse_Load_865(o273', o272''', i16, env, static) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256

(31) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

Some arguments are removed because they cannot influence termination. We removed arguments according to the following replacements:

main_Load_1(x1, x2, x3) → main_Load_1(x1, x3)
createList_JMP_726(x1, x2, x3, x4, x5, x6) → createList_JMP_726(x1, x2, x3, x4)
createList_LE_740(x1, x2, x3, x4, x5, x6) → createList_LE_740(x1, x2, x3, x4)
reverse_Load_865(x1, x2, x3, x4, x5) → reverse_Load_865(x1, x2, x3)

(32) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, static) -{32,32}> createList_JMP_726(i4', o4''', i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i91', o191, i16, o192) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, o212''', i16, o191) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
createList_LE_740(0, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0
reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', o272''', i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256

(33) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from lhss to constraints.

createList_LE_740(0, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0
was transformed to
createList_LE_740(x, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, o212''', i16, o191) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
main_Load_1(i2, static) -{32,32}> createList_JMP_726(i4', o4''', i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i91', o191, i16, o192) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
createList_LE_740(x, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0
reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', o272''', i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256

(35) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

main_Load_1(i2, static) -{32,32}> createList_JMP_726(i4', o4''', i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
was transformed to
main_Load_1(i2, static) -{32,32}> createList_JMP_726(i2 + -1, 1 + 0, i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'

createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, o212''', i16, o191) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
was transformed to
createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1

createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i91', o191, i16, o192) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
was transformed to
createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i88 + -1, o191, i16, o192) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191

reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', o272''', i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256
was transformed to
reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', 1 + o273' + o257 + -1 * o273', i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256

(36) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, static) -{32,32}> createList_JMP_726(i2 + -1, 1 + 0, i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
createList_LE_740(x, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0
createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i88 + -1, o191, i16, o192) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', 1 + o273' + o257 + -1 * o273', i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256

(37) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Simplified expressions.

createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i88 + -1, o191, i16, o192) :|: i88 + -1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
was transformed to
createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i88 - 1, o191, i16, o192) :|: i88 - 1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191

reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', 1 + o273' + o257 + -1 * o273', i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o272''' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257 && 0 <= o256
was transformed to
reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', 1 + o257, i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257

main_Load_1(i2, static) -{32,32}> createList_JMP_726(i2 + -1, 1 + 0, i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 <= 0 && 0 < 2 && 0 < o4''' && 0 <= static && 1 <= i4' && 0 <= 1 && o4''' = 1 + 0 && static''' <= static + 2 && 0 <= static''' && 0 < 1 && 0 <= 2 && o4''' <= 1 + 0 && static'1 <= static''' + 1 && 0 >= 0 && i2 + -1 = i4'
was transformed to
main_Load_1(i2, static) -{32,32}> createList_JMP_726(i2 - 1, 1, i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 < o4''' && 0 <= static && 1 <= i4' && o4''' = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i2 - 1 = i4'

createList_LE_740(x, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o191 && 0 <= o192 && 2 <= i16 && 0 <= 0 && x = 0
was transformed to
createList_LE_740(x, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o192 && 2 <= i16 && x = 0

createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191) :|: o212''' = 1 + o191 && 0 <= o191 && 0 < i96 && 0 < o212''' && o212''' <= 1 + o191 && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96 && 0 <= i96 && 0 < 1
was transformed to
createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191) :|: o212''' = 1 + o191 && 0 < i96 && 0 < o212''' && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_1(#0, static)
Considered paths: all paths from start
Rules:
createList_JMP_726(i88, o191, i16, o192) -{3,3}> createList_LE_740(i88 - 1, o191, i16, o192) :|: i88 - 1 = i91' && 2 <= i16 && 1 <= i88 && 0 <= i91' && 0 <= o192 && 0 < o191
createList_LE_740(i96, o191, i16, o192) -{12,12}> createList_JMP_726(i96, 1 + o191, i16, o191) :|: o212''' = 1 + o191 && 0 < i96 && 0 < o212''' && 2 <= i16 && 0 <= o192 && 0 < o191 && 1 <= i96
createList_LE_740(x, o191, i16, o192) -{8,8}> reverse_Load_865(o191, 0, i16) :|: 0 < o191 && 0 <= o192 && 2 <= i16 && x = 0
reverse_Load_865(o256, o257, i16) -{13,13}> reverse_Load_865(o273', 1 + o257, i16) :|: 0 < o256 && 0 < o272''' && 1 + o273' = o256 && 2 <= i16 && o272''' = o256 + o257 + -1 * o273' && 0 <= o257 && 0 <= o273' && o272''' <= o256 + o257
main_Load_1(i2, static) -{32,32}> createList_JMP_726(i2 - 1, 1, i2, 0) :|: 0 < i4' && 2 <= i2 && 0 <= static'1 && 0 < o4''' && 0 <= static && 1 <= i4' && o4''' = 1 && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i2 - 1 = i4'

(39) koat Proof (EQUIVALENT transformation)

YES(?, 84*ar_0 + 152)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 3) createList_JMP_726(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_LE_740(ar_0 - 1, ar_1, ar_2, ar_3)) [ ar_0 - 1 = i91' /\ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 <= i91' /\ 0 <= ar_3 /\ 0 < ar_1 ]
(Comp: ?, Cost: 12) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0, ar_1 + 1, ar_2, ar_1)) [ o212''' = ar_1 + 1 /\ 0 < ar_0 /\ 0 < o212''' /\ 2 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 8) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(ar_1, 0, ar_2, arityPad)) [ 0 < ar_1 /\ 0 <= ar_3 /\ 2 <= ar_2 /\ ar_0 = 0 ]
(Comp: ?, Cost: 13) reverse_Load_865(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(o273', ar_1 + 1, ar_2, arityPad)) [ 0 < ar_0 /\ 0 < o272''' /\ o273' + 1 = ar_0 /\ 2 <= ar_2 /\ o272''' = ar_0 + ar_1 - o273' /\ 0 <= ar_1 /\ 0 <= o273' /\ o272''' <= ar_0 + ar_1 ]
(Comp: ?, Cost: 32) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0 - 1, 1, ar_0, 0)) [ 0 < i4' /\ 2 <= ar_0 /\ 0 <= static'1 /\ 0 < o4''' /\ 0 <= ar_1 /\ 1 <= i4' /\ o4''' = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 3) createList_JMP_726(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_LE_740(ar_0 - 1, ar_1, ar_2, ar_3)) [ ar_0 - 1 = i91' /\ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 <= i91' /\ 0 <= ar_3 /\ 0 < ar_1 ]
(Comp: ?, Cost: 12) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0, ar_1 + 1, ar_2, ar_1)) [ o212''' = ar_1 + 1 /\ 0 < ar_0 /\ 0 < o212''' /\ 2 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 8) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(ar_1, 0, ar_2, arityPad)) [ 0 < ar_1 /\ 0 <= ar_3 /\ 2 <= ar_2 /\ ar_0 = 0 ]
(Comp: ?, Cost: 13) reverse_Load_865(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(o273', ar_1 + 1, ar_2, arityPad)) [ 0 < ar_0 /\ 0 < o272''' /\ o273' + 1 = ar_0 /\ 2 <= ar_2 /\ o272''' = ar_0 + ar_1 - o273' /\ 0 <= ar_1 /\ 0 <= o273' /\ o272''' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 32) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0 - 1, 1, ar_0, 0)) [ 0 < i4' /\ 2 <= ar_0 /\ 0 <= static'1 /\ 0 < o4''' /\ 0 <= ar_1 /\ 1 <= i4' /\ o4''' = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(createList_JMP_726) = 1
Pol(createList_LE_740) = 1
Pol(reverse_Load_865) = 0
Pol(main_Load_1) = 1
Pol(koat_start) = 1
orients all transitions weakly and the transition
createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(ar_1, 0, ar_2, arityPad)) [ 0 < ar_1 /\ 0 <= ar_3 /\ 2 <= ar_2 /\ ar_0 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 3) createList_JMP_726(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_LE_740(ar_0 - 1, ar_1, ar_2, ar_3)) [ ar_0 - 1 = i91' /\ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 <= i91' /\ 0 <= ar_3 /\ 0 < ar_1 ]
(Comp: ?, Cost: 12) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0, ar_1 + 1, ar_2, ar_1)) [ o212''' = ar_1 + 1 /\ 0 < ar_0 /\ 0 < o212''' /\ 2 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 8) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(ar_1, 0, ar_2, arityPad)) [ 0 < ar_1 /\ 0 <= ar_3 /\ 2 <= ar_2 /\ ar_0 = 0 ]
(Comp: ?, Cost: 13) reverse_Load_865(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(o273', ar_1 + 1, ar_2, arityPad)) [ 0 < ar_0 /\ 0 < o272''' /\ o273' + 1 = ar_0 /\ 2 <= ar_2 /\ o272''' = ar_0 + ar_1 - o273' /\ 0 <= ar_1 /\ 0 <= o273' /\ o272''' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 32) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0 - 1, 1, ar_0, 0)) [ 0 < i4' /\ 2 <= ar_0 /\ 0 <= static'1 /\ 0 < o4''' /\ 0 <= ar_1 /\ 1 <= i4' /\ o4''' = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(createList_JMP_726) = 3*V_1 + V_2 - 2
Pol(createList_LE_740) = 3*V_1 + V_2
Pol(reverse_Load_865) = V_1
Pol(main_Load_1) = 3*V_1 - 4
Pol(koat_start) = 3*V_1 - 4
orients all transitions weakly and the transitions
reverse_Load_865(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(o273', ar_1 + 1, ar_2, arityPad)) [ 0 < ar_0 /\ 0 < o272''' /\ o273' + 1 = ar_0 /\ 2 <= ar_2 /\ o272''' = ar_0 + ar_1 - o273' /\ 0 <= ar_1 /\ 0 <= o273' /\ o272''' <= ar_0 + ar_1 ]
createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0, ar_1 + 1, ar_2, ar_1)) [ o212''' = ar_1 + 1 /\ 0 < ar_0 /\ 0 < o212''' /\ 2 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 1 <= ar_0 ]
createList_JMP_726(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_LE_740(ar_0 - 1, ar_1, ar_2, ar_3)) [ ar_0 - 1 = i91' /\ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 <= i91' /\ 0 <= ar_3 /\ 0 < ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: 3*ar_0 + 4, Cost: 3) createList_JMP_726(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_LE_740(ar_0 - 1, ar_1, ar_2, ar_3)) [ ar_0 - 1 = i91' /\ 2 <= ar_2 /\ 1 <= ar_0 /\ 0 <= i91' /\ 0 <= ar_3 /\ 0 < ar_1 ]
(Comp: 3*ar_0 + 4, Cost: 12) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0, ar_1 + 1, ar_2, ar_1)) [ o212''' = ar_1 + 1 /\ 0 < ar_0 /\ 0 < o212''' /\ 2 <= ar_2 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 8) createList_LE_740(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(ar_1, 0, ar_2, arityPad)) [ 0 < ar_1 /\ 0 <= ar_3 /\ 2 <= ar_2 /\ ar_0 = 0 ]
(Comp: 3*ar_0 + 4, Cost: 13) reverse_Load_865(ar_0, ar_1, ar_2, ar_3) -> Com_1(reverse_Load_865(o273', ar_1 + 1, ar_2, arityPad)) [ 0 < ar_0 /\ 0 < o272''' /\ o273' + 1 = ar_0 /\ 2 <= ar_2 /\ o272''' = ar_0 + ar_1 - o273' /\ 0 <= ar_1 /\ 0 <= o273' /\ o272''' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 32) main_Load_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(createList_JMP_726(ar_0 - 1, 1, ar_0, 0)) [ 0 < i4' /\ 2 <= ar_0 /\ 0 <= static'1 /\ 0 < o4''' /\ 0 <= ar_1 /\ 1 <= i4' /\ o4''' = 1 /\ static''' <= ar_1 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i4' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 84*ar_0 + 152

Time: 0.234 sec (SMT: 0.217 sec)

(0) Obligation:

(1) JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(15)) transformation)

(4) Obligation:

(5) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(6) Obligation:

(7) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(10) Obligation:

(11) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(16) Obligation:

(17) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(20) Obligation:

(21) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(22) Obligation:

(23) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(24) Obligation:

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(15)) transformation)

(26) Obligation:

(27) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(28) Obligation:

(29) StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(30) Obligation:

(31) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID) transformation)

(32) Obligation:

(33) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(34) Obligation:

(35) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(36) Obligation:

(37) ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(38) Obligation:

(39) koat Proof (EQUIVALENT transformation)

(40) BOUNDS(CONSTANT, 152 + 84 * |#0|)