time complexity proof of /tmp/tmpZvwmQu/Mod.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 112 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 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 96 ms)

    ↳16 WeightedIntTrs

        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 23 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), 13 ms)

        ↳24 WeightedIntTrs

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

↳26 JBCComplexityEdges

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

    ↳28 WeightedIntTrs

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

    ↳30 WeightedIntTrs

    ↳31 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 23 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 (⇔, 114 ms)

    ↳40 BOUNDS(CONSTANT, 19 + 81 * |#0|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class Mod {

  public static int mod(int x, int y) {

    while (x >= y && y > 0) {
      x = minus(x,y);

    }
    return x;
  }

  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:
Mod.mod(II)I: Graph of 73 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 65 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 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.
Did no encode lower bounds for putfield and astore.

(6) Obligation:

IntTrs with 65 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_2(i1, i4, env, static) -{0,0}> mod_Load_3(i1, i4, env, static) :|: 0 >= 0
mod_Load_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_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, i4, env, static) -{1,1}> mod_Load_41(i1, i4, env, static) :|: 0 >= 0
mod_Load_41(i1, i4, env, static) -{0,0}> mod_Load_42(i1, i4, env, static) :|: 0 >= 0
mod_Load_42(i1, i4, env, static) -{0,0}> mod_Load_48(i1, i4, env, static) :|: 0 <= static
mod_Load_48(i1, i4, env, static) -{0,0}> mod_Load_49(i1, i4, env, static) :|: 0 >= 0
mod_Load_49(i1, i4, env, static) -{0,0}> mod_Load_50(i1, i4, env, static) :|: 0 >= 0
mod_Load_50(i1, i4, env, static) -{1,1}> mod_Load_51(i1, i4, env, static) :|: 0 >= 0
mod_Load_51(i1, i4, env, static) -{1,1}> mod_LT_54(i1, i4, env, static) :|: 0 >= 0
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_57(i1, i4, env, static) :|: i4 <= i1
mod_LT_57(i1, i4, env, static) -{1,1}> mod_Load_63(i1, i4, env, static) :|: i4 <= i1
mod_Load_63(i1, i4, env, static) -{1,1}> mod_LE_68(i1, i4, env, static) :|: 0 >= 0
mod_LE_68(i1, i4, env, static) -{0,0}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LE_275(i107, i106, i108, env, static) -{0,0}> mod_LE_283(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_LE_283(i107, i106, i108, env, static) -{1,1}> mod_Load_288(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
mod_Load_288(i107, i106, i108, env, static) -{1,1}> mod_Load_292(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_Load_292(i107, i106, i108, env, static) -{1,1}> mod_InvokeMethod_295(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_InvokeMethod_295(i107, i106, i108, env, static) -{1,1}> minus_Load_297(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_Load_297(i108, i106, i107, env, static) -{1,1}> minus_EQ_300(i106, i108, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_EQ_300(i106, i108, i107, env, static) -{1,1}> minus_Load_302(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
minus_Load_302(i108, i106, i107, env, static) -{1,1}> minus_LE_304(i106, i108, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_LE_304(i106, i108, i107, env, static) -{1,1}> minus_Inc_306(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
minus_Inc_306(i108, i106, i107, env, static) -{1,1}> minus_Inc_308(i108, i113, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 1 <= i108 && i106 + -1 = i113
minus_Inc_308(i108, i113, i107, i106, env, static) -{1,1}> minus_JMP_310(i115, i113, i107, i106, env, static) :|: 1 <= i106 && i108 + -1 = i115 && 1 <= i107 && 0 <= i113 && 1 <= i108 && 0 <= i115
minus_JMP_310(i115, i113, i107, i106, env, static) -{1,1}> minus_Load_336(i115, i113, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(i141, i144, i143, i142, env, static) -{0,0}> minus_EQ_354(i141, i144, i143, i142, env, static) :|: 0 <= i144 && 1 <= i144 && 1 <= i141 && 2 <= i143 && 1 <= i142 && 0 <= i141 && 1 <= i143 && 2 <= i142
minus_EQ_352(iconst_0, i115, i107, i106, env, static) -{0,0}> minus_EQ_355(iconst_0, i115, i107, i106, env, static) :|: 1 <= i106 && 0 <= iconst_0 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_EQ_354(i141, i144, i143, i142, env, static) -{1,1}> minus_Load_357(i144, i141, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142 && 0 < i141
minus_EQ_355(iconst_0, i115, i107, i106, env, static) -{1,1}> minus_Load_358(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_Load_357(i144, i141, i143, i142, env, static) -{1,1}> minus_LE_359(i141, i144, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142
minus_Load_358(i115, i107, i106, env, static) -{1,1}> minus_Return_360(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_LE_359(i141, i144, i143, i142, env, static) -{1,1}> minus_Inc_361(i144, i141, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142 && 0 < i141
minus_Return_360(i115, i107, i106, env, static) -{1,1}> mod_Store_362(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Inc_361(i144, i141, i143, i142, env, static) -{1,1}> minus_Inc_363(i144, i151, i143, i142, env, static) :|: 1 <= i144 && 0 <= i151 && 1 <= i141 && 2 <= i143 && i141 + -1 = i151 && 2 <= i142
mod_Store_362(i107, i106, i115, env, static) -{1,1}> mod_JMP_364(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Inc_363(i144, i151, i143, i142, env, static) -{1,1}> minus_JMP_365(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 1 <= i144 && i144 + -1 = i154 && 0 <= i151 && 2 <= i143 && 2 <= i142
mod_JMP_364(i107, i106, i115, env, static) -{1,1}> mod_Load_366(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_JMP_365(i154, i151, i143, i142, env, static) -{1,1}> minus_Load_375(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 0 <= i151 && 2 <= i143 && 2 <= i142
mod_Load_366(i107, i106, i115, env, static) -{1,1}> mod_Load_376(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Load_375(i154, i151, i143, i142, env, static) -{0,0}> minus_Load_336(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 0 <= i151 && 2 <= i143 && 1 <= i142 && 1 <= i143 && 2 <= i142
mod_Load_376(i107, i106, i115, env, static) -{1,1}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_402(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115
mod_LT_402(i107, i106, i115, env, static) -{1,1}> mod_Load_414(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115 && 1 <= i115
mod_Load_414(i107, i106, i115, env, static) -{1,1}> mod_LE_440(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115
mod_LE_440(i107, i106, i115, env, static) -{0,0}> mod_LE_275(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115

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

obtained
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
mod_Load_2(i1, i4, env, static) -{0,0}> mod_Load_3(i1, i4, env, static) :|: 0 >= 0
mod_Load_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_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, i4, env, static) -{1,1}> mod_Load_41(i1, i4, env, static) :|: 0 >= 0
mod_Load_41(i1, i4, env, static) -{0,0}> mod_Load_42(i1, i4, env, static) :|: 0 >= 0
mod_Load_42(i1, i4, env, static) -{0,0}> mod_Load_48(i1, i4, env, static) :|: 0 <= static
mod_Load_48(i1, i4, env, static) -{0,0}> mod_Load_49(i1, i4, env, static) :|: 0 >= 0
mod_Load_49(i1, i4, env, static) -{0,0}> mod_Load_50(i1, i4, env, static) :|: 0 >= 0
mod_Load_50(i1, i4, env, static) -{1,1}> mod_Load_51(i1, i4, env, static) :|: 0 >= 0
mod_Load_51(i1, i4, env, static) -{1,1}> mod_LT_54(i1, i4, env, static) :|: 0 >= 0

obtained
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0 && i4 <= i1
by chaining
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_57(i1, i4, env, static) :|: i4 <= i1
mod_LT_57(i1, i4, env, static) -{1,1}> mod_Load_63(i1, i4, env, static) :|: i4 <= i1
mod_Load_63(i1, i4, env, static) -{1,1}> mod_LE_68(i1, i4, env, static) :|: 0 >= 0
mod_LE_68(i1, i4, env, static) -{0,0}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0

obtained
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i115', i113', i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
by chaining
mod_LE_275(i107, i106, i108, env, static) -{0,0}> mod_LE_283(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_LE_283(i107, i106, i108, env, static) -{1,1}> mod_Load_288(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
mod_Load_288(i107, i106, i108, env, static) -{1,1}> mod_Load_292(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_Load_292(i107, i106, i108, env, static) -{1,1}> mod_InvokeMethod_295(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_InvokeMethod_295(i107, i106, i108, env, static) -{1,1}> minus_Load_297(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_Load_297(i108, i106, i107, env, static) -{1,1}> minus_EQ_300(i106, i108, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_EQ_300(i106, i108, i107, env, static) -{1,1}> minus_Load_302(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
minus_Load_302(i108, i106, i107, env, static) -{1,1}> minus_LE_304(i106, i108, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_LE_304(i106, i108, i107, env, static) -{1,1}> minus_Inc_306(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
minus_Inc_306(i108, i106, i107, env, static) -{1,1}> minus_Inc_308(i108, i113, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 1 <= i108 && i106 + -1 = i113
minus_Inc_308(i108, i113, i107, i106, env, static) -{1,1}> minus_JMP_310(i115, i113, i107, i106, env, static) :|: 1 <= i106 && i108 + -1 = i115 && 1 <= i107 && 0 <= i113 && 1 <= i108 && 0 <= i115
minus_JMP_310(i115, i113, i107, i106, env, static) -{1,1}> minus_Load_336(i115, i113, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115

obtained
minus_EQ_352(0, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0
by chaining
minus_EQ_352(iconst_0, i115, i107, i106, env, static) -{0,0}> minus_EQ_355(iconst_0, i115, i107, i106, env, static) :|: 1 <= i106 && 0 <= iconst_0 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_EQ_355(iconst_0, i115, i107, i106, env, static) -{1,1}> minus_Load_358(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_Load_358(i115, i107, i106, env, static) -{1,1}> minus_Return_360(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Return_360(i115, i107, i106, env, static) -{1,1}> mod_Store_362(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_Store_362(i107, i106, i115, env, static) -{1,1}> mod_JMP_364(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_JMP_364(i107, i106, i115, env, static) -{1,1}> mod_Load_366(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_Load_366(i107, i106, i115, env, static) -{1,1}> mod_Load_376(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_Load_376(i107, i106, i115, env, static) -{1,1}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115

obtained
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107
by chaining
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_402(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115
mod_LT_402(i107, i106, i115, env, static) -{1,1}> mod_Load_414(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115 && 1 <= i115
mod_Load_414(i107, i106, i115, env, static) -{1,1}> mod_LE_440(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115
mod_LE_440(i107, i106, i115, env, static) -{0,0}> mod_LE_275(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115

obtained
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i154', i151', i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
by chaining
minus_EQ_352(i141, i144, i143, i142, env, static) -{0,0}> minus_EQ_354(i141, i144, i143, i142, env, static) :|: 0 <= i144 && 1 <= i144 && 1 <= i141 && 2 <= i143 && 1 <= i142 && 0 <= i141 && 1 <= i143 && 2 <= i142
minus_EQ_354(i141, i144, i143, i142, env, static) -{1,1}> minus_Load_357(i144, i141, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142 && 0 < i141
minus_Load_357(i144, i141, i143, i142, env, static) -{1,1}> minus_LE_359(i141, i144, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142
minus_LE_359(i141, i144, i143, i142, env, static) -{1,1}> minus_Inc_361(i144, i141, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142 && 0 < i141
minus_Inc_361(i144, i141, i143, i142, env, static) -{1,1}> minus_Inc_363(i144, i151, i143, i142, env, static) :|: 1 <= i144 && 0 <= i151 && 1 <= i141 && 2 <= i143 && i141 + -1 = i151 && 2 <= i142
minus_Inc_363(i144, i151, i143, i142, env, static) -{1,1}> minus_JMP_365(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 1 <= i144 && i144 + -1 = i154 && 0 <= i151 && 2 <= i143 && 2 <= i142
minus_JMP_365(i154, i151, i143, i142, env, static) -{1,1}> minus_Load_375(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 0 <= i151 && 2 <= i143 && 2 <= i142
minus_Load_375(i154, i151, i143, i142, env, static) -{0,0}> minus_Load_336(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 0 <= i151 && 2 <= i143 && 1 <= i142 && 1 <= i143 && 2 <= i142

(8) Obligation:

IntTrs with 10 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0 && i4 <= i1
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i115', i113', i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(0, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i154', i151', i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144

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

Moved arithmethic from lhss to constraints.

minus_EQ_352(0, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0
was transformed to
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0 && x = 0

(10) Obligation:

IntTrs with 10 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0 && x = 0
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0 && i4 <= i1
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i115', i113', i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i154', i151', i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107

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

Moved arithmethic from constraints to rhss.

mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i115', i113', i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
was transformed to
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106

minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i154', i151', i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
was transformed to
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144

(12) Obligation:

IntTrs with 10 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0 && i4 <= i1
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0 && x = 0
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107

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

Simplified expressions.

mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0 && i4 <= i1
was transformed to
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: i4 <= i1

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

minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
was transformed to
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 - 1, i141 - 1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 1 <= i142 && i144 - 1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 - 1 = i151' && 1 <= i141 && 0 <= i144

minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0 && x = 0
was transformed to
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && x = 0

mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
was transformed to
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 - 1, i106 - 1, i107, i106, env, static) :|: i108 - 1 = i115' && 0 <= i115' && i106 - 1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106

(14) Obligation:

IntTrs with 10 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && x = 0
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 - 1, i141 - 1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 1 <= i142 && i144 - 1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 - 1 = i151' && 1 <= i141 && 0 <= i144
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: i4 <= i1
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 - 1, i106 - 1, i107, i106, env, static) :|: i108 - 1 = i115' && 0 <= i115' && i106 - 1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107

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

Transformed 65 jbc graph edges to a weighted ITS with 65 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 10 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0 && i4 <= i1
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && 0 <= 0 && x = 0
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107

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

Simplified expressions.

(24) Obligation:

IntTrs with 10 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
minus_EQ_352(x, i115, i107, i106, env, static) -{7,7}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i107 && 0 <= i115 && 1 <= i106 && x = 0
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i144 - 1, i141 - 1, i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 1 <= i142 && i144 - 1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 - 1 = i151' && 1 <= i141 && 0 <= i144
mod_Load_2(i1, i4, env, static) -{17,17}> mod_LT_54(i1, i4, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_56(i1, i4, env, static) :|: i1 < i4
mod_LE_275(i96, i105, i98, env, static) -{0,0}> mod_LE_282(i96, i105, i98, env, static) :|: i105 <= 0
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_401(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i115 < i106 && 0 <= i115
mod_LT_54(i1, i4, env, static) -{2,2}> mod_LE_275(i1, i4, i1, env, static) :|: i4 <= i1
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i108 - 1, i106 - 1, i107, i106, env, static) :|: i108 - 1 = i115' && 0 <= i115' && i106 - 1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
mod_LT_393(i107, i106, i115, env, static) -{2,2}> mod_LE_275(i107, i106, i115, env, static) :|: 0 <= i115 && 1 <= i115 && i106 <= i115 && 1 <= i106 && 1 <= i107

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

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

(26) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(28) Obligation:

IntTrs with 62 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
mod_Load_2(i1, i4, env, static) -{0,0}> mod_Load_3(i1, i4, env, static) :|: 0 >= 0
mod_Load_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_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, i4, env, static) -{1,1}> mod_Load_41(i1, i4, env, static) :|: 0 >= 0
mod_Load_41(i1, i4, env, static) -{0,0}> mod_Load_42(i1, i4, env, static) :|: 0 >= 0
mod_Load_42(i1, i4, env, static) -{0,0}> mod_Load_48(i1, i4, env, static) :|: 0 <= static
mod_Load_48(i1, i4, env, static) -{0,0}> mod_Load_49(i1, i4, env, static) :|: 0 >= 0
mod_Load_49(i1, i4, env, static) -{0,0}> mod_Load_50(i1, i4, env, static) :|: 0 >= 0
mod_Load_50(i1, i4, env, static) -{1,1}> mod_Load_51(i1, i4, env, static) :|: 0 >= 0
mod_Load_51(i1, i4, env, static) -{1,1}> mod_LT_54(i1, i4, env, static) :|: 0 >= 0
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_57(i1, i4, env, static) :|: i4 <= i1
mod_LT_57(i1, i4, env, static) -{1,1}> mod_Load_63(i1, i4, env, static) :|: i4 <= i1
mod_Load_63(i1, i4, env, static) -{1,1}> mod_LE_68(i1, i4, env, static) :|: 0 >= 0
mod_LE_68(i1, i4, env, static) -{0,0}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0
mod_LE_275(i107, i106, i108, env, static) -{0,0}> mod_LE_283(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_LE_283(i107, i106, i108, env, static) -{1,1}> mod_Load_288(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
mod_Load_288(i107, i106, i108, env, static) -{1,1}> mod_Load_292(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_Load_292(i107, i106, i108, env, static) -{1,1}> mod_InvokeMethod_295(i107, i106, i108, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
mod_InvokeMethod_295(i107, i106, i108, env, static) -{1,1}> minus_Load_297(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_Load_297(i108, i106, i107, env, static) -{1,1}> minus_EQ_300(i106, i108, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_EQ_300(i106, i108, i107, env, static) -{1,1}> minus_Load_302(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
minus_Load_302(i108, i106, i107, env, static) -{1,1}> minus_LE_304(i106, i108, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i108
minus_LE_304(i106, i108, i107, env, static) -{1,1}> minus_Inc_306(i108, i106, i107, env, static) :|: 1 <= i106 && 1 <= i107 && 0 < i106 && 1 <= i108
minus_Inc_306(i108, i106, i107, env, static) -{1,1}> minus_Inc_308(i108, i113, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 1 <= i108 && i106 + -1 = i113
minus_Inc_308(i108, i113, i107, i106, env, static) -{1,1}> minus_JMP_310(i115, i113, i107, i106, env, static) :|: 1 <= i106 && i108 + -1 = i115 && 1 <= i107 && 0 <= i113 && 1 <= i108 && 0 <= i115
minus_JMP_310(i115, i113, i107, i106, env, static) -{1,1}> minus_Load_336(i115, i113, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(i141, i144, i143, i142, env, static) -{0,0}> minus_EQ_354(i141, i144, i143, i142, env, static) :|: 0 <= i144 && 1 <= i144 && 1 <= i141 && 2 <= i143 && 1 <= i142 && 0 <= i141 && 1 <= i143 && 2 <= i142
minus_EQ_352(iconst_0, i115, i107, i106, env, static) -{0,0}> minus_EQ_355(iconst_0, i115, i107, i106, env, static) :|: 1 <= i106 && 0 <= iconst_0 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_EQ_354(i141, i144, i143, i142, env, static) -{1,1}> minus_Load_357(i144, i141, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142 && 0 < i141
minus_EQ_355(iconst_0, i115, i107, i106, env, static) -{1,1}> minus_Load_358(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_Load_357(i144, i141, i143, i142, env, static) -{1,1}> minus_LE_359(i141, i144, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142
minus_Load_358(i115, i107, i106, env, static) -{1,1}> minus_Return_360(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_LE_359(i141, i144, i143, i142, env, static) -{1,1}> minus_Inc_361(i144, i141, i143, i142, env, static) :|: 1 <= i144 && 1 <= i141 && 2 <= i143 && 2 <= i142 && 0 < i141
minus_Return_360(i115, i107, i106, env, static) -{1,1}> mod_Store_362(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Inc_361(i144, i141, i143, i142, env, static) -{1,1}> minus_Inc_363(i144, i151, i143, i142, env, static) :|: 1 <= i144 && 0 <= i151 && 1 <= i141 && 2 <= i143 && i141 + -1 = i151 && 2 <= i142
mod_Store_362(i107, i106, i115, env, static) -{1,1}> mod_JMP_364(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Inc_363(i144, i151, i143, i142, env, static) -{1,1}> minus_JMP_365(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 1 <= i144 && i144 + -1 = i154 && 0 <= i151 && 2 <= i143 && 2 <= i142
mod_JMP_364(i107, i106, i115, env, static) -{1,1}> mod_Load_366(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_JMP_365(i154, i151, i143, i142, env, static) -{1,1}> minus_Load_375(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 0 <= i151 && 2 <= i143 && 2 <= i142
mod_Load_366(i107, i106, i115, env, static) -{1,1}> mod_Load_376(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Load_375(i154, i151, i143, i142, env, static) -{0,0}> minus_Load_336(i154, i151, i143, i142, env, static) :|: 0 <= i154 && 0 <= i151 && 2 <= i143 && 1 <= i142 && 1 <= i143 && 2 <= i142
mod_Load_376(i107, i106, i115, env, static) -{1,1}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_402(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115
mod_LT_402(i107, i106, i115, env, static) -{1,1}> mod_Load_414(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115 && 1 <= i115
mod_Load_414(i107, i106, i115, env, static) -{1,1}> mod_LE_440(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115
mod_LE_440(i107, i106, i115, env, static) -{0,0}> mod_LE_275(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115

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

obtained
mod_Load_2(i1, i4, env, static) -{19,19}> mod_LE_275(i1, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && i4 <= i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
mod_Load_2(i1, i4, env, static) -{0,0}> mod_Load_3(i1, i4, env, static) :|: 0 >= 0
mod_Load_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_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_16(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_17(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_19(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_22(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_36(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_39(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_39(i1, i4, env, static) -{1,1}> mod_Load_41(i1, i4, env, static) :|: 0 >= 0
mod_Load_41(i1, i4, env, static) -{0,0}> mod_Load_42(i1, i4, env, static) :|: 0 >= 0
mod_Load_42(i1, i4, env, static) -{0,0}> mod_Load_48(i1, i4, env, static) :|: 0 <= static
mod_Load_48(i1, i4, env, static) -{0,0}> mod_Load_49(i1, i4, env, static) :|: 0 >= 0
mod_Load_49(i1, i4, env, static) -{0,0}> mod_Load_50(i1, i4, env, static) :|: 0 >= 0
mod_Load_50(i1, i4, env, static) -{1,1}> mod_Load_51(i1, i4, env, static) :|: 0 >= 0
mod_Load_51(i1, i4, env, static) -{1,1}> mod_LT_54(i1, i4, env, static) :|: 0 >= 0
mod_LT_54(i1, i4, env, static) -{0,0}> mod_LT_57(i1, i4, env, static) :|: i4 <= i1
mod_LT_57(i1, i4, env, static) -{1,1}> mod_Load_63(i1, i4, env, static) :|: i4 <= i1
mod_Load_63(i1, i4, env, static) -{1,1}> mod_LE_68(i1, i4, env, static) :|: 0 >= 0
mod_LE_68(i1, i4, env, static) -{0,0}> mod_LE_275(i1, i4, i1, env, static) :|: 0 >= 0

obtained
minus_EQ_352(0, i115, i107, i106, env, static) -{9,9}> mod_LE_275(i107, i106, i115, env, static) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0
by chaining
minus_EQ_352(iconst_0, i115, i107, i106, env, static) -{0,0}> minus_EQ_355(iconst_0, i115, i107, i106, env, static) :|: 1 <= i106 && 0 <= iconst_0 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_EQ_355(iconst_0, i115, i107, i106, env, static) -{1,1}> minus_Load_358(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && iconst_0 = 0 && 0 <= i115
minus_Load_358(i115, i107, i106, env, static) -{1,1}> minus_Return_360(i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
minus_Return_360(i115, i107, i106, env, static) -{1,1}> mod_Store_362(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_Store_362(i107, i106, i115, env, static) -{1,1}> mod_JMP_364(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_JMP_364(i107, i106, i115, env, static) -{1,1}> mod_Load_366(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_Load_366(i107, i106, i115, env, static) -{1,1}> mod_Load_376(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_Load_376(i107, i106, i115, env, static) -{1,1}> mod_LT_393(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i115
mod_LT_393(i107, i106, i115, env, static) -{0,0}> mod_LT_402(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115
mod_LT_402(i107, i106, i115, env, static) -{1,1}> mod_Load_414(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && i106 <= i115 && 0 <= i115 && 1 <= i115
mod_Load_414(i107, i106, i115, env, static) -{1,1}> mod_LE_440(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115
mod_LE_440(i107, i106, i115, env, static) -{0,0}> mod_LE_275(i107, i106, i115, env, static) :|: 1 <= i106 && 1 <= i107 && 1 <= i115

(30) Obligation:

IntTrs with 5 rules
Start term: mod_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
mod_Load_2(i1, i4, env, static) -{19,19}> mod_LE_275(i1, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && i4 <= i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
mod_LE_275(i107, i106, i108, env, static) -{11,11}> minus_Load_336(i115', i113', i107, i106, env, static) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
minus_Load_336(i115, i113, i107, i106, env, static) -{1,1}> minus_EQ_352(i113, i115, i107, i106, env, static) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(0, i115, i107, i106, env, static) -{9,9}> mod_LE_275(i107, i106, i115, env, static) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0
minus_EQ_352(i141, i144, i143, i142, env, static) -{6,6}> minus_Load_336(i154', i151', i143, i142, env, static) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144

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

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

mod_Load_2(x1, x2, x3, x4) → mod_Load_2(x1, x2, x4)
mod_LE_275(x1, x2, x3, x4, x5) → mod_LE_275(x1, x2, x3)
minus_Load_336(x1, x2, x3, x4, x5, x6) → minus_Load_336(x1, x2, x3, x4)
minus_EQ_352(x1, x2, x3, x4, x5, x6) → minus_EQ_352(x1, x2, x3, x4)

(32) Obligation:

IntTrs with 5 rules
Start term: mod_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
mod_Load_2(i1, i4, static) -{19,19}> mod_LE_275(i1, i4, i1) :|: 0 >= 0 && 0 < 2 && i4 <= i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i115', i113', i107, i106) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
minus_Load_336(i115, i113, i107, i106) -{1,1}> minus_EQ_352(i113, i115, i107, i106) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(0, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0
minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i154', i151', i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144

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

Moved arithmethic from lhss to constraints.

minus_EQ_352(0, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0
was transformed to
minus_EQ_352(x, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0 && x = 0

(34) Obligation:

IntTrs with 5 rules
Start term: mod_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
minus_EQ_352(x, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0 && x = 0
mod_Load_2(i1, i4, static) -{19,19}> mod_LE_275(i1, i4, i1) :|: 0 >= 0 && 0 < 2 && i4 <= i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i154', i151', i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i115', i113', i107, i106) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
minus_Load_336(i115, i113, i107, i106) -{1,1}> minus_EQ_352(i113, i115, i107, i106) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115

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

Moved arithmethic from constraints to rhss.

minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i154', i151', i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
was transformed to
minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144

mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i115', i113', i107, i106) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
was transformed to
mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106

(36) Obligation:

IntTrs with 5 rules
Start term: mod_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
minus_EQ_352(x, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0 && x = 0
mod_Load_2(i1, i4, static) -{19,19}> mod_LE_275(i1, i4, i1) :|: 0 >= 0 && 0 < 2 && i4 <= i1 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
minus_Load_336(i115, i113, i107, i106) -{1,1}> minus_EQ_352(i113, i115, i107, i106) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115

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

Simplified expressions.

mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i108 + -1, i106 + -1, i107, i106) :|: i108 + -1 = i115' && 0 <= i115' && i106 + -1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
was transformed to
mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i108 - 1, i106 - 1, i107, i106) :|: i108 - 1 = i115' && 0 <= i115' && i106 - 1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106

minus_EQ_352(x, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && 0 <= 0 && x = 0
was transformed to
minus_EQ_352(x, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && x = 0

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

minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i144 + -1, i141 + -1, i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 0 <= i141 && 1 <= i142 && i144 + -1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 + -1 = i151' && 1 <= i141 && 0 <= i144
was transformed to
minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i144 - 1, i141 - 1, i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 1 <= i142 && i144 - 1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 - 1 = i151' && 1 <= i141 && 0 <= i144

(38) Obligation:

IntTrs with 5 rules
Start term: mod_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
mod_LE_275(i107, i106, i108) -{11,11}> minus_Load_336(i108 - 1, i106 - 1, i107, i106) :|: i108 - 1 = i115' && 0 <= i115' && i106 - 1 = i113' && 0 <= i113' && 1 <= i106 && 1 <= i107 && 1 <= i108 && 0 < i106
mod_Load_2(i1, i4, static) -{19,19}> mod_LE_275(i1, i4, i1) :|: i4 <= i1 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
minus_Load_336(i115, i113, i107, i106) -{1,1}> minus_EQ_352(i113, i115, i107, i106) :|: 1 <= i106 && 1 <= i107 && 0 <= i113 && 0 <= i115
minus_EQ_352(i141, i144, i143, i142) -{6,6}> minus_Load_336(i144 - 1, i141 - 1, i143, i142) :|: 1 <= i143 && 2 <= i142 && 0 < i141 && 1 <= i142 && i144 - 1 = i154' && 2 <= i143 && 0 <= i154' && 0 <= i151' && 1 <= i144 && i141 - 1 = i151' && 1 <= i141 && 0 <= i144
minus_EQ_352(x, i115, i107, i106) -{9,9}> mod_LE_275(i107, i106, i115) :|: i106 <= i115 && 1 <= i115 && 0 <= i115 && 1 <= i106 && 1 <= i107 && x = 0

(39) koat Proof (EQUIVALENT transformation)

YES(?, 81*ar_0 + 19)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 11) mod_LE_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_2 - 1, ar_1 - 1, ar_0, ar_1)) [ ar_2 - 1 = i115' /\ 0 <= i115' /\ ar_1 - 1 = i113' /\ 0 <= i113' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_1 ]
(Comp: ?, Cost: 19) mod_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_0, ar_1, ar_0, arityPad)) [ ar_1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 1) minus_Load_336(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_352(ar_1, ar_0, ar_2, ar_3)) [ 1 <= ar_3 /\ 1 <= ar_2 /\ 0 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 6) minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 1 <= ar_2 /\ 2 <= ar_3 /\ 0 < ar_0 /\ 1 <= ar_3 /\ ar_1 - 1 = i154' /\ 2 <= ar_2 /\ 0 <= i154' /\ 0 <= i151' /\ 1 <= ar_1 /\ ar_0 - 1 = i151' /\ 1 <= ar_0 /\ 0 <= ar_1 ]
(Comp: ?, Cost: 9) minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_2, ar_3, ar_1, arityPad)) [ ar_3 <= ar_1 /\ 1 <= ar_1 /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 1 <= ar_2 /\ ar_0 = 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_2(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: 11) mod_LE_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_2 - 1, ar_1 - 1, ar_0, ar_1)) [ ar_2 - 1 = i115' /\ 0 <= i115' /\ ar_1 - 1 = i113' /\ 0 <= i113' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_1 ]
(Comp: 1, Cost: 19) mod_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_0, ar_1, ar_0, arityPad)) [ ar_1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 1) minus_Load_336(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_352(ar_1, ar_0, ar_2, ar_3)) [ 1 <= ar_3 /\ 1 <= ar_2 /\ 0 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 6) minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 1 <= ar_2 /\ 2 <= ar_3 /\ 0 < ar_0 /\ 1 <= ar_3 /\ ar_1 - 1 = i154' /\ 2 <= ar_2 /\ 0 <= i154' /\ 0 <= i151' /\ 1 <= ar_1 /\ ar_0 - 1 = i151' /\ 1 <= ar_0 /\ 0 <= ar_1 ]
(Comp: ?, Cost: 9) minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_2, ar_3, ar_1, arityPad)) [ ar_3 <= ar_1 /\ 1 <= ar_1 /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 1 <= ar_2 /\ ar_0 = 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(mod_LE_275) = 3*V_3
Pol(minus_Load_336) = 3*V_1 + 2
Pol(mod_Load_2) = 3*V_1
Pol(minus_EQ_352) = 3*V_2 + 1
Pol(koat_start) = 3*V_1
orients all transitions weakly and the transitions
mod_LE_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_2 - 1, ar_1 - 1, ar_0, ar_1)) [ ar_2 - 1 = i115' /\ 0 <= i115' /\ ar_1 - 1 = i113' /\ 0 <= i113' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_1 ]
minus_Load_336(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_352(ar_1, ar_0, ar_2, ar_3)) [ 1 <= ar_3 /\ 1 <= ar_2 /\ 0 <= ar_1 /\ 0 <= ar_0 ]
minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_2, ar_3, ar_1, arityPad)) [ ar_3 <= ar_1 /\ 1 <= ar_1 /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 1 <= ar_2 /\ ar_0 = 0 ]
minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 1 <= ar_2 /\ 2 <= ar_3 /\ 0 < ar_0 /\ 1 <= ar_3 /\ ar_1 - 1 = i154' /\ 2 <= ar_2 /\ 0 <= i154' /\ 0 <= i151' /\ 1 <= ar_1 /\ ar_0 - 1 = i151' /\ 1 <= ar_0 /\ 0 <= ar_1 ]
strictly and produces the following problem:
3: T:
(Comp: 3*ar_0, Cost: 11) mod_LE_275(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_2 - 1, ar_1 - 1, ar_0, ar_1)) [ ar_2 - 1 = i115' /\ 0 <= i115' /\ ar_1 - 1 = i113' /\ 0 <= i113' /\ 1 <= ar_1 /\ 1 <= ar_0 /\ 1 <= ar_2 /\ 0 < ar_1 ]
(Comp: 1, Cost: 19) mod_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_0, ar_1, ar_0, arityPad)) [ ar_1 <= ar_0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 3*ar_0, Cost: 1) minus_Load_336(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_EQ_352(ar_1, ar_0, ar_2, ar_3)) [ 1 <= ar_3 /\ 1 <= ar_2 /\ 0 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 3*ar_0, Cost: 6) minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(minus_Load_336(ar_1 - 1, ar_0 - 1, ar_2, ar_3)) [ 1 <= ar_2 /\ 2 <= ar_3 /\ 0 < ar_0 /\ 1 <= ar_3 /\ ar_1 - 1 = i154' /\ 2 <= ar_2 /\ 0 <= i154' /\ 0 <= i151' /\ 1 <= ar_1 /\ ar_0 - 1 = i151' /\ 1 <= ar_0 /\ 0 <= ar_1 ]
(Comp: 3*ar_0, Cost: 9) minus_EQ_352(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LE_275(ar_2, ar_3, ar_1, arityPad)) [ ar_3 <= ar_1 /\ 1 <= ar_1 /\ 0 <= ar_1 /\ 1 <= ar_3 /\ 1 <= ar_2 /\ ar_0 = 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 81*ar_0 + 19

Time: 0.174 sec (SMT: 0.158 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)) 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(9)) 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, 19 + 81 * |#0|)