time complexity proof of /tmp/tmp7dlk7M/DivMinus2.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 117 ms)

    ↳16 WeightedIntTrs

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

        ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

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

        ↳24 WeightedIntTrs

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

↳26 JBCComplexityEdges

    ↳27 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 62 ms)

    ↳28 WeightedIntTrs

    ↳29 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 43 ms)

    ↳30 WeightedIntTrs

    ↳31 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 43 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), 0 ms)

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 173 ms)

    ↳40 BOUNDS(CONSTANT, 17 + 93 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

  public static int minus(int x, int y) {
    while (y != 0) {
      if (y > 0)  {
        y--;
        x--;
      } else  {
        y++;
        x++;
      }
    }
    return x;
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 67 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 67 jbc graph edges to a weighted ITS with 67 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 67 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_1(i2, i3, env, static) -{0,0}> div_ConstantStackPush_4(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, env, static) -{1,1}> div_ConstantStackPush_41(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i3, env, static) -{0,0}> div_ConstantStackPush_42(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i3, env, static) -{0,0}> div_ConstantStackPush_43(i2, i3, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i3, env, static) -{0,0}> div_ConstantStackPush_45(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i3, env, static) -{0,0}> div_ConstantStackPush_46(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_46(i2, i3, env, static) -{1,1}> div_Store_49(i2, i3, iconst_0, env, static) :|: iconst_0 = 0
div_Store_49(i2, i3, iconst_0, env, static) -{1,1}> div_Load_51(i2, i3, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i3, iconst_0, env, static) -{0,0}> div_Load_193(i2, i3, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_Load_193(i72, i73, i74, i75, env, static) -{0,0}> div_Load_334(i72, i73, i74, i75, env, static) :|: i75 <= 1 && 0 <= i75 && i75 <= 2
div_Load_334(i72, i147, i148, i149, env, static) -{0,0}> div_Load_468(i72, i147, i148, i149, env, static) :|: i149 <= 2 && 0 <= i149
div_Load_468(i72, i211, i212, i213, env, static) -{1,1}> div_Load_472(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_Load_472(i72, i211, i212, i213, env, static) -{1,1}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_493(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_LT_493(i72, i211, i212, i213, env, static) -{1,1}> div_Load_501(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_Load_501(i72, i211, i212, i213, env, static) -{1,1}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
div_LE_504(i72, i234, i235, i213, env, static) -{0,0}> div_LE_507(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_LE_507(i72, i234, i235, i213, env, static) -{1,1}> div_Load_509(i72, i234, i235, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_509(i72, i234, i235, i213, env, static) -{1,1}> div_Load_511(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_511(i72, i234, i235, i213, env, static) -{1,1}> div_InvokeMethod_516(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_InvokeMethod_516(i72, i234, i235, i213, env, static) -{1,1}> minus_Load_517(i235, i234, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_517(i235, i234, i72, i213, env, static) -{1,1}> minus_EQ_520(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_EQ_520(i234, i235, i72, i213, env, static) -{1,1}> minus_Load_522(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_522(i235, i234, i72, i213, env, static) -{1,1}> minus_LE_525(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_LE_525(i234, i235, i72, i213, env, static) -{1,1}> minus_Inc_527(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Inc_527(i235, i234, i72, i213, env, static) -{1,1}> minus_Inc_529(i235, i237, i72, i234, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 0 <= i237 && i234 + -1 = i237 && 1 <= i234
minus_Inc_529(i235, i237, i72, i234, i213, env, static) -{1,1}> minus_JMP_531(i238, i237, i72, i234, i213, env, static) :|: i235 + -1 = i238 && 0 <= i238 && 1 <= i235 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_JMP_531(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_Load_535(i238, i237, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{0,0}> minus_EQ_545(i250, i252, i72, i251, i213, env, static) :|: 0 <= i250 && 1 <= i251 && 1 <= i250 && 0 <= i252 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_EQ_542(iconst_0, i238, i72, i234, i213, env, static) -{0,0}> minus_EQ_547(iconst_0, i238, i72, i234, i213, env, static) :|: 0 <= iconst_0 && 0 <= i238 && iconst_0 = 0 && 0 <= i213 && 1 <= i234
minus_EQ_545(i250, i252, i72, i251, i213, env, static) -{1,1}> minus_Load_550(i252, i250, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 < i250
minus_EQ_547(iconst_0, i238, i72, i234, i213, env, static) -{1,1}> minus_Load_553(i238, i72, i234, i213, env, static) :|: 0 <= i238 && iconst_0 = 0 && 0 <= i213 && 1 <= i234
minus_Load_550(i252, i250, i72, i251, i213, env, static) -{1,1}> minus_LE_556(i250, i252, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_Load_553(i238, i72, i234, i213, env, static) -{1,1}> minus_Return_558(i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_LE_556(i250, i252, i72, i251, i213, env, static) -{1,1}> minus_Inc_562(i252, i250, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 < i250
minus_Return_558(i238, i72, i234, i213, env, static) -{1,1}> div_Store_563(i72, i234, i238, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Inc_562(i252, i250, i72, i251, i213, env, static) -{1,1}> minus_Inc_568(i252, i261, i72, i251, i213, env, static) :|: i250 + -1 = i261 && 0 <= i261 && 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251
div_Store_563(i72, i234, i238, i213, env, static) -{1,1}> div_Load_570(i72, i234, i238, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Inc_568(i252, i261, i72, i251, i213, env, static) -{1,1}> minus_JMP_574(i266, i261, i72, i251, i213, env, static) :|: i252 + -1 = i266 && 0 <= i261 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 <= i266
div_Load_570(i72, i234, i238, i213, env, static) -{1,1}> div_ConstantStackPush_576(i72, i234, i213, i238, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_JMP_574(i266, i261, i72, i251, i213, env, static) -{1,1}> minus_Load_580(i266, i261, i72, i251, i213, env, static) :|: 0 <= i261 && 0 <= i213 && 2 <= i251 && 0 <= i266
div_ConstantStackPush_576(i72, i234, i213, i238, env, static) -{1,1}> div_IntArithmetic_581(i72, i234, i213, iconst_1, i238, env, static) :|: iconst_1 = 1 && 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Load_580(i266, i261, i72, i251, i213, env, static) -{0,0}> minus_Load_535(i266, i261, i72, i251, i213, env, static) :|: 0 <= i261 && 1 <= i251 && 0 <= i213 && 2 <= i251 && 0 <= i266
div_IntArithmetic_581(i72, i234, i213, iconst_1, i238, env, static) -{1,1}> div_Store_582(i72, i234, i273, i238, env, static) :|: i213 + iconst_1 = i273 && iconst_1 = 1 && 0 <= i238 && 1 <= i273 && 0 <= i213 && 1 <= i234
div_Store_582(i72, i234, i273, i238, env, static) -{1,1}> div_JMP_583(i72, i234, i238, i273, env, static) :|: 0 <= i238 && 1 <= i273 && 1 <= i234
div_JMP_583(i72, i234, i238, i273, env, static) -{1,1}> div_Load_584(i72, i234, i238, i273, env, static) :|: 0 <= i238 && 1 <= i273 && 1 <= i234
div_Load_584(i72, i234, i238, i273, env, static) -{0,0}> div_Load_468(i72, i234, i238, i273, env, static) :|: 0 <= i273 && 0 <= i238 && 1 <= i273 && 1 <= i234

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

obtained
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
by chaining
div_ConstantStackPush_1(i2, i3, env, static) -{0,0}> div_ConstantStackPush_4(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, env, static) -{1,1}> div_ConstantStackPush_41(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i3, env, static) -{0,0}> div_ConstantStackPush_42(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i3, env, static) -{0,0}> div_ConstantStackPush_43(i2, i3, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i3, env, static) -{0,0}> div_ConstantStackPush_45(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i3, env, static) -{0,0}> div_ConstantStackPush_46(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_46(i2, i3, env, static) -{1,1}> div_Store_49(i2, i3, iconst_0, env, static) :|: iconst_0 = 0
div_Store_49(i2, i3, iconst_0, env, static) -{1,1}> div_Load_51(i2, i3, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i3, iconst_0, env, static) -{0,0}> div_Load_193(i2, i3, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_Load_193(i72, i73, i74, i75, env, static) -{0,0}> div_Load_334(i72, i73, i74, i75, env, static) :|: i75 <= 1 && 0 <= i75 && i75 <= 2
div_Load_334(i72, i147, i148, i149, env, static) -{0,0}> div_Load_468(i72, i147, i148, i149, env, static) :|: i149 <= 2 && 0 <= i149

obtained
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
by chaining
div_Load_468(i72, i211, i212, i213, env, static) -{1,1}> div_Load_472(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_Load_472(i72, i211, i212, i213, env, static) -{1,1}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213

obtained
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
by chaining
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_493(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_LT_493(i72, i211, i212, i213, env, static) -{1,1}> div_Load_501(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_Load_501(i72, i211, i212, i213, env, static) -{1,1}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213

obtained
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i238', i237', i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234
by chaining
div_LE_504(i72, i234, i235, i213, env, static) -{0,0}> div_LE_507(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_LE_507(i72, i234, i235, i213, env, static) -{1,1}> div_Load_509(i72, i234, i235, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_509(i72, i234, i235, i213, env, static) -{1,1}> div_Load_511(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_511(i72, i234, i235, i213, env, static) -{1,1}> div_InvokeMethod_516(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_InvokeMethod_516(i72, i234, i235, i213, env, static) -{1,1}> minus_Load_517(i235, i234, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_517(i235, i234, i72, i213, env, static) -{1,1}> minus_EQ_520(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_EQ_520(i234, i235, i72, i213, env, static) -{1,1}> minus_Load_522(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_522(i235, i234, i72, i213, env, static) -{1,1}> minus_LE_525(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_LE_525(i234, i235, i72, i213, env, static) -{1,1}> minus_Inc_527(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Inc_527(i235, i234, i72, i213, env, static) -{1,1}> minus_Inc_529(i235, i237, i72, i234, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 0 <= i237 && i234 + -1 = i237 && 1 <= i234
minus_Inc_529(i235, i237, i72, i234, i213, env, static) -{1,1}> minus_JMP_531(i238, i237, i72, i234, i213, env, static) :|: i235 + -1 = i238 && 0 <= i238 && 1 <= i235 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_JMP_531(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_Load_535(i238, i237, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234

obtained
minus_EQ_542(0, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213
by chaining
minus_EQ_542(iconst_0, i238, i72, i234, i213, env, static) -{0,0}> minus_EQ_547(iconst_0, i238, i72, i234, i213, env, static) :|: 0 <= iconst_0 && 0 <= i238 && iconst_0 = 0 && 0 <= i213 && 1 <= i234
minus_EQ_547(iconst_0, i238, i72, i234, i213, env, static) -{1,1}> minus_Load_553(i238, i72, i234, i213, env, static) :|: 0 <= i238 && iconst_0 = 0 && 0 <= i213 && 1 <= i234
minus_Load_553(i238, i72, i234, i213, env, static) -{1,1}> minus_Return_558(i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Return_558(i238, i72, i234, i213, env, static) -{1,1}> div_Store_563(i72, i234, i238, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
div_Store_563(i72, i234, i238, i213, env, static) -{1,1}> div_Load_570(i72, i234, i238, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
div_Load_570(i72, i234, i238, i213, env, static) -{1,1}> div_ConstantStackPush_576(i72, i234, i213, i238, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
div_ConstantStackPush_576(i72, i234, i213, i238, env, static) -{1,1}> div_IntArithmetic_581(i72, i234, i213, iconst_1, i238, env, static) :|: iconst_1 = 1 && 0 <= i238 && 0 <= i213 && 1 <= i234
div_IntArithmetic_581(i72, i234, i213, iconst_1, i238, env, static) -{1,1}> div_Store_582(i72, i234, i273, i238, env, static) :|: i213 + iconst_1 = i273 && iconst_1 = 1 && 0 <= i238 && 1 <= i273 && 0 <= i213 && 1 <= i234
div_Store_582(i72, i234, i273, i238, env, static) -{1,1}> div_JMP_583(i72, i234, i238, i273, env, static) :|: 0 <= i238 && 1 <= i273 && 1 <= i234
div_JMP_583(i72, i234, i238, i273, env, static) -{1,1}> div_Load_584(i72, i234, i238, i273, env, static) :|: 0 <= i238 && 1 <= i273 && 1 <= i234
div_Load_584(i72, i234, i238, i273, env, static) -{0,0}> div_Load_468(i72, i234, i238, i273, env, static) :|: 0 <= i273 && 0 <= i238 && 1 <= i273 && 1 <= i234

obtained
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i266', i261', i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
by chaining
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{0,0}> minus_EQ_545(i250, i252, i72, i251, i213, env, static) :|: 0 <= i250 && 1 <= i251 && 1 <= i250 && 0 <= i252 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_EQ_545(i250, i252, i72, i251, i213, env, static) -{1,1}> minus_Load_550(i252, i250, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 < i250
minus_Load_550(i252, i250, i72, i251, i213, env, static) -{1,1}> minus_LE_556(i250, i252, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_LE_556(i250, i252, i72, i251, i213, env, static) -{1,1}> minus_Inc_562(i252, i250, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 < i250
minus_Inc_562(i252, i250, i72, i251, i213, env, static) -{1,1}> minus_Inc_568(i252, i261, i72, i251, i213, env, static) :|: i250 + -1 = i261 && 0 <= i261 && 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_Inc_568(i252, i261, i72, i251, i213, env, static) -{1,1}> minus_JMP_574(i266, i261, i72, i251, i213, env, static) :|: i252 + -1 = i266 && 0 <= i261 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 <= i266
minus_JMP_574(i266, i261, i72, i251, i213, env, static) -{1,1}> minus_Load_580(i266, i261, i72, i251, i213, env, static) :|: 0 <= i261 && 0 <= i213 && 2 <= i251 && 0 <= i266
minus_Load_580(i266, i261, i72, i251, i213, env, static) -{0,0}> minus_Load_535(i266, i261, i72, i251, i213, env, static) :|: 0 <= i261 && 1 <= i251 && 0 <= i213 && 2 <= i251 && 0 <= i266

(8) Obligation:

IntTrs with 9 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i238', i237', i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(0, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i266', i261', i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250

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

Moved arithmethic from lhss to constraints.

minus_EQ_542(0, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213
was transformed to
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0

(10) Obligation:

IntTrs with 9 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i266', i261', i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i238', i237', i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234

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

Moved arithmethic from constraints to rhss.

minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
was transformed to
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0

minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i266', i261', i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
was transformed to
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250

div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i238', i237', i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234
was transformed to
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 + -1, i234 + -1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234

(12) Obligation:

IntTrs with 9 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 + -1, i234 + -1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234

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

Simplified expressions.

minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
was transformed to
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 - 1, i250 - 1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 - 1 = i261' && 0 <= i261' && 1 <= i251 && i252 - 1 = i266' && 1 <= i250

div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 + -1, i234 + -1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234
was transformed to
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 - 1, i234 - 1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 - 1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 - 1 = i237' && 0 < i234

minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
was transformed to
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= i213 && x = 0

div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
was transformed to
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(14) Obligation:

IntTrs with 9 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= i213 && x = 0
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 - 1, i250 - 1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 - 1 = i261' && 0 <= i261' && 1 <= i251 && i252 - 1 = i266' && 1 <= i250
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 - 1, i234 - 1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 - 1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 - 1 = i237' && 0 < i234
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234

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

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

(16) Obligation:

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

(18) Obligation:

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

Moved arithmethic from lhss to constraints.

(20) Obligation:

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

Moved arithmethic from constraints to rhss.

(22) Obligation:

IntTrs with 9 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 + -1, i234 + -1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 + -1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 + -1 = i237' && 0 < i234

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

Simplified expressions.

(24) Obligation:

IntTrs with 9 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
div_Load_468(i72, i211, i212, i213, env, static) -{2,2}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
minus_EQ_542(x, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i213 + 1, env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= i213 && x = 0
div_LT_485(i72, i211, i212, i213, env, static) -{2,2}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213 && i211 <= i212
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i252 - 1, i250 - 1, i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 - 1 = i261' && 0 <= i261' && 1 <= i251 && i252 - 1 = i266' && 1 <= i250
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_492(i72, i211, i212, i213, env, static) :|: i212 < i211 && 0 <= i213
div_LE_504(i72, i233, i212, i213, env, static) -{0,0}> div_LE_506(i72, i233, i212, i213, env, static) :|: i233 <= 0 && 0 <= i213
div_LE_504(i72, i234, i235, i213, env, static) -{11,11}> minus_Load_535(i235 - 1, i234 - 1, i72, i234, i213, env, static) :|: 0 <= i238' && 1 <= i234 && i235 - 1 = i238' && 0 <= i237' && 1 <= i235 && 0 <= i213 && i234 - 1 = i237' && 0 < i234
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234

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

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 65 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_1(i2, i3, env, static) -{0,0}> div_ConstantStackPush_4(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_14(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_14(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_17(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_38(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_38(i2, i3, env, static) -{1,1}> div_ConstantStackPush_41(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_41(i2, i3, env, static) -{0,0}> div_ConstantStackPush_42(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_42(i2, i3, env, static) -{0,0}> div_ConstantStackPush_43(i2, i3, env, static) :|: 0 <= static
div_ConstantStackPush_43(i2, i3, env, static) -{0,0}> div_ConstantStackPush_45(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_45(i2, i3, env, static) -{0,0}> div_ConstantStackPush_46(i2, i3, env, static) :|: 0 >= 0
div_ConstantStackPush_46(i2, i3, env, static) -{1,1}> div_Store_49(i2, i3, iconst_0, env, static) :|: iconst_0 = 0
div_Store_49(i2, i3, iconst_0, env, static) -{1,1}> div_Load_51(i2, i3, iconst_0, env, static) :|: iconst_0 = 0
div_Load_51(i2, i3, iconst_0, env, static) -{0,0}> div_Load_193(i2, i3, i2, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
div_Load_193(i72, i73, i74, i75, env, static) -{0,0}> div_Load_334(i72, i73, i74, i75, env, static) :|: i75 <= 1 && 0 <= i75 && i75 <= 2
div_Load_334(i72, i147, i148, i149, env, static) -{0,0}> div_Load_468(i72, i147, i148, i149, env, static) :|: i149 <= 2 && 0 <= i149
div_Load_468(i72, i211, i212, i213, env, static) -{1,1}> div_Load_472(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_Load_472(i72, i211, i212, i213, env, static) -{1,1}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_493(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_LT_493(i72, i211, i212, i213, env, static) -{1,1}> div_Load_501(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_Load_501(i72, i211, i212, i213, env, static) -{1,1}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LE_504(i72, i234, i235, i213, env, static) -{0,0}> div_LE_507(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_LE_507(i72, i234, i235, i213, env, static) -{1,1}> div_Load_509(i72, i234, i235, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_509(i72, i234, i235, i213, env, static) -{1,1}> div_Load_511(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_511(i72, i234, i235, i213, env, static) -{1,1}> div_InvokeMethod_516(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_InvokeMethod_516(i72, i234, i235, i213, env, static) -{1,1}> minus_Load_517(i235, i234, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_517(i235, i234, i72, i213, env, static) -{1,1}> minus_EQ_520(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_EQ_520(i234, i235, i72, i213, env, static) -{1,1}> minus_Load_522(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_522(i235, i234, i72, i213, env, static) -{1,1}> minus_LE_525(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_LE_525(i234, i235, i72, i213, env, static) -{1,1}> minus_Inc_527(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Inc_527(i235, i234, i72, i213, env, static) -{1,1}> minus_Inc_529(i235, i237, i72, i234, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 0 <= i237 && i234 + -1 = i237 && 1 <= i234
minus_Inc_529(i235, i237, i72, i234, i213, env, static) -{1,1}> minus_JMP_531(i238, i237, i72, i234, i213, env, static) :|: i235 + -1 = i238 && 0 <= i238 && 1 <= i235 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_JMP_531(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_Load_535(i238, i237, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{0,0}> minus_EQ_545(i250, i252, i72, i251, i213, env, static) :|: 0 <= i250 && 1 <= i251 && 1 <= i250 && 0 <= i252 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_EQ_542(iconst_0, i238, i72, i234, i213, env, static) -{0,0}> minus_EQ_547(iconst_0, i238, i72, i234, i213, env, static) :|: 0 <= iconst_0 && 0 <= i238 && iconst_0 = 0 && 0 <= i213 && 1 <= i234
minus_EQ_545(i250, i252, i72, i251, i213, env, static) -{1,1}> minus_Load_550(i252, i250, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 < i250
minus_EQ_547(iconst_0, i238, i72, i234, i213, env, static) -{1,1}> minus_Load_553(i238, i72, i234, i213, env, static) :|: 0 <= i238 && iconst_0 = 0 && 0 <= i213 && 1 <= i234
minus_Load_550(i252, i250, i72, i251, i213, env, static) -{1,1}> minus_LE_556(i250, i252, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251
minus_Load_553(i238, i72, i234, i213, env, static) -{1,1}> minus_Return_558(i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_LE_556(i250, i252, i72, i251, i213, env, static) -{1,1}> minus_Inc_562(i252, i250, i72, i251, i213, env, static) :|: 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 < i250
minus_Return_558(i238, i72, i234, i213, env, static) -{1,1}> div_Store_563(i72, i234, i238, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Inc_562(i252, i250, i72, i251, i213, env, static) -{1,1}> minus_Inc_568(i252, i261, i72, i251, i213, env, static) :|: i250 + -1 = i261 && 0 <= i261 && 1 <= i250 && 0 <= i213 && 1 <= i252 && 2 <= i251
div_Store_563(i72, i234, i238, i213, env, static) -{1,1}> div_Load_570(i72, i234, i238, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Inc_568(i252, i261, i72, i251, i213, env, static) -{1,1}> minus_JMP_574(i266, i261, i72, i251, i213, env, static) :|: i252 + -1 = i266 && 0 <= i261 && 0 <= i213 && 1 <= i252 && 2 <= i251 && 0 <= i266
div_Load_570(i72, i234, i238, i213, env, static) -{1,1}> div_ConstantStackPush_576(i72, i234, i213, i238, env, static) :|: 0 <= i238 && 0 <= i213 && 1 <= i234
minus_JMP_574(i266, i261, i72, i251, i213, env, static) -{1,1}> minus_Load_580(i266, i261, i72, i251, i213, env, static) :|: 0 <= i261 && 0 <= i213 && 2 <= i251 && 0 <= i266
div_ConstantStackPush_576(i72, i234, i213, i238, env, static) -{1,1}> div_IntArithmetic_581(i72, i234, i213, iconst_1, i238, env, static) :|: iconst_1 = 1 && 0 <= i238 && 0 <= i213 && 1 <= i234
minus_Load_580(i266, i261, i72, i251, i213, env, static) -{0,0}> minus_Load_535(i266, i261, i72, i251, i213, env, static) :|: 0 <= i261 && 1 <= i251 && 0 <= i213 && 2 <= i251 && 0 <= i266
div_IntArithmetic_581(i72, i234, i213, iconst_1, i238, env, static) -{1,1}> div_Store_582(i72, i234, i273, i238, env, static) :|: i213 + iconst_1 = i273 && iconst_1 = 1 && 0 <= i238 && 1 <= i273 && 0 <= i213 && 1 <= i234
div_Store_582(i72, i234, i273, i238, env, static) -{1,1}> div_JMP_583(i72, i234, i238, i273, env, static) :|: 0 <= i238 && 1 <= i273 && 1 <= i234
div_JMP_583(i72, i234, i238, i273, env, static) -{1,1}> div_Load_584(i72, i234, i238, i273, env, static) :|: 0 <= i238 && 1 <= i273 && 1 <= i234
div_Load_584(i72, i234, i238, i273, env, static) -{0,0}> div_Load_468(i72, i234, i238, i273, env, static) :|: 0 <= i273 && 0 <= i238 && 1 <= i273 && 1 <= i234

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

obtained
div_Load_468(i72, i211, i212, i213, env, static) -{15,15}> minus_Load_535(i238', i237', i72, i211, i213, env, static) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
by chaining
div_Load_468(i72, i211, i212, i213, env, static) -{1,1}> div_Load_472(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_Load_472(i72, i211, i212, i213, env, static) -{1,1}> div_LT_485(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LT_485(i72, i211, i212, i213, env, static) -{0,0}> div_LT_493(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_LT_493(i72, i211, i212, i213, env, static) -{1,1}> div_Load_501(i72, i211, i212, i213, env, static) :|: i211 <= i212 && 0 <= i213
div_Load_501(i72, i211, i212, i213, env, static) -{1,1}> div_LE_504(i72, i211, i212, i213, env, static) :|: 0 <= i213
div_LE_504(i72, i234, i235, i213, env, static) -{0,0}> div_LE_507(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_LE_507(i72, i234, i235, i213, env, static) -{1,1}> div_Load_509(i72, i234, i235, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_509(i72, i234, i235, i213, env, static) -{1,1}> div_Load_511(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_Load_511(i72, i234, i235, i213, env, static) -{1,1}> div_InvokeMethod_516(i72, i234, i235, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
div_InvokeMethod_516(i72, i234, i235, i213, env, static) -{1,1}> minus_Load_517(i235, i234, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_517(i235, i234, i72, i213, env, static) -{1,1}> minus_EQ_520(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_EQ_520(i234, i235, i72, i213, env, static) -{1,1}> minus_Load_522(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Load_522(i235, i234, i72, i213, env, static) -{1,1}> minus_LE_525(i234, i235, i72, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 1 <= i234
minus_LE_525(i234, i235, i72, i213, env, static) -{1,1}> minus_Inc_527(i235, i234, i72, i213, env, static) :|: 0 < i234 && 1 <= i235 && 0 <= i213 && 1 <= i234
minus_Inc_527(i235, i234, i72, i213, env, static) -{1,1}> minus_Inc_529(i235, i237, i72, i234, i213, env, static) :|: 1 <= i235 && 0 <= i213 && 0 <= i237 && i234 + -1 = i237 && 1 <= i234
minus_Inc_529(i235, i237, i72, i234, i213, env, static) -{1,1}> minus_JMP_531(i238, i237, i72, i234, i213, env, static) :|: i235 + -1 = i238 && 0 <= i238 && 1 <= i235 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_JMP_531(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_Load_535(i238, i237, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234

(30) Obligation:

IntTrs with 5 rules
Start term: div_ConstantStackPush_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_1(i2, i3, env, static) -{17,17}> div_Load_468(i2, i3, i2, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
div_Load_468(i72, i211, i212, i213, env, static) -{15,15}> minus_Load_535(i238', i237', i72, i211, i213, env, static) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
minus_Load_535(i238, i237, i72, i234, i213, env, static) -{1,1}> minus_EQ_542(i237, i238, i72, i234, i213, env, static) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(0, i238, i72, i234, i213, env, static) -{9,9}> div_Load_468(i72, i234, i238, i273', env, static) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213
minus_EQ_542(i250, i252, i72, i251, i213, env, static) -{6,6}> minus_Load_535(i266', i261', i72, i251, i213, env, static) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250

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

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

div_ConstantStackPush_1(x1, x2, x3, x4) → div_ConstantStackPush_1(x1, x2, x4)
div_Load_468(x1, x2, x3, x4, x5, x6) → div_Load_468(x2, x3, x4)
minus_Load_535(x1, x2, x3, x4, x5, x6, x7) → minus_Load_535(x1, x2, x4, x5)
minus_EQ_542(x1, x2, x3, x4, x5, x6, x7) → minus_EQ_542(x1, x2, x4, x5)

(32) Obligation:

IntTrs with 5 rules
Start term: div_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
div_ConstantStackPush_1(i2, i3, static) -{17,17}> div_Load_468(i3, i2, 0) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i238', i237', i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
minus_Load_535(i238, i237, i234, i213) -{1,1}> minus_EQ_542(i237, i238, i234, i213) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(0, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i273') :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213
minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i266', i261', i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250

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

Moved arithmethic from lhss to constraints.

minus_EQ_542(0, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i273') :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213
was transformed to
minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i273') :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0

(34) Obligation:

IntTrs with 5 rules
Start term: div_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i266', i261', i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i238', i237', i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
minus_Load_535(i238, i237, i234, i213) -{1,1}> minus_EQ_542(i237, i238, i234, i213) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
div_ConstantStackPush_1(i2, i3, static) -{17,17}> div_Load_468(i3, i2, 0) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i273') :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0

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

Moved arithmethic from constraints to rhss.

div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i238', i237', i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
was transformed to
div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i212 + -1, i211 + -1, i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211

minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i266', i261', i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
was transformed to
minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250

minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i273') :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
was transformed to
minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i213 + 1) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0

(36) Obligation:

IntTrs with 5 rules
Start term: div_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i212 + -1, i211 + -1, i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
div_ConstantStackPush_1(i2, i3, static) -{17,17}> div_Load_468(i3, i2, 0) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
minus_Load_535(i238, i237, i234, i213) -{1,1}> minus_EQ_542(i237, i238, i234, i213) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i213 + 1) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0

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

Simplified expressions.

div_ConstantStackPush_1(i2, i3, static) -{17,17}> div_Load_468(i3, i2, 0) :|: static'1 <= static''' + 1 && 0 <= 2 && 0 <= 0 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 < 2 && 0 >= 0
was transformed to
div_ConstantStackPush_1(i2, i3, static) -{17,17}> div_Load_468(i3, i2, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i212 + -1, i211 + -1, i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 + -1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 + -1 = i237' && i211 <= i212 && 0 < i211
was transformed to
div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i212 - 1, i211 - 1, i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 - 1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 - 1 = i237' && i211 <= i212 && 0 < i211

minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i213 + 1) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= 0 && 0 <= i213 && x = 0
was transformed to
minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i213 + 1) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= i213 && x = 0

minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i252 + -1, i250 + -1, i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 + -1 = i261' && 0 <= i261' && 1 <= i251 && i252 + -1 = i266' && 1 <= i250 && 0 <= i250
was transformed to
minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i252 - 1, i250 - 1, i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 - 1 = i261' && 0 <= i261' && 1 <= i251 && i252 - 1 = i266' && 1 <= i250

(38) Obligation:

IntTrs with 5 rules
Start term: div_ConstantStackPush_1(#0, #1, static)
Considered paths: all paths from start
Rules:
minus_Load_535(i238, i237, i234, i213) -{1,1}> minus_EQ_542(i237, i238, i234, i213) :|: 0 <= i238 && 0 <= i213 && 0 <= i237 && 1 <= i234
div_ConstantStackPush_1(i2, i3, static) -{17,17}> div_Load_468(i3, i2, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
div_Load_468(i211, i212, i213) -{15,15}> minus_Load_535(i212 - 1, i211 - 1, i211, i213) :|: 0 <= i238' && 1 <= i211 && i212 - 1 = i238' && 0 <= i237' && 1 <= i212 && 0 <= i213 && i211 - 1 = i237' && i211 <= i212 && 0 < i211
minus_EQ_542(x, i238, i234, i213) -{9,9}> div_Load_468(i234, i238, i213 + 1) :|: i213 + 1 = i273' && 1 <= i234 && 1 <= i273' && 0 <= i238 && 0 <= i273' && 0 <= i213 && x = 0
minus_EQ_542(i250, i252, i251, i213) -{6,6}> minus_Load_535(i252 - 1, i250 - 1, i251, i213) :|: 0 <= i252 && 0 <= i266' && 0 < i250 && 2 <= i251 && 1 <= i252 && 0 <= i213 && i250 - 1 = i261' && 0 <= i261' && 1 <= i251 && i252 - 1 = i266' && 1 <= i250

(39) koat Proof (EQUIVALENT transformation)

YES(?, 93*ar_0 + 17)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 1) minus_Load_535(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_542(ar_1, ar_0, ar_2, ar_3)) [ 0 <= ar_0 /\ 0 <= ar_3 /\ 0 <= ar_1 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 17) div_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_1, ar_0, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 15) div_Load_468(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_0, ar_2)) [ 0 <= i238' /\ 1 <= ar_0 /\ ar_1 - 1 = i238' /\ 0 <= i237' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ ar_0 - 1 = i237' /\ ar_0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 9) minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_2, ar_1, ar_3 + 1, arityPad)) [ ar_3 + 1 = i273' /\ 1 <= ar_2 /\ 1 <= i273' /\ 0 <= ar_1 /\ 0 <= i273' /\ 0 <= ar_3 /\ ar_0 = 0 ]
(Comp: ?, Cost: 6) minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 0 <= ar_1 /\ 0 <= i266' /\ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_3 /\ ar_0 - 1 = i261' /\ 0 <= i261' /\ 1 <= ar_2 /\ ar_1 - 1 = i266' /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: ?, Cost: 1) minus_Load_535(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_542(ar_1, ar_0, ar_2, ar_3)) [ 0 <= ar_0 /\ 0 <= ar_3 /\ 0 <= ar_1 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 17) div_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_1, ar_0, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 15) div_Load_468(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_0, ar_2)) [ 0 <= i238' /\ 1 <= ar_0 /\ ar_1 - 1 = i238' /\ 0 <= i237' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ ar_0 - 1 = i237' /\ ar_0 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 9) minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_2, ar_1, ar_3 + 1, arityPad)) [ ar_3 + 1 = i273' /\ 1 <= ar_2 /\ 1 <= i273' /\ 0 <= ar_1 /\ 0 <= i273' /\ 0 <= ar_3 /\ ar_0 = 0 ]
(Comp: ?, Cost: 6) minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 0 <= ar_1 /\ 0 <= i266' /\ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_3 /\ ar_0 - 1 = i261' /\ 0 <= i261' /\ 1 <= ar_2 /\ ar_1 - 1 = i266' /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(minus_Load_535) = 3*V_1 + 2
Pol(minus_EQ_542) = 3*V_2 + 1
Pol(div_ConstantStackPush_1) = 3*V_1
Pol(div_Load_468) = 3*V_2
Pol(koat_start) = 3*V_1
orients all transitions weakly and the transitions
minus_Load_535(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_542(ar_1, ar_0, ar_2, ar_3)) [ 0 <= ar_0 /\ 0 <= ar_3 /\ 0 <= ar_1 /\ 1 <= ar_2 ]
minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 0 <= ar_1 /\ 0 <= i266' /\ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_3 /\ ar_0 - 1 = i261' /\ 0 <= i261' /\ 1 <= ar_2 /\ ar_1 - 1 = i266' /\ 1 <= ar_0 ]
minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_2, ar_1, ar_3 + 1, arityPad)) [ ar_3 + 1 = i273' /\ 1 <= ar_2 /\ 1 <= i273' /\ 0 <= ar_1 /\ 0 <= i273' /\ 0 <= ar_3 /\ ar_0 = 0 ]
div_Load_468(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_0, ar_2)) [ 0 <= i238' /\ 1 <= ar_0 /\ ar_1 - 1 = i238' /\ 0 <= i237' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ ar_0 - 1 = i237' /\ ar_0 <= ar_1 /\ 0 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 3*ar_0, Cost: 1) minus_Load_535(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_542(ar_1, ar_0, ar_2, ar_3)) [ 0 <= ar_0 /\ 0 <= ar_3 /\ 0 <= ar_1 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 17) div_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_1, ar_0, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 3*ar_0, Cost: 15) div_Load_468(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_0, ar_2)) [ 0 <= i238' /\ 1 <= ar_0 /\ ar_1 - 1 = i238' /\ 0 <= i237' /\ 1 <= ar_1 /\ 0 <= ar_2 /\ ar_0 - 1 = i237' /\ ar_0 <= ar_1 /\ 0 < ar_0 ]
(Comp: 3*ar_0, Cost: 9) minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_Load_468(ar_2, ar_1, ar_3 + 1, arityPad)) [ ar_3 + 1 = i273' /\ 1 <= ar_2 /\ 1 <= i273' /\ 0 <= ar_1 /\ 0 <= i273' /\ 0 <= ar_3 /\ ar_0 = 0 ]
(Comp: 3*ar_0, Cost: 6) minus_EQ_542(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_535(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 0 <= ar_1 /\ 0 <= i266' /\ 0 < ar_0 /\ 2 <= ar_2 /\ 1 <= ar_1 /\ 0 <= ar_3 /\ ar_0 - 1 = i261' /\ 0 <= i261' /\ 1 <= ar_2 /\ ar_1 - 1 = i266' /\ 1 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(div_ConstantStackPush_1(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 93*ar_0 + 17

Time: 0.269 sec (SMT: 0.247 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) MovedArithmeticToConstraintsProof (BOTH CONCRETE BOUNDS(ID, 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) JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID) transformation)

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

(31) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(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:

(39) koat Proof (EQUIVALENT transformation)

(40) BOUNDS(CONSTANT, 17 + 93 * |#0|)