time complexity proof of /tmp/tmpFOGRLQ/StupidArray.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

        ↳13 CESProof (⇔, 18 ms)

        ↳14 BOUNDS(CONSTANT, 40)

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 80 ms)

    ↳16 WeightedIntTrs

        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 38 ms)

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

        ↳23 koat Proof (⇔, 6 ms)

        ↳24 BOUNDS(CONSTANT, 40)

↳25 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)), 0 ms)

↳26 JBCComplexityEdges

    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 80 ms)

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

    ↳31 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 23 ms)

    ↳32 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class StupidArray {
  public static void main(String[] args) {
    int i = 0;
    while (true) {
      i = args.length + 1;
      args[i] = new String();
    }
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 57 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 57 jbc graph edges to a weighted ITS with 57 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 57 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o1, env, static) -{0,0}> main_ConstantStackPush_3(o1, env, static) :|: 0 < o1
main_ConstantStackPush_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_13(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_15(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_17(o1, env, static) -{0,0}> langle_clinit_rangle_New_18(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_18(o1, env, static) -{0,0}> langle_clinit_rangle_New_20(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_20(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_21(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_23(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_29(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_31(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_34(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_36(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_36(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_38(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_39(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_ConstantStackPush_46(o1, env, static) :|: 0 < o1
main_ConstantStackPush_46(o1, env, static) -{0,0}> main_ConstantStackPush_48(o1, env, static) :|: 0 < o1
main_ConstantStackPush_48(o1, env, static) -{0,0}> main_ConstantStackPush_49(o1, env, static) :|: 0 <= static && 0 < o1
main_ConstantStackPush_49(o1, env, static) -{0,0}> main_ConstantStackPush_50(o1, env, static) :|: 0 < o1
main_ConstantStackPush_50(o1, env, static) -{0,0}> main_ConstantStackPush_51(o1, env, static) :|: 0 < o1
main_ConstantStackPush_51(o1, env, static) -{1,1}> main_Store_52(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
main_Store_52(o1, iconst_0, env, static) -{1,1}> main_Load_53(o1, env, static) :|: iconst_0 = 0 && 0 < o1
main_Load_53(o1, env, static) -{1,1}> main_ArrayLength_55(o1, env, static) :|: 0 < o1
main_ArrayLength_55(o1, env, static) -{0,0}> main_ArrayLength_138(o1, env, static) :|: 0 < o1
main_ArrayLength_138(a16, env, static) -{0,0}> main_ArrayLength_142(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_142(a16, i8, env, static) -{1,1}> main_ConstantStackPush_144(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_144(a16, i8, env, static) -{1,1}> main_IntArithmetic_146(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_146(a16, i8, iconst_1, env, static) -{1,1}> main_Store_148(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_148(a16, i9, i8, env, static) -{1,1}> main_Load_149(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_149(a16, i9, i8, env, static) -{1,1}> main_Load_150(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_150(a16, i9, i8, env, static) -{1,1}> main_New_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_151(a16, i9, i8, env, static) -{1,1}> main_Duplicate_152(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_152(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_154(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_154(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_185(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_185(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_187(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_189(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_190(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_189(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_198(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_198(a21, i8, env, static) -{1,1}> main_Load_204(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_204(a21, i8, env, static) -{1,1}> main_ArrayLength_210(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_210(a21, i8, env, static) -{0,0}> main_ArrayLength_138(a21, env, static) :|: 0 < a21 && 0 <= i8

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

obtained
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_ConstantStackPush_2(o1, env, static) -{0,0}> main_ConstantStackPush_3(o1, env, static) :|: 0 < o1
main_ConstantStackPush_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_13(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_15(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_17(o1, env, static) -{0,0}> langle_clinit_rangle_New_18(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_18(o1, env, static) -{0,0}> langle_clinit_rangle_New_20(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_20(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_21(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_23(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_29(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_31(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_34(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_36(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_36(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_38(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_39(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_ConstantStackPush_46(o1, env, static) :|: 0 < o1
main_ConstantStackPush_46(o1, env, static) -{0,0}> main_ConstantStackPush_48(o1, env, static) :|: 0 < o1
main_ConstantStackPush_48(o1, env, static) -{0,0}> main_ConstantStackPush_49(o1, env, static) :|: 0 <= static && 0 < o1
main_ConstantStackPush_49(o1, env, static) -{0,0}> main_ConstantStackPush_50(o1, env, static) :|: 0 < o1
main_ConstantStackPush_50(o1, env, static) -{0,0}> main_ConstantStackPush_51(o1, env, static) :|: 0 < o1
main_ConstantStackPush_51(o1, env, static) -{1,1}> main_Store_52(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
main_Store_52(o1, iconst_0, env, static) -{1,1}> main_Load_53(o1, env, static) :|: iconst_0 = 0 && 0 < o1
main_Load_53(o1, env, static) -{1,1}> main_ArrayLength_55(o1, env, static) :|: 0 < o1
main_ArrayLength_55(o1, env, static) -{0,0}> main_ArrayLength_138(o1, env, static) :|: 0 < o1

obtained
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i9', 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
by chaining
main_ArrayLength_138(a16, env, static) -{0,0}> main_ArrayLength_142(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_142(a16, i8, env, static) -{1,1}> main_ConstantStackPush_144(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_144(a16, i8, env, static) -{1,1}> main_IntArithmetic_146(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_146(a16, i8, iconst_1, env, static) -{1,1}> main_Store_148(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_148(a16, i9, i8, env, static) -{1,1}> main_Load_149(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_149(a16, i9, i8, env, static) -{1,1}> main_Load_150(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_150(a16, i9, i8, env, static) -{1,1}> main_New_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_151(a16, i9, i8, env, static) -{1,1}> main_Duplicate_152(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_152(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_154(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_154(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_185(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_185(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_187(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8

obtained
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_138(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
by chaining
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_189(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_189(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_198(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_198(a21, i8, env, static) -{1,1}> main_Load_204(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_204(a21, i8, env, static) -{1,1}> main_ArrayLength_210(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_210(a21, i8, env, static) -{0,0}> main_ArrayLength_138(a21, env, static) :|: 0 < a21 && 0 <= i8

(8) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i9', 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_190(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_138(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21

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

Moved arithmethic from constraints to rhss.

main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i9', 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
was transformed to
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16

(10) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_138(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_190(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16

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

Simplified expressions.

main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1

main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16
was transformed to
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 1 <= i9' && i8 < a16

(12) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_138(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_190(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 1 <= i9' && i8 < a16

(13) CESProof (EQUIVALENT transformation)

proved upper bound 40 using cofloco

(14) BOUNDS(CONSTANT, 40)

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from constraints to rhss.

(20) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_138(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_190(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 0 < 2 && 0 < 1 && 1 <= i9' && i8 < a16

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

Simplified expressions.

(22) Obligation:

IntTrs with 4 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 <= static''' && 0 <= static && static''' <= static + 2 && static'1 <= static''' + 1
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{3,3}> main_ArrayLength_138(a21''', env, static) :|: i9 < i8 && 0 < a21''' && 0 <= i8 && a21''' <= a21 + o17 && 1 <= i9 && 0 < o17 && 0 < a21
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_190(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayLength_138(a16, env, static) -{22,22}> main_ArrayAccess_187(a16, i8 + 1, 1, i8, env, static) :|: i8 + 1 = i9' && 0 <= i8 && 0 < a16 && 1 <= i9' && i8 < a16

(23) koat Proof (EQUIVALENT transformation)

YES(?, 40)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayLength_138(ar_0, ar_1, static'1, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 0 <= static'1 /\ 0 <= static''' /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) main_ArrayAccess_187(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayLength_138(a21''', ar_4, ar_5, arityPad, arityPad, arityPad)) [ ar_1 < ar_3 /\ 0 < a21''' /\ 0 <= ar_3 /\ a21''' <= ar_0 + ar_2 /\ 1 <= ar_1 /\ 0 < ar_2 /\ 0 < ar_0 ]
(Comp: ?, Cost: 0) main_ArrayAccess_187(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayAccess_190(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 22) main_ArrayLength_138(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayAccess_187(ar_0, i8 + 1, 1, i8, ar_1, ar_2)) [ i8 + 1 = i9' /\ 0 <= i8 /\ 0 < ar_0 /\ 1 <= i9' /\ i8 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 1:
main_ArrayAccess_187(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayLength_138(a21''', ar_4, ar_5, arityPad, arityPad, arityPad)) [ ar_1 < ar_3 /\ 0 < a21''' /\ 0 <= ar_3 /\ a21''' <= ar_0 + ar_2 /\ 1 <= ar_1 /\ 0 < ar_2 /\ 0 < ar_0 ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 0) main_ArrayAccess_187(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayAccess_190(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 22) main_ArrayLength_138(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayAccess_187(ar_0, i8 + 1, 1, i8, ar_1, ar_2)) [ i8 + 1 = i9' /\ 0 <= i8 /\ 0 < ar_0 /\ 1 <= i9' /\ i8 < ar_0 ]
(Comp: ?, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayLength_138(ar_0, ar_1, static'1, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 0 <= static'1 /\ 0 <= static''' /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: 1, Cost: 0) main_ArrayAccess_187(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayAccess_190(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 < ar_2 /\ 1 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_3 ]
(Comp: 1, Cost: 22) main_ArrayLength_138(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayAccess_187(ar_0, i8 + 1, 1, i8, ar_1, ar_2)) [ i8 + 1 = i9' /\ 0 <= i8 /\ 0 < ar_0 /\ 1 <= i9' /\ i8 < ar_0 ]
(Comp: 1, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ArrayLength_138(ar_0, ar_1, static'1, arityPad, arityPad, arityPad)) [ 0 < ar_0 /\ 0 <= static'1 /\ 0 <= static''' /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 40

Time: 0.134 sec (SMT: 0.130 sec)

(24) BOUNDS(CONSTANT, 40)

(25) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(23)) transformation)

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

(28) Obligation:

IntTrs with 56 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o1, env, static) -{0,0}> main_ConstantStackPush_3(o1, env, static) :|: 0 < o1
main_ConstantStackPush_3(o1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(o1, env, static) :|: 0 < o1
langle_clinit_rangle_ConstantStackPush_5(o1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o1, env, static) :|: iconst_0 = 0 && 0 < o1
langle_clinit_rangle_ArrayCreate_13(iconst_0, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_15(a2, o1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2 && 0 < o1
langle_clinit_rangle_FieldAccess_15(a2, o1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(o1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2 && 0 < o1
langle_clinit_rangle_New_17(o1, env, static) -{0,0}> langle_clinit_rangle_New_18(o1, env, static) :|: 0 < o1
langle_clinit_rangle_New_18(o1, env, static) -{0,0}> langle_clinit_rangle_New_20(o1, env, static) :|: 0 <= static && 0 < o1
langle_clinit_rangle_New_20(o1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o4, o1, env, static) :|: o4 = 1 && 0 < o4 && 0 < o1
langle_clinit_rangle_Duplicate_21(o4, o1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_23(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_ConstantStackPush_23(o4, o1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o4, NULL, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_clinit_rangle_InvokeMethod_25(o4, NULL, o1, env, static) -{1,1}> langle_init_rangle_Load_27(o4, o1, env, static) :|: NULL = 0 && 0 < o4 && 0 < o1
langle_init_rangle_Load_27(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_29(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_29(o4, o1, env, static) -{1,1}> langle_init_rangle_Load_31(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Load_31(o4, o1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_34(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_InvokeMethod_34(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_36(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_36(o4, o1, env, static) -{1,1}> langle_init_rangle_Return_38(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_init_rangle_Return_38(o4, o1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o4, o1, env, static) :|: 0 < o4 && 0 < o1
langle_clinit_rangle_FieldAccess_39(o4, o1, env, static) -{1,1}> langle_clinit_rangle_Return_40(o1, env, static') :|: 0 <= o4 && 0 < o4 && 0 <= static && 0 < o1 && static' <= static + o4
langle_clinit_rangle_Return_40(o1, env, static) -{1,1}> main_ConstantStackPush_46(o1, env, static) :|: 0 < o1
main_ConstantStackPush_46(o1, env, static) -{0,0}> main_ConstantStackPush_48(o1, env, static) :|: 0 < o1
main_ConstantStackPush_48(o1, env, static) -{0,0}> main_ConstantStackPush_49(o1, env, static) :|: 0 <= static && 0 < o1
main_ConstantStackPush_49(o1, env, static) -{0,0}> main_ConstantStackPush_50(o1, env, static) :|: 0 < o1
main_ConstantStackPush_50(o1, env, static) -{0,0}> main_ConstantStackPush_51(o1, env, static) :|: 0 < o1
main_ConstantStackPush_51(o1, env, static) -{1,1}> main_Store_52(o1, iconst_0, env, static) :|: iconst_0 = 0 && 0 < o1
main_Store_52(o1, iconst_0, env, static) -{1,1}> main_Load_53(o1, env, static) :|: iconst_0 = 0 && 0 < o1
main_Load_53(o1, env, static) -{1,1}> main_ArrayLength_55(o1, env, static) :|: 0 < o1
main_ArrayLength_55(o1, env, static) -{0,0}> main_ArrayLength_138(o1, env, static) :|: 0 < o1
main_ArrayLength_138(a16, env, static) -{0,0}> main_ArrayLength_142(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_142(a16, i8, env, static) -{1,1}> main_ConstantStackPush_144(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_144(a16, i8, env, static) -{1,1}> main_IntArithmetic_146(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_146(a16, i8, iconst_1, env, static) -{1,1}> main_Store_148(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_148(a16, i9, i8, env, static) -{1,1}> main_Load_149(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_149(a16, i9, i8, env, static) -{1,1}> main_Load_150(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_150(a16, i9, i8, env, static) -{1,1}> main_New_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_151(a16, i9, i8, env, static) -{1,1}> main_Duplicate_152(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_152(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_154(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_154(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_185(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_185(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_187(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_189(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_189(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_198(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_198(a21, i8, env, static) -{1,1}> main_Load_204(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_204(a21, i8, env, static) -{1,1}> main_ArrayLength_210(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_210(a21, i8, env, static) -{0,0}> main_ArrayLength_138(a21, env, static) :|: 0 < a21 && 0 <= i8

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

obtained
main_ArrayLength_138(a16, env, static) -{25,25}> main_ArrayLength_138(a21''', env, static) :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'
by chaining
main_ArrayLength_138(a16, env, static) -{0,0}> main_ArrayLength_142(a16, i8, env, static) :|: 0 < a16 && 0 <= i8 && i8 < a16
main_ArrayLength_142(a16, i8, env, static) -{1,1}> main_ConstantStackPush_144(a16, i8, env, static) :|: 0 < a16 && 0 <= i8
main_ConstantStackPush_144(a16, i8, env, static) -{1,1}> main_IntArithmetic_146(a16, i8, iconst_1, env, static) :|: 0 < a16 && iconst_1 = 1 && 0 <= i8
main_IntArithmetic_146(a16, i8, iconst_1, env, static) -{1,1}> main_Store_148(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && iconst_1 = 1 && 0 <= i8 && i8 + iconst_1 = i9
main_Store_148(a16, i9, i8, env, static) -{1,1}> main_Load_149(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_149(a16, i9, i8, env, static) -{1,1}> main_Load_150(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_Load_150(a16, i9, i8, env, static) -{1,1}> main_New_151(a16, i9, i8, env, static) :|: 0 < a16 && 1 <= i9 && 0 <= i8
main_New_151(a16, i9, i8, env, static) -{1,1}> main_Duplicate_152(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && o17 = 1 && 0 <= i8
main_Duplicate_152(a16, i9, o17, i8, env, static) -{1,1}> main_InvokeMethod_154(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_InvokeMethod_154(a16, i9, o17, i8, env, static) -{1,1}> langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_156(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_InvokeMethod_158(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_Load_160(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_161(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_164(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_166(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_168(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_FieldAccess_170(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Load_173(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
langle_init_rangle_ConstantStackPush_174(o17, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_ArrayCreate_176(o17, iconst_0, a16, i9, i8, env, static) -{1,1}> langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) :|: 0 < a16 && 0 < o17 && a18 = 2 && 1 <= i9 && iconst_0 = 0 && 0 < a18 && 0 <= i8
langle_init_rangle_FieldAccess_178(o17, a18, a16, i9, iconst_0, i8, env, static) -{1,1}> langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 < a18 && iconst_0 = 0 && 0 <= i8
langle_init_rangle_Return_183(a16, i9, o17, i8, env, static) -{1,1}> main_ArrayAccess_185(a16, i9, o17, i8, env, static) :|: 0 < a16 && 0 < o17 && 1 <= i9 && 0 <= i8
main_ArrayAccess_185(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_187(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_187(a21, i9, o17, i8, env, static) -{0,0}> main_ArrayAccess_189(a21, i9, o17, i8, env, static) :|: 0 < o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_ArrayAccess_189(a21, i9, o17, i8, env, static) -{1,1}> main_JMP_198(a21', i8, env, static) :|: 0 < a21' && i9 < i8 && 0 < o17 && a21' <= a21 + o17 && 1 <= i9 && 0 < a21 && 0 <= i8
main_JMP_198(a21, i8, env, static) -{1,1}> main_Load_204(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_Load_204(a21, i8, env, static) -{1,1}> main_ArrayLength_210(a21, i8, env, static) :|: 0 < a21 && 0 <= i8
main_ArrayLength_210(a21, i8, env, static) -{0,0}> main_ArrayLength_138(a21, env, static) :|: 0 < a21 && 0 <= i8

(30) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o1, env, static) -{18,18}> main_ArrayLength_138(o1, env, static'1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayLength_138(a16, env, static) -{25,25}> main_ArrayLength_138(a21''', env, static) :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'

(31) 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_138(x1, x2, x3) → main_ArrayLength_138(x1)

(32) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(o1, static) -{18,18}> main_ArrayLength_138(o1) :|: 0 < o1 && 0 <= static'1 && 0 < 1 && 0 <= 1 && 0 < 2 && 0 <= static''' && 0 <= static && static''' <= static + 2 && 0 <= 2 && static'1 <= static''' + 1
main_ArrayLength_138(a16) -{25,25}> main_ArrayLength_138(a21''') :|: i9' < i8 && 0 < a21''' && 0 <= i8 && i8 < a16 && a21''' <= a16 + 1 && 1 <= i9' && 0 < 1 && 0 < a16 && 0 < 2 && i8 + 1 = i9'