time complexity proof of /tmp/tmp2suf6W/DivWithoutMinus.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

        ↳11 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 10 ms)

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

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

        ↳16 WeightedIntTrs

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

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

        ↳23 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 12 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

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

        ↳28 WeightedIntTrs

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

↳30 JBCComplexityEdges

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

    ↳32 WeightedIntTrs

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

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 26 ms)

    ↳36 WeightedIntTrs

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

    ↳38 WeightedIntTrs

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

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

    ↳45 koat Proof (⇔, 164 ms)

    ↳46 BOUNDS(CONSTANT, 32 + 23 * |#0| + 10 * |#0| * |#1| + 10 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class DivWithoutMinus{
  // adaption of the algorithm from [Kolbe 95]
  public static void main(int x, int y) {

    int z = y;
    int res = 0;

    while (z > 0 && (y == 0 || y > 0 && x > 0))	{

      if (y == 0) {
        res++;
        y = z;
      }
      else {
        x--;
        y--;
      }
    }
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
DivWithoutMinus.main(II)V: Graph of 69 nodes with 1 SCC.

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) 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.
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: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_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_15(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i4, env, static) -{1,1}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 <= static
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_53(i1, i4, env, static) :|: 0 >= 0
main_Load_53(i1, i4, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: 0 >= 0
main_Store_54(i1, i4, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_55(i1, i4, env, static) -{1,1}> main_Store_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_58(i1, i4, iconst_0, env, static) -{1,1}> main_Load_59(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_59(i1, i4, iconst_0, env, static) -{1,1}> main_LE_60(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_60(i1, i4, iconst_0, env, static) -{0,0}> main_LE_362(i1, i4, i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_362(i31, i32, i33, i34, iconst_0, env, static) -{0,0}> main_LE_475(i31, i32, i33, i34, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_LE_475(i31, i116, i33, i117, i118, env, static) -{0,0}> main_LE_571(i31, i116, i33, i117, i118, env, static) :|: i118 <= 1 && i118 <= 2 && 0 <= i118
main_LE_571(i31, i156, i33, i157, i158, env, static) -{0,0}> main_LE_827(i31, i156, i33, i157, i158, env, static) :|: 0 <= i158 && i158 <= 2
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_827(i31, i251, i33, i243, i244, env, static) -{0,0}> main_LE_843(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244
main_LE_843(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_847(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_Load_847(i31, i251, i33, i243, i244, env, static) -{0,0}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{0,0}> main_EQ_918(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, iconst_0, i294, i296, env, static) -{0,0}> main_EQ_919(i31, i251, iconst_0, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_EQ_918(i31, i251, i307, i294, i296, env, static) -{1,1}> main_Load_920(i31, i251, i294, i307, i296, env, static) :|: 1 <= i251 && !(i307 = 0) && 0 <= i296
main_EQ_919(i31, i251, iconst_0, i294, i296, env, static) -{1,1}> main_Load_922(i31, i251, i294, iconst_0, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_Load_920(i31, i251, i294, i307, i296, env, static) -{1,1}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_Load_922(i31, i251, i294, iconst_0, i296, env, static) -{1,1}> main_NE_926(i31, i251, iconst_0, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_LE_924(i31, i251, i313, i294, i296, env, static) -{0,0}> main_LE_929(i31, i251, i313, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_NE_926(i31, i251, iconst_0, i294, i296, env, static) -{1,1}> main_Inc_931(i31, i251, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_LE_929(i31, i251, i313, i294, i296, env, static) -{1,1}> main_Load_935(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i313
main_Inc_931(i31, i251, i294, i296, env, static) -{1,1}> main_Load_937(i31, i251, i294, i315, env, static) :|: i296 + 1 = i315 && 1 <= i315 && 1 <= i251 && 0 <= i296
main_Load_935(i31, i251, i294, i313, i296, env, static) -{1,1}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_Load_937(i31, i251, i294, i315, env, static) -{1,1}> main_Store_943(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_LE_941(i31, i251, i322, i313, i296, env, static) -{0,0}> main_LE_947(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Store_943(i31, i251, i294, i315, env, static) -{1,1}> main_JMP_948(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_LE_947(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Load_958(i31, i251, i322, i313, i296, env, static) :|: 0 < i322 && 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_JMP_948(i31, i251, i294, i315, env, static) -{1,1}> main_Load_962(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_Load_958(i31, i251, i322, i313, i296, env, static) -{1,1}> main_NE_967(i31, i251, i313, i322, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Load_962(i31, i251, i294, i315, env, static) -{0,0}> main_Load_999(i31, i251, i294, i251, i315, env, static) :|: 1 <= i315 && 1 <= i251 && 0 <= i315
main_NE_967(i31, i251, i313, i322, i296, env, static) -{1,1}> main_Inc_972(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_972(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Inc_980(i31, i251, i328, i313, i296, env, static) :|: 1 <= i251 && 0 <= i328 && i322 + -1 = i328 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_980(i31, i251, i328, i313, i296, env, static) -{1,1}> main_JMP_982(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && i313 + -1 = i329 && 0 <= i296 && 1 <= i313
main_JMP_982(i31, i251, i328, i329, i296, env, static) -{1,1}> main_Load_998(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296
main_Load_998(i31, i251, i328, i329, i296, env, static) -{0,0}> main_Load_999(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296
main_Load_999(i31, i251, i335, i336, i337, env, static) -{1,1}> main_LE_1003(i31, i251, i335, i336, i337, env, static) :|: 1 <= i251 && 0 <= i337
main_LE_1003(i31, i251, i335, i336, i337, env, static) -{1,1}> main_Load_1011(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_Load_1011(i31, i251, i335, i336, i337, env, static) -{0,0}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 1 <= i251 && 0 <= i337

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

obtained
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_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_15(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i4, env, static) -{1,1}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 <= static
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_53(i1, i4, env, static) :|: 0 >= 0
main_Load_53(i1, i4, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: 0 >= 0
main_Store_54(i1, i4, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_55(i1, i4, env, static) -{1,1}> main_Store_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_58(i1, i4, iconst_0, env, static) -{1,1}> main_Load_59(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_59(i1, i4, iconst_0, env, static) -{1,1}> main_LE_60(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_60(i1, i4, iconst_0, env, static) -{0,0}> main_LE_362(i1, i4, i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_362(i31, i32, i33, i34, iconst_0, env, static) -{0,0}> main_LE_475(i31, i32, i33, i34, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_LE_475(i31, i116, i33, i117, i118, env, static) -{0,0}> main_LE_571(i31, i116, i33, i117, i118, env, static) :|: i118 <= 1 && i118 <= 2 && 0 <= i118
main_LE_571(i31, i156, i33, i157, i158, env, static) -{0,0}> main_LE_827(i31, i156, i33, i157, i158, env, static) :|: 0 <= i158 && i158 <= 2

obtained
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
by chaining
main_LE_827(i31, i251, i33, i243, i244, env, static) -{0,0}> main_LE_843(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244
main_LE_843(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_847(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_Load_847(i31, i251, i33, i243, i244, env, static) -{0,0}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244

obtained
main_EQ_917(i31, i251, 0, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315'
by chaining
main_EQ_917(i31, i251, iconst_0, i294, i296, env, static) -{0,0}> main_EQ_919(i31, i251, iconst_0, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_EQ_919(i31, i251, iconst_0, i294, i296, env, static) -{1,1}> main_Load_922(i31, i251, i294, iconst_0, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_Load_922(i31, i251, i294, iconst_0, i296, env, static) -{1,1}> main_NE_926(i31, i251, iconst_0, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_NE_926(i31, i251, iconst_0, i294, i296, env, static) -{1,1}> main_Inc_931(i31, i251, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_Inc_931(i31, i251, i294, i296, env, static) -{1,1}> main_Load_937(i31, i251, i294, i315, env, static) :|: i296 + 1 = i315 && 1 <= i315 && 1 <= i251 && 0 <= i296
main_Load_937(i31, i251, i294, i315, env, static) -{1,1}> main_Store_943(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_Store_943(i31, i251, i294, i315, env, static) -{1,1}> main_JMP_948(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_JMP_948(i31, i251, i294, i315, env, static) -{1,1}> main_Load_962(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_Load_962(i31, i251, i294, i315, env, static) -{0,0}> main_Load_999(i31, i251, i294, i251, i315, env, static) :|: 1 <= i315 && 1 <= i251 && 0 <= i315

obtained
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
by chaining
main_Load_999(i31, i251, i335, i336, i337, env, static) -{1,1}> main_LE_1003(i31, i251, i335, i336, i337, env, static) :|: 1 <= i251 && 0 <= i337
main_LE_1003(i31, i251, i335, i336, i337, env, static) -{1,1}> main_Load_1011(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_Load_1011(i31, i251, i335, i336, i337, env, static) -{0,0}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 1 <= i251 && 0 <= i337

obtained
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: !(i307 = 0) && 1 <= i251 && 0 <= i296
by chaining
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{0,0}> main_EQ_918(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_918(i31, i251, i307, i294, i296, env, static) -{1,1}> main_Load_920(i31, i251, i294, i307, i296, env, static) :|: 1 <= i251 && !(i307 = 0) && 0 <= i296
main_Load_920(i31, i251, i294, i307, i296, env, static) -{1,1}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296

obtained
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251
by chaining
main_LE_924(i31, i251, i313, i294, i296, env, static) -{0,0}> main_LE_929(i31, i251, i313, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_LE_929(i31, i251, i313, i294, i296, env, static) -{1,1}> main_Load_935(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i313
main_Load_935(i31, i251, i294, i313, i296, env, static) -{1,1}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313

obtained
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
by chaining
main_LE_941(i31, i251, i322, i313, i296, env, static) -{0,0}> main_LE_947(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_LE_947(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Load_958(i31, i251, i322, i313, i296, env, static) :|: 0 < i322 && 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Load_958(i31, i251, i322, i313, i296, env, static) -{1,1}> main_NE_967(i31, i251, i313, i322, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_NE_967(i31, i251, i313, i322, i296, env, static) -{1,1}> main_Inc_972(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_972(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Inc_980(i31, i251, i328, i313, i296, env, static) :|: 1 <= i251 && 0 <= i328 && i322 + -1 = i328 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_980(i31, i251, i328, i313, i296, env, static) -{1,1}> main_JMP_982(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && i313 + -1 = i329 && 0 <= i296 && 1 <= i313
main_JMP_982(i31, i251, i328, i329, i296, env, static) -{1,1}> main_Load_998(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296
main_Load_998(i31, i251, i328, i329, i296, env, static) -{0,0}> main_Load_999(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296

(8) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, 0, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315'
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: !(i307 = 0) && 1 <= i251 && 0 <= i296
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313

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

Moved arithmethic from lhss to constraints.

main_EQ_917(i31, i251, 0, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315'
was transformed to
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0

(10) Obligation:

IntTrs with 11 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: !(i307 = 0) && 1 <= i251 && 0 <= i296
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251

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

Removed div and mod.

main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: !(i307 = 0) && 1 <= i251 && 0 <= i296
was transformed to
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 < 0 && 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 > 0 && 1 <= i251 && 0 <= i296

(12) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 < 0 && 1 <= i251 && 0 <= i296
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 > 0 && 1 <= i251 && 0 <= i296
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251

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

Moved arithmethic from constraints to rhss.

main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
was transformed to
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 + -1, i313 + -1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313

main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
was transformed to
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i296 + 1, env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0

(14) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 + -1, i313 + -1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 < 0 && 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 > 0 && 1 <= i251 && 0 <= i296
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i296 + 1, env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251

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

Simplified expressions.

main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 + -1, i313 + -1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
was transformed to
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 - 1, i313 - 1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 - 1 = i328' && 0 <= i328' && i313 - 1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313

main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 > 0 && 1 <= i251 && 0 <= i296
was transformed to
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 0 < i307 && 1 <= i251 && 0 <= i296

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

(16) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i296 + 1, env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 < 0 && 1 <= i251 && 0 <= i296
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 0 < i307 && 1 <= i251 && 0 <= i296
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 - 1, i313 - 1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 - 1 = i328' && 0 <= i328' && i313 - 1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251

(17) 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.

(18) Obligation:

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

(20) Obligation:

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

Moved arithmethic from lhss to constraints.

(22) Obligation:

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

Removed div and mod.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 + -1, i313 + -1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 + -1 = i328' && 0 <= i328' && i313 + -1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 < 0 && 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 > 0 && 1 <= i251 && 0 <= i296
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= static && 0 <= static'1 && 0 <= 1 && 0 >= 0 && 0 < 2
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i296 + 1, env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251

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

Simplified expressions.

(28) Obligation:

IntTrs with 12 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_827(i31, i250, i33, i243, i244, env, static) -{0,0}> main_LE_842(i31, i250, i33, i243, i244, env, static) :|: i250 <= 0 && 0 <= i244
main_LE_924(i31, i251, i312, i294, i296, env, static) -{0,0}> main_LE_928(i31, i251, i312, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && i312 <= -1
main_EQ_917(i31, i251, x, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i296 + 1, env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_LE_827(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: i307 < 0 && 1 <= i251 && 0 <= i296
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_LE_941(i31, i251, i321, i313, i296, env, static) -{0,0}> main_LE_945(i31, i251, i321, i313, i296, env, static) :|: 1 <= i251 && i321 <= 0 && 0 <= i296 && 1 <= i313
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{2,2}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 0 < i307 && 1 <= i251 && 0 <= i296
main_LE_941(i31, i251, i322, i313, i296, env, static) -{6,6}> main_Load_999(i31, i251, i322 - 1, i313 - 1, i296, env, static) :|: 1 <= i313 && 0 <= i296 && i322 - 1 = i328' && 0 <= i328' && i313 - 1 = i329' && 1 <= i251 && 0 <= i329' && 1 <= i322 && 0 < i322 && 0 < i313
main_Load_2(i1, i4, env, static) -{20,20}> main_LE_827(i1, i4, i1, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_924(i31, i251, i313, i294, i296, env, static) -{2,2}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 0 < i313 && 1 <= i313 && 0 <= i296 && 1 <= i251

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

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

(30) 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

(31) 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.

(32) Obligation:

IntTrs with 62 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_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_15(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i4, env, static) -{1,1}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 <= static
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_53(i1, i4, env, static) :|: 0 >= 0
main_Load_53(i1, i4, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: 0 >= 0
main_Store_54(i1, i4, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_55(i1, i4, env, static) -{1,1}> main_Store_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_58(i1, i4, iconst_0, env, static) -{1,1}> main_Load_59(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_59(i1, i4, iconst_0, env, static) -{1,1}> main_LE_60(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_60(i1, i4, iconst_0, env, static) -{0,0}> main_LE_362(i1, i4, i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_362(i31, i32, i33, i34, iconst_0, env, static) -{0,0}> main_LE_475(i31, i32, i33, i34, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_LE_475(i31, i116, i33, i117, i118, env, static) -{0,0}> main_LE_571(i31, i116, i33, i117, i118, env, static) :|: i118 <= 1 && i118 <= 2 && 0 <= i118
main_LE_571(i31, i156, i33, i157, i158, env, static) -{0,0}> main_LE_827(i31, i156, i33, i157, i158, env, static) :|: 0 <= i158 && i158 <= 2
main_LE_827(i31, i251, i33, i243, i244, env, static) -{0,0}> main_LE_843(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244
main_LE_843(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_847(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_Load_847(i31, i251, i33, i243, i244, env, static) -{0,0}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{0,0}> main_EQ_918(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, iconst_0, i294, i296, env, static) -{0,0}> main_EQ_919(i31, i251, iconst_0, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_EQ_918(i31, i251, i307, i294, i296, env, static) -{1,1}> main_Load_920(i31, i251, i294, i307, i296, env, static) :|: 1 <= i251 && !(i307 = 0) && 0 <= i296
main_EQ_919(i31, i251, iconst_0, i294, i296, env, static) -{1,1}> main_Load_922(i31, i251, i294, iconst_0, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_Load_920(i31, i251, i294, i307, i296, env, static) -{1,1}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_Load_922(i31, i251, i294, iconst_0, i296, env, static) -{1,1}> main_NE_926(i31, i251, iconst_0, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_LE_924(i31, i251, i313, i294, i296, env, static) -{0,0}> main_LE_929(i31, i251, i313, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_NE_926(i31, i251, iconst_0, i294, i296, env, static) -{1,1}> main_Inc_931(i31, i251, i294, i296, env, static) :|: 1 <= i251 && iconst_0 = 0 && 0 <= i296
main_LE_929(i31, i251, i313, i294, i296, env, static) -{1,1}> main_Load_935(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i313
main_Inc_931(i31, i251, i294, i296, env, static) -{1,1}> main_Load_937(i31, i251, i294, i315, env, static) :|: i296 + 1 = i315 && 1 <= i315 && 1 <= i251 && 0 <= i296
main_Load_935(i31, i251, i294, i313, i296, env, static) -{1,1}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_Load_937(i31, i251, i294, i315, env, static) -{1,1}> main_Store_943(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_LE_941(i31, i251, i322, i313, i296, env, static) -{0,0}> main_LE_947(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Store_943(i31, i251, i294, i315, env, static) -{1,1}> main_JMP_948(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_LE_947(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Load_958(i31, i251, i322, i313, i296, env, static) :|: 0 < i322 && 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_JMP_948(i31, i251, i294, i315, env, static) -{1,1}> main_Load_962(i31, i251, i294, i315, env, static) :|: 1 <= i315 && 1 <= i251
main_Load_958(i31, i251, i322, i313, i296, env, static) -{1,1}> main_NE_967(i31, i251, i313, i322, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Load_962(i31, i251, i294, i315, env, static) -{0,0}> main_Load_999(i31, i251, i294, i251, i315, env, static) :|: 1 <= i315 && 1 <= i251 && 0 <= i315
main_NE_967(i31, i251, i313, i322, i296, env, static) -{1,1}> main_Inc_972(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_972(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Inc_980(i31, i251, i328, i313, i296, env, static) :|: 1 <= i251 && 0 <= i328 && i322 + -1 = i328 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_980(i31, i251, i328, i313, i296, env, static) -{1,1}> main_JMP_982(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && i313 + -1 = i329 && 0 <= i296 && 1 <= i313
main_JMP_982(i31, i251, i328, i329, i296, env, static) -{1,1}> main_Load_998(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296
main_Load_998(i31, i251, i328, i329, i296, env, static) -{0,0}> main_Load_999(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296
main_Load_999(i31, i251, i335, i336, i337, env, static) -{1,1}> main_LE_1003(i31, i251, i335, i336, i337, env, static) :|: 1 <= i251 && 0 <= i337
main_LE_1003(i31, i251, i335, i336, i337, env, static) -{1,1}> main_Load_1011(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_Load_1011(i31, i251, i335, i336, i337, env, static) -{0,0}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 1 <= i251 && 0 <= i337

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

obtained
main_Load_2(i1, i4, env, static) -{21,21}> main_Load_916(i1, i4, i1, i4, 0, env, static'1) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_Load_2(i1, i4, env, static) -{0,0}> main_Load_3(i1, i4, env, static) :|: 0 >= 0
main_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_15(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_15(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_18(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_18(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_23(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i4, env, static) -{1,1}> main_Load_48(i1, i4, env, static) :|: 0 >= 0
main_Load_48(i1, i4, env, static) -{0,0}> main_Load_50(i1, i4, env, static) :|: 0 >= 0
main_Load_50(i1, i4, env, static) -{0,0}> main_Load_51(i1, i4, env, static) :|: 0 <= static
main_Load_51(i1, i4, env, static) -{0,0}> main_Load_52(i1, i4, env, static) :|: 0 >= 0
main_Load_52(i1, i4, env, static) -{0,0}> main_Load_53(i1, i4, env, static) :|: 0 >= 0
main_Load_53(i1, i4, env, static) -{1,1}> main_Store_54(i1, i4, env, static) :|: 0 >= 0
main_Store_54(i1, i4, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_55(i1, i4, env, static) -{1,1}> main_Store_58(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_58(i1, i4, iconst_0, env, static) -{1,1}> main_Load_59(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_59(i1, i4, iconst_0, env, static) -{1,1}> main_LE_60(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_60(i1, i4, iconst_0, env, static) -{0,0}> main_LE_362(i1, i4, i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_362(i31, i32, i33, i34, iconst_0, env, static) -{0,0}> main_LE_475(i31, i32, i33, i34, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 <= 1 && iconst_0 = 0
main_LE_475(i31, i116, i33, i117, i118, env, static) -{0,0}> main_LE_571(i31, i116, i33, i117, i118, env, static) :|: i118 <= 1 && i118 <= 2 && 0 <= i118
main_LE_571(i31, i156, i33, i157, i158, env, static) -{0,0}> main_LE_827(i31, i156, i33, i157, i158, env, static) :|: 0 <= i158 && i158 <= 2
main_LE_827(i31, i251, i33, i243, i244, env, static) -{0,0}> main_LE_843(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244
main_LE_843(i31, i251, i33, i243, i244, env, static) -{1,1}> main_Load_847(i31, i251, i33, i243, i244, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i244
main_Load_847(i31, i251, i33, i243, i244, env, static) -{0,0}> main_Load_916(i31, i251, i33, i243, i244, env, static) :|: 1 <= i251 && 0 <= i244

obtained
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{10,10}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && !(i307 = 0)
by chaining
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{0,0}> main_EQ_918(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_918(i31, i251, i307, i294, i296, env, static) -{1,1}> main_Load_920(i31, i251, i294, i307, i296, env, static) :|: 1 <= i251 && !(i307 = 0) && 0 <= i296
main_Load_920(i31, i251, i294, i307, i296, env, static) -{1,1}> main_LE_924(i31, i251, i307, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_LE_924(i31, i251, i313, i294, i296, env, static) -{0,0}> main_LE_929(i31, i251, i313, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_LE_929(i31, i251, i313, i294, i296, env, static) -{1,1}> main_Load_935(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i313
main_Load_935(i31, i251, i294, i313, i296, env, static) -{1,1}> main_LE_941(i31, i251, i294, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i313
main_LE_941(i31, i251, i322, i313, i296, env, static) -{0,0}> main_LE_947(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_LE_947(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Load_958(i31, i251, i322, i313, i296, env, static) :|: 0 < i322 && 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Load_958(i31, i251, i322, i313, i296, env, static) -{1,1}> main_NE_967(i31, i251, i313, i322, i296, env, static) :|: 1 <= i251 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_NE_967(i31, i251, i313, i322, i296, env, static) -{1,1}> main_Inc_972(i31, i251, i322, i313, i296, env, static) :|: 1 <= i251 && 0 < i313 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_972(i31, i251, i322, i313, i296, env, static) -{1,1}> main_Inc_980(i31, i251, i328, i313, i296, env, static) :|: 1 <= i251 && 0 <= i328 && i322 + -1 = i328 && 0 <= i296 && 1 <= i322 && 1 <= i313
main_Inc_980(i31, i251, i328, i313, i296, env, static) -{1,1}> main_JMP_982(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && i313 + -1 = i329 && 0 <= i296 && 1 <= i313
main_JMP_982(i31, i251, i328, i329, i296, env, static) -{1,1}> main_Load_998(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296
main_Load_998(i31, i251, i328, i329, i296, env, static) -{0,0}> main_Load_999(i31, i251, i328, i329, i296, env, static) :|: 1 <= i251 && 0 <= i329 && 0 <= i328 && 0 <= i296

(34) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, env, static) -{21,21}> main_Load_916(i1, i4, i1, i4, 0, env, static'1) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
main_Load_916(i31, i251, i294, i295, i296, env, static) -{1,1}> main_EQ_917(i31, i251, i295, i294, i296, env, static) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i31, i251, 0, i294, i296, env, static) -{7,7}> main_Load_999(i31, i251, i294, i251, i315', env, static) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315'
main_Load_999(i31, i251, i335, i336, i337, env, static) -{2,2}> main_Load_916(i31, i251, i335, i336, i337, env, static) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i31, i251, i307, i294, i296, env, static) -{10,10}> main_Load_999(i31, i251, i328', i329', i296, env, static) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && !(i307 = 0)

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

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

main_Load_2(x1, x2, x3, x4) → main_Load_2(x1, x2, x4)
main_Load_916(x1, x2, x3, x4, x5, x6, x7) → main_Load_916(x2, x3, x4, x5)
main_EQ_917(x1, x2, x3, x4, x5, x6, x7) → main_EQ_917(x2, x3, x4, x5)
main_Load_999(x1, x2, x3, x4, x5, x6, x7) → main_Load_999(x2, x3, x4, x5)

(36) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
main_Load_916(i251, i294, i295, i296) -{1,1}> main_EQ_917(i251, i295, i294, i296) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i251, 0, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i315') :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315'
main_Load_999(i251, i335, i336, i337) -{2,2}> main_Load_916(i251, i335, i336, i337) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && !(i307 = 0)

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

Moved arithmethic from lhss to constraints.

main_EQ_917(i251, 0, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i315') :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315'
was transformed to
main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i315') :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0

(38) Obligation:

IntTrs with 5 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_916(i251, i294, i295, i296) -{1,1}> main_EQ_917(i251, i295, i294, i296) :|: 1 <= i251 && 0 <= i296
main_Load_999(i251, i335, i336, i337) -{2,2}> main_Load_916(i251, i335, i336, i337) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i315') :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && !(i307 = 0)
main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1

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

Removed div and mod.

main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && !(i307 = 0)
was transformed to
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 < 0
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 > 0

(40) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 < 0
main_Load_916(i251, i294, i295, i296) -{1,1}> main_EQ_917(i251, i295, i294, i296) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i328', i329', i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 > 0
main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i315') :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_Load_999(i251, i335, i336, i337) -{2,2}> main_Load_916(i251, i335, i336, i337) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1

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

Moved arithmethic from constraints to rhss.

main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i315') :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
was transformed to
main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i296 + 1) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0

(42) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 + -1, i307 + -1, i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 < 0
main_Load_916(i251, i294, i295, i296) -{1,1}> main_EQ_917(i251, i295, i294, i296) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 + -1, i307 + -1, i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 > 0
main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i296 + 1) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_Load_999(i251, i335, i336, i337) -{2,2}> main_Load_916(i251, i335, i336, i337) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1

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

Simplified expressions.

main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 + -1, i307 + -1, i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 > 0
was transformed to
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 - 1, i307 - 1, i296) :|: 1 <= i307 && 0 <= i296 && 0 <= i328' && i294 - 1 = i328' && 1 <= i251 && 0 <= i329' && i307 - 1 = i329' && 1 <= i294 && 0 < i294 && 0 < i307

main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 + -1, i307 + -1, i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 + -1 = i328' && 1 <= i251 && 0 <= i329' && i307 + -1 = i329' && 1 <= i294 && 0 < i294 && i307 < 0
was transformed to
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 - 1, i307 - 1, i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 - 1 = i328' && 1 <= i251 && 0 <= i329' && i307 - 1 = i329' && 1 <= i294 && 0 < i294 && i307 < 0

main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 0 < 2 && 1 <= i4 && 0 <= 0 && 0 >= 0 && 0 <= 1 && 0 <= static'1 && 0 <= static && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 1 <= i4 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && 0 < i4 && static'1 <= static''' + 1

(44) Obligation:

IntTrs with 6 rules
Start term: main_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_916(i251, i294, i295, i296) -{1,1}> main_EQ_917(i251, i295, i294, i296) :|: 1 <= i251 && 0 <= i296
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 - 1, i307 - 1, i296) :|: 1 <= i307 && 0 <= i296 && 0 < i307 && 0 <= i328' && i294 - 1 = i328' && 1 <= i251 && 0 <= i329' && i307 - 1 = i329' && 1 <= i294 && 0 < i294 && i307 < 0
main_Load_2(i1, i4, static) -{21,21}> main_Load_916(i4, i1, i4, 0) :|: 1 <= i4 && 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && 0 < i4 && static'1 <= static''' + 1
main_Load_999(i251, i335, i336, i337) -{2,2}> main_Load_916(i251, i335, i336, i337) :|: 0 < i251 && 1 <= i251 && 0 <= i337
main_EQ_917(i251, x, i294, i296) -{7,7}> main_Load_999(i251, i294, i251, i296 + 1) :|: 0 <= i296 && 0 <= i315' && 1 <= i251 && 1 <= i315' && i296 + 1 = i315' && x = 0
main_EQ_917(i251, i307, i294, i296) -{10,10}> main_Load_999(i251, i294 - 1, i307 - 1, i296) :|: 1 <= i307 && 0 <= i296 && 0 <= i328' && i294 - 1 = i328' && 1 <= i251 && 0 <= i329' && i307 - 1 = i329' && 1 <= i294 && 0 < i294 && 0 < i307

(45) koat Proof (EQUIVALENT transformation)

YES(?, 23*ar_0 + 10*ar_0*ar_1 + 10*ar_1 + 32)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 1) main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ ar_1 < 0 ]
(Comp: ?, Cost: 21) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ 0 < ar_1 /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 7) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
(Comp: ?, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 1:
main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 < ar_1 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ ar_1 < 0 ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 2) main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
(Comp: ?, Cost: 7) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 21) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ 0 < ar_1 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: ?, Cost: 2) main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ?, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
(Comp: ?, Cost: 7) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ 0 < ar_1 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_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(main_Load_999) = V_2
Pol(main_Load_916) = V_2
Pol(main_EQ_917) = V_3
Pol(main_Load_2) = V_1
Pol(koat_start) = V_1
orients all transitions weakly and the transition
main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: ?, Cost: 2) main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ar_0, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
(Comp: ?, Cost: 7) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ 0 < ar_1 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_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(main_Load_999) = -V_3 + 1
Pol(main_Load_916) = -V_3 + 1
Pol(main_EQ_917) = -V_2 + 1
and size complexities
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-0) = ar_0
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-1) = ar_1
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-2) = ar_2
S("koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]", 0-3) = ar_3
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' /\\ 0 < ar_1 /\\ static'1 <= static''' + 1 ]", 0-0) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' /\\ 0 < ar_1 /\\ static'1 <= static''' + 1 ]", 0-1) = ar_0
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' /\\ 0 < ar_1 /\\ static'1 <= static''' + 1 ]", 0-2) = ar_1
S("main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\\ 0 <= static'1 /\\ 0 <= ar_2 /\\ static''' <= ar_2 + 2 /\\ 0 <= static''' /\\ 0 < ar_1 /\\ static'1 <= static''' + 1 ]", 0-3) = 0
S("main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-0) = ar_1
S("main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-1) = ar_1
S("main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-2) = ar_0
S("main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-3) = ?
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\\ 0 <= i315' /\\ 1 <= ar_0 /\\ 1 <= i315' /\\ ar_3 + 1 = i315' /\\ ar_1 = 0 ]", 0-0) = ar_1
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\\ 0 <= i315' /\\ 1 <= ar_0 /\\ 1 <= i315' /\\ ar_3 + 1 = i315' /\\ ar_1 = 0 ]", 0-1) = ar_0
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\\ 0 <= i315' /\\ 1 <= ar_0 /\\ 1 <= i315' /\\ ar_3 + 1 = i315' /\\ ar_1 = 0 ]", 0-2) = ar_1
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\\ 0 <= i315' /\\ 1 <= ar_0 /\\ 1 <= i315' /\\ ar_3 + 1 = i315' /\\ ar_1 = 0 ]", 0-3) = ?
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\\ 0 <= ar_3 /\\ 0 <= i328' /\\ ar_2 - 1 = i328' /\\ 1 <= ar_0 /\\ 0 <= i329' /\\ ar_1 - 1 = i329' /\\ 1 <= ar_2 /\\ 0 < ar_2 /\\ 0 < ar_1 ]", 0-0) = ar_1
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\\ 0 <= ar_3 /\\ 0 <= i328' /\\ ar_2 - 1 = i328' /\\ 1 <= ar_0 /\\ 0 <= i329' /\\ ar_1 - 1 = i329' /\\ 1 <= ar_2 /\\ 0 < ar_2 /\\ 0 < ar_1 ]", 0-1) = ar_0
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\\ 0 <= ar_3 /\\ 0 <= i328' /\\ ar_2 - 1 = i328' /\\ 1 <= ar_0 /\\ 0 <= i329' /\\ ar_1 - 1 = i329' /\\ 1 <= ar_2 /\\ 0 < ar_2 /\\ 0 < ar_1 ]", 0-2) = ar_1
S("main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\\ 0 <= ar_3 /\\ 0 <= i328' /\\ ar_2 - 1 = i328' /\\ 1 <= ar_0 /\\ 0 <= i329' /\\ ar_1 - 1 = i329' /\\ 1 <= ar_2 /\\ 0 < ar_2 /\\ 0 < ar_1 ]", 0-3) = ?
S("main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-0) = ar_1
S("main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-1) = ar_0
S("main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-2) = ar_1
S("main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\\ 1 <= ar_0 /\\ 0 <= ar_3 ]", 0-3) = ?
orients the transitions
main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
weakly and the transition
main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
strictly and produces the following problem:
5: T:
(Comp: ?, Cost: 2) main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ar_0, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
(Comp: ar_0*ar_1 + ar_0 + ar_1 + 1, Cost: 7) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
(Comp: ?, Cost: 1) main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ 0 < ar_1 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: 2*ar_0 + ar_0*ar_1 + ar_1 + 1, Cost: 2) main_Load_999(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_0, ar_1, ar_2, ar_3)) [ 0 < ar_0 /\ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: ar_0, Cost: 10) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2 - 1, ar_1 - 1, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_3 /\ 0 <= i328' /\ ar_2 - 1 = i328' /\ 1 <= ar_0 /\ 0 <= i329' /\ ar_1 - 1 = i329' /\ 1 <= ar_2 /\ 0 < ar_2 /\ 0 < ar_1 ]
(Comp: ar_0*ar_1 + ar_0 + ar_1 + 1, Cost: 7) main_EQ_917(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_999(ar_0, ar_2, ar_0, ar_3 + 1)) [ 0 <= ar_3 /\ 0 <= i315' /\ 1 <= ar_0 /\ 1 <= i315' /\ ar_3 + 1 = i315' /\ ar_1 = 0 ]
(Comp: 2*ar_0 + ar_0*ar_1 + ar_1 + 2, Cost: 1) main_Load_916(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_EQ_917(ar_0, ar_2, ar_1, ar_3)) [ 1 <= ar_0 /\ 0 <= ar_3 ]
(Comp: 1, Cost: 21) main_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_916(ar_1, ar_0, ar_1, 0)) [ 1 <= ar_1 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ 0 < ar_1 /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 23*ar_0 + 10*ar_0*ar_1 + 10*ar_1 + 32

Time: 0.217 sec (SMT: 0.186 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) 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) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

(29) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(5)) transformation)

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

(45) koat Proof (EQUIVALENT transformation)

(46) BOUNDS(CONSTANT, 32 + 23 * |#0| + 10 * |#0| * |#1| + 10 * |#1|)