time complexity proof of /tmp/tmpfIxcIN/LogIterative.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

    ↳9 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 18 ms)

    ↳10 WeightedIntTrs

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

    ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

    ↳15 koat Proof (⇔, 2 ms)

    ↳16 BOUNDS(CONSTANT, 22 + 12 * |#0|)

↳17 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)), 4 ms)

↳18 JBCComplexityEdges

    ↳19 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 85 ms)

    ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

        ↳35 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳36 WeightedIntTrs

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

        ↳38 WeightedIntTrs

        ↳39 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 8 ms)

        ↳40 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class LogIterative {
  public static int log(int x, int y) {
    int res = 0;
    while (x >= y && y > 1) {
      res++;
      x = x/y;
    }
    return res;
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
LogIterative.log(II)I: Graph of 61 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

Transformed 49 jbc graph edges to a weighted ITS with 49 rules.
Used simplified encoding of division and modulo.
Filtered conditions with variables that do not depend on the variables on the lhs or rhs without taking transitive dependencies into account.
Filtered fields of type java.lang.Object.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 49 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104

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

obtained
log_ConstantStackPush_1(i1, i4, env, static) -{22,22}> log_LE_299(i1, i4, 1, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
by chaining
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63

obtained
log_LE_299(i105, i104, 1, i106, i94, env, static) -{12,12}> log_LE_299(i105, i104, 1, i111', i110', env, static) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
by chaining
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104

(8) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{22,22}> log_LE_299(i1, i4, 1, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
log_LE_299(i105, i104, 1, i106, i94, env, static) -{12,12}> log_LE_299(i105, i104, 1, i111', i110', env, static) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'

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

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

log_ConstantStackPush_1(x1, x2, x3, x4) → log_ConstantStackPush_1(x1, x2, x4)
log_LE_299(x1, x2, x3, x4, x5, x6, x7) → log_LE_299(x1, x2, x4, x5)

(10) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i110') :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'

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

Moved arithmethic from constraints to rhss.

log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i110') :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
was transformed to
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i94 + 1) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'

(12) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i94 + 1) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1

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

Simplified expressions.

log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && i4 <= i1 && 0 < 2 && 0 <= 1
was transformed to
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 <= i1

(14) Obligation:

IntTrs with 2 rules
Start term: log_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
log_LE_299(i105, i104, i106, i94) -{12,12}> log_LE_299(i105, i104, i111', i94 + 1) :|: 1 < i104 && 2 <= i104 && 2 <= i106 && 2 <= i111' && i104 <= i111' && 0 <= i110' && 1 <= i110' && 2 <= i105 && i111' < i106 && 0 <= i111' && 0 <= i94 && i94 + 1 = i110'
log_ConstantStackPush_1(i1, i4, static) -{22,22}> log_LE_299(i1, i4, i1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 <= i1

(15) koat Proof (EQUIVALENT transformation)

YES(?, 12*ar_0 + 22)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 12) log_LE_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, i111', ar_3 + 1)) [ 1 < ar_1 /\ 2 <= ar_1 /\ 2 <= ar_2 /\ 2 <= i111' /\ ar_1 <= i111' /\ 0 <= i110' /\ 1 <= i110' /\ 2 <= ar_0 /\ i111' < ar_2 /\ 0 <= i111' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: ?, Cost: 22) log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, ar_0, 0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_ConstantStackPush_1(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: ?, Cost: 12) log_LE_299(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, i111', ar_3 + 1)) [ 1 < ar_1 /\ 2 <= ar_1 /\ 2 <= ar_2 /\ 2 <= i111' /\ ar_1 <= i111' /\ 0 <= i110' /\ 1 <= i110' /\ 2 <= ar_0 /\ i111' < ar_2 /\ 0 <= i111' /\ 0 <= ar_3 /\ ar_3 + 1 = i110' ]
(Comp: 1, Cost: 22) log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_LE_299(ar_0, ar_1, ar_0, 0)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(log_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

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

Complexity upper bound 12*ar_0 + 22

Time: 0.110 sec (SMT: 0.102 sec)

(16) BOUNDS(CONSTANT, 22 + 12 * |#0|)

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

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

(18) Obligation:

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

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

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

(20) Obligation:

IntTrs with 52 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104

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

obtained
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0

obtained
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
by chaining
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63

obtained
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
by chaining
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i111 < i106 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104

obtained
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
by chaining
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104

(22) Obligation:

IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111

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

Moved arithmethic from lhss to constraints.

log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
was transformed to
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0

log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

(24) Obligation:

IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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

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

Moved arithmethic from constraints to rhss.

log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
was transformed to
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0

log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
was transformed to
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1

(26) Obligation:

IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104

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

Simplified expressions.

log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
was transformed to
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0

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

(28) Obligation:

IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i111' < i106 && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104

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

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

(30) Obligation:

IntTrs with 52 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{0,0}> log_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_44(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_47(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i1, i4, env, static) -{1,1}> log_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, i4, env, static) -{0,0}> log_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i1, i4, env, static) -{0,0}> log_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, i4, env, static) -{0,0}> log_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, i4, env, static) -{0,0}> log_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, i4, env, static) -{1,1}> log_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, i4, iconst_0, env, static) -{1,1}> log_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, i4, iconst_0, env, static) -{1,1}> log_Load_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_Load_55(i1, i4, iconst_0, env, static) -{1,1}> log_LT_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_63(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_LT_63(i1, i4, iconst_0, env, static) -{1,1}> log_Load_68(i1, i4, iconst_0, env, static) :|: iconst_0 = 0 && i4 <= i1
log_Load_68(i1, i4, iconst_0, env, static) -{1,1}> log_ConstantStackPush_72(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_72(i1, i4, iconst_0, env, static) -{1,1}> log_LE_74(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_74(i1, i4, iconst_1, iconst_0, env, static) -{0,0}> log_LE_159(i1, i4, iconst_1, i1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_159(i29, i30, iconst_1, i31, i32, env, static) -{0,0}> log_LE_225(i29, i30, iconst_1, i31, i32, env, static) :|: i32 <= 2 && iconst_1 = 1 && 0 <= i32 && i32 <= 1
log_LE_225(i60, i61, iconst_1, i62, i63, env, static) -{0,0}> log_LE_299(i60, i61, iconst_1, i62, i63, env, static) :|: i63 <= 2 && iconst_1 = 1 && 0 <= i63
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i106 / i104 = i111 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_344(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_344(i105, i104, i111, i110, env, static) -{1,1}> log_Load_351(i105, i104, i111, i110, env, static) :|: 1 <= i110 && i104 <= i111 && 2 <= i105 && 2 <= i111 && 0 <= i111 && 2 <= i104
log_Load_351(i105, i104, i111, i110, env, static) -{1,1}> log_ConstantStackPush_353(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_ConstantStackPush_353(i105, i104, i111, i110, env, static) -{1,1}> log_LE_372(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 2 <= i111 && 2 <= i104
log_LE_372(i105, i104, iconst_1, i111, i110, env, static) -{0,0}> log_LE_299(i105, i104, iconst_1, i111, i110, env, static) :|: 1 <= i110 && iconst_1 = 1 && 2 <= i105 && 0 <= i110 && 2 <= i111 && 2 <= i104

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

obtained
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
by chaining
log_LE_299(i105, i104, iconst_1, i106, i94, env, static) -{0,0}> log_LE_301(i105, i104, iconst_1, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_LE_301(i105, i104, iconst_1, i106, i94, env, static) -{1,1}> log_Inc_314(i105, i104, i106, i94, env, static) :|: 0 <= i94 && 2 <= i106 && iconst_1 < i104 && iconst_1 = 1 && 2 <= i105 && 2 <= i104
log_Inc_314(i105, i104, i106, i94, env, static) -{1,1}> log_Load_317(i105, i104, i106, i110, env, static) :|: 0 <= i94 && i94 + 1 = i110 && 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_317(i105, i104, i106, i110, env, static) -{1,1}> log_Load_320(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_Load_320(i105, i104, i106, i110, env, static) -{1,1}> log_IntArithmetic_321(i105, i104, i106, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && 2 <= i104
log_IntArithmetic_321(i105, i104, i106, i110, env, static) -{1,1}> log_Store_323(i105, i104, i111, i110, env, static) :|: 2 <= i106 && 1 <= i110 && 2 <= i105 && i106 / i104 = i111 && 0 <= i111 && 2 <= i104
log_Store_323(i105, i104, i111, i110, env, static) -{1,1}> log_JMP_326(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_JMP_326(i105, i104, i111, i110, env, static) -{1,1}> log_Load_328(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_328(i105, i104, i111, i110, env, static) -{1,1}> log_Load_329(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_Load_329(i105, i104, i111, i110, env, static) -{1,1}> log_LT_339(i105, i104, i111, i110, env, static) :|: 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104

(32) Obligation:

IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_58(i1, i4, 0, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111

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

Moved arithmethic from lhss to constraints.

log_LE_299(i105, i104, 1, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

(34) Obligation:

IntTrs with 7 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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

(35) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && i106 / i104 = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, x, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

(36) Obligation:

IntTrs with 8 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, iconst_0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, iconst_1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, x, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104

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

Moved arithmethic from constraints to rhss.

log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i110', env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, x, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, 1, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

(38) Obligation:

IntTrs with 8 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: 0 <= 2 && 0 <= 0 && 0 <= 1 && i4 <= i1 && x = 0
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, 1, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, 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

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

Simplified expressions.

log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 - i104 * div < i104 && i106 - i104 * div + i104 > 0 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
was transformed to
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 + -1 * i104 * div < i104 && 0 < i106 + -1 * i104 * div + i104 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1

(40) Obligation:

IntTrs with 8 rules
Start term: log_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_LE_299(i105, i104, x, i106, i94, env, static) -{9,9}> log_LE_299'(i105, i104, 1, i106, i94, env, static) :|: i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1
log_LT_58(i1, i4, x, env, static) -{3,3}> log_LE_299(i1, i4, 1, i1, 0, env, static) :|: i4 <= i1 && x = 0
log_ConstantStackPush_1(i1, i4, env, static) -{19,19}> log_LT_58(i1, i4, 0, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
log_LE_299(i91, i103, iconst_1, i93, i94, env, static) -{0,0}> log_LE_300(i91, i103, 1, i93, i94, env, static) :|: 0 <= i94 && i103 <= 1 && iconst_1 = 1
log_LT_339(i105, i104, i111, i110, env, static) -{3,3}> log_LE_299(i105, i104, 1, i111, i110, env, static) :|: i104 <= i111 && 2 <= i104 && 1 <= i110 && 2 <= i111 && 0 <= i110 && 2 <= i105 && 0 <= i111
log_LT_58(i1, i4, iconst_0, env, static) -{0,0}> log_LT_62(i1, i4, 0, env, static) :|: i1 < i4 && iconst_0 = 0
log_LT_339(i105, i104, i111, i110, env, static) -{0,0}> log_LT_342(i105, i104, i111, i110, env, static) :|: i111 < i104 && 1 <= i110 && 2 <= i105 && 0 <= i111 && 2 <= i104
log_LE_299'(i105, i104, x, i106, i94, env, static) -{9,9}> log_LT_339(i105, i104, i111', i94 + 1, env, static) :|: i106 + -1 * i104 * div < i104 && 0 < i106 + -1 * i104 * div + i104 && i94 + 1 = i110' && 2 <= i104 && 0 <= i94 && 0 <= i111' && div = i111' && 1 <= i110' && 2 <= i105 && 2 <= i106 && 1 < i104 && x = 1