time complexity proof of /tmp/tmpSwh

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 661).

0 JBC problem

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

↳2 JBCTerminationGraph

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

    ↳4 JBCComplexityEdges

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

        ↳6 WeightedIntTrs

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

            ↳8 WeightedIntTrs

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

            ↳10 WeightedIntTrs

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

            ↳12 WeightedIntTrs

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

            ↳14 WeightedIntTrs

            ↳15 CESProof (⇔, 131 ms)

            ↳16 BOUNDS(CONSTANT, 659)

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

        ↳18 WeightedIntTrs

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

    ↳28 JBCComplexityEdges

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

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

        ↳36 WeightedIntTrs

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

        ↳38 WeightedIntTrs

↳39 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 897 ms)

↳40 JBCTerminationGraph

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * An example of nested iterations.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
 */

public class Nested {
    public static void main() {
	for (int i = 0; i < 10; i++)
	    for (int j = 3; j < 12; j += 2) {
		j -= 1;
	    }
    }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Nested.main()V: Graph of 57 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 56 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 56 jbc graph edges to a weighted ITS with 56 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 56 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_19(env, static) :|: 0 <= static
langle_clinit_rangle_New_19(env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_25(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(iconst_0, env, static) -{1,1}> main_GE_56(iconst_0, iconst_10, env, static) :|: iconst_0 = 0 && iconst_10 = 10
main_GE_56(iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_73(iconst_0, env, static) :|: iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_73(iconst_0, env, static) -{1,1}> main_Store_75(iconst_3, iconst_0, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Store_75(iconst_3, iconst_0, env, static) -{1,1}> main_Load_76(iconst_0, iconst_3, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Load_76(iconst_0, iconst_3, env, static) -{0,0}> main_Load_185(iconst_0, iconst_3, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Load_185(iconst_0, i11, env, static) -{0,0}> main_Load_231(iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_Load_231(i24, i25, env, static) -{0,0}> main_Load_277(i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2
main_Load_277(i38, i39, env, static) -{0,0}> main_Load_318(i38, i39, env, static) :|: 0 <= i38 && i38 <= 2
main_Load_318(i52, i53, env, static) -{1,1}> main_ConstantStackPush_319(i53, i52, env, static) :|: 0 <= i52
main_ConstantStackPush_319(i53, i52, env, static) -{1,1}> main_GE_326(i53, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12
main_GE_326(i60, iconst_12, i52, env, static) -{0,0}> main_GE_327(i60, iconst_12, i52, env, static) :|: 0 <= i52 && i60 <= 11 && iconst_12 = 12
main_GE_326(i61, iconst_12, i52, env, static) -{0,0}> main_GE_328(i61, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61
main_GE_327(i60, iconst_12, i52, env, static) -{1,1}> main_Inc_329(i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && i60 <= 11 && iconst_12 = 12
main_GE_328(i61, iconst_12, i52, env, static) -{1,1}> main_Inc_338(i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_329(i52, i60, env, static) -{1,1}> main_Inc_339(i52, i62, env, static) :|: 0 <= i52 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_338(i52, env, static) -{1,1}> main_JMP_340(i63, env, static) :|: 0 <= i52 && 1 <= i63 && i52 + 1 = i63
main_Inc_339(i52, i62, env, static) -{1,1}> main_JMP_341(i52, i64, env, static) :|: 0 <= i52 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_340(i63, env, static) -{1,1}> main_Load_342(i63, env, static) :|: 1 <= i63
main_JMP_341(i52, i64, env, static) -{1,1}> main_Load_343(i52, i64, env, static) :|: 0 <= i52 && i64 <= 12
main_Load_342(i63, env, static) -{1,1}> main_ConstantStackPush_344(i63, env, static) :|: 1 <= i63
main_Load_343(i52, i64, env, static) -{0,0}> main_Load_318(i52, i64, env, static) :|: 0 <= i52 && i64 <= 12
main_ConstantStackPush_344(i63, env, static) -{1,1}> main_GE_345(i63, iconst_10, env, static) :|: 1 <= i63 && iconst_10 = 10
main_GE_345(i71, iconst_10, env, static) -{0,0}> main_GE_346(i71, iconst_10, env, static) :|: iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, iconst_10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_346(i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(i71, env, static) :|: iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(i71, env, static) -{1,1}> main_Store_358(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_358(iconst_3, i71, env, static) -{1,1}> main_Load_360(i71, iconst_3, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_360(i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_361(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_361(iconst_3, i71, env, static) -{1,1}> main_GE_362(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_362(iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_326(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

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

obtained
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
by chaining
main_ConstantStackPush_1(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_19(env, static) :|: 0 <= static
langle_clinit_rangle_New_19(env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_25(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(iconst_0, env, static) -{1,1}> main_GE_56(iconst_0, iconst_10, env, static) :|: iconst_0 = 0 && iconst_10 = 10
main_GE_56(iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_73(iconst_0, env, static) :|: iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_73(iconst_0, env, static) -{1,1}> main_Store_75(iconst_3, iconst_0, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Store_75(iconst_3, iconst_0, env, static) -{1,1}> main_Load_76(iconst_0, iconst_3, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Load_76(iconst_0, iconst_3, env, static) -{0,0}> main_Load_185(iconst_0, iconst_3, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Load_185(iconst_0, i11, env, static) -{0,0}> main_Load_231(iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_Load_231(i24, i25, env, static) -{0,0}> main_Load_277(i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2
main_Load_277(i38, i39, env, static) -{0,0}> main_Load_318(i38, i39, env, static) :|: 0 <= i38 && i38 <= 2

obtained
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
by chaining
main_Load_318(i52, i53, env, static) -{1,1}> main_ConstantStackPush_319(i53, i52, env, static) :|: 0 <= i52
main_ConstantStackPush_319(i53, i52, env, static) -{1,1}> main_GE_326(i53, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12

obtained
main_GE_326(i61, 12, i52, env, static) -{5,5}> main_GE_345(i63', 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63'
by chaining
main_GE_326(i61, iconst_12, i52, env, static) -{0,0}> main_GE_328(i61, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61
main_GE_328(i61, iconst_12, i52, env, static) -{1,1}> main_Inc_338(i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_338(i52, env, static) -{1,1}> main_JMP_340(i63, env, static) :|: 0 <= i52 && 1 <= i63 && i52 + 1 = i63
main_JMP_340(i63, env, static) -{1,1}> main_Load_342(i63, env, static) :|: 1 <= i63
main_Load_342(i63, env, static) -{1,1}> main_ConstantStackPush_344(i63, env, static) :|: 1 <= i63
main_ConstantStackPush_344(i63, env, static) -{1,1}> main_GE_345(i63, iconst_10, env, static) :|: 1 <= i63 && iconst_10 = 10

obtained
main_GE_345(i71, 10, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71
by chaining
main_GE_345(i71, iconst_10, env, static) -{0,0}> main_GE_346(i71, iconst_10, env, static) :|: iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_346(i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(i71, env, static) :|: iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(i71, env, static) -{1,1}> main_Store_358(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_358(iconst_3, i71, env, static) -{1,1}> main_Load_360(i71, iconst_3, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_360(i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_361(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_361(iconst_3, i71, env, static) -{1,1}> main_GE_362(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_362(iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_326(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

obtained
main_GE_326(i60, 12, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12
by chaining
main_GE_326(i60, iconst_12, i52, env, static) -{0,0}> main_GE_327(i60, iconst_12, i52, env, static) :|: 0 <= i52 && i60 <= 11 && iconst_12 = 12
main_GE_327(i60, iconst_12, i52, env, static) -{1,1}> main_Inc_329(i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && i60 <= 11 && iconst_12 = 12
main_Inc_329(i52, i60, env, static) -{1,1}> main_Inc_339(i52, i62, env, static) :|: 0 <= i52 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_339(i52, i62, env, static) -{1,1}> main_JMP_341(i52, i64, env, static) :|: 0 <= i52 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_341(i52, i64, env, static) -{1,1}> main_Load_343(i52, i64, env, static) :|: 0 <= i52 && i64 <= 12
main_Load_343(i52, i64, env, static) -{0,0}> main_Load_318(i52, i64, env, static) :|: 0 <= i52 && i64 <= 12

(8) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
main_GE_326(i61, 12, i52, env, static) -{5,5}> main_GE_345(i63', 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63'
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, iconst_10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_GE_345(i71, 10, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71
main_GE_326(i60, 12, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12

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

Moved arithmethic from lhss to constraints.

main_GE_326(i61, 12, i52, env, static) -{5,5}> main_GE_345(i63', 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63'
was transformed to
main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i63', 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12

main_GE_326(i60, 12, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12

main_GE_345(i71, 10, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71
was transformed to
main_GE_345(i71, x, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71 && x = 10

(10) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i63', 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, iconst_10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
main_GE_345(i71, x, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71 && x = 10

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

Moved arithmethic from constraints to rhss.

main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, iconst_10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
was transformed to
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, 10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72

main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i63', 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12
was transformed to
main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i52 + 1, 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12

main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i60 + -1 + 2, env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12

(12) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, 10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i52 + 1, 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12
main_GE_345(i71, x, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71 && x = 10
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i60 + -1 + 2, env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12

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

Simplified expressions.

main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i60 + -1 + 2, env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12
was transformed to
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i60 + 1, env, static) :|: i60 - 1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12

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

(14) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i60 + 1, env, static) :|: i60 - 1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, 10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
main_GE_345(i71, x, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71 && x = 10
main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i52 + 1, 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12

(15) CESProof (EQUIVALENT transformation)

proved upper bound 659 using cofloco

(16) BOUNDS(CONSTANT, 659)

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

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

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

Simplified expressions.

(26) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_GE_326(i60, x, i52, env, static) -{4,4}> main_Load_318(i52, i60 + 1, env, static) :|: i60 - 1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12 && x = 12
main_GE_345(i72, iconst_10, env, static) -{0,0}> main_GE_347(i72, 10, env, static) :|: iconst_10 = 10 && 10 <= i72 && 1 <= i72
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
main_GE_345(i71, x, env, static) -{5,5}> main_GE_326(3, 12, i71, env, static) :|: i71 < 10 && 1 <= i71 && i71 <= 9 && 0 <= i71 && x = 10
main_GE_326(i61, x, i52, env, static) -{5,5}> main_GE_345(i52 + 1, 10, env, static) :|: 12 <= i61 && 1 <= i63' && 0 <= i52 && i52 + 1 = i63' && x = 12

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

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

(28) Obligation:

Set of 55 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 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.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(30) Obligation:

IntTrs with 55 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(env, static) -{0,0}> main_ConstantStackPush_4(env, static) :|: 0 >= 0
main_ConstantStackPush_4(env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(env, static) -{0,0}> langle_clinit_rangle_New_18(env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(env, static) -{0,0}> langle_clinit_rangle_New_19(env, static) :|: 0 <= static
langle_clinit_rangle_New_19(env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, env, static) -{1,1}> langle_init_rangle_Load_25(o2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, env, static) -{1,1}> langle_init_rangle_Load_29(o2, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, env, static) -{1,1}> langle_init_rangle_Return_34(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, env, static) -{1,1}> langle_init_rangle_Return_36(o2, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, env, static) -{1,1}> langle_clinit_rangle_Return_40(env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(env, static) -{1,1}> main_ConstantStackPush_48(env, static) :|: 0 >= 0
main_ConstantStackPush_48(env, static) -{0,0}> main_ConstantStackPush_49(env, static) :|: 0 >= 0
main_ConstantStackPush_49(env, static) -{0,0}> main_ConstantStackPush_50(env, static) :|: 0 <= static
main_ConstantStackPush_50(env, static) -{0,0}> main_ConstantStackPush_51(env, static) :|: 0 >= 0
main_ConstantStackPush_51(env, static) -{0,0}> main_ConstantStackPush_52(env, static) :|: 0 >= 0
main_ConstantStackPush_52(env, static) -{1,1}> main_Store_53(iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(iconst_0, env, static) -{1,1}> main_Load_54(iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(iconst_0, env, static) -{1,1}> main_GE_56(iconst_0, iconst_10, env, static) :|: iconst_0 = 0 && iconst_10 = 10
main_GE_56(iconst_0, iconst_10, env, static) -{1,1}> main_ConstantStackPush_73(iconst_0, env, static) :|: iconst_0 = 0 && iconst_10 = 10
main_ConstantStackPush_73(iconst_0, env, static) -{1,1}> main_Store_75(iconst_3, iconst_0, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Store_75(iconst_3, iconst_0, env, static) -{1,1}> main_Load_76(iconst_0, iconst_3, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Load_76(iconst_0, iconst_3, env, static) -{0,0}> main_Load_185(iconst_0, iconst_3, env, static) :|: iconst_3 = 3 && iconst_0 = 0
main_Load_185(iconst_0, i11, env, static) -{0,0}> main_Load_231(iconst_0, i11, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_Load_231(i24, i25, env, static) -{0,0}> main_Load_277(i24, i25, env, static) :|: 0 <= i24 && i24 <= 1 && i24 <= 2
main_Load_277(i38, i39, env, static) -{0,0}> main_Load_318(i38, i39, env, static) :|: 0 <= i38 && i38 <= 2
main_Load_318(i52, i53, env, static) -{1,1}> main_ConstantStackPush_319(i53, i52, env, static) :|: 0 <= i52
main_ConstantStackPush_319(i53, i52, env, static) -{1,1}> main_GE_326(i53, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12
main_GE_326(i60, iconst_12, i52, env, static) -{0,0}> main_GE_327(i60, iconst_12, i52, env, static) :|: 0 <= i52 && i60 <= 11 && iconst_12 = 12
main_GE_326(i61, iconst_12, i52, env, static) -{0,0}> main_GE_328(i61, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61
main_GE_327(i60, iconst_12, i52, env, static) -{1,1}> main_Inc_329(i52, i60, env, static) :|: i60 < iconst_12 && 0 <= i52 && i60 <= 11 && iconst_12 = 12
main_GE_328(i61, iconst_12, i52, env, static) -{1,1}> main_Inc_338(i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_329(i52, i60, env, static) -{1,1}> main_Inc_339(i52, i62, env, static) :|: 0 <= i52 && i60 <= 11 && i60 + -1 = i62 && i62 <= 10
main_Inc_338(i52, env, static) -{1,1}> main_JMP_340(i63, env, static) :|: 0 <= i52 && 1 <= i63 && i52 + 1 = i63
main_Inc_339(i52, i62, env, static) -{1,1}> main_JMP_341(i52, i64, env, static) :|: 0 <= i52 && i62 + 2 = i64 && i62 <= 10 && i64 <= 12
main_JMP_340(i63, env, static) -{1,1}> main_Load_342(i63, env, static) :|: 1 <= i63
main_JMP_341(i52, i64, env, static) -{1,1}> main_Load_343(i52, i64, env, static) :|: 0 <= i52 && i64 <= 12
main_Load_342(i63, env, static) -{1,1}> main_ConstantStackPush_344(i63, env, static) :|: 1 <= i63
main_Load_343(i52, i64, env, static) -{0,0}> main_Load_318(i52, i64, env, static) :|: 0 <= i52 && i64 <= 12
main_ConstantStackPush_344(i63, env, static) -{1,1}> main_GE_345(i63, iconst_10, env, static) :|: 1 <= i63 && iconst_10 = 10
main_GE_345(i71, iconst_10, env, static) -{0,0}> main_GE_346(i71, iconst_10, env, static) :|: iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_346(i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(i71, env, static) :|: iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(i71, env, static) -{1,1}> main_Store_358(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_358(iconst_3, i71, env, static) -{1,1}> main_Load_360(i71, iconst_3, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_360(i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_361(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_361(iconst_3, i71, env, static) -{1,1}> main_GE_362(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_362(iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_326(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

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

obtained
main_GE_326(i61, 12, i52, env, static) -{10,10}> main_GE_326(3, 12, i63', env, static) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61
by chaining
main_GE_326(i61, iconst_12, i52, env, static) -{0,0}> main_GE_328(i61, iconst_12, i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61
main_GE_328(i61, iconst_12, i52, env, static) -{1,1}> main_Inc_338(i52, env, static) :|: 0 <= i52 && iconst_12 = 12 && 12 <= i61 && iconst_12 <= i61
main_Inc_338(i52, env, static) -{1,1}> main_JMP_340(i63, env, static) :|: 0 <= i52 && 1 <= i63 && i52 + 1 = i63
main_JMP_340(i63, env, static) -{1,1}> main_Load_342(i63, env, static) :|: 1 <= i63
main_Load_342(i63, env, static) -{1,1}> main_ConstantStackPush_344(i63, env, static) :|: 1 <= i63
main_ConstantStackPush_344(i63, env, static) -{1,1}> main_GE_345(i63, iconst_10, env, static) :|: 1 <= i63 && iconst_10 = 10
main_GE_345(i71, iconst_10, env, static) -{0,0}> main_GE_346(i71, iconst_10, env, static) :|: iconst_10 = 10 && i71 <= 9 && 1 <= i71
main_GE_346(i71, iconst_10, env, static) -{1,1}> main_ConstantStackPush_356(i71, env, static) :|: iconst_10 = 10 && i71 < iconst_10 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_356(i71, env, static) -{1,1}> main_Store_358(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Store_358(iconst_3, i71, env, static) -{1,1}> main_Load_360(i71, iconst_3, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_Load_360(i71, iconst_3, env, static) -{1,1}> main_ConstantStackPush_361(iconst_3, i71, env, static) :|: iconst_3 = 3 && i71 <= 9 && 1 <= i71
main_ConstantStackPush_361(iconst_3, i71, env, static) -{1,1}> main_GE_362(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && i71 <= 9 && 1 <= i71
main_GE_362(iconst_3, iconst_12, i71, env, static) -{0,0}> main_GE_326(iconst_3, iconst_12, i71, env, static) :|: iconst_3 = 3 && iconst_12 = 12 && 0 <= i71 && i71 <= 9 && 1 <= i71

(32) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(env, static) -{22,22}> main_Load_318(0, 3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_Load_318(i52, i53, env, static) -{2,2}> main_GE_326(i53, 12, i52, env, static) :|: 0 <= i52
main_GE_326(i61, 12, i52, env, static) -{10,10}> main_GE_326(3, 12, i63', env, static) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61
main_GE_326(i60, 12, i52, env, static) -{4,4}> main_Load_318(i52, i64', env, static) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12

(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) → main_ConstantStackPush_1(x2)
main_Load_318(x1, x2, x3, x4) → main_Load_318(x1, x2)
main_GE_326(x1, x2, x3, x4, x5) → main_GE_326(x1, x3)

(34) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(static) -{22,22}> main_Load_318(0, 3) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_Load_318(i52, i53) -{2,2}> main_GE_326(i53, i52) :|: 0 <= i52
main_GE_326(i61, i52) -{10,10}> main_GE_326(3, i63') :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61
main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i64') :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12

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

Moved arithmethic from constraints to rhss.

main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i64') :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i60 + -1 + 2) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12

main_GE_326(i61, i52) -{10,10}> main_GE_326(3, i63') :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61
was transformed to
main_GE_326(i61, i52) -{10,10}> main_GE_326(3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61

(36) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(static)
Considered paths: all paths from start
Rules:
main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i60 + -1 + 2) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12
main_GE_326(i61, i52) -{10,10}> main_GE_326(3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61
main_Load_318(i52, i53) -{2,2}> main_GE_326(i53, i52) :|: 0 <= i52
main_ConstantStackPush_1(static) -{22,22}> main_Load_318(0, 3) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2

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

Simplified expressions.

main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i60 + -1 + 2) :|: i60 + -1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12
was transformed to
main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i60 + 1) :|: i60 - 1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12

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

(38) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_1(static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_1(static) -{22,22}> main_Load_318(0, 3) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_GE_326(i60, i52) -{4,4}> main_Load_318(i52, i60 + 1) :|: i60 - 1 = i62' && 0 <= i52 && i64' <= 12 && i60 <= 11 && i62' <= 10 && i62' + 2 = i64' && i60 < 12
main_Load_318(i52, i53) -{2,2}> main_GE_326(i53, i52) :|: 0 <= i52
main_GE_326(i61, i52) -{10,10}> main_GE_326(3, i52 + 1) :|: i52 + 1 = i63' && 1 <= i63' && i63' < 10 && i63' <= 9 && 0 <= i63' && 0 <= i52 && 12 <= i61

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

Constructed TerminationGraph.

(40) Obligation:

Termination Graph based on JBC Program:
Nested.main()V: Graph of 670 nodes with 0 SCCs.