time complexity proof of /tmp/tmpqp_6qJ/AProVE12-cyclic-Length.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(47 + 28 * #0, 47)).

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)), 4 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 31 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), 0 ms)

        ↳16 WeightedIntTrs

        ↳17 CESProof (⇔, 275 ms)

        ↳18 BOUNDS(CONSTANT, max(42 + 28 * #0, 42))

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 133 ms)

    ↳20 WeightedIntTrs

        ↳21 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 43 ms)

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

↳31 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)), 3 ms)

↳32 JBCComplexityEdges

    ↳33 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 98 ms)

    ↳34 WeightedIntTrs

    ↳35 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 68 ms)

    ↳36 WeightedIntTrs

    ↳37 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 46 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

(0) Obligation:

Need to prove time_complexity of the following program:

public class List1 {
	List1 pred, next;

	List1(List1 pred) {
		if (pred != null) {
			pred.next = this;
		}
		this.pred = pred;
	}

	static int length(List1 l) {
		int r = 1;
		while (null != (l = l.next))
			r++;
		return r;
	}

	public static void main(int length) {
		List1 cur = new List1(null);
		List1 first = cur;
		while (length-- > 0) {
			cur = new List1(cur);
		}

		length(first);
	}
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:
- List1: [next]

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 91 jbc graph edges to a weighted ITS with 91 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 91 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_1(i1, env, static) -{0,0}> main_New_3(i1, env, static) :|: 0 >= 0
main_New_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_42(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, env, static) -{1,1}> main_New_51(i1, env, static) :|: 0 >= 0
main_New_51(i1, env, static) -{0,0}> main_New_52(i1, env, static) :|: 0 >= 0
main_New_52(i1, env, static) -{0,0}> main_New_54(i1, env, static) :|: 0 <= static
main_New_54(i1, env, static) -{0,0}> main_New_56(i1, env, static) :|: 0 >= 0
main_New_56(i1, env, static) -{0,0}> main_New_57(i1, env, static) :|: 0 >= 0
main_New_57(i1, env, static) -{1,1}> main_Duplicate_59(i1, o4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
main_Duplicate_59(i1, o4, NULL, env, static) -{1,1}> main_ConstantStackPush_60(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_ConstantStackPush_60(i1, o4, NULL, env, static) -{1,1}> main_InvokeMethod_61(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_61(i1, o4, NULL, env, static) -{1,1}> langle_init_rangle_Load_62(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_62(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_63(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_66(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_66(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_NULL_68(NULL, o4, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_NULL_68(NULL, o4, i1, env, static) -{1,1}> langle_init_rangle_Load_70(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_70(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_71(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_71(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_FieldAccess_72(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_72(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Return_73(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Return_73(i1, o4, NULL, env, static) -{1,1}> main_Store_75(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_75(i1, o4, NULL, env, static) -{1,1}> main_Load_77(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_77(i1, o4, NULL, env, static) -{1,1}> main_Store_78(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_78(i1, o4, NULL, env, static) -{1,1}> main_Load_79(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_79(i1, o4, NULL, env, static) -{0,0}> main_Load_750(i1, i1, o4, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_750(i77, i78, o129, o131, NULL, env, static) -{0,0}> main_Load_972(i77, i78, o129, o131, NULL, env, static) :|: NULL = 0 && 0 < o131 && 0 < o129
main_Load_972(i77, i102, o248, o250, NULL, env, static) -{1,1}> main_Inc_975(i77, i102, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250
main_Inc_975(i77, i102, o248, o250, NULL, env, static) -{1,1}> main_LE_980(i77, i102, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && i102 + -1 = i109
main_LE_980(i77, i116, i117, o248, o250, NULL, env, static) -{0,0}> main_LE_982(i77, i116, i117, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && i116 <= 0 && 0 < o250 && i117 <= -1
main_LE_980(i77, i118, i109, o248, o250, NULL, env, static) -{0,0}> main_LE_983(i77, i118, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 1 <= i118
main_LE_982(i77, i116, i117, o248, o250, NULL, env, static) -{1,1}> main_Load_985(i77, o250, env, static) :|: 0 < o248 && NULL = 0 && i116 <= 0 && 0 < o250 && i117 <= -1
main_LE_983(i77, i118, i109, o248, o250, NULL, env, static) -{1,1}> main_New_987(i77, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < i118 && 0 < o250 && 1 <= i118
main_Load_985(i77, o250, env, static) -{1,1}> main_InvokeMethod_988(i77, o250, env, static) :|: 0 < o250
main_New_987(i77, i109, o248, o250, NULL, env, static) -{1,1}> main_Duplicate_990(i77, o260, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260 && o260 = 1
main_InvokeMethod_988(i77, o250, env, static) -{1,1}> length_ConstantStackPush_992(o250, i77, env, static) :|: 0 < o250
main_Duplicate_990(i77, o260, i109, o248, o250, NULL, env, static) -{1,1}> main_Load_993(i77, o260, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
length_ConstantStackPush_992(o250, i77, env, static) -{1,1}> length_Store_997(iconst_1, o250, i77, env, static) :|: 0 < o250 && iconst_1 = 1
main_Load_993(i77, o260, i109, o248, o250, NULL, env, static) -{1,1}> main_InvokeMethod_995(i77, o260, o248, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
main_InvokeMethod_995(i77, o260, o248, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_999(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
length_Store_997(iconst_1, o250, i77, env, static) -{1,1}> length_ConstantStackPush_1000(o250, iconst_1, i77, env, static) :|: 0 < o250 && iconst_1 = 1
langle_init_rangle_Load_999(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1010(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
length_ConstantStackPush_1000(o250, iconst_1, i77, env, static) -{0,0}> length_ConstantStackPush_1136(o250, iconst_1, i77, env, static) :|: 0 < o250 && 1 <= iconst_1 && iconst_1 = 1 && iconst_1 <= 3
langle_init_rangle_InvokeMethod_1010(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1017(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1017(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_NULL_1023(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_NULL_1023(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1026(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1026(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1040(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1040(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1045(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1046(o281, o260, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o250 && 0 < o260 && 0 < o281
langle_init_rangle_FieldAccess_1045(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1049(o260, o248', i77, i109, o250', NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o250' && o248' = o248 + o260 && o248' <= o248 + o260 && 0 < o248' && 0 < o260 && o250' <= o250 + o260
langle_init_rangle_FieldAccess_1046(o285, o260, i77, i109, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1050(o285, o260, i77, i109, o286, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 <= o286 && 0 < o260 && 1 + o286 = o285
langle_init_rangle_Load_1049(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1065(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1050(o285, o260, i77, i109, o286, NULL, env, static) -{1,1}> langle_init_rangle_Load_1066(o260, o285', i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285' && 0 < o285 && o285' = o285 + o260 + -1 * o286 && 0 <= o286 && 0 < o260 && o285' <= o285 + o260
langle_init_rangle_Load_1065(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1069(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1066(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_Load_1070(o260, o285, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_FieldAccess_1069(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Return_1074(i77, o260, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1070(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1076(o260, o285, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1074(i77, o260, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_Return_1097(i77, o260, i109, o250, NULL, env, static) :|: NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1076(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_Return_1096(i77, o260, i109, o285, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1096(i77, o260, i109, o285, NULL, env, static) -{0,0}> langle_init_rangle_Return_1097(i77, o260, i109, o285, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1097(i77, o328, i109, o327, NULL, env, static) -{1,1}> main_Store_1101(i77, o328, i109, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_Store_1101(i77, o328, i109, o327, NULL, env, static) -{1,1}> main_JMP_1103(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_JMP_1103(i77, i109, o328, o327, NULL, env, static) -{1,1}> main_Load_1114(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_Load_1114(i77, i109, o328, o327, NULL, env, static) -{0,0}> main_Load_972(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
length_ConstantStackPush_1136(o351, i127, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o351, i127, i77, env, static) :|: 1 <= i127 && i127 <= 3 && 0 < o351
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{1,1}> length_Load_1159(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_Load_1159(NULL, o362, i130, i77, env, static) -{1,1}> length_FieldAccess_1160(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_FieldAccess_1160(NULL, o367, i130, i77, env, static) -{0,0}> length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 1 + o369 = o367 && 0 < o367
length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) -{1,1}> length_Duplicate_1164(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 0 < o367
length_Duplicate_1164(NULL, o369, i130, i77, env, static) -{1,1}> length_Store_1166(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_Store_1166(NULL, o369, i130, i77, env, static) -{1,1}> length_EQ_1167(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_EQ_1167(NULL, o370, i130, i77, env, static) -{0,0}> length_EQ_1169(NULL, o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o370 && 0 < o370
length_EQ_1167(NULL, NULL, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL
length_EQ_1169(NULL, o370, i130, i77, env, static) -{1,1}> length_Inc_1171(o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o370
length_Inc_1171(o370, i130, i77, env, static) -{1,1}> length_JMP_1175(o370, i132, i77, env, static) :|: 1 <= i130 && i130 + 1 = i132 && 2 <= i132 && 0 < o370
length_JMP_1175(o370, i132, i77, env, static) -{1,1}> length_ConstantStackPush_1178(o370, i132, i77, env, static) :|: 2 <= i132 && 0 < o370
length_ConstantStackPush_1178(o370, i132, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o370, i132, i77, env, static) :|: 1 <= i132 && 2 <= i132 && 0 < o370

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

obtained
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
main_New_1(i1, env, static) -{0,0}> main_New_3(i1, env, static) :|: 0 >= 0
main_New_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_42(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, env, static) -{1,1}> main_New_51(i1, env, static) :|: 0 >= 0
main_New_51(i1, env, static) -{0,0}> main_New_52(i1, env, static) :|: 0 >= 0
main_New_52(i1, env, static) -{0,0}> main_New_54(i1, env, static) :|: 0 <= static
main_New_54(i1, env, static) -{0,0}> main_New_56(i1, env, static) :|: 0 >= 0
main_New_56(i1, env, static) -{0,0}> main_New_57(i1, env, static) :|: 0 >= 0
main_New_57(i1, env, static) -{1,1}> main_Duplicate_59(i1, o4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
main_Duplicate_59(i1, o4, NULL, env, static) -{1,1}> main_ConstantStackPush_60(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_ConstantStackPush_60(i1, o4, NULL, env, static) -{1,1}> main_InvokeMethod_61(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_61(i1, o4, NULL, env, static) -{1,1}> langle_init_rangle_Load_62(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_62(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_63(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_66(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_66(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_NULL_68(NULL, o4, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_NULL_68(NULL, o4, i1, env, static) -{1,1}> langle_init_rangle_Load_70(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_70(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_71(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_71(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_FieldAccess_72(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_72(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Return_73(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Return_73(i1, o4, NULL, env, static) -{1,1}> main_Store_75(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_75(i1, o4, NULL, env, static) -{1,1}> main_Load_77(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_77(i1, o4, NULL, env, static) -{1,1}> main_Store_78(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_78(i1, o4, NULL, env, static) -{1,1}> main_Load_79(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_79(i1, o4, NULL, env, static) -{0,0}> main_Load_750(i1, i1, o4, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_750(i77, i78, o129, o131, NULL, env, static) -{0,0}> main_Load_972(i77, i78, o129, o131, NULL, env, static) :|: NULL = 0 && 0 < o131 && 0 < o129

obtained
main_Load_972(i77, i102, o248, o250, 0, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
by chaining
main_Load_972(i77, i102, o248, o250, NULL, env, static) -{1,1}> main_Inc_975(i77, i102, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250
main_Inc_975(i77, i102, o248, o250, NULL, env, static) -{1,1}> main_LE_980(i77, i102, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && i102 + -1 = i109

obtained
main_LE_980(i77, i118, i109, o248, o250, 0, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
by chaining
main_LE_980(i77, i118, i109, o248, o250, NULL, env, static) -{0,0}> main_LE_983(i77, i118, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 1 <= i118
main_LE_983(i77, i118, i109, o248, o250, NULL, env, static) -{1,1}> main_New_987(i77, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < i118 && 0 < o250 && 1 <= i118
main_New_987(i77, i109, o248, o250, NULL, env, static) -{1,1}> main_Duplicate_990(i77, o260, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260 && o260 = 1
main_Duplicate_990(i77, o260, i109, o248, o250, NULL, env, static) -{1,1}> main_Load_993(i77, o260, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
main_Load_993(i77, o260, i109, o248, o250, NULL, env, static) -{1,1}> main_InvokeMethod_995(i77, o260, o248, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
main_InvokeMethod_995(i77, o260, o248, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_999(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_999(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1010(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_InvokeMethod_1010(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1017(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1017(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_NULL_1023(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_NULL_1023(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1026(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1026(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1040(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1040(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260

obtained
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
by chaining
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1046(o281, o260, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o250 && 0 < o260 && 0 < o281
langle_init_rangle_FieldAccess_1046(o285, o260, i77, i109, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1050(o285, o260, i77, i109, o286, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 <= o286 && 0 < o260 && 1 + o286 = o285
langle_init_rangle_FieldAccess_1050(o285, o260, i77, i109, o286, NULL, env, static) -{1,1}> langle_init_rangle_Load_1066(o260, o285', i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285' && 0 < o285 && o285' = o285 + o260 + -1 * o286 && 0 <= o286 && 0 < o260 && o285' <= o285 + o260
langle_init_rangle_Load_1066(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_Load_1070(o260, o285, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Load_1070(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1076(o260, o285, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_FieldAccess_1076(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_Return_1096(i77, o260, i109, o285, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1096(i77, o260, i109, o285, NULL, env, static) -{0,0}> langle_init_rangle_Return_1097(i77, o260, i109, o285, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260

obtained
langle_init_rangle_Return_1097(i77, o328, i109, o327, 0, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328
by chaining
langle_init_rangle_Return_1097(i77, o328, i109, o327, NULL, env, static) -{1,1}> main_Store_1101(i77, o328, i109, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_Store_1101(i77, o328, i109, o327, NULL, env, static) -{1,1}> main_JMP_1103(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_JMP_1103(i77, i109, o328, o327, NULL, env, static) -{1,1}> main_Load_1114(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_Load_1114(i77, i109, o328, o327, NULL, env, static) -{0,0}> main_Load_972(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327

obtained
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
by chaining
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1045(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1045(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1049(o260, o248', i77, i109, o250', NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o250' && o248' = o248 + o260 && o248' <= o248 + o260 && 0 < o248' && 0 < o260 && o250' <= o250 + o260
langle_init_rangle_Load_1049(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1065(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1065(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1069(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1069(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Return_1074(i77, o260, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Return_1074(i77, o260, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_Return_1097(i77, o260, i109, o250, NULL, env, static) :|: NULL = 0 && 0 < o250 && 0 < o260

obtained
main_LE_980(i77, i116, i117, o248, o250, 0, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
by chaining
main_LE_980(i77, i116, i117, o248, o250, NULL, env, static) -{0,0}> main_LE_982(i77, i116, i117, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && i116 <= 0 && 0 < o250 && i117 <= -1
main_LE_982(i77, i116, i117, o248, o250, NULL, env, static) -{1,1}> main_Load_985(i77, o250, env, static) :|: 0 < o248 && NULL = 0 && i116 <= 0 && 0 < o250 && i117 <= -1
main_Load_985(i77, o250, env, static) -{1,1}> main_InvokeMethod_988(i77, o250, env, static) :|: 0 < o250
main_InvokeMethod_988(i77, o250, env, static) -{1,1}> length_ConstantStackPush_992(o250, i77, env, static) :|: 0 < o250
length_ConstantStackPush_992(o250, i77, env, static) -{1,1}> length_Store_997(iconst_1, o250, i77, env, static) :|: 0 < o250 && iconst_1 = 1
length_Store_997(iconst_1, o250, i77, env, static) -{1,1}> length_ConstantStackPush_1000(o250, iconst_1, i77, env, static) :|: 0 < o250 && iconst_1 = 1
length_ConstantStackPush_1000(o250, iconst_1, i77, env, static) -{0,0}> length_ConstantStackPush_1136(o250, iconst_1, i77, env, static) :|: 0 < o250 && 1 <= iconst_1 && iconst_1 = 1 && iconst_1 <= 3
length_ConstantStackPush_1136(o351, i127, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o351, i127, i77, env, static) :|: 1 <= i127 && i127 <= 3 && 0 < o351

obtained
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
by chaining
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{1,1}> length_Load_1159(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_Load_1159(NULL, o362, i130, i77, env, static) -{1,1}> length_FieldAccess_1160(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_FieldAccess_1160(NULL, o367, i130, i77, env, static) -{0,0}> length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 1 + o369 = o367 && 0 < o367
length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) -{1,1}> length_Duplicate_1164(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 0 < o367
length_Duplicate_1164(NULL, o369, i130, i77, env, static) -{1,1}> length_Store_1166(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_Store_1166(NULL, o369, i130, i77, env, static) -{1,1}> length_EQ_1167(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369

obtained
length_EQ_1167(0, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132'
by chaining
length_EQ_1167(NULL, o370, i130, i77, env, static) -{0,0}> length_EQ_1169(NULL, o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o370 && 0 < o370
length_EQ_1169(NULL, o370, i130, i77, env, static) -{1,1}> length_Inc_1171(o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o370
length_Inc_1171(o370, i130, i77, env, static) -{1,1}> length_JMP_1175(o370, i132, i77, env, static) :|: 1 <= i130 && i130 + 1 = i132 && 2 <= i132 && 0 < o370
length_JMP_1175(o370, i132, i77, env, static) -{1,1}> length_ConstantStackPush_1178(o370, i132, i77, env, static) :|: 2 <= i132 && 0 < o370
length_ConstantStackPush_1178(o370, i132, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o370, i132, i77, env, static) :|: 1 <= i132 && 2 <= i132 && 0 < o370

(8) Obligation:

IntTrs with 10 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_Load_972(i77, i102, o248, o250, 0, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
main_LE_980(i77, i118, i109, o248, o250, 0, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
langle_init_rangle_Return_1097(i77, o328, i109, o327, 0, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
main_LE_980(i77, i116, i117, o248, o250, 0, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
length_EQ_1167(NULL, NULL, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL
length_EQ_1167(0, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132'

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

Moved arithmethic from lhss to constraints.

main_LE_980(i77, i118, i109, o248, o250, 0, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
was transformed to
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0

langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
was transformed to
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260 && x = 0

main_Load_972(i77, i102, o248, o250, 0, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
was transformed to
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0

main_LE_980(i77, i116, i117, o248, o250, 0, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
was transformed to
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0

langle_init_rangle_Return_1097(i77, o328, i109, o327, 0, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328
was transformed to
langle_init_rangle_Return_1097(i77, o328, i109, o327, x, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328 && x = 0

langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
was transformed to
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0

length_EQ_1167(0, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132'
was transformed to
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0

(10) Obligation:

IntTrs with 10 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260 && x = 0
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
length_EQ_1167(NULL, NULL, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0
langle_init_rangle_Return_1097(i77, o328, i109, o327, x, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328 && x = 0
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0

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

Linearized lhss.

length_EQ_1167(NULL, NULL, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL
was transformed to
length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL

(12) Obligation:

IntTrs with 10 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0
length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
langle_init_rangle_Return_1097(i77, o328, i109, o327, x, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328 && x = 0
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260 && x = 0
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0

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

Moved arithmethic from constraints to rhss.

length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(NULL, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL
was transformed to
length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(0, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL

langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
was transformed to
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, 1 + o286' + o260 + -1 * o286', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0

length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i132', i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0
was transformed to
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i130 + 1, i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0

main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0
was transformed to
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i102 + -1, o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0

(14) Obligation:

IntTrs with 10 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(0, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, 1 + o286' + o260 + -1 * o286', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i130 + 1, i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
langle_init_rangle_Return_1097(i77, o328, i109, o327, x, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328 && x = 0
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260 && x = 0
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i102 + -1, o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0

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

Simplified expressions.

main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i102 + -1, o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248 && x = 0
was transformed to
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i102 - 1, o248, o250, 0, env, static) :|: 0 < o250 && i102 - 1 = i109' && 0 < o248 && x = 0

langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, 1 + o286' + o260 + -1 * o286', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
was transformed to
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, 1 + o260, 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0

length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i130 + 1, i77, env, static) :|: 1 <= i130 && 0 < o370 && 0 <= o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0
was transformed to
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i130 + 1, i77, env, static) :|: 1 <= i130 && 0 < o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0

main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0
was transformed to
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0

main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0
was transformed to
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 0 < o250 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0

main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260 && x = 0
was transformed to
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' = o248 + o260 && x = 0

(16) Obligation:

IntTrs with 10 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 0 < o250 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0
length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(0, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i130 + 1, i77, env, static) :|: 1 <= i130 && 0 < o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i102 - 1, o248, o250, 0, env, static) :|: 0 < o250 && i102 - 1 = i109' && 0 < o248 && x = 0
langle_init_rangle_Return_1097(i77, o328, i109, o327, x, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328 && x = 0
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, 1 + o260, 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' = o248 + o260 && x = 0

(17) CESProof (EQUIVALENT transformation)

proved upper bound max(42 + 28 * #0, 42) using cofloco

(18) BOUNDS(CONSTANT, max(42 + 28 * #0, 42))

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

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

(20) Obligation:

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

(22) Obligation:

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

Moved arithmethic from lhss to constraints.

(24) Obligation:

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

Linearized lhss.

(26) Obligation:

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

Moved arithmethic from constraints to rhss.

(28) Obligation:

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

Simplified expressions.

(30) Obligation:

IntTrs with 10 rules
Start term: main_New_1(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_980(i77, i118, i109, o248, o250, x, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < o250 && 0 < o248 && 0 < i118 && x = 0
main_LE_980(i77, i116, i117, o248, o250, x, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 0 < o250 && i117 <= -1 && i116 <= 0 && 0 < o248 && x = 0
length_EQ_1167(NULL, x, i130, i77, env, static) -{0,0}> length_EQ_1170(0, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= NULL && x = NULL
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{5,5}> length_EQ_1167(0, o369', i130, i77, env, static) :|: 0 < o362 && 0 <= o369' && 1 + o369' = o362 && 1 <= i130
length_EQ_1167(x, o370, i130, i77, env, static) -{3,3}> length_ConstantStackPush_1156(o370, i130 + 1, i77, env, static) :|: 1 <= i130 && 0 < o370 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && x = 0
main_Load_972(i77, i102, o248, o250, x, env, static) -{2,2}> main_LE_980(i77, i102, i102 - 1, o248, o250, 0, env, static) :|: 0 < o250 && i102 - 1 = i109' && 0 < o248 && x = 0
langle_init_rangle_Return_1097(i77, o328, i109, o327, x, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328 && x = 0
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, 1 + o260, 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286' && x = 0
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, x, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' = o248 + o260 && x = 0

(31) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

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

(32) Obligation:

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

Used field analysis yielded the following read fields:
- List1: [next]

Considered paths: all paths from start

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

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

(34) Obligation:

IntTrs with 90 rules
Start term: main_New_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_New_1(i1, env, static) -{0,0}> main_New_3(i1, env, static) :|: 0 >= 0
main_New_3(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_15(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_42(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_45(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i1, env, static) -{1,1}> main_New_51(i1, env, static) :|: 0 >= 0
main_New_51(i1, env, static) -{0,0}> main_New_52(i1, env, static) :|: 0 >= 0
main_New_52(i1, env, static) -{0,0}> main_New_54(i1, env, static) :|: 0 <= static
main_New_54(i1, env, static) -{0,0}> main_New_56(i1, env, static) :|: 0 >= 0
main_New_56(i1, env, static) -{0,0}> main_New_57(i1, env, static) :|: 0 >= 0
main_New_57(i1, env, static) -{1,1}> main_Duplicate_59(i1, o4, NULL, env, static) :|: NULL = 0 && o4 = 1 && 0 < o4
main_Duplicate_59(i1, o4, NULL, env, static) -{1,1}> main_ConstantStackPush_60(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_ConstantStackPush_60(i1, o4, NULL, env, static) -{1,1}> main_InvokeMethod_61(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_InvokeMethod_61(i1, o4, NULL, env, static) -{1,1}> langle_init_rangle_Load_62(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_62(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_63(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_InvokeMethod_63(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_66(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_66(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_NULL_68(NULL, o4, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_NULL_68(NULL, o4, i1, env, static) -{1,1}> langle_init_rangle_Load_70(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_70(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_71(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Load_71(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_FieldAccess_72(o4, NULL, i1, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_FieldAccess_72(o4, NULL, i1, env, static) -{1,1}> langle_init_rangle_Return_73(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
langle_init_rangle_Return_73(i1, o4, NULL, env, static) -{1,1}> main_Store_75(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_75(i1, o4, NULL, env, static) -{1,1}> main_Load_77(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_77(i1, o4, NULL, env, static) -{1,1}> main_Store_78(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Store_78(i1, o4, NULL, env, static) -{1,1}> main_Load_79(i1, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_79(i1, o4, NULL, env, static) -{0,0}> main_Load_750(i1, i1, o4, o4, NULL, env, static) :|: NULL = 0 && 0 < o4
main_Load_750(i77, i78, o129, o131, NULL, env, static) -{0,0}> main_Load_972(i77, i78, o129, o131, NULL, env, static) :|: NULL = 0 && 0 < o131 && 0 < o129
main_Load_972(i77, i102, o248, o250, NULL, env, static) -{1,1}> main_Inc_975(i77, i102, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250
main_Inc_975(i77, i102, o248, o250, NULL, env, static) -{1,1}> main_LE_980(i77, i102, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && i102 + -1 = i109
main_LE_980(i77, i116, i117, o248, o250, NULL, env, static) -{0,0}> main_LE_982(i77, i116, i117, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && i116 <= 0 && 0 < o250 && i117 <= -1
main_LE_980(i77, i118, i109, o248, o250, NULL, env, static) -{0,0}> main_LE_983(i77, i118, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 1 <= i118
main_LE_982(i77, i116, i117, o248, o250, NULL, env, static) -{1,1}> main_Load_985(i77, o250, env, static) :|: 0 < o248 && NULL = 0 && i116 <= 0 && 0 < o250 && i117 <= -1
main_LE_983(i77, i118, i109, o248, o250, NULL, env, static) -{1,1}> main_New_987(i77, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < i118 && 0 < o250 && 1 <= i118
main_Load_985(i77, o250, env, static) -{1,1}> main_InvokeMethod_988(i77, o250, env, static) :|: 0 < o250
main_New_987(i77, i109, o248, o250, NULL, env, static) -{1,1}> main_Duplicate_990(i77, o260, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260 && o260 = 1
main_InvokeMethod_988(i77, o250, env, static) -{1,1}> length_ConstantStackPush_992(o250, i77, env, static) :|: 0 < o250
main_Duplicate_990(i77, o260, i109, o248, o250, NULL, env, static) -{1,1}> main_Load_993(i77, o260, i109, o248, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
length_ConstantStackPush_992(o250, i77, env, static) -{1,1}> length_Store_997(iconst_1, o250, i77, env, static) :|: 0 < o250 && iconst_1 = 1
main_Load_993(i77, o260, i109, o248, o250, NULL, env, static) -{1,1}> main_InvokeMethod_995(i77, o260, o248, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
main_InvokeMethod_995(i77, o260, o248, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_999(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
length_Store_997(iconst_1, o250, i77, env, static) -{1,1}> length_ConstantStackPush_1000(o250, iconst_1, i77, env, static) :|: 0 < o250 && iconst_1 = 1
langle_init_rangle_Load_999(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_InvokeMethod_1010(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
length_ConstantStackPush_1000(o250, iconst_1, i77, env, static) -{0,0}> length_ConstantStackPush_1136(o250, iconst_1, i77, env, static) :|: 0 < o250 && 1 <= iconst_1 && iconst_1 = 1 && iconst_1 <= 3
langle_init_rangle_InvokeMethod_1010(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1017(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1017(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_NULL_1023(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_NULL_1023(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1026(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1026(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1040(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1040(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1045(o248, o260, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1046(o281, o260, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o250 && 0 < o260 && 0 < o281
langle_init_rangle_FieldAccess_1045(o248, o260, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1049(o260, o248', i77, i109, o250', NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o250' && o248' = o248 + o260 && o248' <= o248 + o260 && 0 < o248' && 0 < o260 && o250' <= o250 + o260
langle_init_rangle_FieldAccess_1046(o285, o260, i77, i109, NULL, env, static) -{0,0}> langle_init_rangle_FieldAccess_1050(o285, o260, i77, i109, o286, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 <= o286 && 0 < o260 && 1 + o286 = o285
langle_init_rangle_Load_1049(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Load_1065(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1050(o285, o260, i77, i109, o286, NULL, env, static) -{1,1}> langle_init_rangle_Load_1066(o260, o285', i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285' && 0 < o285 && o285' = o285 + o260 + -1 * o286 && 0 <= o286 && 0 < o260 && o285' <= o285 + o260
langle_init_rangle_Load_1065(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1069(o260, o248, i77, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1066(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_Load_1070(o260, o285, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_FieldAccess_1069(o260, o248, i77, i109, o250, NULL, env, static) -{1,1}> langle_init_rangle_Return_1074(i77, o260, i109, o250, NULL, env, static) :|: 0 < o248 && NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_Load_1070(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_FieldAccess_1076(o260, o285, i77, i109, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1074(i77, o260, i109, o250, NULL, env, static) -{0,0}> langle_init_rangle_Return_1097(i77, o260, i109, o250, NULL, env, static) :|: NULL = 0 && 0 < o250 && 0 < o260
langle_init_rangle_FieldAccess_1076(o260, o285, i77, i109, NULL, env, static) -{1,1}> langle_init_rangle_Return_1096(i77, o260, i109, o285, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1096(i77, o260, i109, o285, NULL, env, static) -{0,0}> langle_init_rangle_Return_1097(i77, o260, i109, o285, NULL, env, static) :|: NULL = 0 && 0 < o285 && 0 < o260
langle_init_rangle_Return_1097(i77, o328, i109, o327, NULL, env, static) -{1,1}> main_Store_1101(i77, o328, i109, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_Store_1101(i77, o328, i109, o327, NULL, env, static) -{1,1}> main_JMP_1103(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_JMP_1103(i77, i109, o328, o327, NULL, env, static) -{1,1}> main_Load_1114(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
main_Load_1114(i77, i109, o328, o327, NULL, env, static) -{0,0}> main_Load_972(i77, i109, o328, o327, NULL, env, static) :|: NULL = 0 && 0 < o328 && 0 < o327
length_ConstantStackPush_1136(o351, i127, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o351, i127, i77, env, static) :|: 1 <= i127 && i127 <= 3 && 0 < o351
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{1,1}> length_Load_1159(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_Load_1159(NULL, o362, i130, i77, env, static) -{1,1}> length_FieldAccess_1160(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_FieldAccess_1160(NULL, o367, i130, i77, env, static) -{0,0}> length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 1 + o369 = o367 && 0 < o367
length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) -{1,1}> length_Duplicate_1164(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 0 < o367
length_Duplicate_1164(NULL, o369, i130, i77, env, static) -{1,1}> length_Store_1166(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_Store_1166(NULL, o369, i130, i77, env, static) -{1,1}> length_EQ_1167(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_EQ_1167(NULL, o370, i130, i77, env, static) -{0,0}> length_EQ_1169(NULL, o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o370 && 0 < o370
length_EQ_1169(NULL, o370, i130, i77, env, static) -{1,1}> length_Inc_1171(o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o370
length_Inc_1171(o370, i130, i77, env, static) -{1,1}> length_JMP_1175(o370, i132, i77, env, static) :|: 1 <= i130 && i130 + 1 = i132 && 2 <= i132 && 0 < o370
length_JMP_1175(o370, i132, i77, env, static) -{1,1}> length_ConstantStackPush_1178(o370, i132, i77, env, static) :|: 2 <= i132 && 0 < o370
length_ConstantStackPush_1178(o370, i132, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o370, i132, i77, env, static) :|: 1 <= i132 && 2 <= i132 && 0 < o370

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

obtained
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{8,8}> length_ConstantStackPush_1156(o369', i132', i77, env, static) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362
by chaining
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{1,1}> length_Load_1159(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_Load_1159(NULL, o362, i130, i77, env, static) -{1,1}> length_FieldAccess_1160(NULL, o362, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o362
length_FieldAccess_1160(NULL, o367, i130, i77, env, static) -{0,0}> length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 1 + o369 = o367 && 0 < o367
length_FieldAccess_1162(NULL, o367, i130, i77, o369, env, static) -{1,1}> length_Duplicate_1164(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369 && 0 < o367
length_Duplicate_1164(NULL, o369, i130, i77, env, static) -{1,1}> length_Store_1166(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_Store_1166(NULL, o369, i130, i77, env, static) -{1,1}> length_EQ_1167(NULL, o369, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o369
length_EQ_1167(NULL, o370, i130, i77, env, static) -{0,0}> length_EQ_1169(NULL, o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 <= o370 && 0 < o370
length_EQ_1169(NULL, o370, i130, i77, env, static) -{1,1}> length_Inc_1171(o370, i130, i77, env, static) :|: 1 <= i130 && NULL = 0 && 0 < o370
length_Inc_1171(o370, i130, i77, env, static) -{1,1}> length_JMP_1175(o370, i132, i77, env, static) :|: 1 <= i130 && i130 + 1 = i132 && 2 <= i132 && 0 < o370
length_JMP_1175(o370, i132, i77, env, static) -{1,1}> length_ConstantStackPush_1178(o370, i132, i77, env, static) :|: 2 <= i132 && 0 < o370
length_ConstantStackPush_1178(o370, i132, i77, env, static) -{0,0}> length_ConstantStackPush_1156(o370, i132, i77, env, static) :|: 1 <= i132 && 2 <= i132 && 0 < o370

(36) Obligation:

IntTrs with 8 rules
Start term: main_New_1(#0, env, static)
Considered paths: all paths from start
Rules:
main_New_1(i1, env, static) -{30,30}> main_Load_972(i1, i1, 1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_Load_972(i77, i102, o248, o250, 0, env, static) -{2,2}> main_LE_980(i77, i102, i109', o248, o250, 0, env, static) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
main_LE_980(i77, i118, i109, o248, o250, 0, env, static) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i77, i109, o250, 0, env, static) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
langle_init_rangle_FieldAccess_1042(o281, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o285''', 0, env, static) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
langle_init_rangle_Return_1097(i77, o328, i109, o327, 0, env, static) -{3,3}> main_Load_972(i77, i109, o328, o327, 0, env, static) :|: 0 < o327 && 0 < o328
langle_init_rangle_FieldAccess_1042(o248, o260, i77, i109, o250, 0, env, static) -{4,4}> langle_init_rangle_Return_1097(i77, o260, i109, o250''', 0, env, static) :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
main_LE_980(i77, i116, i117, o248, o250, 0, env, static) -{5,5}> length_ConstantStackPush_1156(o250, 1, i77, env, static) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
length_ConstantStackPush_1156(o362, i130, i77, env, static) -{8,8}> length_ConstantStackPush_1156(o369', i132', i77, env, static) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362

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

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

main_New_1(x1, x2, x3) → main_New_1(x1, x3)
main_Load_972(x1, x2, x3, x4, x5, x6, x7) → main_Load_972(x2, x3, x4)
main_LE_980(x1, x2, x3, x4, x5, x6, x7, x8) → main_LE_980(x2, x3, x4, x5)
langle_init_rangle_FieldAccess_1042(x1, x2, x3, x4, x5, x6, x7, x8) → langle_init_rangle_FieldAccess_1042(x1, x2, x4, x5)
langle_init_rangle_Return_1097(x1, x2, x3, x4, x5, x6, x7) → langle_init_rangle_Return_1097(x2, x3, x4)
length_ConstantStackPush_1156(x1, x2, x3, x4, x5) → length_ConstantStackPush_1156(x1, x2)

(38) Obligation:

IntTrs with 8 rules
Start term: main_New_1(#0, static)
Considered paths: all paths from start
Rules:
main_New_1(i1, static) -{30,30}> main_Load_972(i1, 1, 1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i109', o248, o250) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
main_LE_980(i118, i109, o248, o250) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i109, o250) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o285''') :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
langle_init_rangle_Return_1097(o328, i109, o327) -{3,3}> main_Load_972(i109, o328, o327) :|: 0 < o327 && 0 < o328
langle_init_rangle_FieldAccess_1042(o248, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o250''') :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
main_LE_980(i116, i117, o248, o250) -{5,5}> length_ConstantStackPush_1156(o250, 1) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i132') :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362

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

Moved arithmethic from constraints to rhss.

main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i109', o248, o250) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
was transformed to
main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i102 + -1, o248, o250) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248

length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i132') :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362
was transformed to
length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i130 + 1) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362

langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o285''') :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
was transformed to
langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, 1 + o286' + o260 + -1 * o286') :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'

(40) Obligation:

IntTrs with 8 rules
Start term: main_New_1(#0, static)
Considered paths: all paths from start
Rules:
main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i102 + -1, o248, o250) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i130 + 1) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362
main_New_1(i1, static) -{30,30}> main_Load_972(i1, 1, 1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_LE_980(i118, i109, o248, o250) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i109, o250) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
langle_init_rangle_FieldAccess_1042(o248, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o250''') :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, 1 + o286' + o260 + -1 * o286') :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
main_LE_980(i116, i117, o248, o250) -{5,5}> length_ConstantStackPush_1156(o250, 1) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
langle_init_rangle_Return_1097(o328, i109, o327) -{3,3}> main_Load_972(i109, o328, o327) :|: 0 < o327 && 0 < o328

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

Simplified expressions.

main_New_1(i1, static) -{30,30}> main_Load_972(i1, 1, 1) :|: static'1 <= static''' + 1 && 0 < 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_New_1(i1, static) -{30,30}> main_Load_972(i1, 1, 1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, 1 + o286' + o260 + -1 * o286') :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
was transformed to
langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, 1 + o260) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'

main_LE_980(i118, i109, o248, o250) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i109, o250) :|: 1 <= i118 && 0 < 1 && 0 < o250 && 0 < o248 && 0 < i118
was transformed to
main_LE_980(i118, i109, o248, o250) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i109, o250) :|: 1 <= i118 && 0 < o250 && 0 < o248 && 0 < i118

langle_init_rangle_FieldAccess_1042(o248, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o250''') :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' <= o248 + o260 && o248''' = o248 + o260
was transformed to
langle_init_rangle_FieldAccess_1042(o248, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o250''') :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' = o248 + o260

length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i130 + 1) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && 0 <= o369' && i130 + 1 = i132' && 0 < o362
was transformed to
length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i130 + 1) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && 0 < o362

main_LE_980(i116, i117, o248, o250) -{5,5}> length_ConstantStackPush_1156(o250, 1) :|: 1 <= 1 && 0 < o250 && 1 <= 3 && i117 <= -1 && i116 <= 0 && 0 < o248
was transformed to
main_LE_980(i116, i117, o248, o250) -{5,5}> length_ConstantStackPush_1156(o250, 1) :|: 0 < o250 && i117 <= -1 && i116 <= 0 && 0 < o248

main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i102 + -1, o248, o250) :|: 0 < o250 && i102 + -1 = i109' && 0 < o248
was transformed to
main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i102 - 1, o248, o250) :|: 0 < o250 && i102 - 1 = i109' && 0 < o248

(42) Obligation:

IntTrs with 8 rules
Start term: main_New_1(#0, static)
Considered paths: all paths from start
Rules:
langle_init_rangle_FieldAccess_1042(o281, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, 1 + o260) :|: o285''' <= o281 + o260 && 0 < o260 && 0 <= o286' && 0 < o285''' && 0 < o250 && 0 < o281 && 1 + o286' = o281 && o285''' = o281 + o260 + -1 * o286'
main_LE_980(i118, i109, o248, o250) -{11,11}> langle_init_rangle_FieldAccess_1042(o248, 1, i109, o250) :|: 1 <= i118 && 0 < o250 && 0 < o248 && 0 < i118
length_ConstantStackPush_1156(o362, i130) -{8,8}> length_ConstantStackPush_1156(o369', i130 + 1) :|: 1 + o369' = o362 && 0 < o369' && 1 <= i130 && 1 <= i132' && 2 <= i132' && i130 + 1 = i132' && 0 < o362
main_Load_972(i102, o248, o250) -{2,2}> main_LE_980(i102, i102 - 1, o248, o250) :|: 0 < o250 && i102 - 1 = i109' && 0 < o248
main_New_1(i1, static) -{30,30}> main_Load_972(i1, 1, 1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_980(i116, i117, o248, o250) -{5,5}> length_ConstantStackPush_1156(o250, 1) :|: 0 < o250 && i117 <= -1 && i116 <= 0 && 0 < o248
langle_init_rangle_FieldAccess_1042(o248, o260, i109, o250) -{4,4}> langle_init_rangle_Return_1097(o260, i109, o250''') :|: o250''' <= o250 + o260 && 0 < o260 && 0 < o250 && 0 < o250''' && 0 < o248 && 0 < o248''' && o248''' = o248 + o260
langle_init_rangle_Return_1097(o328, i109, o327) -{3,3}> main_Load_972(i109, o328, o327) :|: 0 < o327 && 0 < o328