time complexity proof of /tmp/tmpkLCxrL/Log.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

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

    ↳10 WeightedIntTrs

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

    ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

    ↳15 koat Proof (⇔, 103 ms)

    ↳16 BOUNDS(CONSTANT, 19 + 93 * |#0|)

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

↳18 JBCComplexityEdges

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

    ↳20 WeightedIntTrs

        ↳21 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 27 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), 4 ms)

        ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

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

        ↳36 WeightedIntTrs

        ↳37 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 10 ms)

        ↳38 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class Log{
  public static int half(int x) {

    int res = 0;

    while (x > 1) {

      x = x-2;
      res++;

    }

    return res;

  }


  public static int log(int x) {

    int res = 0;

    while (x > 1) {

      x = half(x);
      res++;

    }

    return res;

  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Log.log(I)I: Graph of 72 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 69 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 69 jbc graph edges to a weighted ITS with 69 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 69 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i1, env, static) -{0,0}> log_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> log_ConstantStackPush_46(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_46(i1, env, static) -{0,0}> log_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, env, static) -{0,0}> log_ConstantStackPush_50(i1, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, env, static) -{0,0}> log_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, env, static) -{0,0}> log_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, env, static) -{1,1}> log_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, iconst_0, env, static) -{1,1}> log_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i1, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i1, iconst_0, env, static) -{1,1}> log_LE_58(i1, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i1, iconst_1, iconst_0, env, static) -{0,0}> log_LE_341(i1, i1, iconst_1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_341(i146, i147, iconst_1, i148, env, static) -{0,0}> log_LE_576(i146, i147, iconst_1, i148, env, static) :|: 0 <= i148 && i148 <= 1 && i148 <= 2 && iconst_1 = 1
log_LE_576(i146, i264, iconst_1, i265, env, static) -{0,0}> log_LE_846(i146, i264, iconst_1, i265, env, static) :|: i265 <= 2 && iconst_1 = 1 && 0 <= i265
log_LE_846(i146, i386, iconst_1, i381, env, static) -{0,0}> log_LE_854(i146, i386, iconst_1, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && 2 <= i386
log_LE_854(i146, i386, iconst_1, i381, env, static) -{1,1}> log_Load_865(i146, i386, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && 2 <= i386 && iconst_1 < i386
log_Load_865(i146, i386, i381, env, static) -{1,1}> log_InvokeMethod_868(i146, i386, i381, env, static) :|: 0 <= i381 && 2 <= i386
log_InvokeMethod_868(i146, i386, i381, env, static) -{1,1}> half_ConstantStackPush_871(i386, i146, i381, env, static) :|: 0 <= i381 && 2 <= i386
half_ConstantStackPush_871(i386, i146, i381, env, static) -{1,1}> half_Store_872(iconst_0, i386, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_Store_872(iconst_0, i386, i146, i381, env, static) -{1,1}> half_Load_873(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_Load_873(i386, iconst_0, i146, i381, env, static) -{1,1}> half_ConstantStackPush_874(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_ConstantStackPush_874(i386, iconst_0, i146, i381, env, static) -{1,1}> half_LE_876(i386, iconst_1, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i386
half_LE_876(i386, iconst_1, iconst_0, i146, i381, env, static) -{1,1}> half_Load_882(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i386 && iconst_1 < i386
half_Load_882(i386, iconst_0, i146, i381, env, static) -{1,1}> half_ConstantStackPush_884(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_ConstantStackPush_884(i386, iconst_0, i146, i381, env, static) -{1,1}> half_IntArithmetic_886(i386, iconst_2, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386 && iconst_2 = 2
half_IntArithmetic_886(i386, iconst_2, iconst_0, i146, i381, env, static) -{1,1}> half_Store_888(i388, iconst_0, i146, i381, env, static) :|: i386 - iconst_2 = i388 && 0 <= i381 && 0 <= i388 && iconst_0 = 0 && 2 <= i386 && iconst_2 = 2
half_Store_888(i388, iconst_0, i146, i381, env, static) -{1,1}> half_Inc_889(i388, iconst_0, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_0 = 0
half_Inc_889(i388, iconst_0, i146, i381, env, static) -{1,1}> half_JMP_890(i388, iconst_1, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_1 = 1 && iconst_0 = 0
half_JMP_890(i388, iconst_1, i146, i381, env, static) -{1,1}> half_Load_891(i388, iconst_1, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_1 = 1
half_Load_891(i388, iconst_1, i146, i381, env, static) -{0,0}> half_Load_940(i388, iconst_1, i146, i381, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && 0 <= i381 && 0 <= i388 && iconst_1 = 1
half_Load_940(i410, i411, i146, i381, env, static) -{0,0}> half_Load_991(i410, i411, i146, i381, env, static) :|: i411 <= 3 && 0 <= i410 && 0 <= i381 && i411 <= 2 && 1 <= i411
half_Load_991(i439, i440, i146, i381, env, static) -{0,0}> half_Load_1046(i439, i440, i146, i381, env, static) :|: 0 <= i439 && 0 <= i381 && i440 <= 3 && 1 <= i440
half_Load_1046(i466, i467, i146, i381, env, static) -{1,1}> half_ConstantStackPush_1048(i466, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i466 && 0 <= i381
half_ConstantStackPush_1048(i466, i467, i146, i381, env, static) -{1,1}> half_LE_1055(i466, iconst_1, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i466 && 0 <= i381 && iconst_1 = 1
half_LE_1055(i479, iconst_1, i467, i146, i381, env, static) -{0,0}> half_LE_1056(i479, iconst_1, i467, i146, i381, env, static) :|: 0 <= i479 && 1 <= i467 && 0 <= i381 && iconst_1 = 1 && i479 <= 1
half_LE_1055(i480, iconst_1, i467, i146, i381, env, static) -{0,0}> half_LE_1057(i480, iconst_1, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i480 && 0 <= i381 && iconst_1 = 1 && 2 <= i480
half_LE_1056(i479, iconst_1, i467, i146, i381, env, static) -{1,1}> half_Load_1060(i467, i146, i381, env, static) :|: 0 <= i479 && 1 <= i467 && 0 <= i381 && iconst_1 = 1 && i479 <= iconst_1 && i479 <= 1
half_LE_1057(i480, iconst_1, i467, i146, i381, env, static) -{1,1}> half_Load_1063(i480, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && iconst_1 < i480 && iconst_1 = 1 && 2 <= i480
half_Load_1060(i467, i146, i381, env, static) -{1,1}> half_Return_1065(i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_Load_1063(i480, i467, i146, i381, env, static) -{1,1}> half_ConstantStackPush_1068(i480, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && 2 <= i480
half_Return_1065(i467, i146, i381, env, static) -{1,1}> log_Store_1070(i146, i467, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_ConstantStackPush_1068(i480, i467, i146, i381, env, static) -{1,1}> half_IntArithmetic_1072(i480, iconst_2, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && iconst_2 = 2 && 2 <= i480
log_Store_1070(i146, i467, i381, env, static) -{1,1}> log_Inc_1073(i146, i467, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_IntArithmetic_1072(i480, iconst_2, i467, i146, i381, env, static) -{1,1}> half_Store_1074(i482, i467, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381 && i480 - iconst_2 = i482 && iconst_2 = 2 && 2 <= i480
log_Inc_1073(i146, i467, i381, env, static) -{1,1}> log_JMP_1076(i146, i467, i485, env, static) :|: 1 <= i467 && 0 <= i381 && 1 <= i485 && i381 + 1 = i485
half_Store_1074(i482, i467, i146, i381, env, static) -{1,1}> half_Inc_1079(i482, i467, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381
log_JMP_1076(i146, i467, i485, env, static) -{1,1}> log_Load_1081(i146, i467, i485, env, static) :|: 1 <= i467 && 1 <= i485
half_Inc_1079(i482, i467, i146, i381, env, static) -{1,1}> half_JMP_1084(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381 && i467 + 1 = i488 && 2 <= i488
log_Load_1081(i146, i467, i485, env, static) -{1,1}> log_ConstantStackPush_1087(i146, i467, i485, env, static) :|: 1 <= i467 && 1 <= i485
half_JMP_1084(i482, i488, i146, i381, env, static) -{1,1}> half_Load_1089(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 0 <= i381 && 2 <= i488
log_ConstantStackPush_1087(i146, i467, i485, env, static) -{1,1}> log_LE_1090(i146, i467, iconst_1, i485, env, static) :|: 1 <= i467 && iconst_1 = 1 && 1 <= i485
half_Load_1089(i482, i488, i146, i381, env, static) -{0,0}> half_Load_1046(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 0 <= i381 && 1 <= i488 && 2 <= i488
log_LE_1090(i146, i467, iconst_1, i485, env, static) -{0,0}> log_LE_846(i146, i467, iconst_1, i485, env, static) :|: 1 <= i467 && iconst_1 = 1 && 1 <= i485 && 0 <= i485

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

obtained
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
log_ConstantStackPush_2(i1, env, static) -{0,0}> log_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> log_ConstantStackPush_46(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_46(i1, env, static) -{0,0}> log_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, env, static) -{0,0}> log_ConstantStackPush_50(i1, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, env, static) -{0,0}> log_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, env, static) -{0,0}> log_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, env, static) -{1,1}> log_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, iconst_0, env, static) -{1,1}> log_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i1, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i1, iconst_0, env, static) -{1,1}> log_LE_58(i1, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i1, iconst_1, iconst_0, env, static) -{0,0}> log_LE_341(i1, i1, iconst_1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_341(i146, i147, iconst_1, i148, env, static) -{0,0}> log_LE_576(i146, i147, iconst_1, i148, env, static) :|: 0 <= i148 && i148 <= 1 && i148 <= 2 && iconst_1 = 1
log_LE_576(i146, i264, iconst_1, i265, env, static) -{0,0}> log_LE_846(i146, i264, iconst_1, i265, env, static) :|: i265 <= 2 && iconst_1 = 1 && 0 <= i265

obtained
log_LE_846(i146, i386, 1, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
by chaining
log_LE_846(i146, i386, iconst_1, i381, env, static) -{0,0}> log_LE_854(i146, i386, iconst_1, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && 2 <= i386
log_LE_854(i146, i386, iconst_1, i381, env, static) -{1,1}> log_Load_865(i146, i386, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && 2 <= i386 && iconst_1 < i386
log_Load_865(i146, i386, i381, env, static) -{1,1}> log_InvokeMethod_868(i146, i386, i381, env, static) :|: 0 <= i381 && 2 <= i386
log_InvokeMethod_868(i146, i386, i381, env, static) -{1,1}> half_ConstantStackPush_871(i386, i146, i381, env, static) :|: 0 <= i381 && 2 <= i386
half_ConstantStackPush_871(i386, i146, i381, env, static) -{1,1}> half_Store_872(iconst_0, i386, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_Store_872(iconst_0, i386, i146, i381, env, static) -{1,1}> half_Load_873(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_Load_873(i386, iconst_0, i146, i381, env, static) -{1,1}> half_ConstantStackPush_874(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_ConstantStackPush_874(i386, iconst_0, i146, i381, env, static) -{1,1}> half_LE_876(i386, iconst_1, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i386
half_LE_876(i386, iconst_1, iconst_0, i146, i381, env, static) -{1,1}> half_Load_882(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i386 && iconst_1 < i386
half_Load_882(i386, iconst_0, i146, i381, env, static) -{1,1}> half_ConstantStackPush_884(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_ConstantStackPush_884(i386, iconst_0, i146, i381, env, static) -{1,1}> half_IntArithmetic_886(i386, iconst_2, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386 && iconst_2 = 2
half_IntArithmetic_886(i386, iconst_2, iconst_0, i146, i381, env, static) -{1,1}> half_Store_888(i388, iconst_0, i146, i381, env, static) :|: i386 - iconst_2 = i388 && 0 <= i381 && 0 <= i388 && iconst_0 = 0 && 2 <= i386 && iconst_2 = 2
half_Store_888(i388, iconst_0, i146, i381, env, static) -{1,1}> half_Inc_889(i388, iconst_0, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_0 = 0
half_Inc_889(i388, iconst_0, i146, i381, env, static) -{1,1}> half_JMP_890(i388, iconst_1, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_1 = 1 && iconst_0 = 0
half_JMP_890(i388, iconst_1, i146, i381, env, static) -{1,1}> half_Load_891(i388, iconst_1, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_1 = 1
half_Load_891(i388, iconst_1, i146, i381, env, static) -{0,0}> half_Load_940(i388, iconst_1, i146, i381, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && 0 <= i381 && 0 <= i388 && iconst_1 = 1
half_Load_940(i410, i411, i146, i381, env, static) -{0,0}> half_Load_991(i410, i411, i146, i381, env, static) :|: i411 <= 3 && 0 <= i410 && 0 <= i381 && i411 <= 2 && 1 <= i411
half_Load_991(i439, i440, i146, i381, env, static) -{0,0}> half_Load_1046(i439, i440, i146, i381, env, static) :|: 0 <= i439 && 0 <= i381 && i440 <= 3 && 1 <= i440

obtained
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
by chaining
half_Load_1046(i466, i467, i146, i381, env, static) -{1,1}> half_ConstantStackPush_1048(i466, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i466 && 0 <= i381
half_ConstantStackPush_1048(i466, i467, i146, i381, env, static) -{1,1}> half_LE_1055(i466, iconst_1, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i466 && 0 <= i381 && iconst_1 = 1

obtained
half_LE_1055(i480, 1, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
by chaining
half_LE_1055(i480, iconst_1, i467, i146, i381, env, static) -{0,0}> half_LE_1057(i480, iconst_1, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i480 && 0 <= i381 && iconst_1 = 1 && 2 <= i480
half_LE_1057(i480, iconst_1, i467, i146, i381, env, static) -{1,1}> half_Load_1063(i480, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && iconst_1 < i480 && iconst_1 = 1 && 2 <= i480
half_Load_1063(i480, i467, i146, i381, env, static) -{1,1}> half_ConstantStackPush_1068(i480, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && 2 <= i480
half_ConstantStackPush_1068(i480, i467, i146, i381, env, static) -{1,1}> half_IntArithmetic_1072(i480, iconst_2, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && iconst_2 = 2 && 2 <= i480
half_IntArithmetic_1072(i480, iconst_2, i467, i146, i381, env, static) -{1,1}> half_Store_1074(i482, i467, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381 && i480 - iconst_2 = i482 && iconst_2 = 2 && 2 <= i480
half_Store_1074(i482, i467, i146, i381, env, static) -{1,1}> half_Inc_1079(i482, i467, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381
half_Inc_1079(i482, i467, i146, i381, env, static) -{1,1}> half_JMP_1084(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381 && i467 + 1 = i488 && 2 <= i488
half_JMP_1084(i482, i488, i146, i381, env, static) -{1,1}> half_Load_1089(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 0 <= i381 && 2 <= i488
half_Load_1089(i482, i488, i146, i381, env, static) -{0,0}> half_Load_1046(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 0 <= i381 && 1 <= i488 && 2 <= i488

obtained
half_LE_1055(i479, 1, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479
by chaining
half_LE_1055(i479, iconst_1, i467, i146, i381, env, static) -{0,0}> half_LE_1056(i479, iconst_1, i467, i146, i381, env, static) :|: 0 <= i479 && 1 <= i467 && 0 <= i381 && iconst_1 = 1 && i479 <= 1
half_LE_1056(i479, iconst_1, i467, i146, i381, env, static) -{1,1}> half_Load_1060(i467, i146, i381, env, static) :|: 0 <= i479 && 1 <= i467 && 0 <= i381 && iconst_1 = 1 && i479 <= iconst_1 && i479 <= 1
half_Load_1060(i467, i146, i381, env, static) -{1,1}> half_Return_1065(i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_Return_1065(i467, i146, i381, env, static) -{1,1}> log_Store_1070(i146, i467, i381, env, static) :|: 1 <= i467 && 0 <= i381
log_Store_1070(i146, i467, i381, env, static) -{1,1}> log_Inc_1073(i146, i467, i381, env, static) :|: 1 <= i467 && 0 <= i381
log_Inc_1073(i146, i467, i381, env, static) -{1,1}> log_JMP_1076(i146, i467, i485, env, static) :|: 1 <= i467 && 0 <= i381 && 1 <= i485 && i381 + 1 = i485
log_JMP_1076(i146, i467, i485, env, static) -{1,1}> log_Load_1081(i146, i467, i485, env, static) :|: 1 <= i467 && 1 <= i485
log_Load_1081(i146, i467, i485, env, static) -{1,1}> log_ConstantStackPush_1087(i146, i467, i485, env, static) :|: 1 <= i467 && 1 <= i485
log_ConstantStackPush_1087(i146, i467, i485, env, static) -{1,1}> log_LE_1090(i146, i467, iconst_1, i485, env, static) :|: 1 <= i467 && iconst_1 = 1 && 1 <= i485
log_LE_1090(i146, i467, iconst_1, i485, env, static) -{0,0}> log_LE_846(i146, i467, iconst_1, i485, env, static) :|: 1 <= i467 && iconst_1 = 1 && 1 <= i485 && 0 <= i485

(8) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_LE_846(i146, i386, 1, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
half_LE_1055(i480, 1, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
half_LE_1055(i479, 1, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479

(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_2(x1, x2, x3) → log_ConstantStackPush_2(x1, x3)
log_LE_846(x1, x2, x3, x4, x5, x6) → log_LE_846(x2, x4)
half_Load_1046(x1, x2, x3, x4, x5, x6) → half_Load_1046(x1, x2, x4)
half_LE_1055(x1, x2, x3, x4, x5, x6, x7) → half_LE_1055(x1, x3, x5)

(10) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i1, static) -{19,19}> log_LE_846(i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_LE_846(i386, i381) -{14,14}> half_Load_1046(i388', 1, i381) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
half_Load_1046(i466, i467, i381) -{2,2}> half_LE_1055(i466, i467, i381) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
half_LE_1055(i480, i467, i381) -{7,7}> half_Load_1046(i482', i488', i381) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
half_LE_1055(i479, i467, i381) -{8,8}> log_LE_846(i467, i485') :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479

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

Moved arithmethic from constraints to rhss.

log_LE_846(i386, i381) -{14,14}> half_Load_1046(i388', 1, i381) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
was transformed to
log_LE_846(i386, i381) -{14,14}> half_Load_1046(i386 - 2, 1, i381) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2

half_LE_1055(i479, i467, i381) -{8,8}> log_LE_846(i467, i485') :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479
was transformed to
half_LE_1055(i479, i467, i381) -{8,8}> log_LE_846(i467, i381 + 1) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479

half_LE_1055(i480, i467, i381) -{7,7}> half_Load_1046(i482', i488', i381) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
was transformed to
half_LE_1055(i480, i467, i381) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i381) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480

(12) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i1, static) -{19,19}> log_LE_846(i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_LE_846(i386, i381) -{14,14}> half_Load_1046(i386 - 2, 1, i381) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
half_Load_1046(i466, i467, i381) -{2,2}> half_LE_1055(i466, i467, i381) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
half_LE_1055(i479, i467, i381) -{8,8}> log_LE_846(i467, i381 + 1) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479
half_LE_1055(i480, i467, i381) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i381) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480

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

Simplified expressions.

log_ConstantStackPush_2(i1, static) -{19,19}> log_LE_846(i1, 0) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
log_ConstantStackPush_2(i1, static) -{19,19}> log_LE_846(i1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

log_LE_846(i386, i381) -{14,14}> half_Load_1046(i386 - 2, 1, i381) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
was transformed to
log_LE_846(i386, i381) -{14,14}> half_Load_1046(i386 - 2, 1, i381) :|: 1 < i386 && 2 <= i386 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388'

(14) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
half_LE_1055(i479, i467, i381) -{8,8}> log_LE_846(i467, i381 + 1) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479
log_ConstantStackPush_2(i1, static) -{19,19}> log_LE_846(i1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
half_LE_1055(i480, i467, i381) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i381) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
half_Load_1046(i466, i467, i381) -{2,2}> half_LE_1055(i466, i467, i381) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
log_LE_846(i386, i381) -{14,14}> half_Load_1046(i386 - 2, 1, i381) :|: 1 < i386 && 2 <= i386 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388'

(15) koat Proof (EQUIVALENT transformation)

YES(?, 93*ar_0 + 19)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_1, ar_2 + 1, arityPad)) [ ar_2 + 1 = i485' /\ 0 <= i485' /\ ar_0 <= 1 /\ 1 <= i485' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 19) log_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_0, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 7) half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, ar_1 + 1, ar_2)) [ 2 <= ar_0 /\ 2 <= i488' /\ 0 <= ar_0 /\ 1 <= i488' /\ ar_1 + 1 = i488' /\ 0 <= i482' /\ 0 <= ar_2 /\ ar_0 - 2 = i482' /\ 1 <= ar_1 /\ 1 < ar_0 ]
(Comp: ?, Cost: 2) half_Load_1046(ar_0, ar_1, ar_2) -> Com_1(half_LE_1055(ar_0, ar_1, ar_2)) [ 0 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 14) log_LE_846(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, 1, ar_1)) [ 1 < ar_0 /\ 2 <= ar_0 /\ 0 <= i388' /\ 0 <= ar_1 /\ ar_0 - 2 = i388' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(log_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 8) half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_1, ar_2 + 1, arityPad)) [ ar_2 + 1 = i485' /\ 0 <= i485' /\ ar_0 <= 1 /\ 1 <= i485' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 19) log_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_0, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: ?, Cost: 7) half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, ar_1 + 1, ar_2)) [ 2 <= ar_0 /\ 2 <= i488' /\ 0 <= ar_0 /\ 1 <= i488' /\ ar_1 + 1 = i488' /\ 0 <= i482' /\ 0 <= ar_2 /\ ar_0 - 2 = i482' /\ 1 <= ar_1 /\ 1 < ar_0 ]
(Comp: ?, Cost: 2) half_Load_1046(ar_0, ar_1, ar_2) -> Com_1(half_LE_1055(ar_0, ar_1, ar_2)) [ 0 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 14) log_LE_846(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, 1, ar_1)) [ 1 < ar_0 /\ 2 <= ar_0 /\ 0 <= i388' /\ 0 <= ar_1 /\ ar_0 - 2 = i388' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(log_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(half_LE_1055) = 3*V_1 + 4*V_2 - 1
Pol(log_LE_846) = 3*V_1 - 1
Pol(log_ConstantStackPush_2) = 3*V_1
Pol(half_Load_1046) = 3*V_1 + 4*V_2
Pol(koat_start) = 3*V_1
orients all transitions weakly and the transitions
log_LE_846(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, 1, ar_1)) [ 1 < ar_0 /\ 2 <= ar_0 /\ 0 <= i388' /\ 0 <= ar_1 /\ ar_0 - 2 = i388' ]
half_Load_1046(ar_0, ar_1, ar_2) -> Com_1(half_LE_1055(ar_0, ar_1, ar_2)) [ 0 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_1, ar_2 + 1, arityPad)) [ ar_2 + 1 = i485' /\ 0 <= i485' /\ ar_0 <= 1 /\ 1 <= i485' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ 0 <= ar_0 ]
half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, ar_1 + 1, ar_2)) [ 2 <= ar_0 /\ 2 <= i488' /\ 0 <= ar_0 /\ 1 <= i488' /\ ar_1 + 1 = i488' /\ 0 <= i482' /\ 0 <= ar_2 /\ ar_0 - 2 = i482' /\ 1 <= ar_1 /\ 1 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 3*ar_0, Cost: 8) half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_1, ar_2 + 1, arityPad)) [ ar_2 + 1 = i485' /\ 0 <= i485' /\ ar_0 <= 1 /\ 1 <= i485' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 19) log_ConstantStackPush_2(ar_0, ar_1, ar_2) -> Com_1(log_LE_846(ar_0, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_1 + 2 /\ 0 <= ar_1 /\ 0 <= static'1 ]
(Comp: 3*ar_0, Cost: 7) half_LE_1055(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, ar_1 + 1, ar_2)) [ 2 <= ar_0 /\ 2 <= i488' /\ 0 <= ar_0 /\ 1 <= i488' /\ ar_1 + 1 = i488' /\ 0 <= i482' /\ 0 <= ar_2 /\ ar_0 - 2 = i482' /\ 1 <= ar_1 /\ 1 < ar_0 ]
(Comp: 3*ar_0, Cost: 2) half_Load_1046(ar_0, ar_1, ar_2) -> Com_1(half_LE_1055(ar_0, ar_1, ar_2)) [ 0 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 3*ar_0, Cost: 14) log_LE_846(ar_0, ar_1, ar_2) -> Com_1(half_Load_1046(ar_0 - 2, 1, ar_1)) [ 1 < ar_0 /\ 2 <= ar_0 /\ 0 <= i388' /\ 0 <= ar_1 /\ ar_0 - 2 = i388' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(log_ConstantStackPush_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 93*ar_0 + 19

Time: 0.136 sec (SMT: 0.125 sec)

(16) BOUNDS(CONSTANT, 19 + 93 * |#0|)

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

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

(18) Obligation:

Set of 70 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 70 jbc graph edges to a weighted ITS with 70 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 70 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i1, env, static) -{0,0}> log_ConstantStackPush_4(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_4(i1, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i1, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i1, env, static) -{1,1}> langle_init_rangle_InvokeMethod_32(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_32(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, env, static) -{1,1}> langle_clinit_rangle_Return_40(i1, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, env, static) -{1,1}> log_ConstantStackPush_46(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_46(i1, env, static) -{0,0}> log_ConstantStackPush_48(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i1, env, static) -{0,0}> log_ConstantStackPush_50(i1, env, static) :|: 0 <= static
log_ConstantStackPush_50(i1, env, static) -{0,0}> log_ConstantStackPush_51(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i1, env, static) -{0,0}> log_ConstantStackPush_52(i1, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i1, env, static) -{1,1}> log_Store_53(i1, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i1, iconst_0, env, static) -{1,1}> log_Load_54(i1, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i1, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i1, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i1, iconst_0, env, static) -{1,1}> log_LE_58(i1, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i1, iconst_1, iconst_0, env, static) -{0,0}> log_LE_341(i1, i1, iconst_1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_341(i146, i147, iconst_1, i148, env, static) -{0,0}> log_LE_576(i146, i147, iconst_1, i148, env, static) :|: 0 <= i148 && i148 <= 1 && i148 <= 2 && iconst_1 = 1
log_LE_576(i146, i264, iconst_1, i265, env, static) -{0,0}> log_LE_846(i146, i264, iconst_1, i265, env, static) :|: i265 <= 2 && iconst_1 = 1 && 0 <= i265
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, iconst_1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1
log_LE_846(i146, i386, iconst_1, i381, env, static) -{0,0}> log_LE_854(i146, i386, iconst_1, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && 2 <= i386
log_LE_854(i146, i386, iconst_1, i381, env, static) -{1,1}> log_Load_865(i146, i386, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && 2 <= i386 && iconst_1 < i386
log_Load_865(i146, i386, i381, env, static) -{1,1}> log_InvokeMethod_868(i146, i386, i381, env, static) :|: 0 <= i381 && 2 <= i386
log_InvokeMethod_868(i146, i386, i381, env, static) -{1,1}> half_ConstantStackPush_871(i386, i146, i381, env, static) :|: 0 <= i381 && 2 <= i386
half_ConstantStackPush_871(i386, i146, i381, env, static) -{1,1}> half_Store_872(iconst_0, i386, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_Store_872(iconst_0, i386, i146, i381, env, static) -{1,1}> half_Load_873(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_Load_873(i386, iconst_0, i146, i381, env, static) -{1,1}> half_ConstantStackPush_874(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_ConstantStackPush_874(i386, iconst_0, i146, i381, env, static) -{1,1}> half_LE_876(i386, iconst_1, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i386
half_LE_876(i386, iconst_1, iconst_0, i146, i381, env, static) -{1,1}> half_Load_882(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i386 && iconst_1 < i386
half_Load_882(i386, iconst_0, i146, i381, env, static) -{1,1}> half_ConstantStackPush_884(i386, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386
half_ConstantStackPush_884(i386, iconst_0, i146, i381, env, static) -{1,1}> half_IntArithmetic_886(i386, iconst_2, iconst_0, i146, i381, env, static) :|: 0 <= i381 && iconst_0 = 0 && 2 <= i386 && iconst_2 = 2
half_IntArithmetic_886(i386, iconst_2, iconst_0, i146, i381, env, static) -{1,1}> half_Store_888(i388, iconst_0, i146, i381, env, static) :|: i386 - iconst_2 = i388 && 0 <= i381 && 0 <= i388 && iconst_0 = 0 && 2 <= i386 && iconst_2 = 2
half_Store_888(i388, iconst_0, i146, i381, env, static) -{1,1}> half_Inc_889(i388, iconst_0, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_0 = 0
half_Inc_889(i388, iconst_0, i146, i381, env, static) -{1,1}> half_JMP_890(i388, iconst_1, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_1 = 1 && iconst_0 = 0
half_JMP_890(i388, iconst_1, i146, i381, env, static) -{1,1}> half_Load_891(i388, iconst_1, i146, i381, env, static) :|: 0 <= i381 && 0 <= i388 && iconst_1 = 1
half_Load_891(i388, iconst_1, i146, i381, env, static) -{0,0}> half_Load_940(i388, iconst_1, i146, i381, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && 0 <= i381 && 0 <= i388 && iconst_1 = 1
half_Load_940(i410, i411, i146, i381, env, static) -{0,0}> half_Load_991(i410, i411, i146, i381, env, static) :|: i411 <= 3 && 0 <= i410 && 0 <= i381 && i411 <= 2 && 1 <= i411
half_Load_991(i439, i440, i146, i381, env, static) -{0,0}> half_Load_1046(i439, i440, i146, i381, env, static) :|: 0 <= i439 && 0 <= i381 && i440 <= 3 && 1 <= i440
half_Load_1046(i466, i467, i146, i381, env, static) -{1,1}> half_ConstantStackPush_1048(i466, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i466 && 0 <= i381
half_ConstantStackPush_1048(i466, i467, i146, i381, env, static) -{1,1}> half_LE_1055(i466, iconst_1, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i466 && 0 <= i381 && iconst_1 = 1
half_LE_1055(i479, iconst_1, i467, i146, i381, env, static) -{0,0}> half_LE_1056(i479, iconst_1, i467, i146, i381, env, static) :|: 0 <= i479 && 1 <= i467 && 0 <= i381 && iconst_1 = 1 && i479 <= 1
half_LE_1055(i480, iconst_1, i467, i146, i381, env, static) -{0,0}> half_LE_1057(i480, iconst_1, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i480 && 0 <= i381 && iconst_1 = 1 && 2 <= i480
half_LE_1056(i479, iconst_1, i467, i146, i381, env, static) -{1,1}> half_Load_1060(i467, i146, i381, env, static) :|: 0 <= i479 && 1 <= i467 && 0 <= i381 && iconst_1 = 1 && i479 <= iconst_1 && i479 <= 1
half_LE_1057(i480, iconst_1, i467, i146, i381, env, static) -{1,1}> half_Load_1063(i480, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && iconst_1 < i480 && iconst_1 = 1 && 2 <= i480
half_Load_1060(i467, i146, i381, env, static) -{1,1}> half_Return_1065(i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_Load_1063(i480, i467, i146, i381, env, static) -{1,1}> half_ConstantStackPush_1068(i480, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && 2 <= i480
half_Return_1065(i467, i146, i381, env, static) -{1,1}> log_Store_1070(i146, i467, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_ConstantStackPush_1068(i480, i467, i146, i381, env, static) -{1,1}> half_IntArithmetic_1072(i480, iconst_2, i467, i146, i381, env, static) :|: 1 <= i467 && 0 <= i381 && iconst_2 = 2 && 2 <= i480
log_Store_1070(i146, i467, i381, env, static) -{1,1}> log_Inc_1073(i146, i467, i381, env, static) :|: 1 <= i467 && 0 <= i381
half_IntArithmetic_1072(i480, iconst_2, i467, i146, i381, env, static) -{1,1}> half_Store_1074(i482, i467, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381 && i480 - iconst_2 = i482 && iconst_2 = 2 && 2 <= i480
log_Inc_1073(i146, i467, i381, env, static) -{1,1}> log_JMP_1076(i146, i467, i485, env, static) :|: 1 <= i467 && 0 <= i381 && 1 <= i485 && i381 + 1 = i485
half_Store_1074(i482, i467, i146, i381, env, static) -{1,1}> half_Inc_1079(i482, i467, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381
log_JMP_1076(i146, i467, i485, env, static) -{1,1}> log_Load_1081(i146, i467, i485, env, static) :|: 1 <= i467 && 1 <= i485
half_Inc_1079(i482, i467, i146, i381, env, static) -{1,1}> half_JMP_1084(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 1 <= i467 && 0 <= i381 && i467 + 1 = i488 && 2 <= i488
log_Load_1081(i146, i467, i485, env, static) -{1,1}> log_ConstantStackPush_1087(i146, i467, i485, env, static) :|: 1 <= i467 && 1 <= i485
half_JMP_1084(i482, i488, i146, i381, env, static) -{1,1}> half_Load_1089(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 0 <= i381 && 2 <= i488
log_ConstantStackPush_1087(i146, i467, i485, env, static) -{1,1}> log_LE_1090(i146, i467, iconst_1, i485, env, static) :|: 1 <= i467 && iconst_1 = 1 && 1 <= i485
half_Load_1089(i482, i488, i146, i381, env, static) -{0,0}> half_Load_1046(i482, i488, i146, i381, env, static) :|: 0 <= i482 && 0 <= i381 && 1 <= i488 && 2 <= i488
log_LE_1090(i146, i467, iconst_1, i485, env, static) -{0,0}> log_LE_846(i146, i467, iconst_1, i485, env, static) :|: 1 <= i467 && iconst_1 = 1 && 1 <= i485 && 0 <= i485

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

(22) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, iconst_1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1
log_LE_846(i146, i386, 1, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
half_LE_1055(i480, 1, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
half_LE_1055(i479, 1, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479

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

Moved arithmethic from lhss to constraints.

log_LE_846(i146, i386, 1, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2
was transformed to
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1

half_LE_1055(i480, 1, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480
was transformed to
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1

half_LE_1055(i479, 1, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479
was transformed to
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1

(24) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, iconst_1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1

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

Moved arithmethic from constraints to rhss.

half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i485', env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1
was transformed to
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i381 + 1, env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1

log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, iconst_1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1
was transformed to
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, 1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1

half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i482', i488', i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1
was transformed to
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1

log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i388', 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1
was transformed to
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1

(26) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i381 + 1, env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, 1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1

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

Simplified expressions.

log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1
was transformed to
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 2 <= i386 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && x = 1

(28) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i381 + 1, env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 2 <= i386 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && x = 1
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, 1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1

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

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

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

(32) Obligation:

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

Moved arithmethic from lhss to constraints.

(34) Obligation:

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

Moved arithmethic from constraints to rhss.

(36) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= static''' && 0 <= 2 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= 1 && 0 <= static'1 && 0 < 2 && 0 >= 0
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i381 + 1, env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, 1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 1 <= 1 && 2 <= i386 && 1 <= 3 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && 1 <= 2 && x = 1

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

Simplified expressions.

(38) Obligation:

IntTrs with 6 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
half_Load_1046(i466, i467, i146, i381, env, static) -{2,2}> half_LE_1055(i466, 1, i467, i146, i381, env, static) :|: 0 <= i381 && 1 <= i467 && 0 <= i466
half_LE_1055(i479, x, i467, i146, i381, env, static) -{8,8}> log_LE_846(i146, i467, 1, i381 + 1, env, static) :|: i381 + 1 = i485' && 0 <= i485' && i479 <= 1 && 1 <= i485' && 1 <= i467 && 0 <= i381 && 0 <= i479 && x = 1
half_LE_1055(i480, x, i467, i146, i381, env, static) -{7,7}> half_Load_1046(i480 - 2, i467 + 1, i146, i381, env, static) :|: 2 <= i480 && 2 <= i488' && 0 <= i480 && 1 <= i488' && i467 + 1 = i488' && 0 <= i482' && 0 <= i381 && i480 - 2 = i482' && 1 <= i467 && 1 < i480 && x = 1
log_ConstantStackPush_2(i1, env, static) -{19,19}> log_LE_846(i1, i1, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
log_LE_846(i146, i386, x, i381, env, static) -{14,14}> half_Load_1046(i386 - 2, 1, i146, i381, env, static) :|: 1 < i386 && 2 <= i386 && 0 <= i388' && 0 <= i381 && i386 - 2 = i388' && x = 1
log_LE_846(i146, i385, iconst_1, i381, env, static) -{0,0}> log_LE_853(i146, i385, 1, i381, env, static) :|: i385 <= 1 && 0 <= i381 && iconst_1 = 1