time complexity proof of /tmp/tmp4w8pIb/AG313.jar

The time complexity of the given JBC problem could be proven to be BOUNDS(CONSTANT, max(46 + 14 * #0 + -14 * #1, 46)).

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

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

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

        ↳19 CESProof (⇔, 51 ms)

        ↳20 BOUNDS(CONSTANT, max(34, 34 + 14 * #0 + -14 * #1))

    ↳21 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 95 ms)

    ↳22 WeightedIntTrs

        ↳23 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 42 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

        ↳27 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳28 WeightedIntTrs

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

        ↳30 WeightedIntTrs

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

        ↳32 WeightedIntTrs

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

        ↳34 WeightedIntTrs

↳35 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(12)), 10 ms)

↳36 JBCComplexityEdges

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

    ↳38 WeightedIntTrs

    ↳39 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 38 ms)

    ↳40 WeightedIntTrs

    ↳41 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 29 ms)

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

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

    ↳46 WeightedIntTrs

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

    ↳48 WeightedIntTrs

(0) Obligation:

Need to prove time_complexity of the following program:

public class AG313 {

  public static int quot(int x, int y) {
    int i = 0;
    if(x==0) return 0;
    while (x > 0 && y > 0) {
      i += 1;
      x = (x - 1)- (y - 1);

    }
    return i;
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
AG313.quot(II)I: Graph of 68 nodes with 1 SCC.

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

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

(4) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 56 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_ConstantStackPush_1(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_43(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_43(i1, i4, env, static) -{1,1}> quot_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_47(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_48(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_51(i1, i4, env, static) :|: 0 <= static
quot_ConstantStackPush_51(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_52(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_53(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_53(i1, i4, env, static) -{1,1}> quot_Store_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Store_54(i1, i4, iconst_0, env, static) -{1,1}> quot_Load_56(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Load_56(i1, i4, iconst_0, env, static) -{1,1}> quot_NE_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_58(i8, i4, iconst_0, env, static) -{0,0}> quot_NE_61(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_58(iconst_0, i4, iconst_0, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0
quot_NE_61(i8, i4, iconst_0, env, static) -{1,1}> quot_Load_63(i8, i4, iconst_0, env, static) :|: iconst_0 = 0 && !(i8 = 0)
quot_Load_63(i8, i4, iconst_0, env, static) -{1,1}> quot_LE_70(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, iconst_0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_70(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_76(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_76(i16, i4, iconst_0, env, static) -{1,1}> quot_Load_84(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0 && 0 < i16
quot_Load_84(i16, i4, iconst_0, env, static) -{1,1}> quot_LE_90(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_90(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_169(i16, i4, i16, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0
quot_LE_169(i16, i50, i51, i52, env, static) -{0,0}> quot_LE_266(i16, i50, i51, i52, env, static) :|: 0 <= i52 && i52 <= 1 && i52 <= 2 && 1 <= i16 && 1 <= i51
quot_LE_266(i16, i99, i100, i101, env, static) -{0,0}> quot_LE_333(i16, i99, i100, i101, env, static) :|: 0 <= i101 && 1 <= i16 && i101 <= 2 && 1 <= i100
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_333(i16, i147, i138, i139, env, static) -{0,0}> quot_LE_337(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 <= i139 && 1 <= i147
quot_LE_337(i16, i147, i138, i139, env, static) -{1,1}> quot_Inc_341(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 < i147 && 1 <= i147 && 0 <= i139
quot_Inc_341(i16, i147, i138, i139, env, static) -{1,1}> quot_Load_346(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && i139 + 1 = i150 && 1 <= i147 && 0 <= i139
quot_Load_346(i16, i147, i138, i150, env, static) -{1,1}> quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 1 <= i147
quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) -{1,1}> quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) -{1,1}> quot_Load_354(i16, i147, i153, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147 && i138 - iconst_1 = i153
quot_Load_354(i16, i147, i153, i150, env, static) -{1,1}> quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && 1 <= i147
quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) -{1,1}> quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) -{1,1}> quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) :|: 0 <= i154 && i147 - iconst_1 = i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) -{1,1}> quot_Store_363(i16, i147, i155, i150, env, static) :|: 0 <= i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && i153 - i154 = i155 && 1 <= i147
quot_Store_363(i16, i147, i155, i150, env, static) -{1,1}> quot_JMP_365(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_JMP_365(i16, i147, i155, i150, env, static) -{1,1}> quot_Load_367(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_Load_367(i16, i147, i155, i150, env, static) -{1,1}> quot_LE_374(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_LE_374(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_376(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_376(i16, i147, i168, i150, env, static) -{1,1}> quot_Load_384(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 0 < i168 && 1 <= i147
quot_Load_384(i16, i147, i168, i150, env, static) -{1,1}> quot_LE_395(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_395(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 <= i150 && 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147

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

obtained
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
quot_ConstantStackPush_1(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_43(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_43(i1, i4, env, static) -{1,1}> quot_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_47(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_48(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_51(i1, i4, env, static) :|: 0 <= static
quot_ConstantStackPush_51(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_52(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_53(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_53(i1, i4, env, static) -{1,1}> quot_Store_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Store_54(i1, i4, iconst_0, env, static) -{1,1}> quot_Load_56(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Load_56(i1, i4, iconst_0, env, static) -{1,1}> quot_NE_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0

obtained
quot_NE_58(i8, i4, 0, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0)
by chaining
quot_NE_58(i8, i4, iconst_0, env, static) -{0,0}> quot_NE_61(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_61(i8, i4, iconst_0, env, static) -{1,1}> quot_Load_63(i8, i4, iconst_0, env, static) :|: iconst_0 = 0 && !(i8 = 0)
quot_Load_63(i8, i4, iconst_0, env, static) -{1,1}> quot_LE_70(i8, i4, iconst_0, env, static) :|: iconst_0 = 0

obtained
quot_LE_70(i16, i4, 0, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0
by chaining
quot_LE_70(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_76(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_76(i16, i4, iconst_0, env, static) -{1,1}> quot_Load_84(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0 && 0 < i16
quot_Load_84(i16, i4, iconst_0, env, static) -{1,1}> quot_LE_90(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_90(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_169(i16, i4, i16, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0
quot_LE_169(i16, i50, i51, i52, env, static) -{0,0}> quot_LE_266(i16, i50, i51, i52, env, static) :|: 0 <= i52 && i52 <= 1 && i52 <= 2 && 1 <= i16 && 1 <= i51
quot_LE_266(i16, i99, i100, i101, env, static) -{0,0}> quot_LE_333(i16, i99, i100, i101, env, static) :|: 0 <= i101 && 1 <= i16 && i101 <= 2 && 1 <= i100

obtained
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
by chaining
quot_LE_333(i16, i147, i138, i139, env, static) -{0,0}> quot_LE_337(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 <= i139 && 1 <= i147
quot_LE_337(i16, i147, i138, i139, env, static) -{1,1}> quot_Inc_341(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 < i147 && 1 <= i147 && 0 <= i139
quot_Inc_341(i16, i147, i138, i139, env, static) -{1,1}> quot_Load_346(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && i139 + 1 = i150 && 1 <= i147 && 0 <= i139
quot_Load_346(i16, i147, i138, i150, env, static) -{1,1}> quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 1 <= i147
quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) -{1,1}> quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) -{1,1}> quot_Load_354(i16, i147, i153, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147 && i138 - iconst_1 = i153
quot_Load_354(i16, i147, i153, i150, env, static) -{1,1}> quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && 1 <= i147
quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) -{1,1}> quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) -{1,1}> quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) :|: 0 <= i154 && i147 - iconst_1 = i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) -{1,1}> quot_Store_363(i16, i147, i155, i150, env, static) :|: 0 <= i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && i153 - i154 = i155 && 1 <= i147
quot_Store_363(i16, i147, i155, i150, env, static) -{1,1}> quot_JMP_365(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_JMP_365(i16, i147, i155, i150, env, static) -{1,1}> quot_Load_367(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_Load_367(i16, i147, i155, i150, env, static) -{1,1}> quot_LE_374(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147

obtained
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
by chaining
quot_LE_374(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_376(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_376(i16, i147, i168, i150, env, static) -{1,1}> quot_Load_384(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 0 < i168 && 1 <= i147
quot_Load_384(i16, i147, i168, i150, env, static) -{1,1}> quot_LE_395(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_395(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 <= i150 && 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147

(8) Obligation:

IntTrs with 9 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
quot_NE_58(iconst_0, i4, iconst_0, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0
quot_NE_58(i8, i4, 0, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0)
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, iconst_0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_70(i16, i4, 0, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150

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

Moved arithmethic from lhss to constraints.

quot_LE_70(i16, i4, 0, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0
was transformed to
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0

quot_NE_58(i8, i4, 0, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0)
was transformed to
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0) && x = 0

(10) Obligation:

IntTrs with 9 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_NE_58(iconst_0, i4, iconst_0, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, iconst_0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0) && x = 0

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

Linearized lhss.

quot_NE_58(iconst_0, i4, iconst_0, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0
was transformed to
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0

(12) Obligation:

IntTrs with 9 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0) && x = 0
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, iconst_0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0

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

Removed div and mod.

quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: !(i8 = 0) && x = 0
was transformed to
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 < 0 && x = 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 > 0 && x = 0

(14) Obligation:

IntTrs with 10 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, iconst_0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 < 0 && x = 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 > 0 && x = 0
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0

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

Moved arithmethic from constraints to rhss.

quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, iconst_0, env, static) :|: i15 <= -1 && iconst_0 = 0
was transformed to
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, 0, env, static) :|: i15 <= -1 && iconst_0 = 0

quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
was transformed to
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' - i147 - 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(iconst_0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0
was transformed to
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0

(16) Obligation:

IntTrs with 10 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, 0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' - i147 - 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 > 0 && x = 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 < 0 && x = 0

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

Simplified expressions.

quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0
was transformed to
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 1 <= i16 && 0 < i16 && x = 0

quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
was transformed to
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' - i147 - 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
was transformed to
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' + -1 * i147 + 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' + -1 * i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 > 0 && x = 0
was transformed to
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: 0 < i8 && x = 0

(18) Obligation:

IntTrs with 10 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 1 <= i16 && 0 < i16 && x = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' + -1 * i147 + 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' + -1 * i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, 0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 < 0 && x = 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: 0 < i8 && x = 0

(19) CESProof (EQUIVALENT transformation)

proved upper bound max(34, 34 + 14 * #0 + -14 * #1) using cofloco

(20) BOUNDS(CONSTANT, max(34, 34 + 14 * #0 + -14 * #1))

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

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

(22) Obligation:

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

(24) Obligation:

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

Moved arithmethic from lhss to constraints.

(26) Obligation:

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

Linearized lhss.

(28) Obligation:

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

Removed div and mod.

(30) Obligation:

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

Moved arithmethic from constraints to rhss.

(32) Obligation:

IntTrs with 10 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 0 <= 2 && 1 <= i16 && 0 < i16 && 0 <= 1 && 0 <= 0 && x = 0
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, 0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' - i147 - 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 > 0 && x = 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 < 0 && x = 0

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

Simplified expressions.

(34) Obligation:

IntTrs with 10 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
quot_LE_70(i16, i4, x, env, static) -{2,2}> quot_LE_333(i16, i4, i16, 0, env, static) :|: 1 <= i16 && 0 < i16 && x = 0
quot_LE_374(i16, i147, i168, i150, env, static) -{2,2}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 < i168 && 1 <= i147 && 1 <= i16 && 1 <= i150 && 1 <= i168 && 0 <= i150
quot_LE_333(i16, i147, i138, i139, env, static) -{12,12}> quot_LE_374(i16, i147, i153' + -1 * i147 + 1, i139 + 1, env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i150' && 1 <= i16 && 1 <= i138 && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' + -1 * i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_ConstantStackPush_1(i1, i4, env, static) -{18,18}> quot_NE_58(i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
quot_LE_333(i16, i146, i138, i139, env, static) -{0,0}> quot_LE_336(i16, i146, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && i146 <= 0 && 0 <= i139
quot_NE_58(iconst_0, i4, x, env, static) -{0,0}> quot_NE_62(0, i4, env, static) :|: iconst_0 = 0 && x = iconst_0
quot_LE_70(i15, i4, iconst_0, env, static) -{0,0}> quot_LE_75(i15, i4, 0, env, static) :|: i15 <= -1 && iconst_0 = 0
quot_LE_374(i16, i147, i167, i150, env, static) -{0,0}> quot_LE_375(i16, i147, i167, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147 && i167 <= 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: i8 < 0 && x = 0
quot_NE_58(i8, i4, x, env, static) -{2,2}> quot_LE_70(i8, i4, 0, env, static) :|: 0 < i8 && x = 0

(35) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(12)) transformation)

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

(36) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(38) Obligation:

IntTrs with 52 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
quot_ConstantStackPush_1(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_43(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_43(i1, i4, env, static) -{1,1}> quot_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_47(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_48(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_51(i1, i4, env, static) :|: 0 <= static
quot_ConstantStackPush_51(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_52(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_53(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_53(i1, i4, env, static) -{1,1}> quot_Store_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Store_54(i1, i4, iconst_0, env, static) -{1,1}> quot_Load_56(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Load_56(i1, i4, iconst_0, env, static) -{1,1}> quot_NE_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_58(i8, i4, iconst_0, env, static) -{0,0}> quot_NE_61(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_61(i8, i4, iconst_0, env, static) -{1,1}> quot_Load_63(i8, i4, iconst_0, env, static) :|: iconst_0 = 0 && !(i8 = 0)
quot_Load_63(i8, i4, iconst_0, env, static) -{1,1}> quot_LE_70(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_LE_70(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_76(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_76(i16, i4, iconst_0, env, static) -{1,1}> quot_Load_84(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0 && 0 < i16
quot_Load_84(i16, i4, iconst_0, env, static) -{1,1}> quot_LE_90(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_90(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_169(i16, i4, i16, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0
quot_LE_169(i16, i50, i51, i52, env, static) -{0,0}> quot_LE_266(i16, i50, i51, i52, env, static) :|: 0 <= i52 && i52 <= 1 && i52 <= 2 && 1 <= i16 && 1 <= i51
quot_LE_266(i16, i99, i100, i101, env, static) -{0,0}> quot_LE_333(i16, i99, i100, i101, env, static) :|: 0 <= i101 && 1 <= i16 && i101 <= 2 && 1 <= i100
quot_LE_333(i16, i147, i138, i139, env, static) -{0,0}> quot_LE_337(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 <= i139 && 1 <= i147
quot_LE_337(i16, i147, i138, i139, env, static) -{1,1}> quot_Inc_341(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 < i147 && 1 <= i147 && 0 <= i139
quot_Inc_341(i16, i147, i138, i139, env, static) -{1,1}> quot_Load_346(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && i139 + 1 = i150 && 1 <= i147 && 0 <= i139
quot_Load_346(i16, i147, i138, i150, env, static) -{1,1}> quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 1 <= i147
quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) -{1,1}> quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) -{1,1}> quot_Load_354(i16, i147, i153, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147 && i138 - iconst_1 = i153
quot_Load_354(i16, i147, i153, i150, env, static) -{1,1}> quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && 1 <= i147
quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) -{1,1}> quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) -{1,1}> quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) :|: 0 <= i154 && i147 - iconst_1 = i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) -{1,1}> quot_Store_363(i16, i147, i155, i150, env, static) :|: 0 <= i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && i153 - i154 = i155 && 1 <= i147
quot_Store_363(i16, i147, i155, i150, env, static) -{1,1}> quot_JMP_365(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_JMP_365(i16, i147, i155, i150, env, static) -{1,1}> quot_Load_367(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_Load_367(i16, i147, i155, i150, env, static) -{1,1}> quot_LE_374(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_LE_374(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_376(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_376(i16, i147, i168, i150, env, static) -{1,1}> quot_Load_384(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 0 < i168 && 1 <= i147
quot_Load_384(i16, i147, i168, i150, env, static) -{1,1}> quot_LE_395(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_395(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 <= i150 && 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147

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

obtained
quot_ConstantStackPush_1(i1, i4, env, static) -{22,22}> quot_LE_333(i1, i4, i1, 0, env, static'1) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && !(i1 = 0)
by chaining
quot_ConstantStackPush_1(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_3(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_25(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_26(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_43(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_43(i1, i4, env, static) -{1,1}> quot_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_47(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_48(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_48(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_51(i1, i4, env, static) :|: 0 <= static
quot_ConstantStackPush_51(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_52(i1, i4, env, static) -{0,0}> quot_ConstantStackPush_53(i1, i4, env, static) :|: 0 >= 0
quot_ConstantStackPush_53(i1, i4, env, static) -{1,1}> quot_Store_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Store_54(i1, i4, iconst_0, env, static) -{1,1}> quot_Load_56(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_Load_56(i1, i4, iconst_0, env, static) -{1,1}> quot_NE_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_58(i8, i4, iconst_0, env, static) -{0,0}> quot_NE_61(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_NE_61(i8, i4, iconst_0, env, static) -{1,1}> quot_Load_63(i8, i4, iconst_0, env, static) :|: iconst_0 = 0 && !(i8 = 0)
quot_Load_63(i8, i4, iconst_0, env, static) -{1,1}> quot_LE_70(i8, i4, iconst_0, env, static) :|: iconst_0 = 0
quot_LE_70(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_76(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_76(i16, i4, iconst_0, env, static) -{1,1}> quot_Load_84(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0 && 0 < i16
quot_Load_84(i16, i4, iconst_0, env, static) -{1,1}> quot_LE_90(i16, i4, iconst_0, env, static) :|: 1 <= i16 && iconst_0 = 0
quot_LE_90(i16, i4, iconst_0, env, static) -{0,0}> quot_LE_169(i16, i4, i16, iconst_0, env, static) :|: 0 <= iconst_0 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0
quot_LE_169(i16, i50, i51, i52, env, static) -{0,0}> quot_LE_266(i16, i50, i51, i52, env, static) :|: 0 <= i52 && i52 <= 1 && i52 <= 2 && 1 <= i16 && 1 <= i51
quot_LE_266(i16, i99, i100, i101, env, static) -{0,0}> quot_LE_333(i16, i99, i100, i101, env, static) :|: 0 <= i101 && 1 <= i16 && i101 <= 2 && 1 <= i100

obtained
quot_LE_333(i16, i147, i138, i139, env, static) -{14,14}> quot_LE_333(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
by chaining
quot_LE_333(i16, i147, i138, i139, env, static) -{0,0}> quot_LE_337(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 <= i139 && 1 <= i147
quot_LE_337(i16, i147, i138, i139, env, static) -{1,1}> quot_Inc_341(i16, i147, i138, i139, env, static) :|: 1 <= i138 && 1 <= i16 && 0 < i147 && 1 <= i147 && 0 <= i139
quot_Inc_341(i16, i147, i138, i139, env, static) -{1,1}> quot_Load_346(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && i139 + 1 = i150 && 1 <= i147 && 0 <= i139
quot_Load_346(i16, i147, i138, i150, env, static) -{1,1}> quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 1 <= i147
quot_ConstantStackPush_349(i16, i147, i138, i150, env, static) -{1,1}> quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_351(i16, i147, i138, iconst_1, i150, env, static) -{1,1}> quot_Load_354(i16, i147, i153, i150, env, static) :|: 1 <= i138 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147 && i138 - iconst_1 = i153
quot_Load_354(i16, i147, i153, i150, env, static) -{1,1}> quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && 1 <= i147
quot_ConstantStackPush_356(i16, i147, i153, i150, env, static) -{1,1}> quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_358(i16, i147, i153, iconst_1, i150, env, static) -{1,1}> quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) :|: 0 <= i154 && i147 - iconst_1 = i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && iconst_1 = 1 && 1 <= i147
quot_IntArithmetic_361(i16, i147, i153, i154, i150, env, static) -{1,1}> quot_Store_363(i16, i147, i155, i150, env, static) :|: 0 <= i154 && 1 <= i150 && 1 <= i16 && 0 <= i153 && i153 - i154 = i155 && 1 <= i147
quot_Store_363(i16, i147, i155, i150, env, static) -{1,1}> quot_JMP_365(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_JMP_365(i16, i147, i155, i150, env, static) -{1,1}> quot_Load_367(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_Load_367(i16, i147, i155, i150, env, static) -{1,1}> quot_LE_374(i16, i147, i155, i150, env, static) :|: 1 <= i150 && 1 <= i16 && 1 <= i147
quot_LE_374(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_376(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_376(i16, i147, i168, i150, env, static) -{1,1}> quot_Load_384(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 0 < i168 && 1 <= i147
quot_Load_384(i16, i147, i168, i150, env, static) -{1,1}> quot_LE_395(i16, i147, i168, i150, env, static) :|: 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147
quot_LE_395(i16, i147, i168, i150, env, static) -{0,0}> quot_LE_333(i16, i147, i168, i150, env, static) :|: 0 <= i150 && 1 <= i150 && 1 <= i168 && 1 <= i16 && 1 <= i147

(40) Obligation:

IntTrs with 2 rules
Start term: quot_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
quot_ConstantStackPush_1(i1, i4, env, static) -{22,22}> quot_LE_333(i1, i4, i1, 0, env, static'1) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && !(i1 = 0)
quot_LE_333(i16, i147, i138, i139, env, static) -{14,14}> quot_LE_333(i16, i147, i155', i150', env, static) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

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

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

quot_ConstantStackPush_1(x1, x2, x3, x4) → quot_ConstantStackPush_1(x1, x2, x4)
quot_LE_333(x1, x2, x3, x4, x5, x6) → quot_LE_333(x1, x2, x3, x4)

(42) Obligation:

IntTrs with 2 rules
Start term: quot_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && !(i1 = 0)
quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i155', i150') :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

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

Removed div and mod.

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

(44) Obligation:

IntTrs with 3 rules
Start term: quot_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && i1 > 0
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && i1 < 0
quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i155', i150') :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

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

Moved arithmethic from constraints to rhss.

quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i155', i150') :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
was transformed to
quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i153' - i147 - 1, i139 + 1) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

(46) Obligation:

IntTrs with 3 rules
Start term: quot_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && i1 > 0
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 0 >= 0 && 1 <= i1 && 0 < i1 && 0 <= 2 && 0 < 2 && 0 <= 0 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= 1 && 0 <= static''' && static'1 <= static''' + 1 && i1 < 0
quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i153' - i147 - 1, i139 + 1) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

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

Simplified expressions.

quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i153' - i147 - 1, i139 + 1) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' - i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
was transformed to
quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i153' + -1 * i147 + 1, i139 + 1) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' + -1 * i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'

(48) Obligation:

IntTrs with 3 rules
Start term: quot_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
quot_LE_333(i16, i147, i138, i139) -{14,14}> quot_LE_333(i16, i147, i153' + -1 * i147 + 1, i139 + 1) :|: 0 <= i139 && 1 <= i147 && 0 < i147 && 1 <= i16 && 0 < i155' && 1 <= i155' && 1 <= i138 && 0 <= i150' && 1 <= i150' && 0 <= i154' && 0 <= i153' && i147 - 1 = i154' && i153' + -1 * i154' = i155' && i139 + 1 = i150' && i138 - 1 = i153'
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 1 <= i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && 0 < i1
quot_ConstantStackPush_1(i1, i4, static) -{22,22}> quot_LE_333(i1, i4, i1, 0) :|: 1 <= i1 && 0 < i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1 && i1 < 0