time complexity proof of /tmp/tmp

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(3 + 19 * #0, 41)).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

    ↳8 WeightedIntTrs

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

    ↳10 WeightedIntTrs

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

    ↳12 WeightedIntTrs

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

    ↳14 WeightedIntTrs

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

↳16 JBCComplexityEdges

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 114 ms)

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

        ↳27 CESProof (⇔, 217 ms)

        ↳28 BOUNDS(CONSTANT, max(38, 19 * #0))

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

    ↳30 WeightedIntTrs

        ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 0 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), 2 ms)

        ↳38 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class LogAG{

  // adapted from Arts&Giesl, 2001

  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-2)+1;
      res++;

    }

    return res;

  }

}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 62 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 62 jbc graph edges to a weighted ITS with 62 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 62 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_4(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_21(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_21(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_26(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_29(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_29(i2, env, static) -{0,0}> langle_clinit_rangle_New_31(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_31(i2, env, static) -{0,0}> langle_clinit_rangle_New_33(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_33(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_39(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_39(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_40(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_42(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_42(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_43(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_43(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_47(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i2, env, static) -{1,1}> log_ConstantStackPush_48(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 <= static
log_ConstantStackPush_50(i2, env, static) -{0,0}> log_ConstantStackPush_51(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i2, env, static) -{0,0}> log_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i2, iconst_1, iconst_0, env, static) -{0,0}> log_LE_153(i2, i2, iconst_1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_153(i42, i43, iconst_1, i44, env, static) -{0,0}> log_LE_226(i42, i43, iconst_1, i44, env, static) :|: i44 <= 2 && iconst_1 = 1 && i44 <= 1 && 0 <= i44
log_LE_226(i42, i79, iconst_1, i80, env, static) -{0,0}> log_LE_317(i42, i79, iconst_1, i80, env, static) :|: 0 <= i80 && iconst_1 = 1 && i80 <= 2
log_LE_317(i42, i118, iconst_1, i112, env, static) -{0,0}> log_LE_325(i42, i118, iconst_1, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_1 = 1
log_LE_325(i42, i118, iconst_1, i112, env, static) -{1,1}> log_Load_340(i42, i118, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_1 = 1 && iconst_1 < i118
log_Load_340(i42, i118, i112, env, static) -{1,1}> log_ConstantStackPush_342(i42, i118, i112, env, static) :|: 0 <= i112 && 2 <= i118
log_ConstantStackPush_342(i42, i118, i112, env, static) -{1,1}> log_IntArithmetic_345(i42, i118, iconst_2, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_2 = 2
log_IntArithmetic_345(i42, i118, iconst_2, i112, env, static) -{1,1}> log_InvokeMethod_347(i42, i121, i112, env, static) :|: 0 <= i112 && i118 - iconst_2 = i121 && 2 <= i118 && 0 <= i121 && iconst_2 = 2
log_InvokeMethod_347(i42, i121, i112, env, static) -{1,1}> half_ConstantStackPush_348(i121, i42, i112, env, static) :|: 0 <= i112 && 0 <= i121
half_ConstantStackPush_348(i121, i42, i112, env, static) -{1,1}> half_Store_349(iconst_0, i121, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Store_349(iconst_0, i121, i42, i112, env, static) -{1,1}> half_Load_350(i121, iconst_0, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Load_350(i121, iconst_0, i42, i112, env, static) -{0,0}> half_Load_644(i121, iconst_0, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Load_644(i270, i271, i42, i112, env, static) -{1,1}> half_ConstantStackPush_648(i270, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_ConstantStackPush_648(i270, i271, i42, i112, env, static) -{1,1}> half_LE_655(i270, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270 && iconst_1 = 1
half_LE_655(i279, iconst_1, i271, i42, i112, env, static) -{0,0}> half_LE_656(i279, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && i279 <= 1 && 0 <= i279 && iconst_1 = 1
half_LE_655(i280, iconst_1, i271, i42, i112, env, static) -{0,0}> half_LE_657(i280, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i280 && iconst_1 = 1 && 2 <= i280
half_LE_656(i279, iconst_1, i271, i42, i112, env, static) -{1,1}> half_Load_659(i271, i42, i112, env, static) :|: 0 <= i112 && i279 <= 1 && 0 <= i279 && i279 <= iconst_1 && iconst_1 = 1
half_LE_657(i280, iconst_1, i271, i42, i112, env, static) -{1,1}> half_Load_660(i280, i271, i42, i112, env, static) :|: 0 <= i112 && iconst_1 < i280 && iconst_1 = 1 && 2 <= i280
half_Load_659(i271, i42, i112, env, static) -{1,1}> half_Return_661(i271, i42, i112, env, static) :|: 0 <= i112
half_Load_660(i280, i271, i42, i112, env, static) -{1,1}> half_ConstantStackPush_662(i280, i271, i42, i112, env, static) :|: 0 <= i112 && 2 <= i280
half_Return_661(i271, i42, i112, env, static) -{1,1}> log_ConstantStackPush_664(i42, i271, i112, env, static) :|: 0 <= i112
half_ConstantStackPush_662(i280, i271, i42, i112, env, static) -{1,1}> half_IntArithmetic_666(i280, iconst_2, i271, i42, i112, env, static) :|: 0 <= i112 && 2 <= i280 && iconst_2 = 2
log_ConstantStackPush_664(i42, i271, i112, env, static) -{1,1}> log_IntArithmetic_668(i42, i271, iconst_1, i112, env, static) :|: 0 <= i112 && iconst_1 = 1
half_IntArithmetic_666(i280, iconst_2, i271, i42, i112, env, static) -{1,1}> half_Store_670(i281, i271, i42, i112, env, static) :|: i280 - iconst_2 = i281 && 0 <= i112 && 0 <= i281 && 2 <= i280 && iconst_2 = 2
log_IntArithmetic_668(i42, i271, iconst_1, i112, env, static) -{1,1}> log_Store_673(i42, i282, i112, env, static) :|: i271 + iconst_1 = i282 && 0 <= i112 && iconst_1 = 1
half_Store_670(i281, i271, i42, i112, env, static) -{1,1}> half_Inc_674(i281, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
log_Store_673(i42, i282, i112, env, static) -{1,1}> log_Inc_676(i42, i282, i112, env, static) :|: 0 <= i112
half_Inc_674(i281, i271, i42, i112, env, static) -{1,1}> half_JMP_678(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281 && i271 + 1 = i283
log_Inc_676(i42, i282, i112, env, static) -{1,1}> log_JMP_679(i42, i282, i284, env, static) :|: 0 <= i112 && i112 + 1 = i284 && 1 <= i284
half_JMP_678(i281, i283, i42, i112, env, static) -{1,1}> half_Load_680(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
log_JMP_679(i42, i282, i284, env, static) -{1,1}> log_Load_684(i42, i282, i284, env, static) :|: 1 <= i284
half_Load_680(i281, i283, i42, i112, env, static) -{0,0}> half_Load_644(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
log_Load_684(i42, i282, i284, env, static) -{1,1}> log_ConstantStackPush_685(i42, i282, i284, env, static) :|: 1 <= i284
log_ConstantStackPush_685(i42, i282, i284, env, static) -{1,1}> log_LE_686(i42, i282, iconst_1, i284, env, static) :|: iconst_1 = 1 && 1 <= i284
log_LE_686(i42, i282, iconst_1, i284, env, static) -{0,0}> log_LE_317(i42, i282, iconst_1, i284, env, static) :|: 0 <= i284 && iconst_1 = 1 && 1 <= i284

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

obtained
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
by chaining
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_4(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_21(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_21(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_26(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_29(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_29(i2, env, static) -{0,0}> langle_clinit_rangle_New_31(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_31(i2, env, static) -{0,0}> langle_clinit_rangle_New_33(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_33(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_39(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_39(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_40(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_42(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_42(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_43(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_43(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_47(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i2, env, static) -{1,1}> log_ConstantStackPush_48(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 <= static
log_ConstantStackPush_50(i2, env, static) -{0,0}> log_ConstantStackPush_51(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i2, env, static) -{0,0}> log_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i2, iconst_1, iconst_0, env, static) -{0,0}> log_LE_153(i2, i2, iconst_1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_153(i42, i43, iconst_1, i44, env, static) -{0,0}> log_LE_226(i42, i43, iconst_1, i44, env, static) :|: i44 <= 2 && iconst_1 = 1 && i44 <= 1 && 0 <= i44
log_LE_226(i42, i79, iconst_1, i80, env, static) -{0,0}> log_LE_317(i42, i79, iconst_1, i80, env, static) :|: 0 <= i80 && iconst_1 = 1 && i80 <= 2

obtained
log_LE_317(i42, i118, 1, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
by chaining
log_LE_317(i42, i118, iconst_1, i112, env, static) -{0,0}> log_LE_325(i42, i118, iconst_1, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_1 = 1
log_LE_325(i42, i118, iconst_1, i112, env, static) -{1,1}> log_Load_340(i42, i118, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_1 = 1 && iconst_1 < i118
log_Load_340(i42, i118, i112, env, static) -{1,1}> log_ConstantStackPush_342(i42, i118, i112, env, static) :|: 0 <= i112 && 2 <= i118
log_ConstantStackPush_342(i42, i118, i112, env, static) -{1,1}> log_IntArithmetic_345(i42, i118, iconst_2, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_2 = 2
log_IntArithmetic_345(i42, i118, iconst_2, i112, env, static) -{1,1}> log_InvokeMethod_347(i42, i121, i112, env, static) :|: 0 <= i112 && i118 - iconst_2 = i121 && 2 <= i118 && 0 <= i121 && iconst_2 = 2
log_InvokeMethod_347(i42, i121, i112, env, static) -{1,1}> half_ConstantStackPush_348(i121, i42, i112, env, static) :|: 0 <= i112 && 0 <= i121
half_ConstantStackPush_348(i121, i42, i112, env, static) -{1,1}> half_Store_349(iconst_0, i121, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Store_349(iconst_0, i121, i42, i112, env, static) -{1,1}> half_Load_350(i121, iconst_0, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Load_350(i121, iconst_0, i42, i112, env, static) -{0,0}> half_Load_644(i121, iconst_0, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121

obtained
half_Load_644(i270, i271, i42, i112, env, static) -{2,2}> half_LE_655(i270, 1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
by chaining
half_Load_644(i270, i271, i42, i112, env, static) -{1,1}> half_ConstantStackPush_648(i270, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_ConstantStackPush_648(i270, i271, i42, i112, env, static) -{1,1}> half_LE_655(i270, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270 && iconst_1 = 1

obtained
half_LE_655(i280, 1, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
by chaining
half_LE_655(i280, iconst_1, i271, i42, i112, env, static) -{0,0}> half_LE_657(i280, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i280 && iconst_1 = 1 && 2 <= i280
half_LE_657(i280, iconst_1, i271, i42, i112, env, static) -{1,1}> half_Load_660(i280, i271, i42, i112, env, static) :|: 0 <= i112 && iconst_1 < i280 && iconst_1 = 1 && 2 <= i280
half_Load_660(i280, i271, i42, i112, env, static) -{1,1}> half_ConstantStackPush_662(i280, i271, i42, i112, env, static) :|: 0 <= i112 && 2 <= i280
half_ConstantStackPush_662(i280, i271, i42, i112, env, static) -{1,1}> half_IntArithmetic_666(i280, iconst_2, i271, i42, i112, env, static) :|: 0 <= i112 && 2 <= i280 && iconst_2 = 2
half_IntArithmetic_666(i280, iconst_2, i271, i42, i112, env, static) -{1,1}> half_Store_670(i281, i271, i42, i112, env, static) :|: i280 - iconst_2 = i281 && 0 <= i112 && 0 <= i281 && 2 <= i280 && iconst_2 = 2
half_Store_670(i281, i271, i42, i112, env, static) -{1,1}> half_Inc_674(i281, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
half_Inc_674(i281, i271, i42, i112, env, static) -{1,1}> half_JMP_678(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281 && i271 + 1 = i283
half_JMP_678(i281, i283, i42, i112, env, static) -{1,1}> half_Load_680(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
half_Load_680(i281, i283, i42, i112, env, static) -{0,0}> half_Load_644(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281

obtained
half_LE_655(i279, 1, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'
by chaining
half_LE_655(i279, iconst_1, i271, i42, i112, env, static) -{0,0}> half_LE_656(i279, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && i279 <= 1 && 0 <= i279 && iconst_1 = 1
half_LE_656(i279, iconst_1, i271, i42, i112, env, static) -{1,1}> half_Load_659(i271, i42, i112, env, static) :|: 0 <= i112 && i279 <= 1 && 0 <= i279 && i279 <= iconst_1 && iconst_1 = 1
half_Load_659(i271, i42, i112, env, static) -{1,1}> half_Return_661(i271, i42, i112, env, static) :|: 0 <= i112
half_Return_661(i271, i42, i112, env, static) -{1,1}> log_ConstantStackPush_664(i42, i271, i112, env, static) :|: 0 <= i112
log_ConstantStackPush_664(i42, i271, i112, env, static) -{1,1}> log_IntArithmetic_668(i42, i271, iconst_1, i112, env, static) :|: 0 <= i112 && iconst_1 = 1
log_IntArithmetic_668(i42, i271, iconst_1, i112, env, static) -{1,1}> log_Store_673(i42, i282, i112, env, static) :|: i271 + iconst_1 = i282 && 0 <= i112 && iconst_1 = 1
log_Store_673(i42, i282, i112, env, static) -{1,1}> log_Inc_676(i42, i282, i112, env, static) :|: 0 <= i112
log_Inc_676(i42, i282, i112, env, static) -{1,1}> log_JMP_679(i42, i282, i284, env, static) :|: 0 <= i112 && i112 + 1 = i284 && 1 <= i284
log_JMP_679(i42, i282, i284, env, static) -{1,1}> log_Load_684(i42, i282, i284, env, static) :|: 1 <= i284
log_Load_684(i42, i282, i284, env, static) -{1,1}> log_ConstantStackPush_685(i42, i282, i284, env, static) :|: 1 <= i284
log_ConstantStackPush_685(i42, i282, i284, env, static) -{1,1}> log_LE_686(i42, i282, iconst_1, i284, env, static) :|: iconst_1 = 1 && 1 <= i284
log_LE_686(i42, i282, iconst_1, i284, env, static) -{0,0}> log_LE_317(i42, i282, iconst_1, i284, env, static) :|: 0 <= i284 && iconst_1 = 1 && 1 <= i284

(8) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: all paths from start
Rules:
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
log_LE_317(i42, i118, 1, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
half_Load_644(i270, i271, i42, i112, env, static) -{2,2}> half_LE_655(i270, 1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_LE_655(i280, 1, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
half_LE_655(i279, 1, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'

(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_317(x1, x2, x3, x4, x5, x6) → log_LE_317(x2, x4)
half_Load_644(x1, x2, x3, x4, x5, x6) → half_Load_644(x1, x2, x4)
half_LE_655(x1, x2, x3, x4, x5, x6, x7) → half_LE_655(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(i2, static) -{19,19}> log_LE_317(i2, 0) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
log_LE_317(i118, i112) -{7,7}> half_Load_644(i121', 0, i112) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
half_Load_644(i270, i271, i112) -{2,2}> half_LE_655(i270, i271, i112) :|: 0 <= i112 && 0 <= i270
half_LE_655(i280, i271, i112) -{7,7}> half_Load_644(i281', i283', i112) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
half_LE_655(i279, i271, i112) -{10,10}> log_LE_317(i282', i284') :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'

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

Moved arithmethic from constraints to rhss.

log_LE_317(i118, i112) -{7,7}> half_Load_644(i121', 0, i112) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
was transformed to
log_LE_317(i118, i112) -{7,7}> half_Load_644(i118 - 2, 0, i112) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'

half_LE_655(i280, i271, i112) -{7,7}> half_Load_644(i281', i283', i112) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
was transformed to
half_LE_655(i280, i271, i112) -{7,7}> half_Load_644(i280 - 2, i271 + 1, i112) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'

half_LE_655(i279, i271, i112) -{10,10}> log_LE_317(i282', i284') :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'
was transformed to
half_LE_655(i279, i271, i112) -{10,10}> log_LE_317(i271 + 1, i112 + 1) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'

(12) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
log_LE_317(i118, i112) -{7,7}> half_Load_644(i118 - 2, 0, i112) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
half_Load_644(i270, i271, i112) -{2,2}> half_LE_655(i270, i271, i112) :|: 0 <= i112 && 0 <= i270
half_LE_655(i280, i271, i112) -{7,7}> half_Load_644(i280 - 2, i271 + 1, i112) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
half_LE_655(i279, i271, i112) -{10,10}> log_LE_317(i271 + 1, i112 + 1) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'
log_ConstantStackPush_2(i2, static) -{19,19}> log_LE_317(i2, 0) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2

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

Simplified expressions.

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

(14) Obligation:

IntTrs with 5 rules
Start term: log_ConstantStackPush_2(#0, static)
Considered paths: all paths from start
Rules:
half_Load_644(i270, i271, i112) -{2,2}> half_LE_655(i270, i271, i112) :|: 0 <= i112 && 0 <= i270
half_LE_655(i279, i271, i112) -{10,10}> log_LE_317(i271 + 1, i112 + 1) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'
log_LE_317(i118, i112) -{7,7}> half_Load_644(i118 - 2, 0, i112) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
log_ConstantStackPush_2(i2, static) -{19,19}> log_LE_317(i2, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
half_LE_655(i280, i271, i112) -{7,7}> half_Load_644(i280 - 2, i271 + 1, i112) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'

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

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

(16) Obligation:

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

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

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

(18) Obligation:

IntTrs with 63 rules
Start term: log_ConstantStackPush_2(#0, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
log_ConstantStackPush_2(i2, env, static) -{0,0}> log_ConstantStackPush_4(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_4(i2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_21(iconst_0, i2, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_21(iconst_0, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_26(a2, i2, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_26(a2, i2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_29(i2, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_29(i2, env, static) -{0,0}> langle_clinit_rangle_New_31(i2, env, static) :|: 0 >= 0
langle_clinit_rangle_New_31(i2, env, static) -{0,0}> langle_clinit_rangle_New_33(i2, env, static) :|: 0 <= static
langle_clinit_rangle_New_33(i2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_35(o2, i2, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_35(o2, i2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_38(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_38(o2, i2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_39(o2, NULL, i2, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_39(o2, NULL, i2, env, static) -{1,1}> langle_init_rangle_Load_40(o2, i2, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_40(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_41(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_41(o2, i2, env, static) -{1,1}> langle_init_rangle_Load_42(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Load_42(o2, i2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_43(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_43(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_44(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_44(o2, i2, env, static) -{1,1}> langle_init_rangle_Return_45(o2, i2, env, static) :|: 0 < o2
langle_init_rangle_Return_45(o2, i2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_46(o2, i2, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_46(o2, i2, env, static) -{1,1}> langle_clinit_rangle_Return_47(i2, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_47(i2, env, static) -{1,1}> log_ConstantStackPush_48(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_48(i2, env, static) -{0,0}> log_ConstantStackPush_49(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_49(i2, env, static) -{0,0}> log_ConstantStackPush_50(i2, env, static) :|: 0 <= static
log_ConstantStackPush_50(i2, env, static) -{0,0}> log_ConstantStackPush_51(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_51(i2, env, static) -{0,0}> log_ConstantStackPush_52(i2, env, static) :|: 0 >= 0
log_ConstantStackPush_52(i2, env, static) -{1,1}> log_Store_53(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Store_53(i2, iconst_0, env, static) -{1,1}> log_Load_54(i2, iconst_0, env, static) :|: iconst_0 = 0
log_Load_54(i2, iconst_0, env, static) -{1,1}> log_ConstantStackPush_55(i2, iconst_0, env, static) :|: iconst_0 = 0
log_ConstantStackPush_55(i2, iconst_0, env, static) -{1,1}> log_LE_58(i2, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
log_LE_58(i2, iconst_1, iconst_0, env, static) -{0,0}> log_LE_153(i2, i2, iconst_1, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0
log_LE_153(i42, i43, iconst_1, i44, env, static) -{0,0}> log_LE_226(i42, i43, iconst_1, i44, env, static) :|: i44 <= 2 && iconst_1 = 1 && i44 <= 1 && 0 <= i44
log_LE_226(i42, i79, iconst_1, i80, env, static) -{0,0}> log_LE_317(i42, i79, iconst_1, i80, env, static) :|: 0 <= i80 && iconst_1 = 1 && i80 <= 2
log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, iconst_1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1
log_LE_317(i42, i118, iconst_1, i112, env, static) -{0,0}> log_LE_325(i42, i118, iconst_1, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_1 = 1
log_LE_325(i42, i118, iconst_1, i112, env, static) -{1,1}> log_Load_340(i42, i118, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_1 = 1 && iconst_1 < i118
log_Load_340(i42, i118, i112, env, static) -{1,1}> log_ConstantStackPush_342(i42, i118, i112, env, static) :|: 0 <= i112 && 2 <= i118
log_ConstantStackPush_342(i42, i118, i112, env, static) -{1,1}> log_IntArithmetic_345(i42, i118, iconst_2, i112, env, static) :|: 0 <= i112 && 2 <= i118 && iconst_2 = 2
log_IntArithmetic_345(i42, i118, iconst_2, i112, env, static) -{1,1}> log_InvokeMethod_347(i42, i121, i112, env, static) :|: 0 <= i112 && i118 - iconst_2 = i121 && 2 <= i118 && 0 <= i121 && iconst_2 = 2
log_InvokeMethod_347(i42, i121, i112, env, static) -{1,1}> half_ConstantStackPush_348(i121, i42, i112, env, static) :|: 0 <= i112 && 0 <= i121
half_ConstantStackPush_348(i121, i42, i112, env, static) -{1,1}> half_Store_349(iconst_0, i121, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Store_349(iconst_0, i121, i42, i112, env, static) -{1,1}> half_Load_350(i121, iconst_0, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Load_350(i121, iconst_0, i42, i112, env, static) -{0,0}> half_Load_644(i121, iconst_0, i42, i112, env, static) :|: 0 <= i112 && iconst_0 = 0 && 0 <= i121
half_Load_644(i270, i271, i42, i112, env, static) -{1,1}> half_ConstantStackPush_648(i270, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_ConstantStackPush_648(i270, i271, i42, i112, env, static) -{1,1}> half_LE_655(i270, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270 && iconst_1 = 1
half_LE_655(i279, iconst_1, i271, i42, i112, env, static) -{0,0}> half_LE_656(i279, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && i279 <= 1 && 0 <= i279 && iconst_1 = 1
half_LE_655(i280, iconst_1, i271, i42, i112, env, static) -{0,0}> half_LE_657(i280, iconst_1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i280 && iconst_1 = 1 && 2 <= i280
half_LE_656(i279, iconst_1, i271, i42, i112, env, static) -{1,1}> half_Load_659(i271, i42, i112, env, static) :|: 0 <= i112 && i279 <= 1 && 0 <= i279 && i279 <= iconst_1 && iconst_1 = 1
half_LE_657(i280, iconst_1, i271, i42, i112, env, static) -{1,1}> half_Load_660(i280, i271, i42, i112, env, static) :|: 0 <= i112 && iconst_1 < i280 && iconst_1 = 1 && 2 <= i280
half_Load_659(i271, i42, i112, env, static) -{1,1}> half_Return_661(i271, i42, i112, env, static) :|: 0 <= i112
half_Load_660(i280, i271, i42, i112, env, static) -{1,1}> half_ConstantStackPush_662(i280, i271, i42, i112, env, static) :|: 0 <= i112 && 2 <= i280
half_Return_661(i271, i42, i112, env, static) -{1,1}> log_ConstantStackPush_664(i42, i271, i112, env, static) :|: 0 <= i112
half_ConstantStackPush_662(i280, i271, i42, i112, env, static) -{1,1}> half_IntArithmetic_666(i280, iconst_2, i271, i42, i112, env, static) :|: 0 <= i112 && 2 <= i280 && iconst_2 = 2
log_ConstantStackPush_664(i42, i271, i112, env, static) -{1,1}> log_IntArithmetic_668(i42, i271, iconst_1, i112, env, static) :|: 0 <= i112 && iconst_1 = 1
half_IntArithmetic_666(i280, iconst_2, i271, i42, i112, env, static) -{1,1}> half_Store_670(i281, i271, i42, i112, env, static) :|: i280 - iconst_2 = i281 && 0 <= i112 && 0 <= i281 && 2 <= i280 && iconst_2 = 2
log_IntArithmetic_668(i42, i271, iconst_1, i112, env, static) -{1,1}> log_Store_673(i42, i282, i112, env, static) :|: i271 + iconst_1 = i282 && 0 <= i112 && iconst_1 = 1
half_Store_670(i281, i271, i42, i112, env, static) -{1,1}> half_Inc_674(i281, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
log_Store_673(i42, i282, i112, env, static) -{1,1}> log_Inc_676(i42, i282, i112, env, static) :|: 0 <= i112
half_Inc_674(i281, i271, i42, i112, env, static) -{1,1}> half_JMP_678(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281 && i271 + 1 = i283
log_Inc_676(i42, i282, i112, env, static) -{1,1}> log_JMP_679(i42, i282, i284, env, static) :|: 0 <= i112 && i112 + 1 = i284 && 1 <= i284
half_JMP_678(i281, i283, i42, i112, env, static) -{1,1}> half_Load_680(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
log_JMP_679(i42, i282, i284, env, static) -{1,1}> log_Load_684(i42, i282, i284, env, static) :|: 1 <= i284
half_Load_680(i281, i283, i42, i112, env, static) -{0,0}> half_Load_644(i281, i283, i42, i112, env, static) :|: 0 <= i112 && 0 <= i281
log_Load_684(i42, i282, i284, env, static) -{1,1}> log_ConstantStackPush_685(i42, i282, i284, env, static) :|: 1 <= i284
log_ConstantStackPush_685(i42, i282, i284, env, static) -{1,1}> log_LE_686(i42, i282, iconst_1, i284, env, static) :|: iconst_1 = 1 && 1 <= i284
log_LE_686(i42, i282, iconst_1, i284, env, static) -{0,0}> log_LE_317(i42, i282, iconst_1, i284, env, static) :|: 0 <= i284 && iconst_1 = 1 && 1 <= i284

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

(20) 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(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, iconst_1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1
log_LE_317(i42, i118, 1, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
half_Load_644(i270, i271, i42, i112, env, static) -{2,2}> half_LE_655(i270, 1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_LE_655(i280, 1, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
half_LE_655(i279, 1, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'

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

Moved arithmethic from lhss to constraints.

half_LE_655(i280, 1, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281'
was transformed to
half_LE_655(i280, x, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281' && x = 1

half_LE_655(i279, 1, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282'
was transformed to
half_LE_655(i279, x, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282' && x = 1

log_LE_317(i42, i118, 1, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121'
was transformed to
log_LE_317(i42, i118, x, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121' && x = 1

(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:
half_LE_655(i280, x, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281' && x = 1
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, iconst_1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1
half_Load_644(i270, i271, i42, i112, env, static) -{2,2}> half_LE_655(i270, 1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_LE_655(i279, x, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282' && x = 1
log_LE_317(i42, i118, x, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121' && x = 1

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

Moved arithmethic from constraints to rhss.

log_LE_317(i42, i118, x, i112, env, static) -{7,7}> half_Load_644(i121', 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121' && x = 1
was transformed to
log_LE_317(i42, i118, x, i112, env, static) -{7,7}> half_Load_644(i118 - 2, 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121' && x = 1

log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, iconst_1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1
was transformed to
log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, 1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1

half_LE_655(i280, x, i271, i42, i112, env, static) -{7,7}> half_Load_644(i281', i283', i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281' && x = 1
was transformed to
half_LE_655(i280, x, i271, i42, i112, env, static) -{7,7}> half_Load_644(i280 - 2, i271 + 1, i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281' && x = 1

half_LE_655(i279, x, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i282', 1, i284', env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282' && x = 1
was transformed to
half_LE_655(i279, x, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i271 + 1, 1, i112 + 1, env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282' && 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:
log_LE_317(i42, i118, x, i112, env, static) -{7,7}> half_Load_644(i118 - 2, 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121' && x = 1
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, 1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1
half_Load_644(i270, i271, i42, i112, env, static) -{2,2}> half_LE_655(i270, 1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
half_LE_655(i280, x, i271, i42, i112, env, static) -{7,7}> half_Load_644(i280 - 2, i271 + 1, i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281' && x = 1
half_LE_655(i279, x, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i271 + 1, 1, i112 + 1, env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282' && x = 1

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

Simplified expressions.

log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && 0 <= 0 && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
was transformed to
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'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:
log_LE_317(i42, i117, iconst_1, i112, env, static) -{0,0}> log_LE_324(i42, i117, 1, i112, env, static) :|: 0 <= i112 && i117 <= 1 && iconst_1 = 1
half_Load_644(i270, i271, i42, i112, env, static) -{2,2}> half_LE_655(i270, 1, i271, i42, i112, env, static) :|: 0 <= i112 && 0 <= i270
log_LE_317(i42, i118, x, i112, env, static) -{7,7}> half_Load_644(i118 - 2, 0, i42, i112, env, static) :|: 1 < i118 && 0 <= i121' && 2 <= i118 && 0 <= i112 && i118 - 2 = i121' && x = 1
half_LE_655(i280, x, i271, i42, i112, env, static) -{7,7}> half_Load_644(i280 - 2, i271 + 1, i42, i112, env, static) :|: i271 + 1 = i283' && 0 <= i112 && 0 <= i281' && 1 < i280 && 2 <= i280 && 0 <= i280 && i280 - 2 = i281' && x = 1
half_LE_655(i279, x, i271, i42, i112, env, static) -{10,10}> log_LE_317(i42, i271 + 1, 1, i112 + 1, env, static) :|: i279 <= 1 && 1 <= i284' && 0 <= i279 && 0 <= i284' && 0 <= i112 && i112 + 1 = i284' && i271 + 1 = i282' && x = 1
log_ConstantStackPush_2(i2, env, static) -{19,19}> log_LE_317(i2, i2, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(27) CESProof (EQUIVALENT transformation)

proved upper bound max(38, 19 * #0) using cofloco

(28) BOUNDS(CONSTANT, max(38, 19 * #0))

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

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

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

Simplified expressions.

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

(27) CESProof (EQUIVALENT transformation)

(28) BOUNDS(CONSTANT, max(38, 19 * #0))

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation: