The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, 30 + 14 * |#0|).

(0) Obligation:

Need to prove time_complexity of the following program:

public class DivMinus {
  public static int div(int x, int y) {
    int res = 0;
    while (x >= y && y > 0) {
      x = x-y;
      res = res + 1;
    }
    return res;
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
DivMinus.div(II)I: Graph of 62 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 53 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 53 jbc graph edges to a weighted ITS with 53 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 53 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{0,0}> div_ConstantStackPush_4(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(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}> div_ConstantStackPush_41(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i4, env, static) -{0,0}> div_ConstantStackPush_42(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i4, env, static) -{0,0}> div_ConstantStackPush_43(i2, i4, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i4, env, static) -{0,0}> div_ConstantStackPush_45(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i4, env, static) -{0,0}> div_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_47(i2, i4, env, static) -{1,1}> div_Store_50(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Store_50(i2, i4, iconst_0, env, static) -{1,1}> div_Load_51(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i4, iconst_0, env, static) -{1,1}> div_Load_53(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_53(i2, i4, iconst_0, env, static) -{1,1}> div_LT_70(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_82(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_LT_82(i2, i4, iconst_0, env, static) -{1,1}> div_Load_84(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_Load_84(i2, i4, iconst_0, env, static) -{1,1}> div_LE_86(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LE_86(i2, i4, iconst_0, env, static) -{0,0}> div_LE_187(i2, i4, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_LE_187(i31, i32, i33, i34, env, static) -{0,0}> div_LE_249(i31, i32, i33, i34, env, static) :|: i34 <= 2 && i34 <= 1 && 0 <= i34
div_LE_249(i61, i62, i63, i64, env, static) -{0,0}> div_LE_311(i61, i62, i63, i64, env, static) :|: i64 <= 2 && 0 <= i64
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LE_311(i105, i104, i106, i94, env, static) -{0,0}> div_LE_315(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_LE_315(i105, i104, i106, i94, env, static) -{1,1}> div_Load_318(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 < i104 && 1 <= i104 && 1 <= i105
div_Load_318(i105, i104, i106, i94, env, static) -{1,1}> div_Load_320(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_Load_320(i105, i104, i106, i94, env, static) -{1,1}> div_IntArithmetic_323(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_IntArithmetic_323(i105, i104, i106, i94, env, static) -{1,1}> div_Store_328(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 <= i109 && 1 <= i104 && i106 - i104 = i109 && 1 <= i105
div_Store_328(i105, i104, i109, i94, env, static) -{1,1}> div_Load_331(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_Load_331(i105, i104, i109, i94, env, static) -{1,1}> div_ConstantStackPush_332(i105, i104, i94, i109, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_ConstantStackPush_332(i105, i104, i94, i109, env, static) -{1,1}> div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) :|: 0 <= i94 && 0 <= i109 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) -{1,1}> div_Store_334(i105, i104, i110, i109, env, static) :|: 0 <= i94 && i94 + iconst_1 = i110 && 0 <= i109 && 1 <= i110 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_Store_334(i105, i104, i110, i109, env, static) -{1,1}> div_JMP_336(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_JMP_336(i105, i104, i109, i110, env, static) -{1,1}> div_Load_338(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_338(i105, i104, i109, i110, env, static) -{1,1}> div_Load_341(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_341(i105, i104, i109, i110, env, static) -{1,1}> div_LT_359(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_368(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_LT_368(i105, i104, i109, i110, env, static) -{1,1}> div_Load_373(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i109 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_Load_373(i105, i104, i109, i110, env, static) -{1,1}> div_LE_413(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 1 <= i104 && 1 <= i105
div_LE_413(i105, i104, i109, i110, env, static) -{0,0}> div_LE_311(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 0 <= i110 && 1 <= i104 && 1 <= i105

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

obtained
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_ConstantStackPush_2(i2, i4, env, static) -{0,0}> div_ConstantStackPush_4(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(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}> div_ConstantStackPush_41(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i4, env, static) -{0,0}> div_ConstantStackPush_42(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i4, env, static) -{0,0}> div_ConstantStackPush_43(i2, i4, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i4, env, static) -{0,0}> div_ConstantStackPush_45(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i4, env, static) -{0,0}> div_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_47(i2, i4, env, static) -{1,1}> div_Store_50(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Store_50(i2, i4, iconst_0, env, static) -{1,1}> div_Load_51(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i4, iconst_0, env, static) -{1,1}> div_Load_53(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_53(i2, i4, iconst_0, env, static) -{1,1}> div_LT_70(i2, i4, iconst_0, env, static) :|: iconst_0 = 0

obtained
div_LT_70(i2, i4, 0, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1
by chaining
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_82(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_LT_82(i2, i4, iconst_0, env, static) -{1,1}> div_Load_84(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_Load_84(i2, i4, iconst_0, env, static) -{1,1}> div_LE_86(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LE_86(i2, i4, iconst_0, env, static) -{0,0}> div_LE_187(i2, i4, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_LE_187(i31, i32, i33, i34, env, static) -{0,0}> div_LE_249(i31, i32, i33, i34, env, static) :|: i34 <= 2 && i34 <= 1 && 0 <= i34
div_LE_249(i61, i62, i63, i64, env, static) -{0,0}> div_LE_311(i61, i62, i63, i64, env, static) :|: i64 <= 2 && 0 <= i64

obtained
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
by chaining
div_LE_311(i105, i104, i106, i94, env, static) -{0,0}> div_LE_315(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_LE_315(i105, i104, i106, i94, env, static) -{1,1}> div_Load_318(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 < i104 && 1 <= i104 && 1 <= i105
div_Load_318(i105, i104, i106, i94, env, static) -{1,1}> div_Load_320(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_Load_320(i105, i104, i106, i94, env, static) -{1,1}> div_IntArithmetic_323(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_IntArithmetic_323(i105, i104, i106, i94, env, static) -{1,1}> div_Store_328(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 <= i109 && 1 <= i104 && i106 - i104 = i109 && 1 <= i105
div_Store_328(i105, i104, i109, i94, env, static) -{1,1}> div_Load_331(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_Load_331(i105, i104, i109, i94, env, static) -{1,1}> div_ConstantStackPush_332(i105, i104, i94, i109, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_ConstantStackPush_332(i105, i104, i94, i109, env, static) -{1,1}> div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) :|: 0 <= i94 && 0 <= i109 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) -{1,1}> div_Store_334(i105, i104, i110, i109, env, static) :|: 0 <= i94 && i94 + iconst_1 = i110 && 0 <= i109 && 1 <= i110 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_Store_334(i105, i104, i110, i109, env, static) -{1,1}> div_JMP_336(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_JMP_336(i105, i104, i109, i110, env, static) -{1,1}> div_Load_338(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_338(i105, i104, i109, i110, env, static) -{1,1}> div_Load_341(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_341(i105, i104, i109, i110, env, static) -{1,1}> div_LT_359(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105

obtained
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109
by chaining
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_368(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_LT_368(i105, i104, i109, i110, env, static) -{1,1}> div_Load_373(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i109 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_Load_373(i105, i104, i109, i110, env, static) -{1,1}> div_LE_413(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 1 <= i104 && 1 <= i105
div_LE_413(i105, i104, i109, i110, env, static) -{0,0}> div_LE_311(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 0 <= i110 && 1 <= i104 && 1 <= i105

(8) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LT_70(i2, i4, 0, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

Moved arithmethic from lhss to constraints.

div_LT_70(i2, i4, 0, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1
was transformed to
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0

(10) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

Moved arithmethic from constraints to rhss.

div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
was transformed to
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 - i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'

div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
was transformed to
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, 0, env, static) :|: i2 < i4 && iconst_0 = 0

(12) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 - i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, 0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

Simplified expressions.

div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0
was transformed to
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: i4 <= i2 && x = 0

div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 - i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
was transformed to
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 + -1 * i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 + -1 * i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'

(14) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, 0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 + -1 * i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 + -1 * i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: i4 <= i2 && x = 0
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

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

IntTrs with 53 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{0,0}> div_ConstantStackPush_4(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(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}> div_ConstantStackPush_41(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i4, env, static) -{0,0}> div_ConstantStackPush_42(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i4, env, static) -{0,0}> div_ConstantStackPush_43(i2, i4, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i4, env, static) -{0,0}> div_ConstantStackPush_45(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i4, env, static) -{0,0}> div_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_47(i2, i4, env, static) -{1,1}> div_Store_50(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Store_50(i2, i4, iconst_0, env, static) -{1,1}> div_Load_51(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i4, iconst_0, env, static) -{1,1}> div_Load_53(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_53(i2, i4, iconst_0, env, static) -{1,1}> div_LT_70(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_82(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_LT_82(i2, i4, iconst_0, env, static) -{1,1}> div_Load_84(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_Load_84(i2, i4, iconst_0, env, static) -{1,1}> div_LE_86(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LE_86(i2, i4, iconst_0, env, static) -{0,0}> div_LE_187(i2, i4, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_LE_187(i31, i32, i33, i34, env, static) -{0,0}> div_LE_249(i31, i32, i33, i34, env, static) :|: i34 <= 2 && i34 <= 1 && 0 <= i34
div_LE_249(i61, i62, i63, i64, env, static) -{0,0}> div_LE_311(i61, i62, i63, i64, env, static) :|: i64 <= 2 && 0 <= i64
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LE_311(i105, i104, i106, i94, env, static) -{0,0}> div_LE_315(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_LE_315(i105, i104, i106, i94, env, static) -{1,1}> div_Load_318(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 < i104 && 1 <= i104 && 1 <= i105
div_Load_318(i105, i104, i106, i94, env, static) -{1,1}> div_Load_320(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_Load_320(i105, i104, i106, i94, env, static) -{1,1}> div_IntArithmetic_323(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_IntArithmetic_323(i105, i104, i106, i94, env, static) -{1,1}> div_Store_328(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 <= i109 && 1 <= i104 && i106 - i104 = i109 && 1 <= i105
div_Store_328(i105, i104, i109, i94, env, static) -{1,1}> div_Load_331(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_Load_331(i105, i104, i109, i94, env, static) -{1,1}> div_ConstantStackPush_332(i105, i104, i94, i109, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_ConstantStackPush_332(i105, i104, i94, i109, env, static) -{1,1}> div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) :|: 0 <= i94 && 0 <= i109 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) -{1,1}> div_Store_334(i105, i104, i110, i109, env, static) :|: 0 <= i94 && i94 + iconst_1 = i110 && 0 <= i109 && 1 <= i110 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_Store_334(i105, i104, i110, i109, env, static) -{1,1}> div_JMP_336(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_JMP_336(i105, i104, i109, i110, env, static) -{1,1}> div_Load_338(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_338(i105, i104, i109, i110, env, static) -{1,1}> div_Load_341(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_341(i105, i104, i109, i110, env, static) -{1,1}> div_LT_359(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_368(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_LT_368(i105, i104, i109, i110, env, static) -{1,1}> div_Load_373(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i109 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_Load_373(i105, i104, i109, i110, env, static) -{1,1}> div_LE_413(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 1 <= i104 && 1 <= i105
div_LE_413(i105, i104, i109, i110, env, static) -{0,0}> div_LE_311(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 0 <= i110 && 1 <= i104 && 1 <= i105

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

obtained
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_ConstantStackPush_2(i2, i4, env, static) -{0,0}> div_ConstantStackPush_4(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(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}> div_ConstantStackPush_41(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i4, env, static) -{0,0}> div_ConstantStackPush_42(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i4, env, static) -{0,0}> div_ConstantStackPush_43(i2, i4, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i4, env, static) -{0,0}> div_ConstantStackPush_45(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i4, env, static) -{0,0}> div_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_47(i2, i4, env, static) -{1,1}> div_Store_50(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Store_50(i2, i4, iconst_0, env, static) -{1,1}> div_Load_51(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i4, iconst_0, env, static) -{1,1}> div_Load_53(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_53(i2, i4, iconst_0, env, static) -{1,1}> div_LT_70(i2, i4, iconst_0, env, static) :|: iconst_0 = 0

obtained
div_LT_70(i2, i4, 0, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1
by chaining
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_82(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_LT_82(i2, i4, iconst_0, env, static) -{1,1}> div_Load_84(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_Load_84(i2, i4, iconst_0, env, static) -{1,1}> div_LE_86(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LE_86(i2, i4, iconst_0, env, static) -{0,0}> div_LE_187(i2, i4, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_LE_187(i31, i32, i33, i34, env, static) -{0,0}> div_LE_249(i31, i32, i33, i34, env, static) :|: i34 <= 2 && i34 <= 1 && 0 <= i34
div_LE_249(i61, i62, i63, i64, env, static) -{0,0}> div_LE_311(i61, i62, i63, i64, env, static) :|: i64 <= 2 && 0 <= i64

obtained
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
by chaining
div_LE_311(i105, i104, i106, i94, env, static) -{0,0}> div_LE_315(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_LE_315(i105, i104, i106, i94, env, static) -{1,1}> div_Load_318(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 < i104 && 1 <= i104 && 1 <= i105
div_Load_318(i105, i104, i106, i94, env, static) -{1,1}> div_Load_320(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_Load_320(i105, i104, i106, i94, env, static) -{1,1}> div_IntArithmetic_323(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_IntArithmetic_323(i105, i104, i106, i94, env, static) -{1,1}> div_Store_328(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 <= i109 && 1 <= i104 && i106 - i104 = i109 && 1 <= i105
div_Store_328(i105, i104, i109, i94, env, static) -{1,1}> div_Load_331(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_Load_331(i105, i104, i109, i94, env, static) -{1,1}> div_ConstantStackPush_332(i105, i104, i94, i109, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_ConstantStackPush_332(i105, i104, i94, i109, env, static) -{1,1}> div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) :|: 0 <= i94 && 0 <= i109 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) -{1,1}> div_Store_334(i105, i104, i110, i109, env, static) :|: 0 <= i94 && i94 + iconst_1 = i110 && 0 <= i109 && 1 <= i110 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_Store_334(i105, i104, i110, i109, env, static) -{1,1}> div_JMP_336(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_JMP_336(i105, i104, i109, i110, env, static) -{1,1}> div_Load_338(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_338(i105, i104, i109, i110, env, static) -{1,1}> div_Load_341(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_341(i105, i104, i109, i110, env, static) -{1,1}> div_LT_359(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105

obtained
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109
by chaining
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_368(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_LT_368(i105, i104, i109, i110, env, static) -{1,1}> div_Load_373(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i109 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_Load_373(i105, i104, i109, i110, env, static) -{1,1}> div_LE_413(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 1 <= i104 && 1 <= i105
div_LE_413(i105, i104, i109, i110, env, static) -{0,0}> div_LE_311(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 0 <= i110 && 1 <= i104 && 1 <= i105

(18) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LT_70(i2, i4, 0, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

Moved arithmethic from lhss to constraints.

div_LT_70(i2, i4, 0, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1
was transformed to
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0

(20) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

Moved arithmethic from constraints to rhss.

div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
was transformed to
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 - i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'

div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, iconst_0, env, static) :|: i2 < i4 && iconst_0 = 0
was transformed to
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, 0, env, static) :|: i2 < i4 && iconst_0 = 0

(22) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 - i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, 0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

Simplified expressions.

div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, 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
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 <= 1 && x = 0
was transformed to
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: i4 <= i2 && x = 0

div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 - i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
was transformed to
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 + -1 * i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 + -1 * i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'

(24) Obligation:

IntTrs with 7 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{19,19}> div_LT_70(i2, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
div_LE_311(i91, i103, i93, i94, env, static) -{0,0}> div_LE_314(i91, i103, i93, i94, env, static) :|: 0 <= i94 && i103 <= 0
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_367(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i109 < i104 && 1 <= i104 && 1 <= i105
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_81(i2, i4, 0, env, static) :|: i2 < i4 && iconst_0 = 0
div_LE_311(i105, i104, i106, i94, env, static) -{12,12}> div_LT_359(i105, i104, i106 + -1 * i104, i94 + 1, env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 + -1 * i104 = i109' && 0 <= i109' && 1 <= i110' && 0 <= i94 && i94 + 1 = i110'
div_LT_70(i2, i4, x, env, static) -{2,2}> div_LE_311(i2, i4, i2, 0, env, static) :|: i4 <= i2 && x = 0
div_LT_359(i105, i104, i109, i110, env, static) -{2,2}> div_LE_311(i105, i104, i109, i110, env, static) :|: i104 <= i109 && 1 <= i105 && 0 <= i109 && 1 <= i104 && 0 <= i110 && 1 <= i110 && 1 <= i109

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

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

(26) Obligation:

Set of 50 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 50 jbc graph edges to a weighted ITS with 50 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 50 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{0,0}> div_ConstantStackPush_4(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(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}> div_ConstantStackPush_41(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i4, env, static) -{0,0}> div_ConstantStackPush_42(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i4, env, static) -{0,0}> div_ConstantStackPush_43(i2, i4, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i4, env, static) -{0,0}> div_ConstantStackPush_45(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i4, env, static) -{0,0}> div_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_47(i2, i4, env, static) -{1,1}> div_Store_50(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Store_50(i2, i4, iconst_0, env, static) -{1,1}> div_Load_51(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i4, iconst_0, env, static) -{1,1}> div_Load_53(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_53(i2, i4, iconst_0, env, static) -{1,1}> div_LT_70(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_82(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_LT_82(i2, i4, iconst_0, env, static) -{1,1}> div_Load_84(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_Load_84(i2, i4, iconst_0, env, static) -{1,1}> div_LE_86(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LE_86(i2, i4, iconst_0, env, static) -{0,0}> div_LE_187(i2, i4, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_LE_187(i31, i32, i33, i34, env, static) -{0,0}> div_LE_249(i31, i32, i33, i34, env, static) :|: i34 <= 2 && i34 <= 1 && 0 <= i34
div_LE_249(i61, i62, i63, i64, env, static) -{0,0}> div_LE_311(i61, i62, i63, i64, env, static) :|: i64 <= 2 && 0 <= i64
div_LE_311(i105, i104, i106, i94, env, static) -{0,0}> div_LE_315(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_LE_315(i105, i104, i106, i94, env, static) -{1,1}> div_Load_318(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 < i104 && 1 <= i104 && 1 <= i105
div_Load_318(i105, i104, i106, i94, env, static) -{1,1}> div_Load_320(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_Load_320(i105, i104, i106, i94, env, static) -{1,1}> div_IntArithmetic_323(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_IntArithmetic_323(i105, i104, i106, i94, env, static) -{1,1}> div_Store_328(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 <= i109 && 1 <= i104 && i106 - i104 = i109 && 1 <= i105
div_Store_328(i105, i104, i109, i94, env, static) -{1,1}> div_Load_331(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_Load_331(i105, i104, i109, i94, env, static) -{1,1}> div_ConstantStackPush_332(i105, i104, i94, i109, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_ConstantStackPush_332(i105, i104, i94, i109, env, static) -{1,1}> div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) :|: 0 <= i94 && 0 <= i109 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) -{1,1}> div_Store_334(i105, i104, i110, i109, env, static) :|: 0 <= i94 && i94 + iconst_1 = i110 && 0 <= i109 && 1 <= i110 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_Store_334(i105, i104, i110, i109, env, static) -{1,1}> div_JMP_336(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_JMP_336(i105, i104, i109, i110, env, static) -{1,1}> div_Load_338(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_338(i105, i104, i109, i110, env, static) -{1,1}> div_Load_341(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_341(i105, i104, i109, i110, env, static) -{1,1}> div_LT_359(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_368(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_LT_368(i105, i104, i109, i110, env, static) -{1,1}> div_Load_373(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i109 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_Load_373(i105, i104, i109, i110, env, static) -{1,1}> div_LE_413(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 1 <= i104 && 1 <= i105
div_LE_413(i105, i104, i109, i110, env, static) -{0,0}> div_LE_311(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 0 <= i110 && 1 <= i104 && 1 <= i105

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

obtained
div_ConstantStackPush_2(i2, i4, env, static) -{21,21}> div_LE_311(i2, i4, i2, 0, env, static'1) :|: 0 < 2 && 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 1 && static'1 <= static''' + 1
by chaining
div_ConstantStackPush_2(i2, i4, env, static) -{0,0}> div_ConstantStackPush_4(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_9(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_11(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_15(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_15(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_16(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_18(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_20(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_33(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(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}> div_ConstantStackPush_41(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i4, env, static) -{0,0}> div_ConstantStackPush_42(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i4, env, static) -{0,0}> div_ConstantStackPush_43(i2, i4, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i4, env, static) -{0,0}> div_ConstantStackPush_45(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i4, env, static) -{0,0}> div_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
div_ConstantStackPush_47(i2, i4, env, static) -{1,1}> div_Store_50(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Store_50(i2, i4, iconst_0, env, static) -{1,1}> div_Load_51(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i4, iconst_0, env, static) -{1,1}> div_Load_53(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_Load_53(i2, i4, iconst_0, env, static) -{1,1}> div_LT_70(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LT_70(i2, i4, iconst_0, env, static) -{0,0}> div_LT_82(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_LT_82(i2, i4, iconst_0, env, static) -{1,1}> div_Load_84(i2, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i2
div_Load_84(i2, i4, iconst_0, env, static) -{1,1}> div_LE_86(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
div_LE_86(i2, i4, iconst_0, env, static) -{0,0}> div_LE_187(i2, i4, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_LE_187(i31, i32, i33, i34, env, static) -{0,0}> div_LE_249(i31, i32, i33, i34, env, static) :|: i34 <= 2 && i34 <= 1 && 0 <= i34
div_LE_249(i61, i62, i63, i64, env, static) -{0,0}> div_LE_311(i61, i62, i63, i64, env, static) :|: i64 <= 2 && 0 <= i64

obtained
div_LE_311(i105, i104, i106, i94, env, static) -{14,14}> div_LE_311(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'
by chaining
div_LE_311(i105, i104, i106, i94, env, static) -{0,0}> div_LE_315(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_LE_315(i105, i104, i106, i94, env, static) -{1,1}> div_Load_318(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 < i104 && 1 <= i104 && 1 <= i105
div_Load_318(i105, i104, i106, i94, env, static) -{1,1}> div_Load_320(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_Load_320(i105, i104, i106, i94, env, static) -{1,1}> div_IntArithmetic_323(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 1 <= i104 && 1 <= i105
div_IntArithmetic_323(i105, i104, i106, i94, env, static) -{1,1}> div_Store_328(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 1 <= i106 && 0 <= i109 && 1 <= i104 && i106 - i104 = i109 && 1 <= i105
div_Store_328(i105, i104, i109, i94, env, static) -{1,1}> div_Load_331(i105, i104, i109, i94, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_Load_331(i105, i104, i109, i94, env, static) -{1,1}> div_ConstantStackPush_332(i105, i104, i94, i109, env, static) :|: 0 <= i94 && 0 <= i109 && 1 <= i104 && 1 <= i105
div_ConstantStackPush_332(i105, i104, i94, i109, env, static) -{1,1}> div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) :|: 0 <= i94 && 0 <= i109 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_IntArithmetic_333(i105, i104, i94, iconst_1, i109, env, static) -{1,1}> div_Store_334(i105, i104, i110, i109, env, static) :|: 0 <= i94 && i94 + iconst_1 = i110 && 0 <= i109 && 1 <= i110 && iconst_1 = 1 && 1 <= i104 && 1 <= i105
div_Store_334(i105, i104, i110, i109, env, static) -{1,1}> div_JMP_336(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_JMP_336(i105, i104, i109, i110, env, static) -{1,1}> div_Load_338(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_338(i105, i104, i109, i110, env, static) -{1,1}> div_Load_341(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_Load_341(i105, i104, i109, i110, env, static) -{1,1}> div_LT_359(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i104 && 1 <= i105
div_LT_359(i105, i104, i109, i110, env, static) -{0,0}> div_LT_368(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_LT_368(i105, i104, i109, i110, env, static) -{1,1}> div_Load_373(i105, i104, i109, i110, env, static) :|: 0 <= i109 && 1 <= i110 && 1 <= i109 && i104 <= i109 && 1 <= i104 && 1 <= i105
div_Load_373(i105, i104, i109, i110, env, static) -{1,1}> div_LE_413(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 1 <= i104 && 1 <= i105
div_LE_413(i105, i104, i109, i110, env, static) -{0,0}> div_LE_311(i105, i104, i109, i110, env, static) :|: 1 <= i110 && 1 <= i109 && 0 <= i110 && 1 <= i104 && 1 <= i105

(30) Obligation:

IntTrs with 2 rules
Start term: div_ConstantStackPush_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_2(i2, i4, env, static) -{21,21}> div_LE_311(i2, i4, i2, 0, env, static'1) :|: 0 < 2 && 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 1 && static'1 <= static''' + 1
div_LE_311(i105, i104, i106, i94, env, static) -{14,14}> div_LE_311(i105, i104, i109', i110', env, static) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'

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

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

div_ConstantStackPush_2(x1, x2, x3, x4) → div_ConstantStackPush_2(x1, x2, x4)
div_LE_311(x1, x2, x3, x4, x5, x6) → div_LE_311(x1, x2, x3, x4)

(32) Obligation:

IntTrs with 2 rules
Start term: div_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_2(i2, i4, static) -{21,21}> div_LE_311(i2, i4, i2, 0) :|: 0 < 2 && 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 1 && static'1 <= static''' + 1
div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i109', i110') :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'

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

Moved arithmethic from constraints to rhss.

div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i109', i110') :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'
was transformed to
div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i106 - i104, i94 + 1) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'

(34) Obligation:

IntTrs with 2 rules
Start term: div_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_2(i2, i4, static) -{21,21}> div_LE_311(i2, i4, i2, 0) :|: 0 < 2 && 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 1 && static'1 <= static''' + 1
div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i106 - i104, i94 + 1) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'

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

Simplified expressions.

div_ConstantStackPush_2(i2, i4, static) -{21,21}> div_LE_311(i2, i4, i2, 0) :|: 0 < 2 && 0 <= 2 && 0 <= 0 && i4 <= i2 && 0 >= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 1 && static'1 <= static''' + 1
was transformed to
div_ConstantStackPush_2(i2, i4, static) -{21,21}> div_LE_311(i2, i4, i2, 0) :|: i4 <= i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i106 - i104, i94 + 1) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 - i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'
was transformed to
div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i106 + -1 * i104, i94 + 1) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 + -1 * i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'

(36) Obligation:

IntTrs with 2 rules
Start term: div_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_2(i2, i4, static) -{21,21}> div_LE_311(i2, i4, i2, 0) :|: i4 <= i2 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
div_LE_311(i105, i104, i106, i94) -{14,14}> div_LE_311(i105, i104, i106 + -1 * i104, i94 + 1) :|: 0 < i104 && 1 <= i105 && 1 <= i106 && 1 <= i104 && i106 + -1 * i104 = i109' && 0 <= i110' && i104 <= i109' && 1 <= i110' && 1 <= i109' && 0 <= i109' && 0 <= i94 && i94 + 1 = i110'

(37) koat Proof (EQUIVALENT transformation)

YES(?, 14*ar_0 + 21)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 21) div_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_0, 0)) [ ar_1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 14) div_LE_311(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_2 - ar_1, ar_3 + 1)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 - ar_1 = i109' /\ 0 <= i110' /\ ar_1 <= i109' /\ 1 <= i110' /\ 1 <= i109' /\ 0 <= i109' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 21) div_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_0, 0)) [ ar_1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 14) div_LE_311(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_2 - ar_1, ar_3 + 1)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 - ar_1 = i109' /\ 0 <= i110' /\ ar_1 <= i109' /\ 1 <= i110' /\ 1 <= i109' /\ 0 <= i109' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(div_ConstantStackPush_2) = V_1
Pol(div_LE_311) = V_3
Pol(koat_start) = V_1
orients all transitions weakly and the transition
div_LE_311(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_2 - ar_1, ar_3 + 1)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 - ar_1 = i109' /\ 0 <= i110' /\ ar_1 <= i109' /\ 1 <= i110' /\ 1 <= i109' /\ 0 <= i109' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 21) div_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_0, 0)) [ ar_1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ar_0, Cost: 14) div_LE_311(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_LE_311(ar_0, ar_1, ar_2 - ar_1, ar_3 + 1)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 1 <= ar_1 /\ ar_2 - ar_1 = i109' /\ 0 <= i110' /\ ar_1 <= i109' /\ 1 <= i110' /\ 1 <= i109' /\ 0 <= i109' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 14*ar_0 + 21

Time: 0.113 sec (SMT: 0.080 sec)

(38) BOUNDS(CONSTANT, 21 + 14 * |#0|)