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

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 92 + 168 * |args|).

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(46)), 30 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

        ↳15 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 5 ms)

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 200 ms)

    ↳18 WeightedIntTrs

        ↳19 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 77 ms)

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

        ↳27 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 16 ms)

        ↳28 WeightedIntTrs

↳29 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(46)), 15 ms)

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 166 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 71 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 30 ms)

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

    ↳43 koat Proof (⇔, 249 ms)

    ↳44 BOUNDS(CONSTANT, 46 + 168 * |args|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

class List {
	List n;

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

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

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

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

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

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ListReverseAcyclicList.main([Ljava/lang/String;)V: Graph of 145 nodes with 2 SCCs.

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

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

(4) Obligation:

Set of 100 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 100 jbc graph edges to a weighted ITS with 100 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.

(6) Obligation:

IntTrs with 100 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_26(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_26(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_46(o2, env, static) :|: 0 < o2
main_Load_46(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_48(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2
main_Load_51(o2, env, static) -{1,1}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_56(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_56(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_56(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_58(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_ConstantStackPush_70(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_ConstantStackPush_70(a6, i8, i6, env, static) -{1,1}> main_InvokeMethod_77(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_77(a6, i8, NULL, i6, env, static) -{0,0}> main_InvokeMethod_81(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_81(a6, i8, NULL, i6, env, static) -{1,1}> createList_Inc_85(i8, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
createList_Inc_85(i8, NULL, a6, i6, env, static) -{1,1}> createList_Load_92(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8 && i8 + -1 = i10 && -1 <= i10
createList_Load_92(i10, NULL, a6, i6, env, static) -{1,1}> createList_LE_100(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && -1 <= i10
createList_LE_100(i17, NULL, a6, i6, env, static) -{0,0}> createList_LE_113(i17, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && i17 <= 0 && 0 < a6 && -1 <= i17
createList_LE_100(i18, NULL, a6, i6, env, static) -{0,0}> createList_LE_115(i18, NULL, a6, i6, env, static) :|: -1 <= i18 && NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < a6
createList_LE_113(i17, NULL, a6, i6, env, static) -{1,1}> createList_Load_119(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && i17 <= 0 && 0 < a6 && -1 <= i17
createList_LE_115(i18, NULL, a6, i6, env, static) -{1,1}> createList_New_121(i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < i18 && 0 < a6
createList_Load_119(NULL, a6, i6, env, static) -{1,1}> createList_Return_126(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_New_121(i18, NULL, a6, i6, env, static) -{1,1}> createList_Duplicate_128(o17, i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < o17 && o17 = 1 && 0 < a6
createList_Return_126(NULL, a6, i6, env, static) -{1,1}> main_Store_134(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_Duplicate_128(o17, i18, NULL, a6, i6, env, static) -{1,1}> createList_Load_137(o17, i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
main_Store_134(a6, NULL, i6, env, static) -{1,1}> main_Load_141(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_Load_137(o17, i18, NULL, a6, i6, env, static) -{1,1}> createList_InvokeMethod_144(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
main_Load_141(a6, NULL, i6, env, static) -{1,1}> main_InvokeMethod_146(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_InvokeMethod_144(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_Load_147(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
main_InvokeMethod_146(a6, NULL, i6, env, static) -{1,1}> reverse_ConstantStackPush_150(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
langle_init_rangle_Load_147(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_153(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
reverse_ConstantStackPush_150(NULL, a6, i6, env, static) -{1,1}> reverse_Store_156(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
langle_init_rangle_InvokeMethod_153(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_Load_157(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
reverse_Store_156(NULL, a6, i6, env, static) -{1,1}> reverse_Load_162(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
langle_init_rangle_Load_157(o17, NULL, i18, a6, i6, env, static) -{0,0}> langle_init_rangle_Load_509(o17, NULL, i18, a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 <= NULL && 0 < a6
reverse_Load_162(NULL, a6, i6, env, static) -{0,0}> reverse_Load_632(NULL, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
langle_init_rangle_Load_509(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_Load_513(o115, o116, i52, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_513(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_FieldAccess_516(o115, o116, i52, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_FieldAccess_516(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_Return_520(o115', i52, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && o115' <= o115 + o116 && 0 < o115' && 0 < o115 && o115' = o115 + o116 && 0 < a67
langle_init_rangle_Return_520(o115, i52, a67, o116, i6, env, static) -{1,1}> createList_Store_522(o115, i52, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Store_522(o115, i52, a67, o116, i6, env, static) -{1,1}> createList_JMP_524(i52, o115, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_JMP_524(i52, o115, a67, o116, i6, env, static) -{1,1}> createList_Inc_526(i52, o115, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Inc_526(i52, o115, a67, o116, i6, env, static) -{1,1}> createList_Load_529(i55, o115, a67, o116, i6, env, static) :|: i52 + -1 = i55 && 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 <= i55 && 0 < o115 && 0 < a67
createList_Load_529(i55, o115, a67, o116, i6, env, static) -{1,1}> createList_LE_536(i55, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= i55 && 0 < o115 && 0 < a67
createList_LE_536(iconst_0, o115, a67, o116, i6, env, static) -{0,0}> createList_LE_539(iconst_0, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o115 && 0 < a67
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{0,0}> createList_LE_540(i60, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= i60 && 0 < o115 && 1 <= i60 && 0 < a67
createList_LE_539(iconst_0, o115, a67, o116, i6, env, static) -{1,1}> createList_Load_543(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o115 && 0 < a67
createList_LE_540(i60, o115, a67, o116, i6, env, static) -{1,1}> createList_New_547(i60, o115, a67, o116, i6, env, static) :|: 0 < i60 && 0 <= o116 && 1 <= i6 && 0 < o115 && 1 <= i60 && 0 < a67
createList_Load_543(o115, a67, o116, i6, env, static) -{1,1}> createList_Return_550(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_New_547(i60, o115, a67, o116, i6, env, static) -{1,1}> createList_Duplicate_553(o137, i60, o115, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && o137 = 1 && 0 < a67
createList_Return_550(o115, a67, o116, i6, env, static) -{1,1}> main_Store_556(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Duplicate_553(o137, i60, o115, a67, NULL, o116, i6, env, static) -{1,1}> createList_Load_559(o137, i60, o115, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
main_Store_556(a67, o115, i6, o116, env, static) -{1,1}> main_Load_562(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Load_559(o137, i60, o115, a67, NULL, o116, i6, env, static) -{1,1}> createList_InvokeMethod_565(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
main_Load_562(a67, o115, i6, o116, env, static) -{1,1}> main_InvokeMethod_568(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_InvokeMethod_565(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_Load_570(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
main_InvokeMethod_568(a67, o115, i6, o116, env, static) -{1,1}> reverse_ConstantStackPush_572(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_570(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_575(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
reverse_ConstantStackPush_572(o115, a67, o116, i6, env, static) -{1,1}> reverse_Store_577(NULL, o115, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_InvokeMethod_575(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_Load_582(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
reverse_Store_577(NULL, o115, a67, o116, i6, env, static) -{1,1}> reverse_Load_586(o115, NULL, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_582(o137, o115, i60, a67, NULL, o116, i6, env, static) -{0,0}> langle_init_rangle_Load_509(o137, o115, i60, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 <= o115 && 0 < o115 && 1 <= i60 && 0 < a67
reverse_Load_586(o115, NULL, a67, o116, i6, env, static) -{0,0}> reverse_Load_632(o115, NULL, a67, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 <= o115 && 0 <= NULL && 0 < o115 && 0 < a67
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
reverse_NULL_635(o181, o171, a99, i6, env, static) -{0,0}> reverse_NULL_637(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o181 && 0 <= o171
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(NULL, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
reverse_NULL_637(o181, o171, a99, i6, env, static) -{1,1}> reverse_Load_641(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Load_641(o181, o171, a99, i6, env, static) -{1,1}> reverse_Store_645(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Store_645(o182, o171, a99, i6, env, static) -{0,0}> reverse_Store_652(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 1 + o183 = o182 && 0 <= o171
reverse_Store_652(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Load_657(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_657(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Store_662(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_662(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_663(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_663(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_664(o182, o183, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_664(o182, o183, o171, a99, i6, env, static) -{1,1}> reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) -{1,1}> reverse_Load_668(o183, o182', a99, o171, i6, env, static) :|: o182' = o182 + o171 + -1 * o183 && 1 <= i6 && 0 < o182' && o182' <= o182 + o171 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_668(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Store_670(o182, o183, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_670(o182, o183, a99, o171, i6, env, static) -{1,1}> reverse_JMP_675(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_JMP_675(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Load_690(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_690(o183, o182, a99, o171, i6, env, static) -{0,0}> reverse_Load_632(o183, o182, a99, i6, env, static) :|: 0 <= o182 && 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171

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

obtained
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
by chaining
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_26(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_26(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_46(o2, env, static) :|: 0 < o2
main_Load_46(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_48(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2
main_Load_51(o2, env, static) -{1,1}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_56(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5

obtained
main_ArrayAccess_56(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
by chaining
main_ArrayAccess_56(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_58(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6

obtained
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i10', 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
by chaining
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_ConstantStackPush_70(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_ConstantStackPush_70(a6, i8, i6, env, static) -{1,1}> main_InvokeMethod_77(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_77(a6, i8, NULL, i6, env, static) -{0,0}> main_InvokeMethod_81(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_81(a6, i8, NULL, i6, env, static) -{1,1}> createList_Inc_85(i8, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
createList_Inc_85(i8, NULL, a6, i6, env, static) -{1,1}> createList_Load_92(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8 && i8 + -1 = i10 && -1 <= i10
createList_Load_92(i10, NULL, a6, i6, env, static) -{1,1}> createList_LE_100(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && -1 <= i10

obtained
createList_LE_100(i18, 0, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
by chaining
createList_LE_100(i18, NULL, a6, i6, env, static) -{0,0}> createList_LE_115(i18, NULL, a6, i6, env, static) :|: -1 <= i18 && NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < a6
createList_LE_115(i18, NULL, a6, i6, env, static) -{1,1}> createList_New_121(i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < i18 && 0 < a6
createList_New_121(i18, NULL, a6, i6, env, static) -{1,1}> createList_Duplicate_128(o17, i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < o17 && o17 = 1 && 0 < a6
createList_Duplicate_128(o17, i18, NULL, a6, i6, env, static) -{1,1}> createList_Load_137(o17, i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
createList_Load_137(o17, i18, NULL, a6, i6, env, static) -{1,1}> createList_InvokeMethod_144(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
createList_InvokeMethod_144(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_Load_147(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
langle_init_rangle_Load_147(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_153(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
langle_init_rangle_InvokeMethod_153(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_Load_157(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
langle_init_rangle_Load_157(o17, NULL, i18, a6, i6, env, static) -{0,0}> langle_init_rangle_Load_509(o17, NULL, i18, a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 <= NULL && 0 < a6

obtained
langle_init_rangle_Load_509(o115, o116, i52, a67, 0, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
by chaining
langle_init_rangle_Load_509(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_Load_513(o115, o116, i52, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_513(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_FieldAccess_516(o115, o116, i52, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_FieldAccess_516(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_Return_520(o115', i52, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && o115' <= o115 + o116 && 0 < o115' && 0 < o115 && o115' = o115 + o116 && 0 < a67
langle_init_rangle_Return_520(o115, i52, a67, o116, i6, env, static) -{1,1}> createList_Store_522(o115, i52, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Store_522(o115, i52, a67, o116, i6, env, static) -{1,1}> createList_JMP_524(i52, o115, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_JMP_524(i52, o115, a67, o116, i6, env, static) -{1,1}> createList_Inc_526(i52, o115, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Inc_526(i52, o115, a67, o116, i6, env, static) -{1,1}> createList_Load_529(i55, o115, a67, o116, i6, env, static) :|: i52 + -1 = i55 && 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 <= i55 && 0 < o115 && 0 < a67
createList_Load_529(i55, o115, a67, o116, i6, env, static) -{1,1}> createList_LE_536(i55, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= i55 && 0 < o115 && 0 < a67

obtained
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
by chaining
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{0,0}> createList_LE_540(i60, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= i60 && 0 < o115 && 1 <= i60 && 0 < a67
createList_LE_540(i60, o115, a67, o116, i6, env, static) -{1,1}> createList_New_547(i60, o115, a67, o116, i6, env, static) :|: 0 < i60 && 0 <= o116 && 1 <= i6 && 0 < o115 && 1 <= i60 && 0 < a67
createList_New_547(i60, o115, a67, o116, i6, env, static) -{1,1}> createList_Duplicate_553(o137, i60, o115, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && o137 = 1 && 0 < a67
createList_Duplicate_553(o137, i60, o115, a67, NULL, o116, i6, env, static) -{1,1}> createList_Load_559(o137, i60, o115, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
createList_Load_559(o137, i60, o115, a67, NULL, o116, i6, env, static) -{1,1}> createList_InvokeMethod_565(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
createList_InvokeMethod_565(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_Load_570(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
langle_init_rangle_Load_570(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_575(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
langle_init_rangle_InvokeMethod_575(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_Load_582(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
langle_init_rangle_Load_582(o137, o115, i60, a67, NULL, o116, i6, env, static) -{0,0}> langle_init_rangle_Load_509(o137, o115, i60, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 <= o115 && 0 < o115 && 1 <= i60 && 0 < a67

obtained
createList_LE_536(0, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115
by chaining
createList_LE_536(iconst_0, o115, a67, o116, i6, env, static) -{0,0}> createList_LE_539(iconst_0, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o115 && 0 < a67
createList_LE_539(iconst_0, o115, a67, o116, i6, env, static) -{1,1}> createList_Load_543(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o115 && 0 < a67
createList_Load_543(o115, a67, o116, i6, env, static) -{1,1}> createList_Return_550(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Return_550(o115, a67, o116, i6, env, static) -{1,1}> main_Store_556(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
main_Store_556(a67, o115, i6, o116, env, static) -{1,1}> main_Load_562(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
main_Load_562(a67, o115, i6, o116, env, static) -{1,1}> main_InvokeMethod_568(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
main_InvokeMethod_568(a67, o115, i6, o116, env, static) -{1,1}> reverse_ConstantStackPush_572(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
reverse_ConstantStackPush_572(o115, a67, o116, i6, env, static) -{1,1}> reverse_Store_577(NULL, o115, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
reverse_Store_577(NULL, o115, a67, o116, i6, env, static) -{1,1}> reverse_Load_586(o115, NULL, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
reverse_Load_586(o115, NULL, a67, o116, i6, env, static) -{0,0}> reverse_Load_632(o115, NULL, a67, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 <= o115 && 0 <= NULL && 0 < o115 && 0 < a67

obtained
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
by chaining
reverse_NULL_635(o181, o171, a99, i6, env, static) -{0,0}> reverse_NULL_637(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o181 && 0 <= o171
reverse_NULL_637(o181, o171, a99, i6, env, static) -{1,1}> reverse_Load_641(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Load_641(o181, o171, a99, i6, env, static) -{1,1}> reverse_Store_645(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Store_645(o182, o171, a99, i6, env, static) -{0,0}> reverse_Store_652(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 1 + o183 = o182 && 0 <= o171
reverse_Store_652(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Load_657(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_657(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Store_662(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_662(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_663(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_663(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_664(o182, o183, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_664(o182, o183, o171, a99, i6, env, static) -{1,1}> reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) -{1,1}> reverse_Load_668(o183, o182', a99, o171, i6, env, static) :|: o182' = o182 + o171 + -1 * o183 && 1 <= i6 && 0 < o182' && o182' <= o182 + o171 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_668(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Store_670(o182, o183, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_670(o182, o183, a99, o171, i6, env, static) -{1,1}> reverse_JMP_675(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_JMP_675(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Load_690(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_690(o183, o182, a99, o171, i6, env, static) -{0,0}> reverse_Load_632(o183, o182, a99, i6, env, static) :|: 0 <= o182 && 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171

obtained
createList_LE_100(i17, 0, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6
by chaining
createList_LE_100(i17, NULL, a6, i6, env, static) -{0,0}> createList_LE_113(i17, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && i17 <= 0 && 0 < a6 && -1 <= i17
createList_LE_113(i17, NULL, a6, i6, env, static) -{1,1}> createList_Load_119(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && i17 <= 0 && 0 < a6 && -1 <= i17
createList_Load_119(NULL, a6, i6, env, static) -{1,1}> createList_Return_126(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_Return_126(NULL, a6, i6, env, static) -{1,1}> main_Store_134(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
main_Store_134(a6, NULL, i6, env, static) -{1,1}> main_Load_141(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
main_Load_141(a6, NULL, i6, env, static) -{1,1}> main_InvokeMethod_146(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
main_InvokeMethod_146(a6, NULL, i6, env, static) -{1,1}> reverse_ConstantStackPush_150(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
reverse_ConstantStackPush_150(NULL, a6, i6, env, static) -{1,1}> reverse_Store_156(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
reverse_Store_156(NULL, a6, i6, env, static) -{1,1}> reverse_Load_162(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
reverse_Load_162(NULL, a6, i6, env, static) -{0,0}> reverse_Load_632(NULL, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6

(8) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_56(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_56(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i10', 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
createList_LE_100(i18, 0, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
langle_init_rangle_Load_509(o115, o116, i52, a67, 0, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
createList_LE_536(0, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(NULL, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
createList_LE_100(i17, 0, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6

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

Moved arithmethic from lhss to constraints.

createList_LE_100(i17, 0, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6
was transformed to
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6 && x = 0

createList_LE_100(i18, 0, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
was transformed to
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18 && x = 0

main_ArrayAccess_56(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
was transformed to
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0

createList_LE_536(0, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115
was transformed to
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0

langle_init_rangle_Load_509(o115, o116, i52, a67, 0, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
was transformed to
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0

(10) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6 && x = 0
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18 && x = 0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(NULL, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
main_ArrayAccess_56(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i10', 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0

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

Linearized lhss.

main_ArrayAccess_56(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

(12) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6 && x = 0
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18 && x = 0
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(NULL, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i10', 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171

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

Moved arithmethic from constraints to rhss.

langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0
was transformed to
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0

main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
was transformed to
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6

reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
was transformed to
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'

reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(NULL, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
was transformed to
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(0, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171

main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i10', 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
was transformed to
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i8' + -1, 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12

(14) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0
main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6 && x = 0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18 && x = 0
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(0, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i8' + -1, 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60

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

Simplified expressions.

main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i8' + -1, 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
was transformed to
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i8' - 1, 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' - 1 = i10' && 0 < o12

main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
was transformed to
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0

createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6 && x = 0
was transformed to
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 1 <= i6 && x = 0

createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18 && x = 0
was transformed to
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 1 <= i6 && 0 < i18 && x = 0

reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
was transformed to
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', 1 + o171, a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && o182''' <= o181 + o171 && o182''' = o181 + o171 + -1 * o183'

main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1

langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0
was transformed to
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i52 - 1, o115 + o116, a67, o116, i6, env, static) :|: 0 < a67 && i52 - 1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0

createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
was transformed to
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && x = 0

createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
was transformed to
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115

(16) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i52 - 1, o115 + o116, a67, o116, i6, env, static) :|: 0 < a67 && i52 - 1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(0, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && x = 0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 1 <= i6 && x = 0
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i8' - 1, 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' - 1 = i10' && 0 < o12
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', 1 + o171, a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && o182''' <= o181 + o171 && o182''' = o181 + o171 + -1 * o183'
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 1 <= i6 && 0 < i18 && x = 0

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

Transformed 100 jbc graph edges to a weighted ITS with 100 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.

(18) Obligation:

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

(20) Obligation:

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

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

Linearized lhss.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 13 rules
Start term: main_Load_1(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
langle_init_rangle_Load_509(o115, o116, i52, a67, x, i6, env, static) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116 && x = 0
main_ArrayAccess_56(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_57(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_ArrayAccess_56(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
createList_LE_100(i17, x, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6 && x = 0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
reverse_NULL_635(o181, o171, a99, i6, env, static) -{12,12}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6, env, static) :|: 0 < o181 && 0 <= o171 && 1 + o183' = o181 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o181 + o171 && 0 <= o181 && o182''' = o181 + o171 + -1 * o183'
createList_LE_100(i18, x, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18 && x = 0
reverse_NULL_635(NULL, o171, a99, i6, env, static) -{0,0}> reverse_NULL_639(0, o171, a99, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a99 && 0 <= NULL && 0 <= o171
main_Load_1(o2, env, static) -{17,17}> main_ArrayAccess_56(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, o12, i6, env, static) -{5,5}> createList_LE_100(i8' + -1, 0, a6, i6, env, static) :|: i8' <= o12 && -1 <= i10' && 0 <= o12 && 0 < a6 && 0 <= i8' && 1 <= i6 && i8' + -1 = i10' && 0 < o12
createList_LE_536(x, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60

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

Simplified expressions.

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(46)) transformation)

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

(30) Obligation:

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

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

Considered paths: all paths from start

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

Transformed 97 jbc graph edges to a weighted ITS with 97 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.

(32) Obligation:

IntTrs with 97 rules
Start term: main_Load_1(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_26(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_26(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_46(o2, env, static) :|: 0 < o2
main_Load_46(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_48(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2
main_Load_51(o2, env, static) -{1,1}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_56(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_56(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_58(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_ConstantStackPush_70(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_ConstantStackPush_70(a6, i8, i6, env, static) -{1,1}> main_InvokeMethod_77(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_77(a6, i8, NULL, i6, env, static) -{0,0}> main_InvokeMethod_81(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_81(a6, i8, NULL, i6, env, static) -{1,1}> createList_Inc_85(i8, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
createList_Inc_85(i8, NULL, a6, i6, env, static) -{1,1}> createList_Load_92(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8 && i8 + -1 = i10 && -1 <= i10
createList_Load_92(i10, NULL, a6, i6, env, static) -{1,1}> createList_LE_100(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && -1 <= i10
createList_LE_100(i17, NULL, a6, i6, env, static) -{0,0}> createList_LE_113(i17, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && i17 <= 0 && 0 < a6 && -1 <= i17
createList_LE_100(i18, NULL, a6, i6, env, static) -{0,0}> createList_LE_115(i18, NULL, a6, i6, env, static) :|: -1 <= i18 && NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < a6
createList_LE_113(i17, NULL, a6, i6, env, static) -{1,1}> createList_Load_119(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && i17 <= 0 && 0 < a6 && -1 <= i17
createList_LE_115(i18, NULL, a6, i6, env, static) -{1,1}> createList_New_121(i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < i18 && 0 < a6
createList_Load_119(NULL, a6, i6, env, static) -{1,1}> createList_Return_126(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_New_121(i18, NULL, a6, i6, env, static) -{1,1}> createList_Duplicate_128(o17, i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 1 <= i6 && 0 < o17 && o17 = 1 && 0 < a6
createList_Return_126(NULL, a6, i6, env, static) -{1,1}> main_Store_134(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_Duplicate_128(o17, i18, NULL, a6, i6, env, static) -{1,1}> createList_Load_137(o17, i18, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
main_Store_134(a6, NULL, i6, env, static) -{1,1}> main_Load_141(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_Load_137(o17, i18, NULL, a6, i6, env, static) -{1,1}> createList_InvokeMethod_144(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
main_Load_141(a6, NULL, i6, env, static) -{1,1}> main_InvokeMethod_146(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
createList_InvokeMethod_144(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_Load_147(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
main_InvokeMethod_146(a6, NULL, i6, env, static) -{1,1}> reverse_ConstantStackPush_150(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
langle_init_rangle_Load_147(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_153(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
reverse_ConstantStackPush_150(NULL, a6, i6, env, static) -{1,1}> reverse_Store_156(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
langle_init_rangle_InvokeMethod_153(o17, NULL, i18, a6, i6, env, static) -{1,1}> langle_init_rangle_Load_157(o17, NULL, i18, a6, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 < a6
reverse_Store_156(NULL, a6, i6, env, static) -{1,1}> reverse_Load_162(NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6
langle_init_rangle_Load_157(o17, NULL, i18, a6, i6, env, static) -{0,0}> langle_init_rangle_Load_509(o17, NULL, i18, a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i18 && 0 < o17 && 1 <= i6 && 0 <= NULL && 0 < a6
reverse_Load_162(NULL, a6, i6, env, static) -{0,0}> reverse_Load_632(NULL, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
langle_init_rangle_Load_509(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_Load_513(o115, o116, i52, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_513(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_FieldAccess_516(o115, o116, i52, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_FieldAccess_516(o115, o116, i52, a67, NULL, i6, env, static) -{1,1}> langle_init_rangle_Return_520(o115', i52, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i52 && 1 <= i6 && o115' <= o115 + o116 && 0 < o115' && 0 < o115 && o115' = o115 + o116 && 0 < a67
langle_init_rangle_Return_520(o115, i52, a67, o116, i6, env, static) -{1,1}> createList_Store_522(o115, i52, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Store_522(o115, i52, a67, o116, i6, env, static) -{1,1}> createList_JMP_524(i52, o115, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_JMP_524(i52, o115, a67, o116, i6, env, static) -{1,1}> createList_Inc_526(i52, o115, a67, o116, i6, env, static) :|: 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Inc_526(i52, o115, a67, o116, i6, env, static) -{1,1}> createList_Load_529(i55, o115, a67, o116, i6, env, static) :|: i52 + -1 = i55 && 1 <= i52 && 0 <= o116 && 1 <= i6 && 0 <= i55 && 0 < o115 && 0 < a67
createList_Load_529(i55, o115, a67, o116, i6, env, static) -{1,1}> createList_LE_536(i55, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= i55 && 0 < o115 && 0 < a67
createList_LE_536(iconst_0, o115, a67, o116, i6, env, static) -{0,0}> createList_LE_539(iconst_0, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= iconst_0 && iconst_0 = 0 && 0 < o115 && 0 < a67
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{0,0}> createList_LE_540(i60, o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 <= i60 && 0 < o115 && 1 <= i60 && 0 < a67
createList_LE_539(iconst_0, o115, a67, o116, i6, env, static) -{1,1}> createList_Load_543(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && iconst_0 <= 0 && iconst_0 = 0 && 0 < o115 && 0 < a67
createList_LE_540(i60, o115, a67, o116, i6, env, static) -{1,1}> createList_New_547(i60, o115, a67, o116, i6, env, static) :|: 0 < i60 && 0 <= o116 && 1 <= i6 && 0 < o115 && 1 <= i60 && 0 < a67
createList_Load_543(o115, a67, o116, i6, env, static) -{1,1}> createList_Return_550(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_New_547(i60, o115, a67, o116, i6, env, static) -{1,1}> createList_Duplicate_553(o137, i60, o115, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && o137 = 1 && 0 < a67
createList_Return_550(o115, a67, o116, i6, env, static) -{1,1}> main_Store_556(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Duplicate_553(o137, i60, o115, a67, NULL, o116, i6, env, static) -{1,1}> createList_Load_559(o137, i60, o115, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
main_Store_556(a67, o115, i6, o116, env, static) -{1,1}> main_Load_562(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_Load_559(o137, i60, o115, a67, NULL, o116, i6, env, static) -{1,1}> createList_InvokeMethod_565(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
main_Load_562(a67, o115, i6, o116, env, static) -{1,1}> main_InvokeMethod_568(a67, o115, i6, o116, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
createList_InvokeMethod_565(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_Load_570(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
main_InvokeMethod_568(a67, o115, i6, o116, env, static) -{1,1}> reverse_ConstantStackPush_572(o115, a67, o116, i6, env, static) :|: 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_570(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_InvokeMethod_575(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
reverse_ConstantStackPush_572(o115, a67, o116, i6, env, static) -{1,1}> reverse_Store_577(NULL, o115, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_InvokeMethod_575(o137, o115, i60, a67, NULL, o116, i6, env, static) -{1,1}> langle_init_rangle_Load_582(o137, o115, i60, a67, NULL, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 < o115 && 1 <= i60 && 0 < a67
reverse_Store_577(NULL, o115, a67, o116, i6, env, static) -{1,1}> reverse_Load_586(o115, NULL, a67, o116, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o115 && 0 < a67
langle_init_rangle_Load_582(o137, o115, i60, a67, NULL, o116, i6, env, static) -{0,0}> langle_init_rangle_Load_509(o137, o115, i60, a67, NULL, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 < o137 && 0 <= o115 && 0 < o115 && 1 <= i60 && 0 < a67
reverse_Load_586(o115, NULL, a67, o116, i6, env, static) -{0,0}> reverse_Load_632(o115, NULL, a67, i6, env, static) :|: NULL = 0 && 0 <= o116 && 1 <= i6 && 0 <= o115 && 0 <= NULL && 0 < o115 && 0 < a67
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
reverse_NULL_635(o181, o171, a99, i6, env, static) -{0,0}> reverse_NULL_637(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o181 && 0 <= o171
reverse_NULL_637(o181, o171, a99, i6, env, static) -{1,1}> reverse_Load_641(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Load_641(o181, o171, a99, i6, env, static) -{1,1}> reverse_Store_645(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Store_645(o182, o171, a99, i6, env, static) -{0,0}> reverse_Store_652(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 1 + o183 = o182 && 0 <= o171
reverse_Store_652(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Load_657(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_657(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Store_662(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_662(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_663(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_663(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_664(o182, o183, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_664(o182, o183, o171, a99, i6, env, static) -{1,1}> reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) -{1,1}> reverse_Load_668(o183, o182', a99, o171, i6, env, static) :|: o182' = o182 + o171 + -1 * o183 && 1 <= i6 && 0 < o182' && o182' <= o182 + o171 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_668(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Store_670(o182, o183, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_670(o182, o183, a99, o171, i6, env, static) -{1,1}> reverse_JMP_675(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_JMP_675(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Load_690(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_690(o183, o182, a99, o171, i6, env, static) -{0,0}> reverse_Load_632(o183, o182, a99, i6, env, static) :|: 0 <= o182 && 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171

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

obtained
main_Load_1(o2, env, static) -{23,23}> createList_LE_100(i10', 0, o2, i5', env, static'1) :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(o2, env, static) -{0,0}> main_Load_3(o2, env, static) :|: 0 < o2
main_Load_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(o2, env, static) -{0,0}> langle_clinit_rangle_New_18(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_18(o2, env, static) -{0,0}> langle_clinit_rangle_New_19(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_19(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_24(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_26(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_26(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_37(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_41(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_41(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_46(o2, env, static) :|: 0 < o2
main_Load_46(o2, env, static) -{0,0}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_48(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_51(o2, env, static) :|: 0 < o2
main_Load_51(o2, env, static) -{1,1}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_ArrayAccess_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_53(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_56(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_56(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_58(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_ConstantStackPush_70(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_ConstantStackPush_70(a6, i8, i6, env, static) -{1,1}> main_InvokeMethod_77(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_77(a6, i8, NULL, i6, env, static) -{0,0}> main_InvokeMethod_81(a6, i8, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
main_InvokeMethod_81(a6, i8, NULL, i6, env, static) -{1,1}> createList_Inc_85(i8, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8
createList_Inc_85(i8, NULL, a6, i6, env, static) -{1,1}> createList_Load_92(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && 0 <= i8 && i8 + -1 = i10 && -1 <= i10
createList_Load_92(i10, NULL, a6, i6, env, static) -{1,1}> createList_LE_100(i10, NULL, a6, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 < a6 && -1 <= i10

obtained
reverse_Load_632(o170, o171, a99, i6, env, static) -{13,13}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
by chaining
reverse_Load_632(o170, o171, a99, i6, env, static) -{1,1}> reverse_NULL_635(o170, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o170 && 0 <= o171
reverse_NULL_635(o181, o171, a99, i6, env, static) -{0,0}> reverse_NULL_637(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o181 && 0 <= o171
reverse_NULL_637(o181, o171, a99, i6, env, static) -{1,1}> reverse_Load_641(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Load_641(o181, o171, a99, i6, env, static) -{1,1}> reverse_Store_645(o181, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 < o181 && 0 <= o171
reverse_Store_645(o182, o171, a99, i6, env, static) -{0,0}> reverse_Store_652(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 1 + o183 = o182 && 0 <= o171
reverse_Store_652(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Load_657(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_657(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_659(o182, o171, a99, o183, i6, env, static) -{1,1}> reverse_Store_662(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_662(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_663(o183, o171, o182, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_663(o183, o171, o182, a99, i6, env, static) -{1,1}> reverse_Load_664(o182, o183, o171, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_664(o182, o183, o171, a99, i6, env, static) -{1,1}> reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_FieldAccess_665(o182, o171, o183, a99, i6, env, static) -{1,1}> reverse_Load_668(o183, o182', a99, o171, i6, env, static) :|: o182' = o182 + o171 + -1 * o183 && 1 <= i6 && 0 < o182' && o182' <= o182 + o171 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_668(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Store_670(o182, o183, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Store_670(o182, o183, a99, o171, i6, env, static) -{1,1}> reverse_JMP_675(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_JMP_675(o183, o182, a99, o171, i6, env, static) -{1,1}> reverse_Load_690(o183, o182, a99, o171, i6, env, static) :|: 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171
reverse_Load_690(o183, o182, a99, o171, i6, env, static) -{0,0}> reverse_Load_632(o183, o182, a99, i6, env, static) :|: 0 <= o182 && 1 <= i6 && 0 < a99 && 0 <= o183 && 0 < o182 && 0 <= o171

(34) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, env, static) -{23,23}> createList_LE_100(i10', 0, o2, i5', env, static'1) :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
createList_LE_100(i18, 0, a6, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, 0, i6, env, static) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
langle_init_rangle_Load_509(o115, o116, i52, a67, 0, i6, env, static) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6, env, static) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
createList_LE_536(i60, o115, a67, o116, i6, env, static) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, 0, i6, env, static) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
createList_LE_536(0, o115, a67, o116, i6, env, static) -{8,8}> reverse_Load_632(o115, 0, a67, i6, env, static) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115
reverse_Load_632(o170, o171, a99, i6, env, static) -{13,13}> reverse_Load_632(o183', o182''', a99, i6, env, static) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
createList_LE_100(i17, 0, a6, i6, env, static) -{8,8}> reverse_Load_632(0, 0, a6, i6, env, static) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6

(35) 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_LE_100(x1, x2, x3, x4, x5, x6) → createList_LE_100(x1, x3, x4)
langle_init_rangle_Load_509(x1, x2, x3, x4, x5, x6, x7, x8) → langle_init_rangle_Load_509(x1, x2, x3, x4, x6)
createList_LE_536(x1, x2, x3, x4, x5, x6, x7) → createList_LE_536(x1, x2, x3, x4, x5)
reverse_Load_632(x1, x2, x3, x4, x5, x6) → reverse_Load_632(x1, x2, x3, x4)

(36) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, static) -{23,23}> createList_LE_100(i10', o2, i5') :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
createList_LE_100(i18, a6, i6) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, i6) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
createList_LE_536(i60, o115, a67, o116, i6) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, i6) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
createList_LE_536(0, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115
reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', o182''', a99, i6) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
createList_LE_100(i17, a6, i6) -{8,8}> reverse_Load_632(0, 0, a6, i6) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6

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

Moved arithmethic from lhss to constraints.

createList_LE_536(0, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115
was transformed to
createList_LE_536(x, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0

(38) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', o182''', a99, i6) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
main_Load_1(o2, static) -{23,23}> createList_LE_100(i10', o2, i5') :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
createList_LE_536(x, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
createList_LE_536(i60, o115, a67, o116, i6) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, i6) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
createList_LE_100(i17, a6, i6) -{8,8}> reverse_Load_632(0, 0, a6, i6) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6
createList_LE_100(i18, a6, i6) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, i6) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18

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

Moved arithmethic from constraints to rhss.

main_Load_1(o2, static) -{23,23}> createList_LE_100(i10', o2, i5') :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(o2, static) -{23,23}> createList_LE_100(i8' + -1, o2, i5') :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1

reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', o182''', a99, i6) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
was transformed to
reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'

langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i55', o115''', a67, o116, i6) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
was transformed to
langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116

(40) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
main_Load_1(o2, static) -{23,23}> createList_LE_100(i8' + -1, o2, i5') :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
createList_LE_536(i60, o115, a67, o116, i6) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, i6) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
createList_LE_100(i17, a6, i6) -{8,8}> reverse_Load_632(0, 0, a6, i6) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6
createList_LE_100(i18, a6, i6) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, i6) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
createList_LE_536(x, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0

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

Simplified expressions.

createList_LE_536(i60, o115, a67, o116, i6) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, i6) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115 && 0 <= o115 && 0 < 1 && 0 <= i60
was transformed to
createList_LE_536(i60, o115, a67, o116, i6) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, i6) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115

createList_LE_100(i17, a6, i6) -{8,8}> reverse_Load_632(0, 0, a6, i6) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 0 <= 0 && 1 <= i6
was transformed to
createList_LE_100(i17, a6, i6) -{8,8}> reverse_Load_632(0, 0, a6, i6) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 1 <= i6

langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i52 + -1, o115 + o116, a67, o116, i6) :|: o115''' <= o115 + o116 && 0 < a67 && i52 + -1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
was transformed to
langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i52 - 1, o115 + o116, a67, o116, i6) :|: 0 < a67 && i52 - 1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116

main_Load_1(o2, static) -{23,23}> createList_LE_100(i8' + -1, o2, i5') :|: 0 < 2 && -1 <= i10' && 0 <= static'1 && 0 < o2 && 0 <= 1 && 1 <= i5' && 0 <= o8' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' + -1 = i10' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(o2, static) -{23,23}> createList_LE_100(i8' - 1, o2, i5') :|: -1 <= i10' && 0 <= static'1 && 0 < o2 && 1 <= i5' && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' - 1 = i10' && static'1 <= static''' + 1

createList_LE_100(i18, a6, i6) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, i6) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 0 <= 0 && 1 <= i6 && 0 < 1 && 0 < i18
was transformed to
createList_LE_100(i18, a6, i6) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, i6) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 1 <= i6 && 0 < i18

reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', 1 + o183' + o171 + -1 * o183', a99, i6) :|: 0 <= o170 && 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && 0 <= o182''' && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
was transformed to
reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', 1 + o171, a99, i6) :|: 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'

createList_LE_536(x, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 <= 0 && 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && 0 <= o115 && x = 0
was transformed to
createList_LE_536(x, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && x = 0

(42) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(args, static)
Considered paths: all paths from start
Rules:
createList_LE_536(i60, o115, a67, o116, i6) -{7,7}> langle_init_rangle_Load_509(1, o115, i60, a67, i6) :|: 0 < i60 && 0 < a67 && 0 <= o116 && 1 <= i60 && 1 <= i6 && 0 < o115
langle_init_rangle_Load_509(o115, o116, i52, a67, i6) -{8,8}> createList_LE_536(i52 - 1, o115 + o116, a67, o116, i6) :|: 0 < a67 && i52 - 1 = i55' && 0 < o115''' && 0 < o115 && 0 <= i55' && 1 <= i6 && 0 <= o116 && 1 <= i52 && o115''' = o115 + o116
createList_LE_100(i18, a6, i6) -{7,7}> langle_init_rangle_Load_509(1, 0, i18, a6, i6) :|: -1 <= i18 && 0 < a6 && 1 <= i18 && 1 <= i6 && 0 < i18
main_Load_1(o2, static) -{23,23}> createList_LE_100(i8' - 1, o2, i5') :|: -1 <= i10' && 0 <= static'1 && 0 < o2 && 1 <= i5' && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && 0 <= i8' && static''' <= static + 2 && i8' - 1 = i10' && static'1 <= static''' + 1
reverse_Load_632(o170, o171, a99, i6) -{13,13}> reverse_Load_632(o183', 1 + o171, a99, i6) :|: 0 <= o171 && 0 < o170 && 0 < o182''' && 0 < a99 && 0 <= o183' && 1 <= i6 && o182''' <= o170 + o171 && 1 + o183' = o170 && o182''' = o170 + o171 + -1 * o183'
createList_LE_536(x, o115, a67, o116, i6) -{8,8}> reverse_Load_632(o115, 0, a67, i6) :|: 0 < a67 && 0 < o115 && 0 <= o116 && 1 <= i6 && x = 0
createList_LE_100(i17, a6, i6) -{8,8}> reverse_Load_632(0, 0, a6, i6) :|: -1 <= i17 && 0 < a6 && i17 <= 0 && 1 <= i6

(43) koat Proof (EQUIVALENT transformation)

YES(?, 168*ar_0 + 46)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 7) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, ar_1, ar_0, ar_2, ar_4)) [ 0 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_3 /\ 1 <= ar_0 /\ 1 <= ar_4 /\ 0 < ar_1 ]
(Comp: ?, Cost: 8) langle_init_rangle_Load_509(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_536(ar_2 - 1, ar_0 + ar_1, ar_3, ar_1, ar_4)) [ 0 < ar_3 /\ ar_2 - 1 = i55' /\ 0 < o115''' /\ 0 < ar_0 /\ 0 <= i55' /\ 1 <= ar_4 /\ 0 <= ar_1 /\ 1 <= ar_2 /\ o115''' = ar_0 + ar_1 ]
(Comp: ?, Cost: 7) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, 0, ar_0, ar_1, ar_2)) [ -1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_0 ]
(Comp: ?, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_100(i8' - 1, ar_0, i5', arityPad, arityPad)) [ -1 <= i10' /\ 0 <= static'1 /\ 0 < ar_0 /\ 1 <= i5' /\ 0 <= ar_1 /\ 0 < i5' /\ 0 <= static''' /\ i5' < ar_0 /\ i8' <= o8' /\ o8' < ar_0 /\ 0 < o8' /\ 0 <= i8' /\ static''' <= ar_1 + 2 /\ i8' - 1 = i10' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 13) reverse_Load_632(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(o183', ar_1 + 1, ar_2, ar_3, arityPad)) [ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < o182''' /\ 0 < ar_2 /\ 0 <= o183' /\ 1 <= ar_3 /\ o182''' <= ar_0 + ar_1 /\ o183' + 1 = ar_0 /\ o182''' = ar_0 + ar_1 - o183' ]
(Comp: ?, Cost: 8) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(ar_1, 0, ar_2, ar_4, arityPad)) [ 0 < ar_2 /\ 0 < ar_1 /\ 0 <= ar_3 /\ 1 <= ar_4 /\ ar_0 = 0 ]
(Comp: ?, Cost: 8) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(0, 0, ar_1, ar_2, arityPad)) [ -1 <= ar_0 /\ 0 < ar_1 /\ ar_0 <= 0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 7) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, ar_1, ar_0, ar_2, ar_4)) [ 0 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_3 /\ 1 <= ar_0 /\ 1 <= ar_4 /\ 0 < ar_1 ]
(Comp: ?, Cost: 8) langle_init_rangle_Load_509(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_536(ar_2 - 1, ar_0 + ar_1, ar_3, ar_1, ar_4)) [ 0 < ar_3 /\ ar_2 - 1 = i55' /\ 0 < o115''' /\ 0 < ar_0 /\ 0 <= i55' /\ 1 <= ar_4 /\ 0 <= ar_1 /\ 1 <= ar_2 /\ o115''' = ar_0 + ar_1 ]
(Comp: 1, Cost: 7) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, 0, ar_0, ar_1, ar_2)) [ -1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_0 ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_100(i8' - 1, ar_0, i5', arityPad, arityPad)) [ -1 <= i10' /\ 0 <= static'1 /\ 0 < ar_0 /\ 1 <= i5' /\ 0 <= ar_1 /\ 0 < i5' /\ 0 <= static''' /\ i5' < ar_0 /\ i8' <= o8' /\ o8' < ar_0 /\ 0 < o8' /\ 0 <= i8' /\ static''' <= ar_1 + 2 /\ i8' - 1 = i10' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 13) reverse_Load_632(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(o183', ar_1 + 1, ar_2, ar_3, arityPad)) [ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < o182''' /\ 0 < ar_2 /\ 0 <= o183' /\ 1 <= ar_3 /\ o182''' <= ar_0 + ar_1 /\ o183' + 1 = ar_0 /\ o182''' = ar_0 + ar_1 - o183' ]
(Comp: ?, Cost: 8) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(ar_1, 0, ar_2, ar_4, arityPad)) [ 0 < ar_2 /\ 0 < ar_1 /\ 0 <= ar_3 /\ 1 <= ar_4 /\ ar_0 = 0 ]
(Comp: 1, Cost: 8) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(0, 0, ar_1, ar_2, arityPad)) [ -1 <= ar_0 /\ 0 < ar_1 /\ ar_0 <= 0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(createList_LE_536) = 1
Pol(langle_init_rangle_Load_509) = 1
Pol(createList_LE_100) = 1
Pol(main_Load_1) = 1
Pol(reverse_Load_632) = 0
Pol(koat_start) = 1
orients all transitions weakly and the transition
createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(ar_1, 0, ar_2, ar_4, arityPad)) [ 0 < ar_2 /\ 0 < ar_1 /\ 0 <= ar_3 /\ 1 <= ar_4 /\ ar_0 = 0 ]
strictly and produces the following problem:
3: T:
(Comp: ?, Cost: 7) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, ar_1, ar_0, ar_2, ar_4)) [ 0 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_3 /\ 1 <= ar_0 /\ 1 <= ar_4 /\ 0 < ar_1 ]
(Comp: ?, Cost: 8) langle_init_rangle_Load_509(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_536(ar_2 - 1, ar_0 + ar_1, ar_3, ar_1, ar_4)) [ 0 < ar_3 /\ ar_2 - 1 = i55' /\ 0 < o115''' /\ 0 < ar_0 /\ 0 <= i55' /\ 1 <= ar_4 /\ 0 <= ar_1 /\ 1 <= ar_2 /\ o115''' = ar_0 + ar_1 ]
(Comp: 1, Cost: 7) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, 0, ar_0, ar_1, ar_2)) [ -1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_0 ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_100(i8' - 1, ar_0, i5', arityPad, arityPad)) [ -1 <= i10' /\ 0 <= static'1 /\ 0 < ar_0 /\ 1 <= i5' /\ 0 <= ar_1 /\ 0 < i5' /\ 0 <= static''' /\ i5' < ar_0 /\ i8' <= o8' /\ o8' < ar_0 /\ 0 < o8' /\ 0 <= i8' /\ static''' <= ar_1 + 2 /\ i8' - 1 = i10' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 13) reverse_Load_632(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(o183', ar_1 + 1, ar_2, ar_3, arityPad)) [ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < o182''' /\ 0 < ar_2 /\ 0 <= o183' /\ 1 <= ar_3 /\ o182''' <= ar_0 + ar_1 /\ o183' + 1 = ar_0 /\ o182''' = ar_0 + ar_1 - o183' ]
(Comp: 1, Cost: 8) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(ar_1, 0, ar_2, ar_4, arityPad)) [ 0 < ar_2 /\ 0 < ar_1 /\ 0 <= ar_3 /\ 1 <= ar_4 /\ ar_0 = 0 ]
(Comp: 1, Cost: 8) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(0, 0, ar_1, ar_2, arityPad)) [ -1 <= ar_0 /\ 0 < ar_1 /\ ar_0 <= 0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(createList_LE_536) = 3*V_1 + V_2 + 2
Pol(langle_init_rangle_Load_509) = V_1 + V_2 + 3*V_3
Pol(createList_LE_100) = 3*V_1 + 3*V_2
Pol(main_Load_1) = 6*V_1
Pol(reverse_Load_632) = V_1
Pol(koat_start) = 6*V_1
orients all transitions weakly and the transitions
reverse_Load_632(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(o183', ar_1 + 1, ar_2, ar_3, arityPad)) [ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < o182''' /\ 0 < ar_2 /\ 0 <= o183' /\ 1 <= ar_3 /\ o182''' <= ar_0 + ar_1 /\ o183' + 1 = ar_0 /\ o182''' = ar_0 + ar_1 - o183' ]
langle_init_rangle_Load_509(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_536(ar_2 - 1, ar_0 + ar_1, ar_3, ar_1, ar_4)) [ 0 < ar_3 /\ ar_2 - 1 = i55' /\ 0 < o115''' /\ 0 < ar_0 /\ 0 <= i55' /\ 1 <= ar_4 /\ 0 <= ar_1 /\ 1 <= ar_2 /\ o115''' = ar_0 + ar_1 ]
createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, ar_1, ar_0, ar_2, ar_4)) [ 0 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_3 /\ 1 <= ar_0 /\ 1 <= ar_4 /\ 0 < ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: 6*ar_0, Cost: 7) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, ar_1, ar_0, ar_2, ar_4)) [ 0 < ar_0 /\ 0 < ar_2 /\ 0 <= ar_3 /\ 1 <= ar_0 /\ 1 <= ar_4 /\ 0 < ar_1 ]
(Comp: 6*ar_0, Cost: 8) langle_init_rangle_Load_509(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_536(ar_2 - 1, ar_0 + ar_1, ar_3, ar_1, ar_4)) [ 0 < ar_3 /\ ar_2 - 1 = i55' /\ 0 < o115''' /\ 0 < ar_0 /\ 0 <= i55' /\ 1 <= ar_4 /\ 0 <= ar_1 /\ 1 <= ar_2 /\ o115''' = ar_0 + ar_1 ]
(Comp: 1, Cost: 7) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(langle_init_rangle_Load_509(1, 0, ar_0, ar_1, ar_2)) [ -1 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_0 ]
(Comp: 1, Cost: 23) main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(createList_LE_100(i8' - 1, ar_0, i5', arityPad, arityPad)) [ -1 <= i10' /\ 0 <= static'1 /\ 0 < ar_0 /\ 1 <= i5' /\ 0 <= ar_1 /\ 0 < i5' /\ 0 <= static''' /\ i5' < ar_0 /\ i8' <= o8' /\ o8' < ar_0 /\ 0 < o8' /\ 0 <= i8' /\ static''' <= ar_1 + 2 /\ i8' - 1 = i10' /\ static'1 <= static''' + 1 ]
(Comp: 6*ar_0, Cost: 13) reverse_Load_632(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(o183', ar_1 + 1, ar_2, ar_3, arityPad)) [ 0 <= ar_1 /\ 0 < ar_0 /\ 0 < o182''' /\ 0 < ar_2 /\ 0 <= o183' /\ 1 <= ar_3 /\ o182''' <= ar_0 + ar_1 /\ o183' + 1 = ar_0 /\ o182''' = ar_0 + ar_1 - o183' ]
(Comp: 1, Cost: 8) createList_LE_536(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(ar_1, 0, ar_2, ar_4, arityPad)) [ 0 < ar_2 /\ 0 < ar_1 /\ 0 <= ar_3 /\ 1 <= ar_4 /\ ar_0 = 0 ]
(Comp: 1, Cost: 8) createList_LE_100(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(reverse_Load_632(0, 0, ar_1, ar_2, arityPad)) [ -1 <= ar_0 /\ 0 < ar_1 /\ ar_0 <= 0 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 168*ar_0 + 46

Time: 0.338 sec (SMT: 0.314 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(46)) 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) LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(46)) transformation)

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

(43) koat Proof (EQUIVALENT transformation)

(44) BOUNDS(CONSTANT, 46 + 168 * |args|)