time complexity proof of /tmp/tmpgb7i1S/Duplicate.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 37 + 12 * |#0| + 24 * |#1|).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 39 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 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 140 ms)

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

        ↳19 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 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 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)), 16 ms)

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

    ↳37 koat Proof (⇔, 62 ms)

    ↳38 BOUNDS(CONSTANT, 32 + 12 * |#0| + 24 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class Duplicate{

  public static int round (int x) {

    if (x % 2 == 0) return x;
    else return x+1;
  }


  public static void main(int x, int y) {

    while ((x > y) && (y > 2)) {
      x++;
      y = 2*y;

    }
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Duplicate.main(II)V: Graph of 53 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 48 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 48 jbc graph edges to a weighted ITS with 48 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 48 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_44(i2, i4, env, static) :|: 0 >= 0
main_Load_44(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{1,1}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_LE_54(i2, i4, env, static) :|: 0 >= 0
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_67(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_67(i2, i4, env, static) -{1,1}> main_LE_69(i2, i4, iconst_2, env, static) :|: iconst_2 = 2
main_LE_69(i2, i4, iconst_2, env, static) -{0,0}> main_LE_140(i2, i4, i4, iconst_2, i2, env, static) :|: iconst_2 = 2
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, iconst_2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
main_LE_140(i36, i37, i52, iconst_2, i53, env, static) -{0,0}> main_LE_150(i36, i37, i52, iconst_2, i53, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53
main_LE_150(i36, i37, i52, iconst_2, i53, env, static) -{1,1}> main_Inc_159(i36, i37, i53, i52, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53 && iconst_2 < i52
main_Inc_159(i36, i37, i53, i52, env, static) -{1,1}> main_ConstantStackPush_161(i36, i37, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && i53 + 1 = i56 && 4 <= i53
main_ConstantStackPush_161(i36, i37, i56, i52, env, static) -{1,1}> main_Load_162(i36, i37, iconst_2, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_Load_162(i36, i37, iconst_2, i56, i52, env, static) -{1,1}> main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) -{1,1}> main_Store_164(i36, i37, i57, i56, env, static) :|: iconst_2 * i52 = i57 && 3 <= i52 && 5 <= i56 && 6 <= i57 && iconst_2 = 2
main_Store_164(i36, i37, i57, i56, env, static) -{1,1}> main_JMP_165(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_JMP_165(i36, i37, i56, i57, env, static) -{1,1}> main_Load_167(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_167(i36, i37, i56, i57, env, static) -{1,1}> main_Load_170(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_170(i36, i37, i56, i57, env, static) -{1,1}> main_LE_180(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_185(i36, i37, i56, i57, env, static) :|: 5 <= i56 && i56 <= i57 && 6 <= i57
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_186(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57
main_LE_186(i36, i37, i56, i57, env, static) -{1,1}> main_Load_196(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57 && 7 <= i56
main_Load_196(i36, i37, i56, i57, env, static) -{1,1}> main_ConstantStackPush_199(i36, i37, i57, i56, env, static) :|: 6 <= i57 && 7 <= i56
main_ConstantStackPush_199(i36, i37, i57, i56, env, static) -{1,1}> main_LE_204(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56
main_LE_204(i36, i37, i57, iconst_2, i56, env, static) -{0,0}> main_LE_140(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56

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

obtained
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_44(i2, i4, env, static) :|: 0 >= 0
main_Load_44(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{1,1}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_LE_54(i2, i4, env, static) :|: 0 >= 0

obtained
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2 && 0 >= 0
by chaining
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_67(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_67(i2, i4, env, static) -{1,1}> main_LE_69(i2, i4, iconst_2, env, static) :|: iconst_2 = 2
main_LE_69(i2, i4, iconst_2, env, static) -{0,0}> main_LE_140(i2, i4, i4, iconst_2, i2, env, static) :|: iconst_2 = 2

obtained
main_LE_140(i36, i37, i52, 2, i53, env, static) -{9,9}> main_LE_180(i36, i37, i56', i57', env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57'
by chaining
main_LE_140(i36, i37, i52, iconst_2, i53, env, static) -{0,0}> main_LE_150(i36, i37, i52, iconst_2, i53, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53
main_LE_150(i36, i37, i52, iconst_2, i53, env, static) -{1,1}> main_Inc_159(i36, i37, i53, i52, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53 && iconst_2 < i52
main_Inc_159(i36, i37, i53, i52, env, static) -{1,1}> main_ConstantStackPush_161(i36, i37, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && i53 + 1 = i56 && 4 <= i53
main_ConstantStackPush_161(i36, i37, i56, i52, env, static) -{1,1}> main_Load_162(i36, i37, iconst_2, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_Load_162(i36, i37, iconst_2, i56, i52, env, static) -{1,1}> main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) -{1,1}> main_Store_164(i36, i37, i57, i56, env, static) :|: iconst_2 * i52 = i57 && 3 <= i52 && 5 <= i56 && 6 <= i57 && iconst_2 = 2
main_Store_164(i36, i37, i57, i56, env, static) -{1,1}> main_JMP_165(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_JMP_165(i36, i37, i56, i57, env, static) -{1,1}> main_Load_167(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_167(i36, i37, i56, i57, env, static) -{1,1}> main_Load_170(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_170(i36, i37, i56, i57, env, static) -{1,1}> main_LE_180(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57

obtained
main_LE_180(i36, i37, i56, i57, env, static) -{3,3}> main_LE_140(i36, i37, i57, 2, i56, env, static) :|: 5 <= i56 && 7 <= i56 && 6 <= i57 && i57 < i56
by chaining
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_186(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57
main_LE_186(i36, i37, i56, i57, env, static) -{1,1}> main_Load_196(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57 && 7 <= i56
main_Load_196(i36, i37, i56, i57, env, static) -{1,1}> main_ConstantStackPush_199(i36, i37, i57, i56, env, static) :|: 6 <= i57 && 7 <= i56
main_ConstantStackPush_199(i36, i37, i57, i56, env, static) -{1,1}> main_LE_204(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56
main_LE_204(i36, i37, i57, iconst_2, i56, env, static) -{0,0}> main_LE_140(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56

(8) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2 && 0 >= 0
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, iconst_2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
main_LE_140(i36, i37, i52, 2, i53, env, static) -{9,9}> main_LE_180(i36, i37, i56', i57', env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57'
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_185(i36, i37, i56, i57, env, static) :|: 5 <= i56 && i56 <= i57 && 6 <= i57
main_LE_180(i36, i37, i56, i57, env, static) -{3,3}> main_LE_140(i36, i37, i57, 2, i56, env, static) :|: 5 <= i56 && 7 <= i56 && 6 <= i57 && i57 < i56

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

Moved arithmethic from lhss to constraints.

main_LE_140(i36, i37, i52, 2, i53, env, static) -{9,9}> main_LE_180(i36, i37, i56', i57', env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57'
was transformed to
main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i56', i57', env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2

(10) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i56', i57', env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2 && 0 >= 0
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, iconst_2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
main_LE_180(i36, i37, i56, i57, env, static) -{3,3}> main_LE_140(i36, i37, i57, 2, i56, env, static) :|: 5 <= i56 && 7 <= i56 && 6 <= i57 && i57 < i56
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_185(i36, i37, i56, i57, env, static) :|: 5 <= i56 && i56 <= i57 && 6 <= i57

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

Moved arithmethic from constraints to rhss.

main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, iconst_2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
was transformed to
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, 2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2

main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i56', i57', env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2
was transformed to
main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i53 + 1, 2 * i52, env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2

(12) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2 && 0 >= 0
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, 2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
main_LE_180(i36, i37, i56, i57, env, static) -{3,3}> main_LE_140(i36, i37, i57, 2, i56, env, static) :|: 5 <= i56 && 7 <= i56 && 6 <= i57 && i57 < i56
main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i53 + 1, 2 * i52, env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_185(i36, i37, i56, i57, env, static) :|: 5 <= i56 && i56 <= i57 && 6 <= i57

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

Simplified expressions.

main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2 && 0 >= 0
was transformed to
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2

(14) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, 2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i53 + 1, 2 * i52, env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2
main_LE_180(i36, i37, i56, i57, env, static) -{3,3}> main_LE_140(i36, i37, i57, 2, i56, env, static) :|: 5 <= i56 && 7 <= i56 && 6 <= i57 && i57 < i56
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_185(i36, i37, i56, i57, env, static) :|: 5 <= i56 && i56 <= i57 && 6 <= i57

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

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

IntTrs with 7 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_1(i2, i4, env, static) -{17,17}> main_LE_54(i2, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
main_LE_54(i2, i4, env, static) -{3,3}> main_LE_140(i2, i4, i4, 2, i2, env, static) :|: i4 < i2 && 0 >= 0
main_LE_140(i36, i37, i51, iconst_2, i38, env, static) -{0,0}> main_LE_149(i36, i37, i51, 2, i38, env, static) :|: i51 <= 2 && iconst_2 = 2
main_LE_180(i36, i37, i56, i57, env, static) -{3,3}> main_LE_140(i36, i37, i57, 2, i56, env, static) :|: 5 <= i56 && 7 <= i56 && 6 <= i57 && i57 < i56
main_LE_140(i36, i37, i52, x, i53, env, static) -{9,9}> main_LE_180(i36, i37, i53 + 1, 2 * i52, env, static) :|: i53 + 1 = i56' && 5 <= i56' && 6 <= i57' && 3 <= i52 && 4 <= i53 && 2 < i52 && 2 * i52 = i57' && x = 2
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_56(i2, i4, env, static) :|: i2 <= i4
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_185(i36, i37, i56, i57, env, static) :|: 5 <= i56 && i56 <= i57 && 6 <= i57

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

Simplified expressions.

(24) Obligation:

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

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

(26) Obligation:

Set of 45 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 45 jbc graph edges to a weighted ITS with 45 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 45 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_44(i2, i4, env, static) :|: 0 >= 0
main_Load_44(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{1,1}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_LE_54(i2, i4, env, static) :|: 0 >= 0
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_67(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_67(i2, i4, env, static) -{1,1}> main_LE_69(i2, i4, iconst_2, env, static) :|: iconst_2 = 2
main_LE_69(i2, i4, iconst_2, env, static) -{0,0}> main_LE_140(i2, i4, i4, iconst_2, i2, env, static) :|: iconst_2 = 2
main_LE_140(i36, i37, i52, iconst_2, i53, env, static) -{0,0}> main_LE_150(i36, i37, i52, iconst_2, i53, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53
main_LE_150(i36, i37, i52, iconst_2, i53, env, static) -{1,1}> main_Inc_159(i36, i37, i53, i52, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53 && iconst_2 < i52
main_Inc_159(i36, i37, i53, i52, env, static) -{1,1}> main_ConstantStackPush_161(i36, i37, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && i53 + 1 = i56 && 4 <= i53
main_ConstantStackPush_161(i36, i37, i56, i52, env, static) -{1,1}> main_Load_162(i36, i37, iconst_2, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_Load_162(i36, i37, iconst_2, i56, i52, env, static) -{1,1}> main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) -{1,1}> main_Store_164(i36, i37, i57, i56, env, static) :|: iconst_2 * i52 = i57 && 3 <= i52 && 5 <= i56 && 6 <= i57 && iconst_2 = 2
main_Store_164(i36, i37, i57, i56, env, static) -{1,1}> main_JMP_165(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_JMP_165(i36, i37, i56, i57, env, static) -{1,1}> main_Load_167(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_167(i36, i37, i56, i57, env, static) -{1,1}> main_Load_170(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_170(i36, i37, i56, i57, env, static) -{1,1}> main_LE_180(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_186(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57
main_LE_186(i36, i37, i56, i57, env, static) -{1,1}> main_Load_196(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57 && 7 <= i56
main_Load_196(i36, i37, i56, i57, env, static) -{1,1}> main_ConstantStackPush_199(i36, i37, i57, i56, env, static) :|: 6 <= i57 && 7 <= i56
main_ConstantStackPush_199(i36, i37, i57, i56, env, static) -{1,1}> main_LE_204(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56
main_LE_204(i36, i37, i57, iconst_2, i56, env, static) -{0,0}> main_LE_140(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56

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

obtained
main_Load_1(i2, i4, env, static) -{20,20}> main_LE_140(i2, i4, i4, 2, i2, env, static'1) :|: static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 < i2
by chaining
main_Load_1(i2, i4, env, static) -{0,0}> main_Load_3(i2, i4, env, static) :|: 0 >= 0
main_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i4, env, static) -{1,1}> main_Load_41(i2, i4, env, static) :|: 0 >= 0
main_Load_41(i2, i4, env, static) -{0,0}> main_Load_42(i2, i4, env, static) :|: 0 >= 0
main_Load_42(i2, i4, env, static) -{0,0}> main_Load_43(i2, i4, env, static) :|: 0 <= static
main_Load_43(i2, i4, env, static) -{0,0}> main_Load_44(i2, i4, env, static) :|: 0 >= 0
main_Load_44(i2, i4, env, static) -{0,0}> main_Load_45(i2, i4, env, static) :|: 0 >= 0
main_Load_45(i2, i4, env, static) -{1,1}> main_Load_47(i2, i4, env, static) :|: 0 >= 0
main_Load_47(i2, i4, env, static) -{1,1}> main_LE_54(i2, i4, env, static) :|: 0 >= 0
main_LE_54(i2, i4, env, static) -{0,0}> main_LE_57(i2, i4, env, static) :|: i4 < i2
main_LE_57(i2, i4, env, static) -{1,1}> main_Load_63(i2, i4, env, static) :|: i4 < i2
main_Load_63(i2, i4, env, static) -{1,1}> main_ConstantStackPush_67(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_67(i2, i4, env, static) -{1,1}> main_LE_69(i2, i4, iconst_2, env, static) :|: iconst_2 = 2
main_LE_69(i2, i4, iconst_2, env, static) -{0,0}> main_LE_140(i2, i4, i4, iconst_2, i2, env, static) :|: iconst_2 = 2

obtained
main_LE_140(i36, i37, i52, 2, i53, env, static) -{12,12}> main_LE_140(i36, i37, i57', 2, i56', env, static) :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'
by chaining
main_LE_140(i36, i37, i52, iconst_2, i53, env, static) -{0,0}> main_LE_150(i36, i37, i52, iconst_2, i53, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53
main_LE_150(i36, i37, i52, iconst_2, i53, env, static) -{1,1}> main_Inc_159(i36, i37, i53, i52, env, static) :|: 3 <= i52 && iconst_2 = 2 && 4 <= i53 && iconst_2 < i52
main_Inc_159(i36, i37, i53, i52, env, static) -{1,1}> main_ConstantStackPush_161(i36, i37, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && i53 + 1 = i56 && 4 <= i53
main_ConstantStackPush_161(i36, i37, i56, i52, env, static) -{1,1}> main_Load_162(i36, i37, iconst_2, i56, i52, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_Load_162(i36, i37, iconst_2, i56, i52, env, static) -{1,1}> main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) :|: 3 <= i52 && 5 <= i56 && iconst_2 = 2
main_IntArithmetic_163(i36, i37, iconst_2, i52, i56, env, static) -{1,1}> main_Store_164(i36, i37, i57, i56, env, static) :|: iconst_2 * i52 = i57 && 3 <= i52 && 5 <= i56 && 6 <= i57 && iconst_2 = 2
main_Store_164(i36, i37, i57, i56, env, static) -{1,1}> main_JMP_165(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_JMP_165(i36, i37, i56, i57, env, static) -{1,1}> main_Load_167(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_167(i36, i37, i56, i57, env, static) -{1,1}> main_Load_170(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_Load_170(i36, i37, i56, i57, env, static) -{1,1}> main_LE_180(i36, i37, i56, i57, env, static) :|: 5 <= i56 && 6 <= i57
main_LE_180(i36, i37, i56, i57, env, static) -{0,0}> main_LE_186(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57
main_LE_186(i36, i37, i56, i57, env, static) -{1,1}> main_Load_196(i36, i37, i56, i57, env, static) :|: i57 < i56 && 5 <= i56 && 6 <= i57 && 7 <= i56
main_Load_196(i36, i37, i56, i57, env, static) -{1,1}> main_ConstantStackPush_199(i36, i37, i57, i56, env, static) :|: 6 <= i57 && 7 <= i56
main_ConstantStackPush_199(i36, i37, i57, i56, env, static) -{1,1}> main_LE_204(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56
main_LE_204(i36, i37, i57, iconst_2, i56, env, static) -{0,0}> main_LE_140(i36, i37, i57, iconst_2, i56, env, static) :|: 6 <= i57 && iconst_2 = 2 && 7 <= i56

(30) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, env, static) -{20,20}> main_LE_140(i2, i4, i4, 2, i2, env, static'1) :|: static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 < i2
main_LE_140(i36, i37, i52, 2, i53, env, static) -{12,12}> main_LE_140(i36, i37, i57', 2, i56', env, static) :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'

(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_Load_1(x1, x2, x3, x4) → main_Load_1(x1, x2, x4)
main_LE_140(x1, x2, x3, x4, x5, x6, x7) → main_LE_140(x3, x5)

(32) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, static) -{20,20}> main_LE_140(i4, i2) :|: static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 < i2
main_LE_140(i52, i53) -{12,12}> main_LE_140(i57', i56') :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'

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

Moved arithmethic from constraints to rhss.

main_LE_140(i52, i53) -{12,12}> main_LE_140(i57', i56') :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'
was transformed to
main_LE_140(i52, i53) -{12,12}> main_LE_140(2 * i52, i53 + 1) :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'

(34) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_LE_140(i52, i53) -{12,12}> main_LE_140(2 * i52, i53 + 1) :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'
main_Load_1(i2, i4, static) -{20,20}> main_LE_140(i4, i2) :|: static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 < i2

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

Simplified expressions.

main_Load_1(i2, i4, static) -{20,20}> main_LE_140(i4, i2) :|: static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && i4 < i2
was transformed to
main_Load_1(i2, i4, static) -{20,20}> main_LE_140(i4, i2) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 < i2

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_1(i2, i4, static) -{20,20}> main_LE_140(i4, i2) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 < i2
main_LE_140(i52, i53) -{12,12}> main_LE_140(2 * i52, i53 + 1) :|: 2 * i52 = i57' && 7 <= i56' && 2 < i52 && 6 <= i57' && 5 <= i56' && i57' < i56' && 4 <= i53 && 3 <= i52 && i53 + 1 = i56'

(37) koat Proof (EQUIVALENT transformation)

YES(?, 12*ar_0 + 24*ar_1 + 32)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 20) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(ar_1, ar_0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 12) main_LE_140(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(2*ar_0, ar_1 + 1, arityPad)) [ 2*ar_0 = i57' /\ 7 <= i56' /\ 2 < ar_0 /\ 6 <= i57' /\ 5 <= i56' /\ i57' < i56' /\ 4 <= ar_1 /\ 3 <= ar_0 /\ ar_1 + 1 = i56' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(ar_1, ar_0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 12) main_LE_140(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(2*ar_0, ar_1 + 1, arityPad)) [ 2*ar_0 = i57' /\ 7 <= i56' /\ 2 < ar_0 /\ 6 <= i57' /\ 5 <= i56' /\ i57' < i56' /\ 4 <= ar_1 /\ 3 <= ar_0 /\ ar_1 + 1 = i56' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_Load_1) = V_1 - 2*V_2 + 1
Pol(main_LE_140) = -2*V_1 + V_2 + 1
Pol(koat_start) = V_1 - 2*V_2 + 1
orients all transitions weakly and the transition
main_LE_140(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(2*ar_0, ar_1 + 1, arityPad)) [ 2*ar_0 = i57' /\ 7 <= i56' /\ 2 < ar_0 /\ 6 <= i57' /\ 5 <= i56' /\ i57' < i56' /\ 4 <= ar_1 /\ 3 <= ar_0 /\ ar_1 + 1 = i56' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 20) main_Load_1(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(ar_1, ar_0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 < ar_0 ]
(Comp: ar_0 + 2*ar_1 + 1, Cost: 12) main_LE_140(ar_0, ar_1, ar_2) -> Com_1(main_LE_140(2*ar_0, ar_1 + 1, arityPad)) [ 2*ar_0 = i57' /\ 7 <= i56' /\ 2 < ar_0 /\ 6 <= i57' /\ 5 <= i56' /\ i57' < i56' /\ 4 <= ar_1 /\ 3 <= ar_0 /\ ar_1 + 1 = i56' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(main_Load_1(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 12*ar_0 + 24*ar_1 + 32

Time: 0.108 sec (SMT: 0.100 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(16) Obligation:

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

(18) Obligation:

(19) MovedArithmeticToConstraintsProof (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) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

(37) koat Proof (EQUIVALENT transformation)

(38) BOUNDS(CONSTANT, 32 + 12 * |#0| + 24 * |#1|)