time complexity proof of /tmp/tmpiVnz8i/Loop1.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 29 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(2)), 10 ms)

↳16 JBCComplexityEdges

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

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 90 ms)

    ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

        ↳33 CESProof (⇔, 131 ms)

        ↳34 BOUNDS(CONSTANT, 14 + 6 * args)

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * A very simple loop over an array.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
 */

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

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Loop1.main([Ljava/lang/String;)V: Graph of 42 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 39 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(o2, env, static) -{0,0}> langle_clinit_rangle_New_16(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_16(o2, env, static) -{0,0}> langle_clinit_rangle_New_17(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_17(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_19(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_23(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_23(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_28(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_34(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_34(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_36(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_38(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_38(o2, env, static) -{1,1}> main_ConstantStackPush_41(o2, env, static) :|: 0 < o2
main_ConstantStackPush_41(o2, env, static) -{0,0}> main_ConstantStackPush_42(o2, env, static) :|: 0 < o2
main_ConstantStackPush_42(o2, env, static) -{0,0}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_49(o2, env, static) :|: 0 < o2
main_ConstantStackPush_49(o2, env, static) -{1,1}> main_Store_51(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_51(o2, iconst_0, env, static) -{1,1}> main_Load_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_53(o2, iconst_0, env, static) -{1,1}> main_Load_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_55(o2, iconst_0, env, static) -{1,1}> main_ArrayLength_57(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayLength_57(o2, iconst_0, env, static) -{0,0}> main_ArrayLength_105(o2, iconst_0, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o2 && iconst_0 <= 1 && iconst_0 = 0
main_ArrayLength_105(o10, i12, i11, env, static) -{0,0}> main_ArrayLength_172(o10, i12, i11, env, static) :|: i11 <= 2 && 0 <= i11 && i12 <= 2 && 0 <= i12 && 0 < o10 && i12 <= 1 && i11 <= 1
main_ArrayLength_172(o20, i24, i23, env, static) -{0,0}> main_ArrayLength_208(o20, i24, i23, env, static) :|: 0 <= i24 && 0 < o20 && i23 <= 2 && i24 <= 2 && 0 <= i23
main_ArrayLength_208(a27, i32, i31, env, static) -{0,0}> main_ArrayLength_213(a27, i32, i31, i36, env, static) :|: 0 <= i31 && 0 <= i36 && i36 < a27 && 0 <= i32 && 0 < a27
main_ArrayLength_213(a27, i32, i31, i36, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_221(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_GE_221(a27, i32, i36, i31, env, static) -{1,1}> main_Inc_228(a27, i31, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_Inc_228(a27, i31, i36, env, static) -{1,1}> main_JMP_232(a27, i38, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 1 <= i38 && 0 < a27 && i31 + 1 = i38
main_JMP_232(a27, i38, i36, env, static) -{1,1}> main_Load_233(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_233(a27, i38, i36, env, static) -{1,1}> main_Load_236(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_236(a27, i38, i36, env, static) -{1,1}> main_ArrayLength_238(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_ArrayLength_238(a27, i38, i36, env, static) -{0,0}> main_ArrayLength_208(a27, i38, i38, env, static) :|: 1 <= i36 && 0 <= i38 && 1 <= i38 && 0 < a27

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

obtained
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
by chaining
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(o2, env, static) -{0,0}> langle_clinit_rangle_New_16(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_16(o2, env, static) -{0,0}> langle_clinit_rangle_New_17(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_17(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_19(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_23(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_23(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_28(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_34(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_34(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_36(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_38(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_38(o2, env, static) -{1,1}> main_ConstantStackPush_41(o2, env, static) :|: 0 < o2
main_ConstantStackPush_41(o2, env, static) -{0,0}> main_ConstantStackPush_42(o2, env, static) :|: 0 < o2
main_ConstantStackPush_42(o2, env, static) -{0,0}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_49(o2, env, static) :|: 0 < o2
main_ConstantStackPush_49(o2, env, static) -{1,1}> main_Store_51(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_51(o2, iconst_0, env, static) -{1,1}> main_Load_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_53(o2, iconst_0, env, static) -{1,1}> main_Load_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_55(o2, iconst_0, env, static) -{1,1}> main_ArrayLength_57(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayLength_57(o2, iconst_0, env, static) -{0,0}> main_ArrayLength_105(o2, iconst_0, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o2 && iconst_0 <= 1 && iconst_0 = 0
main_ArrayLength_105(o10, i12, i11, env, static) -{0,0}> main_ArrayLength_172(o10, i12, i11, env, static) :|: i11 <= 2 && 0 <= i11 && i12 <= 2 && 0 <= i12 && 0 < o10 && i12 <= 1 && i11 <= 1
main_ArrayLength_172(o20, i24, i23, env, static) -{0,0}> main_ArrayLength_208(o20, i24, i23, env, static) :|: 0 <= i24 && 0 < o20 && i23 <= 2 && i24 <= 2 && 0 <= i23

obtained
main_ArrayLength_208(a27, i32, i31, env, static) -{6,6}> main_ArrayLength_208(a27, i38', i38', env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36
by chaining
main_ArrayLength_208(a27, i32, i31, env, static) -{0,0}> main_ArrayLength_213(a27, i32, i31, i36, env, static) :|: 0 <= i31 && 0 <= i36 && i36 < a27 && 0 <= i32 && 0 < a27
main_ArrayLength_213(a27, i32, i31, i36, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_221(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_GE_221(a27, i32, i36, i31, env, static) -{1,1}> main_Inc_228(a27, i31, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_Inc_228(a27, i31, i36, env, static) -{1,1}> main_JMP_232(a27, i38, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 1 <= i38 && 0 < a27 && i31 + 1 = i38
main_JMP_232(a27, i38, i36, env, static) -{1,1}> main_Load_233(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_233(a27, i38, i36, env, static) -{1,1}> main_Load_236(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_236(a27, i38, i36, env, static) -{1,1}> main_ArrayLength_238(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_ArrayLength_238(a27, i38, i36, env, static) -{0,0}> main_ArrayLength_208(a27, i38, i38, env, static) :|: 1 <= i36 && 0 <= i38 && 1 <= i38 && 0 < a27

(8) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
main_ArrayLength_208(a27, i32, i31, env, static) -{6,6}> main_ArrayLength_208(a27, i38', i38', env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36

(9) 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_2(x1, x2, x3) → main_ConstantStackPush_2(x1, x3)
main_ArrayLength_208(x1, x2, x3, x4, x5) → main_ArrayLength_208(x1, x2, x3)

(10) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(args, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, static) -{19,19}> main_ArrayLength_208(o2, 0, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
main_ArrayLength_208(a27, i32, i31) -{6,6}> main_ArrayLength_208(a27, i38', i38') :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36

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

Moved arithmethic from constraints to rhss.

main_ArrayLength_208(a27, i32, i31) -{6,6}> main_ArrayLength_208(a27, i38', i38') :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36
was transformed to
main_ArrayLength_208(a27, i32, i31) -{6,6}> main_ArrayLength_208(a27, i31 + 1, i31 + 1) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36

(12) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(args, static)
Considered paths: all paths from start
Rules:
main_ArrayLength_208(a27, i32, i31) -{6,6}> main_ArrayLength_208(a27, i31 + 1, i31 + 1) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36
main_ConstantStackPush_2(o2, static) -{19,19}> main_ArrayLength_208(o2, 0, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1

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

Simplified expressions.

main_ConstantStackPush_2(o2, static) -{19,19}> main_ArrayLength_208(o2, 0, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
was transformed to
main_ConstantStackPush_2(o2, static) -{19,19}> main_ArrayLength_208(o2, 0, 0) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 <= static'1

(14) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(args, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o2, static) -{19,19}> main_ArrayLength_208(o2, 0, 0) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 <= static'1
main_ArrayLength_208(a27, i32, i31) -{6,6}> main_ArrayLength_208(a27, i31 + 1, i31 + 1) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && 0 <= i32 && i36 < a27 && i32 < i36

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

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

(16) Obligation:

Set of 40 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

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

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

IntTrs with 40 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{0,0}> main_ConstantStackPush_3(o2, env, static) :|: 0 < o2
main_ConstantStackPush_3(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_11(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_11(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(o2, env, static) -{0,0}> langle_clinit_rangle_New_16(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_16(o2, env, static) -{0,0}> langle_clinit_rangle_New_17(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_17(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_19(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_21(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_22(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_23(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_23(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_26(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_28(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_28(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_30(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_32(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_32(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_34(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_34(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_36(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_38(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_38(o2, env, static) -{1,1}> main_ConstantStackPush_41(o2, env, static) :|: 0 < o2
main_ConstantStackPush_41(o2, env, static) -{0,0}> main_ConstantStackPush_42(o2, env, static) :|: 0 < o2
main_ConstantStackPush_42(o2, env, static) -{0,0}> main_ConstantStackPush_46(o2, env, static) :|: 0 < o2 && 0 <= static
main_ConstantStackPush_46(o2, env, static) -{0,0}> main_ConstantStackPush_47(o2, env, static) :|: 0 < o2
main_ConstantStackPush_47(o2, env, static) -{0,0}> main_ConstantStackPush_49(o2, env, static) :|: 0 < o2
main_ConstantStackPush_49(o2, env, static) -{1,1}> main_Store_51(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Store_51(o2, iconst_0, env, static) -{1,1}> main_Load_53(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_53(o2, iconst_0, env, static) -{1,1}> main_Load_55(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_Load_55(o2, iconst_0, env, static) -{1,1}> main_ArrayLength_57(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayLength_57(o2, iconst_0, env, static) -{0,0}> main_ArrayLength_105(o2, iconst_0, iconst_0, env, static) :|: 0 <= iconst_0 && 0 < o2 && iconst_0 <= 1 && iconst_0 = 0
main_ArrayLength_105(o10, i12, i11, env, static) -{0,0}> main_ArrayLength_172(o10, i12, i11, env, static) :|: i11 <= 2 && 0 <= i11 && i12 <= 2 && 0 <= i12 && 0 < o10 && i12 <= 1 && i11 <= 1
main_ArrayLength_172(o20, i24, i23, env, static) -{0,0}> main_ArrayLength_208(o20, i24, i23, env, static) :|: 0 <= i24 && 0 < o20 && i23 <= 2 && i24 <= 2 && 0 <= i23
main_ArrayLength_208(a27, i32, i31, env, static) -{0,0}> main_ArrayLength_213(a27, i32, i31, i36, env, static) :|: 0 <= i31 && 0 <= i36 && i36 < a27 && 0 <= i32 && 0 < a27
main_ArrayLength_213(a27, i32, i31, i36, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_220(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27 && i36 <= i32
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_221(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_GE_221(a27, i32, i36, i31, env, static) -{1,1}> main_Inc_228(a27, i31, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_Inc_228(a27, i31, i36, env, static) -{1,1}> main_JMP_232(a27, i38, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 1 <= i38 && 0 < a27 && i31 + 1 = i38
main_JMP_232(a27, i38, i36, env, static) -{1,1}> main_Load_233(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_233(a27, i38, i36, env, static) -{1,1}> main_Load_236(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_236(a27, i38, i36, env, static) -{1,1}> main_ArrayLength_238(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_ArrayLength_238(a27, i38, i36, env, static) -{0,0}> main_ArrayLength_208(a27, i38, i38, env, static) :|: 1 <= i36 && 0 <= i38 && 1 <= i38 && 0 < a27

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

obtained
main_ArrayLength_208(a27, i32, i31, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 < a27 && 0 <= i32 && i36 < a27 && 0 <= i31 && 0 <= i36
by chaining
main_ArrayLength_208(a27, i32, i31, env, static) -{0,0}> main_ArrayLength_213(a27, i32, i31, i36, env, static) :|: 0 <= i31 && 0 <= i36 && i36 < a27 && 0 <= i32 && 0 < a27
main_ArrayLength_213(a27, i32, i31, i36, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27

obtained
main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i38', i38', env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32
by chaining
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_221(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_GE_221(a27, i32, i36, i31, env, static) -{1,1}> main_Inc_228(a27, i31, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 0 <= i36 && i32 < i36 && 0 <= i32 && 0 < a27
main_Inc_228(a27, i31, i36, env, static) -{1,1}> main_JMP_232(a27, i38, i36, env, static) :|: 0 <= i31 && 1 <= i36 && 1 <= i38 && 0 < a27 && i31 + 1 = i38
main_JMP_232(a27, i38, i36, env, static) -{1,1}> main_Load_233(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_233(a27, i38, i36, env, static) -{1,1}> main_Load_236(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_Load_236(a27, i38, i36, env, static) -{1,1}> main_ArrayLength_238(a27, i38, i36, env, static) :|: 1 <= i36 && 1 <= i38 && 0 < a27
main_ArrayLength_238(a27, i38, i36, env, static) -{0,0}> main_ArrayLength_208(a27, i38, i38, env, static) :|: 1 <= i36 && 0 <= i38 && 1 <= i38 && 0 < a27

(20) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
main_ArrayLength_208(a27, i32, i31, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 < a27 && 0 <= i32 && i36 < a27 && 0 <= i31 && 0 <= i36
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_220(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27 && i36 <= i32
main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i38', i38', env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32

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

Moved arithmethic from constraints to rhss.

main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i38', i38', env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32
was transformed to
main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i31 + 1, i31 + 1, env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32

(22) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i31 + 1, i31 + 1, env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32
main_ArrayLength_208(a27, i32, i31, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 < a27 && 0 <= i32 && i36 < a27 && 0 <= i31 && 0 <= i36
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_220(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27 && i36 <= i32

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

Simplified expressions.

main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && static''' <= static + 2 && 0 <= 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 < 1 && 0 <= static'1 && 0 < 2 && 0 <= 1
was transformed to
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 <= static'1

(24) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i31 + 1, i31 + 1, env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32
main_ArrayLength_208(a27, i32, i31, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 < a27 && 0 <= i32 && i36 < a27 && 0 <= i31 && 0 <= i36
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 <= static'1
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_220(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27 && i36 <= i32

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

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

(26) Obligation:

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

(28) Obligation:

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

Moved arithmethic from constraints to rhss.

(30) Obligation:

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

Simplified expressions.

(32) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_GE_219(a27, i32, i36, i31, env, static) -{5,5}> main_ArrayLength_208(a27, i31 + 1, i31 + 1, env, static) :|: i31 + 1 = i38' && 0 < a27 && 0 <= i36 && 1 <= i38' && 0 <= i31 && 1 <= i36 && 0 <= i38' && i32 < i36 && 0 <= i32
main_ArrayLength_208(a27, i32, i31, env, static) -{1,1}> main_GE_219(a27, i32, i36, i31, env, static) :|: 0 < a27 && 0 <= i32 && i36 < a27 && 0 <= i31 && 0 <= i36
main_ConstantStackPush_2(o2, env, static) -{19,19}> main_ArrayLength_208(o2, 0, 0, env, static'1) :|: static'1 <= static''' + 1 && static''' <= static + 2 && 0 <= static''' && 0 < o2 && 0 <= static && 0 <= static'1
main_GE_219(a27, i32, i36, i31, env, static) -{0,0}> main_GE_220(a27, i32, i36, i31, env, static) :|: 0 <= i31 && 0 <= i36 && 0 <= i32 && 0 < a27 && i36 <= i32

(33) CESProof (EQUIVALENT transformation)

proved upper bound 14 + 6 * args using cofloco

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) CESProof (EQUIVALENT transformation)

(34) BOUNDS(CONSTANT, 14 + 6 * args)