time complexity proof of /tmp/tmpSuASZF/Sequence.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 2 + 1652 / 3).

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 0 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

        ↳15 CESProof (⇔, 120 ms)

        ↳16 BOUNDS(CONSTANT, 1652 / 3)

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

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

↳27 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 0 ms)

↳28 JBCComplexityEdges

    ↳29 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 107 ms)

    ↳30 WeightedIntTrs

    ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳32 WeightedIntTrs

    ↳33 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 42 ms)

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class Sequence {
    public static void main(String[] args) {
	for (int i = 0; i < 100; i++) {};

	for (int j = 5; j < 21; j += 3) {};
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

Transformed 55 jbc graph edges to a weighted ITS with 55 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 55 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(o2, env, static) -{0,0}> main_ConstantStackPush_4(o2, env, static) :|: 0 < o2
main_ConstantStackPush_4(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_14(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(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_19(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_19(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_24(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_26(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(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_ConstantStackPush_48(o2, env, static) :|: 0 < o2
main_ConstantStackPush_48(o2, env, static) -{0,0}> main_ConstantStackPush_49(o2, env, static) :|: 0 < o2
main_ConstantStackPush_49(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_100, env, static) :|: 0 < o2 && iconst_100 = 100 && iconst_0 = 0
main_GE_56(o2, iconst_0, iconst_100, env, static) -{1,1}> main_Inc_59(o2, iconst_0, env, static) :|: 0 < o2 && iconst_100 = 100 && iconst_0 = 0
main_Inc_59(o2, iconst_0, env, static) -{1,1}> main_JMP_61(o2, iconst_1, env, static) :|: 0 < o2 && iconst_1 = 1 && iconst_0 = 0
main_JMP_61(o2, iconst_1, env, static) -{1,1}> main_Load_69(o2, iconst_1, env, static) :|: 0 < o2 && iconst_1 = 1
main_Load_69(o2, iconst_1, env, static) -{0,0}> main_Load_103(o2, iconst_1, env, static) :|: iconst_1 <= 2 && 0 < o2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_103(o20, i1, env, static) -{0,0}> main_Load_126(o20, i1, env, static) :|: 0 < o20 && 1 <= i1 && i1 <= 2 && i1 <= 3
main_Load_126(o44, i6, env, static) -{0,0}> main_Load_147(o44, i6, env, static) :|: 0 < o44 && 1 <= i6 && i6 <= 3
main_Load_147(o66, i10, env, static) -{1,1}> main_ConstantStackPush_148(o66, i10, env, static) :|: 1 <= i10 && 0 < o66
main_ConstantStackPush_148(o66, i10, env, static) -{1,1}> main_GE_154(o66, i10, iconst_100, env, static) :|: 1 <= i10 && iconst_100 = 100 && 0 < o66
main_GE_154(o66, i16, iconst_100, env, static) -{0,0}> main_GE_157(o66, i16, iconst_100, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && 0 < o66
main_GE_154(o66, i17, iconst_100, env, static) -{0,0}> main_GE_158(o66, i17, iconst_100, env, static) :|: iconst_100 = 100 && 1 <= i17 && 0 < o66 && 100 <= i17
main_GE_157(o66, i16, iconst_100, env, static) -{1,1}> main_Inc_162(o66, i16, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && 0 < o66 && i16 < iconst_100
main_GE_158(o66, i17, iconst_100, env, static) -{1,1}> main_ConstantStackPush_168(o66, env, static) :|: iconst_100 <= i17 && iconst_100 = 100 && 0 < o66 && 100 <= i17
main_Inc_162(o66, i16, env, static) -{1,1}> main_JMP_169(o66, i18, env, static) :|: i16 + 1 = i18 && 1 <= i16 && i16 <= 99 && 0 < o66 && 2 <= i18 && i18 <= 100
main_ConstantStackPush_168(o66, env, static) -{1,1}> main_Store_170(o66, iconst_5, env, static) :|: iconst_5 = 5 && 0 < o66
main_JMP_169(o66, i18, env, static) -{1,1}> main_Load_171(o66, i18, env, static) :|: 0 < o66 && 2 <= i18 && i18 <= 100
main_Store_170(o66, iconst_5, env, static) -{1,1}> main_Load_173(o66, iconst_5, env, static) :|: iconst_5 = 5 && 0 < o66
main_Load_171(o66, i18, env, static) -{0,0}> main_Load_147(o66, i18, env, static) :|: 1 <= i18 && 0 < o66 && 2 <= i18 && i18 <= 100
main_Load_173(o66, iconst_5, env, static) -{0,0}> main_Load_212(o66, iconst_5, env, static) :|: iconst_5 <= 11 && iconst_5 = 5 && 0 < o66 && 5 <= iconst_5
main_Load_212(o102, i20, env, static) -{0,0}> main_Load_229(o102, i20, env, static) :|: i20 <= 14 && 5 <= i20 && i20 <= 11 && 0 < o102
main_Load_229(o114, i25, env, static) -{0,0}> main_Load_245(o114, i25, env, static) :|: 0 < o114 && i25 <= 14 && 5 <= i25
main_Load_245(o122, i28, env, static) -{1,1}> main_ConstantStackPush_246(o122, i28, env, static) :|: 0 < o122
main_ConstantStackPush_246(o122, i28, env, static) -{1,1}> main_GE_247(o122, i28, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122
main_GE_247(o122, i34, iconst_21, env, static) -{0,0}> main_GE_250(o122, i34, iconst_21, env, static) :|: i34 <= 20 && iconst_21 = 21 && 0 < o122
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35
main_GE_250(o122, i34, iconst_21, env, static) -{1,1}> main_Inc_255(o122, i34, env, static) :|: i34 <= 20 && i34 < iconst_21 && iconst_21 = 21 && 0 < o122
main_Inc_255(o122, i34, env, static) -{1,1}> main_JMP_262(o122, i36, env, static) :|: i34 <= 20 && i36 <= 23 && i34 + 3 = i36 && 0 < o122
main_JMP_262(o122, i36, env, static) -{1,1}> main_Load_267(o122, i36, env, static) :|: i36 <= 23 && 0 < o122
main_Load_267(o122, i36, env, static) -{0,0}> main_Load_245(o122, i36, env, static) :|: i36 <= 23 && 0 < o122

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

obtained
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
by chaining
main_ConstantStackPush_1(o2, env, static) -{0,0}> main_ConstantStackPush_4(o2, env, static) :|: 0 < o2
main_ConstantStackPush_4(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_14(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(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_19(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_19(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_24(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_26(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(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_ConstantStackPush_48(o2, env, static) :|: 0 < o2
main_ConstantStackPush_48(o2, env, static) -{0,0}> main_ConstantStackPush_49(o2, env, static) :|: 0 < o2
main_ConstantStackPush_49(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_100, env, static) :|: 0 < o2 && iconst_100 = 100 && iconst_0 = 0
main_GE_56(o2, iconst_0, iconst_100, env, static) -{1,1}> main_Inc_59(o2, iconst_0, env, static) :|: 0 < o2 && iconst_100 = 100 && iconst_0 = 0
main_Inc_59(o2, iconst_0, env, static) -{1,1}> main_JMP_61(o2, iconst_1, env, static) :|: 0 < o2 && iconst_1 = 1 && iconst_0 = 0
main_JMP_61(o2, iconst_1, env, static) -{1,1}> main_Load_69(o2, iconst_1, env, static) :|: 0 < o2 && iconst_1 = 1
main_Load_69(o2, iconst_1, env, static) -{0,0}> main_Load_103(o2, iconst_1, env, static) :|: iconst_1 <= 2 && 0 < o2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_103(o20, i1, env, static) -{0,0}> main_Load_126(o20, i1, env, static) :|: 0 < o20 && 1 <= i1 && i1 <= 2 && i1 <= 3
main_Load_126(o44, i6, env, static) -{0,0}> main_Load_147(o44, i6, env, static) :|: 0 < o44 && 1 <= i6 && i6 <= 3

obtained
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
by chaining
main_Load_147(o66, i10, env, static) -{1,1}> main_ConstantStackPush_148(o66, i10, env, static) :|: 1 <= i10 && 0 < o66
main_ConstantStackPush_148(o66, i10, env, static) -{1,1}> main_GE_154(o66, i10, iconst_100, env, static) :|: 1 <= i10 && iconst_100 = 100 && 0 < o66

obtained
main_GE_154(o66, i17, 100, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
by chaining
main_GE_154(o66, i17, iconst_100, env, static) -{0,0}> main_GE_158(o66, i17, iconst_100, env, static) :|: iconst_100 = 100 && 1 <= i17 && 0 < o66 && 100 <= i17
main_GE_158(o66, i17, iconst_100, env, static) -{1,1}> main_ConstantStackPush_168(o66, env, static) :|: iconst_100 <= i17 && iconst_100 = 100 && 0 < o66 && 100 <= i17
main_ConstantStackPush_168(o66, env, static) -{1,1}> main_Store_170(o66, iconst_5, env, static) :|: iconst_5 = 5 && 0 < o66
main_Store_170(o66, iconst_5, env, static) -{1,1}> main_Load_173(o66, iconst_5, env, static) :|: iconst_5 = 5 && 0 < o66
main_Load_173(o66, iconst_5, env, static) -{0,0}> main_Load_212(o66, iconst_5, env, static) :|: iconst_5 <= 11 && iconst_5 = 5 && 0 < o66 && 5 <= iconst_5
main_Load_212(o102, i20, env, static) -{0,0}> main_Load_229(o102, i20, env, static) :|: i20 <= 14 && 5 <= i20 && i20 <= 11 && 0 < o102
main_Load_229(o114, i25, env, static) -{0,0}> main_Load_245(o114, i25, env, static) :|: 0 < o114 && i25 <= 14 && 5 <= i25

obtained
main_Load_245(o122, i28, env, static) -{2,2}> main_GE_247(o122, i28, 21, env, static) :|: 0 < o122
by chaining
main_Load_245(o122, i28, env, static) -{1,1}> main_ConstantStackPush_246(o122, i28, env, static) :|: 0 < o122
main_ConstantStackPush_246(o122, i28, env, static) -{1,1}> main_GE_247(o122, i28, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122

obtained
main_GE_247(o122, i34, 21, env, static) -{3,3}> main_Load_245(o122, i36', env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36'
by chaining
main_GE_247(o122, i34, iconst_21, env, static) -{0,0}> main_GE_250(o122, i34, iconst_21, env, static) :|: i34 <= 20 && iconst_21 = 21 && 0 < o122
main_GE_250(o122, i34, iconst_21, env, static) -{1,1}> main_Inc_255(o122, i34, env, static) :|: i34 <= 20 && i34 < iconst_21 && iconst_21 = 21 && 0 < o122
main_Inc_255(o122, i34, env, static) -{1,1}> main_JMP_262(o122, i36, env, static) :|: i34 <= 20 && i36 <= 23 && i34 + 3 = i36 && 0 < o122
main_JMP_262(o122, i36, env, static) -{1,1}> main_Load_267(o122, i36, env, static) :|: i36 <= 23 && 0 < o122
main_Load_267(o122, i36, env, static) -{0,0}> main_Load_245(o122, i36, env, static) :|: i36 <= 23 && 0 < o122

obtained
main_GE_154(o66, i16, 100, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'
by chaining
main_GE_154(o66, i16, iconst_100, env, static) -{0,0}> main_GE_157(o66, i16, iconst_100, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && 0 < o66
main_GE_157(o66, i16, iconst_100, env, static) -{1,1}> main_Inc_162(o66, i16, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && 0 < o66 && i16 < iconst_100
main_Inc_162(o66, i16, env, static) -{1,1}> main_JMP_169(o66, i18, env, static) :|: i16 + 1 = i18 && 1 <= i16 && i16 <= 99 && 0 < o66 && 2 <= i18 && i18 <= 100
main_JMP_169(o66, i18, env, static) -{1,1}> main_Load_171(o66, i18, env, static) :|: 0 < o66 && 2 <= i18 && i18 <= 100
main_Load_171(o66, i18, env, static) -{0,0}> main_Load_147(o66, i18, env, static) :|: 1 <= i18 && 0 < o66 && 2 <= i18 && i18 <= 100

(8) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17, 100, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
main_Load_245(o122, i28, env, static) -{2,2}> main_GE_247(o122, i28, 21, env, static) :|: 0 < o122
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35
main_GE_247(o122, i34, 21, env, static) -{3,3}> main_Load_245(o122, i36', env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36'
main_GE_154(o66, i16, 100, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'

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

Moved arithmethic from lhss to constraints.

main_GE_154(o66, i16, 100, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'
was transformed to
main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100

main_GE_154(o66, i17, 100, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
was transformed to
main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11 && x = 100

main_GE_247(o122, i34, 21, env, static) -{3,3}> main_Load_245(o122, i36', env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36'
was transformed to
main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i36', env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21

(10) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35
main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100
main_Load_245(o122, i28, env, static) -{2,2}> main_GE_247(o122, i28, 21, env, static) :|: 0 < o122
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11 && x = 100
main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i36', env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21

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

Moved arithmethic from constraints to rhss.

main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35
was transformed to
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, 21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35

main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i36', env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21
was transformed to
main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i34 + 3, env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21

main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100
was transformed to
main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100

(12) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, 21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35
main_Load_245(o122, i28, env, static) -{2,2}> main_GE_247(o122, i28, 21, env, static) :|: 0 < o122
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i34 + 3, env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11 && x = 100
main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100

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

Simplified expressions.

main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 0 < o2 && 0 <= static && 0 <= static''' && static''' <= static + 2 && static'1 <= static''' + 1

main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11 && x = 100
was transformed to
main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 0 < o66 && 1 <= i17 && x = 100

(14) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i34 + 3, env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 0 < o2 && 0 <= static && 0 <= static''' && static''' <= static + 2 && static'1 <= static''' + 1
main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100
main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 0 < o66 && 1 <= i17 && x = 100
main_Load_245(o122, i28, env, static) -{2,2}> main_GE_247(o122, i28, 21, env, static) :|: 0 < o122
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, 21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35

(15) CESProof (EQUIVALENT transformation)

proved upper bound 1652 / 3 using cofloco

(16) BOUNDS(CONSTANT, 1652 / 3)

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

Transformed 55 jbc graph edges to a weighted ITS with 55 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) MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID) transformation)

Moved arithmethic from constraints to rhss.

(24) Obligation:

IntTrs with 7 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_247(o122, i35, iconst_21, env, static) -{0,0}> main_GE_251(o122, i35, 21, env, static) :|: iconst_21 = 21 && 0 < o122 && 21 <= i35
main_Load_245(o122, i28, env, static) -{2,2}> main_GE_247(o122, i28, 21, env, static) :|: 0 < o122
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
main_GE_247(o122, i34, x, env, static) -{3,3}> main_Load_245(o122, i34 + 3, env, static) :|: i34 < 21 && i36' <= 23 && 0 < o122 && i34 <= 20 && i34 + 3 = i36' && x = 21
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17, x, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11 && x = 100
main_GE_154(o66, i16, x, env, static) -{3,3}> main_Load_147(o66, i16 + 1, env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18' && x = 100

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

Simplified expressions.

(26) Obligation:

(27) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)) transformation)

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

(28) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(30) Obligation:

IntTrs with 54 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o2, env, static) -{0,0}> main_ConstantStackPush_4(o2, env, static) :|: 0 < o2
main_ConstantStackPush_4(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_14(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(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_19(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_19(o2, env, static) -{0,0}> langle_clinit_rangle_New_20(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_20(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_22(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_24(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_26(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_27(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_29(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_31(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_33(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_36(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_38(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_ConstantStackPush_48(o2, env, static) :|: 0 < o2
main_ConstantStackPush_48(o2, env, static) -{0,0}> main_ConstantStackPush_49(o2, env, static) :|: 0 < o2
main_ConstantStackPush_49(o2, env, static) -{0,0}> main_ConstantStackPush_50(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_50(o2, env, static) -{0,0}> main_ConstantStackPush_51(o2, env, static) :|: 0 < o2
main_ConstantStackPush_51(o2, env, static) -{0,0}> main_ConstantStackPush_52(o2, env, static) :|: 0 < o2
main_ConstantStackPush_52(o2, env, static) -{1,1}> main_Store_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_53(o2, iconst_0, env, static) -{1,1}> main_Load_54(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_54(o2, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ConstantStackPush_55(o2, iconst_0, env, static) -{1,1}> main_GE_56(o2, iconst_0, iconst_100, env, static) :|: 0 < o2 && iconst_100 = 100 && iconst_0 = 0
main_GE_56(o2, iconst_0, iconst_100, env, static) -{1,1}> main_Inc_59(o2, iconst_0, env, static) :|: 0 < o2 && iconst_100 = 100 && iconst_0 = 0
main_Inc_59(o2, iconst_0, env, static) -{1,1}> main_JMP_61(o2, iconst_1, env, static) :|: 0 < o2 && iconst_1 = 1 && iconst_0 = 0
main_JMP_61(o2, iconst_1, env, static) -{1,1}> main_Load_69(o2, iconst_1, env, static) :|: 0 < o2 && iconst_1 = 1
main_Load_69(o2, iconst_1, env, static) -{0,0}> main_Load_103(o2, iconst_1, env, static) :|: iconst_1 <= 2 && 0 < o2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_103(o20, i1, env, static) -{0,0}> main_Load_126(o20, i1, env, static) :|: 0 < o20 && 1 <= i1 && i1 <= 2 && i1 <= 3
main_Load_126(o44, i6, env, static) -{0,0}> main_Load_147(o44, i6, env, static) :|: 0 < o44 && 1 <= i6 && i6 <= 3
main_Load_147(o66, i10, env, static) -{1,1}> main_ConstantStackPush_148(o66, i10, env, static) :|: 1 <= i10 && 0 < o66
main_ConstantStackPush_148(o66, i10, env, static) -{1,1}> main_GE_154(o66, i10, iconst_100, env, static) :|: 1 <= i10 && iconst_100 = 100 && 0 < o66
main_GE_154(o66, i16, iconst_100, env, static) -{0,0}> main_GE_157(o66, i16, iconst_100, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && 0 < o66
main_GE_154(o66, i17, iconst_100, env, static) -{0,0}> main_GE_158(o66, i17, iconst_100, env, static) :|: iconst_100 = 100 && 1 <= i17 && 0 < o66 && 100 <= i17
main_GE_157(o66, i16, iconst_100, env, static) -{1,1}> main_Inc_162(o66, i16, env, static) :|: 1 <= i16 && iconst_100 = 100 && i16 <= 99 && 0 < o66 && i16 < iconst_100
main_GE_158(o66, i17, iconst_100, env, static) -{1,1}> main_ConstantStackPush_168(o66, env, static) :|: iconst_100 <= i17 && iconst_100 = 100 && 0 < o66 && 100 <= i17
main_Inc_162(o66, i16, env, static) -{1,1}> main_JMP_169(o66, i18, env, static) :|: i16 + 1 = i18 && 1 <= i16 && i16 <= 99 && 0 < o66 && 2 <= i18 && i18 <= 100
main_ConstantStackPush_168(o66, env, static) -{1,1}> main_Store_170(o66, iconst_5, env, static) :|: iconst_5 = 5 && 0 < o66
main_JMP_169(o66, i18, env, static) -{1,1}> main_Load_171(o66, i18, env, static) :|: 0 < o66 && 2 <= i18 && i18 <= 100
main_Store_170(o66, iconst_5, env, static) -{1,1}> main_Load_173(o66, iconst_5, env, static) :|: iconst_5 = 5 && 0 < o66
main_Load_171(o66, i18, env, static) -{0,0}> main_Load_147(o66, i18, env, static) :|: 1 <= i18 && 0 < o66 && 2 <= i18 && i18 <= 100
main_Load_173(o66, iconst_5, env, static) -{0,0}> main_Load_212(o66, iconst_5, env, static) :|: iconst_5 <= 11 && iconst_5 = 5 && 0 < o66 && 5 <= iconst_5
main_Load_212(o102, i20, env, static) -{0,0}> main_Load_229(o102, i20, env, static) :|: i20 <= 14 && 5 <= i20 && i20 <= 11 && 0 < o102
main_Load_229(o114, i25, env, static) -{0,0}> main_Load_245(o114, i25, env, static) :|: 0 < o114 && i25 <= 14 && 5 <= i25
main_Load_245(o122, i28, env, static) -{1,1}> main_ConstantStackPush_246(o122, i28, env, static) :|: 0 < o122
main_ConstantStackPush_246(o122, i28, env, static) -{1,1}> main_GE_247(o122, i28, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122
main_GE_247(o122, i34, iconst_21, env, static) -{0,0}> main_GE_250(o122, i34, iconst_21, env, static) :|: i34 <= 20 && iconst_21 = 21 && 0 < o122
main_GE_250(o122, i34, iconst_21, env, static) -{1,1}> main_Inc_255(o122, i34, env, static) :|: i34 <= 20 && i34 < iconst_21 && iconst_21 = 21 && 0 < o122
main_Inc_255(o122, i34, env, static) -{1,1}> main_JMP_262(o122, i36, env, static) :|: i34 <= 20 && i36 <= 23 && i34 + 3 = i36 && 0 < o122
main_JMP_262(o122, i36, env, static) -{1,1}> main_Load_267(o122, i36, env, static) :|: i36 <= 23 && 0 < o122
main_Load_267(o122, i36, env, static) -{0,0}> main_Load_245(o122, i36, env, static) :|: i36 <= 23 && 0 < o122

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

obtained
main_Load_245(o122, i28, env, static) -{5,5}> main_Load_245(o122, i36', env, static) :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'
by chaining
main_Load_245(o122, i28, env, static) -{1,1}> main_ConstantStackPush_246(o122, i28, env, static) :|: 0 < o122
main_ConstantStackPush_246(o122, i28, env, static) -{1,1}> main_GE_247(o122, i28, iconst_21, env, static) :|: iconst_21 = 21 && 0 < o122
main_GE_247(o122, i34, iconst_21, env, static) -{0,0}> main_GE_250(o122, i34, iconst_21, env, static) :|: i34 <= 20 && iconst_21 = 21 && 0 < o122
main_GE_250(o122, i34, iconst_21, env, static) -{1,1}> main_Inc_255(o122, i34, env, static) :|: i34 <= 20 && i34 < iconst_21 && iconst_21 = 21 && 0 < o122
main_Inc_255(o122, i34, env, static) -{1,1}> main_JMP_262(o122, i36, env, static) :|: i34 <= 20 && i36 <= 23 && i34 + 3 = i36 && 0 < o122
main_JMP_262(o122, i36, env, static) -{1,1}> main_Load_267(o122, i36, env, static) :|: i36 <= 23 && 0 < o122
main_Load_267(o122, i36, env, static) -{0,0}> main_Load_245(o122, i36, env, static) :|: i36 <= 23 && 0 < o122

(32) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_1(o2, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o2, env, static) -{22,22}> main_Load_147(o2, 1, env, static'1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
main_Load_147(o66, i10, env, static) -{2,2}> main_GE_154(o66, i10, 100, env, static) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17, 100, env, static) -{3,3}> main_Load_245(o66, 5, env, static) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
main_Load_245(o122, i28, env, static) -{5,5}> main_Load_245(o122, i36', env, static) :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'
main_GE_154(o66, i16, 100, env, static) -{3,3}> main_Load_147(o66, i18', env, static) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'

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

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

main_ConstantStackPush_1(x1, x2, x3) → main_ConstantStackPush_1(x1, x3)
main_Load_147(x1, x2, x3, x4) → main_Load_147(x1, x2)
main_GE_154(x1, x2, x3, x4, x5) → main_GE_154(x1, x2)
main_Load_245(x1, x2, x3, x4) → main_Load_245(x1, x2)

(34) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_1(o2, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(o2, static) -{22,22}> main_Load_147(o2, 1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
main_Load_147(o66, i10) -{2,2}> main_GE_154(o66, i10) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17) -{3,3}> main_Load_245(o66, 5) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
main_Load_245(o122, i28) -{5,5}> main_Load_245(o122, i36') :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'
main_GE_154(o66, i16) -{3,3}> main_Load_147(o66, i18') :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'

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

Moved arithmethic from constraints to rhss.

main_GE_154(o66, i16) -{3,3}> main_Load_147(o66, i18') :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'
was transformed to
main_GE_154(o66, i16) -{3,3}> main_Load_147(o66, i16 + 1) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'

main_Load_245(o122, i28) -{5,5}> main_Load_245(o122, i36') :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'
was transformed to
main_Load_245(o122, i28) -{5,5}> main_Load_245(o122, i28 + 3) :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'

(36) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_1(o2, static)
Considered paths: all paths from start
Rules:
main_GE_154(o66, i16) -{3,3}> main_Load_147(o66, i16 + 1) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'
main_Load_147(o66, i10) -{2,2}> main_GE_154(o66, i10) :|: 1 <= i10 && 0 < o66
main_Load_245(o122, i28) -{5,5}> main_Load_245(o122, i28 + 3) :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'
main_GE_154(o66, i17) -{3,3}> main_Load_245(o66, 5) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
main_ConstantStackPush_1(o2, static) -{22,22}> main_Load_147(o2, 1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2

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

Simplified expressions.

main_ConstantStackPush_1(o2, static) -{22,22}> main_Load_147(o2, 1) :|: 0 <= static'1 && 1 <= 3 && 0 < 2 && 0 < o2 && 1 <= 1 && 0 <= 1 && 0 < 1 && 0 <= static && 0 <= static''' && static''' <= static + 2 && 1 <= 2 && static'1 <= static''' + 1 && 0 <= 2
was transformed to
main_ConstantStackPush_1(o2, static) -{22,22}> main_Load_147(o2, 1) :|: 0 <= static'1 && 0 < o2 && 0 <= static && 0 <= static''' && static''' <= static + 2 && static'1 <= static''' + 1

main_GE_154(o66, i17) -{3,3}> main_Load_245(o66, 5) :|: 100 <= i17 && 5 <= 5 && 0 < o66 && 5 <= 14 && 1 <= i17 && 5 <= 11
was transformed to
main_GE_154(o66, i17) -{3,3}> main_Load_245(o66, 5) :|: 100 <= i17 && 0 < o66 && 1 <= i17

(38) Obligation:

IntTrs with 5 rules
Start term: main_ConstantStackPush_1(o2, static)
Considered paths: all paths from start
Rules:
main_Load_147(o66, i10) -{2,2}> main_GE_154(o66, i10) :|: 1 <= i10 && 0 < o66
main_GE_154(o66, i17) -{3,3}> main_Load_245(o66, 5) :|: 100 <= i17 && 0 < o66 && 1 <= i17
main_Load_245(o122, i28) -{5,5}> main_Load_245(o122, i28 + 3) :|: i28 < 21 && i36' <= 23 && 0 < o122 && i28 <= 20 && i28 + 3 = i36'
main_GE_154(o66, i16) -{3,3}> main_Load_147(o66, i16 + 1) :|: 1 <= i16 && i18' <= 100 && i16 <= 99 && 2 <= i18' && 1 <= i18' && 0 < o66 && i16 < 100 && i16 + 1 = i18'
main_ConstantStackPush_1(o2, static) -{22,22}> main_Load_147(o2, 1) :|: 0 <= static'1 && 0 < o2 && 0 <= static && 0 <= static''' && static''' <= static + 2 && static'1 <= static''' + 1