time complexity proof of /tmp/tmpt53Zz7/PlusSwap.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

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

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 36 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), 5 ms)

        ↳14 WeightedIntTrs

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

    ↳16 WeightedIntTrs

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

        ↳24 WeightedIntTrs

        ↳25 koat Proof (⇔, 121 ms)

        ↳26 BOUNDS(CONSTANT, 30 + 12 * |#0| + 12 * |#1|)

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

↳28 JBCComplexityEdges

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

    ↳30 WeightedIntTrs

    ↳31 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 26 ms)

    ↳32 WeightedIntTrs

    ↳33 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 27 ms)

    ↳34 WeightedIntTrs

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

    ↳36 WeightedIntTrs

    ↳37 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 3 ms)

    ↳38 WeightedIntTrs

    ↳39 koat Proof (⇔, 72 ms)

    ↳40 BOUNDS(CONSTANT, 29 + 12 * |#0| + 12 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class PlusSwap{
  public static void main(int x, int y) {
    int z;
    int res = 0;

    while (y > 0) {

      z = x;
      x = y-1;
      y = z;
      res++;

    }

    res = res + x;
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

Set of 57 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 57 jbc graph edges to a weighted ITS with 57 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 57 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(i2, i4, env, static) -{0,0}> main_ConstantStackPush_3(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i2, i4, env, static) -{1,1}> main_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, i4, env, static) -{0,0}> main_ConstantStackPush_48(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i2, i4, env, static) -{0,0}> main_ConstantStackPush_51(i2, i4, env, static) :|: 0 <= static
main_ConstantStackPush_51(i2, i4, env, static) -{0,0}> main_ConstantStackPush_52(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i2, i4, env, static) -{0,0}> main_ConstantStackPush_53(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_53(i2, i4, env, static) -{1,1}> main_Store_54(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_54(i2, i4, iconst_0, env, static) -{1,1}> main_Load_56(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_56(i2, i4, iconst_0, env, static) -{1,1}> main_LE_59(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, iconst_0, env, static) :|: i11 <= 0 && iconst_0 = 0
main_LE_59(i2, i12, iconst_0, env, static) -{0,0}> main_LE_62(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_LE_62(i2, i12, iconst_0, env, static) -{1,1}> main_Load_66(i2, i12, iconst_0, env, static) :|: 0 < i12 && iconst_0 = 0 && 1 <= i12
main_Load_66(i2, i12, iconst_0, env, static) -{1,1}> main_Store_68(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Store_68(i2, i12, iconst_0, env, static) -{1,1}> main_Load_70(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Load_70(i2, i12, iconst_0, env, static) -{1,1}> main_ConstantStackPush_74(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_ConstantStackPush_74(i2, i12, iconst_0, env, static) -{1,1}> main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12
main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) -{1,1}> main_Store_82(i2, i12, i13, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && i12 - iconst_1 = i13 && 1 <= i12 && 0 <= i13
main_Store_82(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Load_84(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Load_84(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Store_86(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Store_86(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Inc_88(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Inc_88(i2, i12, i13, iconst_0, env, static) -{1,1}> main_JMP_91(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_JMP_91(i2, i12, i13, iconst_1, env, static) -{1,1}> main_Load_101(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_101(i2, i12, i13, iconst_1, env, static) -{0,0}> main_Load_518(i2, i12, i13, i2, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_518(i48, i12, i49, i50, i51, env, static) -{0,0}> main_Load_586(i48, i12, i49, i50, i51, env, static) :|: 0 <= i49 && i51 <= 3 && i51 <= 2 && 1 <= i12 && 1 <= i51
main_Load_586(i48, i12, i167, i168, i169, env, static) -{0,0}> main_Load_690(i48, i12, i167, i168, i169, env, static) :|: 1 <= i169 && 1 <= i12 && i169 <= 3 && 0 <= i167
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i268, i243, i245, env, static) -{0,0}> main_LE_701(i48, i12, i268, i243, i245, env, static) :|: 0 <= i243 && i268 <= 0 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i269, i243, i245, env, static) -{0,0}> main_LE_702(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_LE_702(i48, i12, i269, i243, i245, env, static) -{1,1}> main_Load_708(i48, i12, i243, i269, i245, env, static) :|: 0 < i269 && 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_708(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Store_713(i48, i12, i243, i269, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Store_713(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Load_719(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_719(i48, i12, i269, i243, i245, env, static) -{1,1}> main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) -{1,1}> main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && 1 <= i245 && 1 <= i12
main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) -{1,1}> main_Store_736(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && i269 - iconst_1 = i286 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_736(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Load_739(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Load_739(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Store_741(i48, i12, i243, i286, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_741(i48, i12, i243, i286, i245, env, static) -{1,1}> main_Inc_744(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Inc_744(i48, i12, i286, i243, i245, env, static) -{1,1}> main_JMP_747(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i245 && 1 <= i12 && 0 <= i286 && i245 + 1 = i295
main_JMP_747(i48, i12, i286, i243, i295, env, static) -{1,1}> main_Load_753(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i12 && 0 <= i286
main_Load_753(i48, i12, i286, i243, i295, env, static) -{0,0}> main_Load_690(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 1 <= i295 && 2 <= i295 && 1 <= i12 && 0 <= i286

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

obtained
main_ConstantStackPush_2(i2, i4, env, static) -{18,18}> main_LE_59(i2, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
by chaining
main_ConstantStackPush_2(i2, i4, env, static) -{0,0}> main_ConstantStackPush_3(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i2, i4, env, static) -{1,1}> main_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, i4, env, static) -{0,0}> main_ConstantStackPush_48(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i2, i4, env, static) -{0,0}> main_ConstantStackPush_51(i2, i4, env, static) :|: 0 <= static
main_ConstantStackPush_51(i2, i4, env, static) -{0,0}> main_ConstantStackPush_52(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i2, i4, env, static) -{0,0}> main_ConstantStackPush_53(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_53(i2, i4, env, static) -{1,1}> main_Store_54(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_54(i2, i4, iconst_0, env, static) -{1,1}> main_Load_56(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_56(i2, i4, iconst_0, env, static) -{1,1}> main_LE_59(i2, i4, iconst_0, env, static) :|: iconst_0 = 0

obtained
main_LE_59(i2, i12, 0, env, static) -{11,11}> main_Load_690(i2, i12, i13', i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2
by chaining
main_LE_59(i2, i12, iconst_0, env, static) -{0,0}> main_LE_62(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_LE_62(i2, i12, iconst_0, env, static) -{1,1}> main_Load_66(i2, i12, iconst_0, env, static) :|: 0 < i12 && iconst_0 = 0 && 1 <= i12
main_Load_66(i2, i12, iconst_0, env, static) -{1,1}> main_Store_68(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Store_68(i2, i12, iconst_0, env, static) -{1,1}> main_Load_70(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Load_70(i2, i12, iconst_0, env, static) -{1,1}> main_ConstantStackPush_74(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_ConstantStackPush_74(i2, i12, iconst_0, env, static) -{1,1}> main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12
main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) -{1,1}> main_Store_82(i2, i12, i13, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && i12 - iconst_1 = i13 && 1 <= i12 && 0 <= i13
main_Store_82(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Load_84(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Load_84(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Store_86(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Store_86(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Inc_88(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Inc_88(i2, i12, i13, iconst_0, env, static) -{1,1}> main_JMP_91(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_JMP_91(i2, i12, i13, iconst_1, env, static) -{1,1}> main_Load_101(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_101(i2, i12, i13, iconst_1, env, static) -{0,0}> main_Load_518(i2, i12, i13, i2, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_518(i48, i12, i49, i50, i51, env, static) -{0,0}> main_Load_586(i48, i12, i49, i50, i51, env, static) :|: 0 <= i49 && i51 <= 3 && i51 <= 2 && 1 <= i12 && 1 <= i51
main_Load_586(i48, i12, i167, i168, i169, env, static) -{0,0}> main_Load_690(i48, i12, i167, i168, i169, env, static) :|: 1 <= i169 && 1 <= i12 && i169 <= 3 && 0 <= i167

obtained
main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i286', i243, i295', env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'
by chaining
main_LE_699(i48, i12, i269, i243, i245, env, static) -{0,0}> main_LE_702(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_LE_702(i48, i12, i269, i243, i245, env, static) -{1,1}> main_Load_708(i48, i12, i243, i269, i245, env, static) :|: 0 < i269 && 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_708(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Store_713(i48, i12, i243, i269, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Store_713(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Load_719(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_719(i48, i12, i269, i243, i245, env, static) -{1,1}> main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) -{1,1}> main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && 1 <= i245 && 1 <= i12
main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) -{1,1}> main_Store_736(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && i269 - iconst_1 = i286 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_736(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Load_739(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Load_739(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Store_741(i48, i12, i243, i286, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_741(i48, i12, i243, i286, i245, env, static) -{1,1}> main_Inc_744(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Inc_744(i48, i12, i286, i243, i245, env, static) -{1,1}> main_JMP_747(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i245 && 1 <= i12 && 0 <= i286 && i245 + 1 = i295
main_JMP_747(i48, i12, i286, i243, i295, env, static) -{1,1}> main_Load_753(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i12 && 0 <= i286
main_Load_753(i48, i12, i286, i243, i295, env, static) -{0,0}> main_Load_690(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 1 <= i295 && 2 <= i295 && 1 <= i12 && 0 <= i286

(8) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(i2, i4, env, static) -{18,18}> main_LE_59(i2, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0
main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, iconst_0, env, static) :|: i11 <= 0 && iconst_0 = 0
main_LE_59(i2, i12, 0, env, static) -{11,11}> main_Load_690(i2, i12, i13', i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i268, i243, i245, env, static) -{0,0}> main_LE_701(i48, i12, i268, i243, i245, env, static) :|: 0 <= i243 && i268 <= 0 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i286', i243, i295', env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'

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

Moved arithmethic from lhss to constraints.

main_LE_59(i2, i12, 0, env, static) -{11,11}> main_Load_690(i2, i12, i13', i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2
was transformed to
main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i13', i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2 && x = 0

(10) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, iconst_0, env, static) :|: i11 <= 0 && iconst_0 = 0
main_LE_699(i48, i12, i268, i243, i245, env, static) -{0,0}> main_LE_701(i48, i12, i268, i243, i245, env, static) :|: 0 <= i243 && i268 <= 0 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i286', i243, i295', env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'
main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i13', i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2 && x = 0
main_ConstantStackPush_2(i2, i4, env, static) -{18,18}> main_LE_59(i2, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0

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

Moved arithmethic from constraints to rhss.

main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, iconst_0, env, static) :|: i11 <= 0 && iconst_0 = 0
was transformed to
main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, 0, env, static) :|: i11 <= 0 && iconst_0 = 0

main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i286', i243, i295', env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'
was transformed to
main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i269 - 1, i243, i245 + 1, env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'

main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i13', i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2 && x = 0
was transformed to
main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i12 - 1, i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2 && x = 0

(12) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, 0, env, static) :|: i11 <= 0 && iconst_0 = 0
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i268, i243, i245, env, static) -{0,0}> main_LE_701(i48, i12, i268, i243, i245, env, static) :|: 0 <= i243 && i268 <= 0 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i269 - 1, i243, i245 + 1, env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'
main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i12 - 1, i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2 && x = 0
main_ConstantStackPush_2(i2, i4, env, static) -{18,18}> main_LE_59(i2, i4, 0, env, static'1) :|: 0 <= 2 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2 && 0 >= 0

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

Simplified expressions.

main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i12 - 1, i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= 3 && 1 <= 1 && 1 <= i12 && i12 - 1 = i13' && 1 <= 2 && x = 0
was transformed to
main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i12 - 1, i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= i12 && i12 - 1 = i13' && x = 0

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

(14) Obligation:

IntTrs with 6 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_LE_59(i2, i12, x, env, static) -{11,11}> main_Load_690(i2, i12, i12 - 1, i2, 1, env, static) :|: 0 < i12 && 0 <= i13' && 1 <= i12 && i12 - 1 = i13' && x = 0
main_LE_699(i48, i12, i269, i243, i245, env, static) -{11,11}> main_Load_690(i48, i12, i269 - 1, i243, i245 + 1, env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i269 && 1 <= i12 && 1 <= i269 && 2 <= i295' && 1 <= i245 && 0 <= i243 && 1 <= i295' && i269 - 1 = i286'
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_ConstantStackPush_2(i2, i4, env, static) -{18,18}> main_LE_59(i2, i4, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_LE_699(i48, i12, i268, i243, i245, env, static) -{0,0}> main_LE_701(i48, i12, i268, i243, i245, env, static) :|: 0 <= i243 && i268 <= 0 && 1 <= i245 && 1 <= i12
main_LE_59(i2, i11, iconst_0, env, static) -{0,0}> main_LE_61(i2, i11, 0, env, static) :|: i11 <= 0 && iconst_0 = 0

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

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

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

Simplified expressions.

(24) Obligation:

(25) koat Proof (EQUIVALENT transformation)

YES(?, 12*ar_0 + 12*ar_1 + 30)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 11) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_690(ar_0, ar_1, ar_1 - 1, ar_0, 1, ar_3, ar_4)) [ 0 < ar_1 /\ 0 <= i13' /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ ar_2 = 0 ]
(Comp: ?, Cost: 11) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1, ar_5, ar_6)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
(Comp: ?, Cost: 1) main_Load_690(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_699(ar_0, ar_1, ar_3, ar_2, ar_4, ar_5, ar_6)) [ 0 <= ar_2 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_59(ar_0, ar_1, 0, ar_2, static'1, arityPad, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 0) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 0) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_LE_61(ar_0, ar_1, 0, ar_3, ar_4, arityPad, arityPad)) [ ar_1 <= 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5, ar_6)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [ar_0, ar_1, ar_2, ar_3, ar_4].
We thus obtain the following problem:
2: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
(Comp: ?, Cost: 0) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_61(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_1 <= 0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 0) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_59(ar_0, ar_1, 0, ar_2, static'1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_690(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_699(ar_0, ar_1, ar_3, ar_2, ar_4)) [ 0 <= ar_2 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 11) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
(Comp: ?, Cost: 11) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_1 - 1, ar_0, 1)) [ 0 < ar_1 /\ 0 <= i13' /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ ar_2 = 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
(Comp: 1, Cost: 0) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_61(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_1 <= 0 /\ ar_2 = 0 ]
(Comp: ?, Cost: 0) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_59(ar_0, ar_1, 0, ar_2, static'1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_690(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_699(ar_0, ar_1, ar_3, ar_2, ar_4)) [ 0 <= ar_2 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 11) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
(Comp: 1, Cost: 11) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_1 - 1, ar_0, 1)) [ 0 < ar_1 /\ 0 <= i13' /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ ar_2 = 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 1
Pol(main_ConstantStackPush_2) = 1
Pol(main_LE_59) = 1
Pol(main_LE_61) = 0
Pol(main_LE_699) = 1
Pol(main_LE_701) = 0
Pol(main_Load_690) = 1
orients all transitions weakly and the transition
main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
(Comp: 1, Cost: 0) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_61(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_1 <= 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_59(ar_0, ar_1, 0, ar_2, static'1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_690(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_699(ar_0, ar_1, ar_3, ar_2, ar_4)) [ 0 <= ar_2 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 11) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
(Comp: 1, Cost: 11) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_1 - 1, ar_0, 1)) [ 0 < ar_1 /\ 0 <= i13' /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ ar_2 = 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = V_1 + V_2
Pol(main_ConstantStackPush_2) = V_1 + V_2
Pol(main_LE_59) = V_1 + V_2
Pol(main_LE_61) = V_1 + V_2
Pol(main_LE_699) = V_3 + V_4
Pol(main_LE_701) = V_3 + V_4
Pol(main_Load_690) = V_3 + V_4
orients all transitions weakly and the transition
main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
strictly and produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
(Comp: 1, Cost: 0) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_61(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_1 <= 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_59(ar_0, ar_1, 0, ar_2, static'1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_Load_690(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_699(ar_0, ar_1, ar_3, ar_2, ar_4)) [ 0 <= ar_2 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 11) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
(Comp: 1, Cost: 11) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_1 - 1, ar_0, 1)) [ 0 < ar_1 /\ 0 <= i13' /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ ar_2 = 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 5 produces the following problem:
6: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
(Comp: 1, Cost: 0) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_61(ar_0, ar_1, 0, ar_3, ar_4)) [ ar_1 <= 0 /\ ar_2 = 0 ]
(Comp: 1, Cost: 0) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_701(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= ar_3 /\ ar_2 <= 0 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 18) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_59(ar_0, ar_1, 0, ar_2, static'1)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_3 + 2 /\ 0 <= ar_3 /\ 0 <= static'1 ]
(Comp: ar_0 + ar_1 + 1, Cost: 1) main_Load_690(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_LE_699(ar_0, ar_1, ar_3, ar_2, ar_4)) [ 0 <= ar_2 /\ 1 <= ar_4 /\ 1 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 11) main_LE_699(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_2 - 1, ar_3, ar_4 + 1)) [ ar_4 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_1 /\ 1 <= ar_2 /\ 2 <= i295' /\ 1 <= ar_4 /\ 0 <= ar_3 /\ 1 <= i295' /\ ar_2 - 1 = i286' ]
(Comp: 1, Cost: 11) main_LE_59(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_690(ar_0, ar_1, ar_1 - 1, ar_0, 1)) [ 0 < ar_1 /\ 0 <= i13' /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ ar_2 = 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 12*ar_0 + 12*ar_1 + 30

Time: 0.160 sec (SMT: 0.143 sec)

(26) BOUNDS(CONSTANT, 30 + 12 * |#0| + 12 * |#1|)

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

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

(28) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(30) Obligation:

IntTrs with 55 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i2, i4, env, static) -{0,0}> main_ConstantStackPush_3(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i2, i4, env, static) -{1,1}> main_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, i4, env, static) -{0,0}> main_ConstantStackPush_48(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i2, i4, env, static) -{0,0}> main_ConstantStackPush_51(i2, i4, env, static) :|: 0 <= static
main_ConstantStackPush_51(i2, i4, env, static) -{0,0}> main_ConstantStackPush_52(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i2, i4, env, static) -{0,0}> main_ConstantStackPush_53(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_53(i2, i4, env, static) -{1,1}> main_Store_54(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_54(i2, i4, iconst_0, env, static) -{1,1}> main_Load_56(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_56(i2, i4, iconst_0, env, static) -{1,1}> main_LE_59(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_59(i2, i12, iconst_0, env, static) -{0,0}> main_LE_62(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_LE_62(i2, i12, iconst_0, env, static) -{1,1}> main_Load_66(i2, i12, iconst_0, env, static) :|: 0 < i12 && iconst_0 = 0 && 1 <= i12
main_Load_66(i2, i12, iconst_0, env, static) -{1,1}> main_Store_68(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Store_68(i2, i12, iconst_0, env, static) -{1,1}> main_Load_70(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Load_70(i2, i12, iconst_0, env, static) -{1,1}> main_ConstantStackPush_74(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_ConstantStackPush_74(i2, i12, iconst_0, env, static) -{1,1}> main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12
main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) -{1,1}> main_Store_82(i2, i12, i13, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && i12 - iconst_1 = i13 && 1 <= i12 && 0 <= i13
main_Store_82(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Load_84(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Load_84(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Store_86(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Store_86(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Inc_88(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Inc_88(i2, i12, i13, iconst_0, env, static) -{1,1}> main_JMP_91(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_JMP_91(i2, i12, i13, iconst_1, env, static) -{1,1}> main_Load_101(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_101(i2, i12, i13, iconst_1, env, static) -{0,0}> main_Load_518(i2, i12, i13, i2, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_518(i48, i12, i49, i50, i51, env, static) -{0,0}> main_Load_586(i48, i12, i49, i50, i51, env, static) :|: 0 <= i49 && i51 <= 3 && i51 <= 2 && 1 <= i12 && 1 <= i51
main_Load_586(i48, i12, i167, i168, i169, env, static) -{0,0}> main_Load_690(i48, i12, i167, i168, i169, env, static) :|: 1 <= i169 && 1 <= i12 && i169 <= 3 && 0 <= i167
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i269, i243, i245, env, static) -{0,0}> main_LE_702(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_LE_702(i48, i12, i269, i243, i245, env, static) -{1,1}> main_Load_708(i48, i12, i243, i269, i245, env, static) :|: 0 < i269 && 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_708(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Store_713(i48, i12, i243, i269, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Store_713(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Load_719(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_719(i48, i12, i269, i243, i245, env, static) -{1,1}> main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) -{1,1}> main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && 1 <= i245 && 1 <= i12
main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) -{1,1}> main_Store_736(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && i269 - iconst_1 = i286 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_736(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Load_739(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Load_739(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Store_741(i48, i12, i243, i286, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_741(i48, i12, i243, i286, i245, env, static) -{1,1}> main_Inc_744(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Inc_744(i48, i12, i286, i243, i245, env, static) -{1,1}> main_JMP_747(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i245 && 1 <= i12 && 0 <= i286 && i245 + 1 = i295
main_JMP_747(i48, i12, i286, i243, i295, env, static) -{1,1}> main_Load_753(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i12 && 0 <= i286
main_Load_753(i48, i12, i286, i243, i295, env, static) -{0,0}> main_Load_690(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 1 <= i295 && 2 <= i295 && 1 <= i12 && 0 <= i286

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

obtained
main_ConstantStackPush_2(i2, i4, env, static) -{29,29}> main_Load_690(i2, i4, i13', i2, 1, env, static'1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
by chaining
main_ConstantStackPush_2(i2, i4, env, static) -{0,0}> main_ConstantStackPush_3(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_21(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_24(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_27(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_27(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_45(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_45(i2, i4, env, static) -{1,1}> main_ConstantStackPush_47(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i2, i4, env, static) -{0,0}> main_ConstantStackPush_48(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_48(i2, i4, env, static) -{0,0}> main_ConstantStackPush_51(i2, i4, env, static) :|: 0 <= static
main_ConstantStackPush_51(i2, i4, env, static) -{0,0}> main_ConstantStackPush_52(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i2, i4, env, static) -{0,0}> main_ConstantStackPush_53(i2, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_53(i2, i4, env, static) -{1,1}> main_Store_54(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_54(i2, i4, iconst_0, env, static) -{1,1}> main_Load_56(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_56(i2, i4, iconst_0, env, static) -{1,1}> main_LE_59(i2, i4, iconst_0, env, static) :|: iconst_0 = 0
main_LE_59(i2, i12, iconst_0, env, static) -{0,0}> main_LE_62(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_LE_62(i2, i12, iconst_0, env, static) -{1,1}> main_Load_66(i2, i12, iconst_0, env, static) :|: 0 < i12 && iconst_0 = 0 && 1 <= i12
main_Load_66(i2, i12, iconst_0, env, static) -{1,1}> main_Store_68(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Store_68(i2, i12, iconst_0, env, static) -{1,1}> main_Load_70(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_Load_70(i2, i12, iconst_0, env, static) -{1,1}> main_ConstantStackPush_74(i2, i12, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12
main_ConstantStackPush_74(i2, i12, iconst_0, env, static) -{1,1}> main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12
main_IntArithmetic_79(i2, i12, iconst_1, iconst_0, env, static) -{1,1}> main_Store_82(i2, i12, i13, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && i12 - iconst_1 = i13 && 1 <= i12 && 0 <= i13
main_Store_82(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Load_84(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Load_84(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Store_86(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Store_86(i2, i12, i13, iconst_0, env, static) -{1,1}> main_Inc_88(i2, i12, i13, iconst_0, env, static) :|: iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_Inc_88(i2, i12, i13, iconst_0, env, static) -{1,1}> main_JMP_91(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0 && 1 <= i12 && 0 <= i13
main_JMP_91(i2, i12, i13, iconst_1, env, static) -{1,1}> main_Load_101(i2, i12, i13, iconst_1, env, static) :|: iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_101(i2, i12, i13, iconst_1, env, static) -{0,0}> main_Load_518(i2, i12, i13, i2, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1 && 1 <= i12 && 0 <= i13
main_Load_518(i48, i12, i49, i50, i51, env, static) -{0,0}> main_Load_586(i48, i12, i49, i50, i51, env, static) :|: 0 <= i49 && i51 <= 3 && i51 <= 2 && 1 <= i12 && 1 <= i51
main_Load_586(i48, i12, i167, i168, i169, env, static) -{0,0}> main_Load_690(i48, i12, i167, i168, i169, env, static) :|: 1 <= i169 && 1 <= i12 && i169 <= 3 && 0 <= i167

obtained
main_Load_690(i48, i12, i243, i244, i245, env, static) -{12,12}> main_Load_690(i48, i12, i286', i243, i295', env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'
by chaining
main_Load_690(i48, i12, i243, i244, i245, env, static) -{1,1}> main_LE_699(i48, i12, i244, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12
main_LE_699(i48, i12, i269, i243, i245, env, static) -{0,0}> main_LE_702(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_LE_702(i48, i12, i269, i243, i245, env, static) -{1,1}> main_Load_708(i48, i12, i243, i269, i245, env, static) :|: 0 < i269 && 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_708(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Store_713(i48, i12, i243, i269, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Store_713(i48, i12, i243, i269, i245, env, static) -{1,1}> main_Load_719(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_Load_719(i48, i12, i269, i243, i245, env, static) -{1,1}> main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && 1 <= i245 && 1 <= i12
main_ConstantStackPush_724(i48, i12, i269, i243, i245, env, static) -{1,1}> main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && 1 <= i245 && 1 <= i12
main_IntArithmetic_731(i48, i12, i269, iconst_1, i243, i245, env, static) -{1,1}> main_Store_736(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i269 && iconst_1 = 1 && i269 - iconst_1 = i286 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_736(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Load_739(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Load_739(i48, i12, i286, i243, i245, env, static) -{1,1}> main_Store_741(i48, i12, i243, i286, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Store_741(i48, i12, i243, i286, i245, env, static) -{1,1}> main_Inc_744(i48, i12, i286, i243, i245, env, static) :|: 0 <= i243 && 1 <= i245 && 1 <= i12 && 0 <= i286
main_Inc_744(i48, i12, i286, i243, i245, env, static) -{1,1}> main_JMP_747(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i245 && 1 <= i12 && 0 <= i286 && i245 + 1 = i295
main_JMP_747(i48, i12, i286, i243, i295, env, static) -{1,1}> main_Load_753(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 2 <= i295 && 1 <= i12 && 0 <= i286
main_Load_753(i48, i12, i286, i243, i295, env, static) -{0,0}> main_Load_690(i48, i12, i286, i243, i295, env, static) :|: 0 <= i243 && 1 <= i295 && 2 <= i295 && 1 <= i12 && 0 <= i286

(32) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i2, i4, env, static) -{29,29}> main_Load_690(i2, i4, i13', i2, 1, env, static'1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
main_Load_690(i48, i12, i243, i244, i245, env, static) -{12,12}> main_Load_690(i48, i12, i286', i243, i295', env, static) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'

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

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

main_ConstantStackPush_2(x1, x2, x3, x4) → main_ConstantStackPush_2(x1, x2, x4)
main_Load_690(x1, x2, x3, x4, x5, x6, x7) → main_Load_690(x2, x3, x4, x5)

(34) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i13', i2, 1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
main_Load_690(i12, i243, i244, i245) -{12,12}> main_Load_690(i12, i286', i243, i295') :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'

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

Moved arithmethic from constraints to rhss.

main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i13', i2, 1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i4 - 1, i2, 1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1

main_Load_690(i12, i243, i244, i245) -{12,12}> main_Load_690(i12, i286', i243, i295') :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'
was transformed to
main_Load_690(i12, i243, i244, i245) -{12,12}> main_Load_690(i12, i244 - 1, i243, i245 + 1) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'

(36) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i4 - 1, i2, 1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
main_Load_690(i12, i243, i244, i245) -{12,12}> main_Load_690(i12, i244 - 1, i243, i245 + 1) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'

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

Simplified expressions.

main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i4 - 1, i2, 1) :|: 0 >= 0 && 0 <= i13' && 0 < 2 && 1 <= 3 && 0 <= static'1 && 1 <= 1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 1 <= 2 && 0 < i4 && 0 <= 2 && static'1 <= static''' + 1
was transformed to
main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i4 - 1, i2, 1) :|: 0 <= i13' && 0 <= static'1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && static''' <= static + 2 && 0 <= static''' && 0 < i4 && static'1 <= static''' + 1

(38) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_690(i12, i243, i244, i245) -{12,12}> main_Load_690(i12, i244 - 1, i243, i245 + 1) :|: i245 + 1 = i295' && 0 <= i286' && 0 < i244 && 1 <= i12 && 1 <= i245 && 2 <= i295' && 0 <= i243 && 1 <= i295' && 1 <= i244 && i244 - 1 = i286'
main_ConstantStackPush_2(i2, i4, static) -{29,29}> main_Load_690(i4, i4 - 1, i2, 1) :|: 0 <= i13' && 0 <= static'1 && 1 <= i4 && i4 - 1 = i13' && 0 <= static && static''' <= static + 2 && 0 <= static''' && 0 < i4 && static'1 <= static''' + 1

(39) koat Proof (EQUIVALENT transformation)

YES(?, 12*ar_0 + 12*ar_1 + 29)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 12) main_Load_690(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_0, ar_2 - 1, ar_1, ar_3 + 1)) [ ar_3 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_0 /\ 1 <= ar_3 /\ 2 <= i295' /\ 0 <= ar_1 /\ 1 <= i295' /\ 1 <= ar_2 /\ ar_2 - 1 = i286' ]
(Comp: ?, Cost: 29) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_1, ar_1 - 1, ar_0, 1)) [ 0 <= i13' /\ 0 <= static'1 /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ 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_ConstantStackPush_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: 12) main_Load_690(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_0, ar_2 - 1, ar_1, ar_3 + 1)) [ ar_3 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_0 /\ 1 <= ar_3 /\ 2 <= i295' /\ 0 <= ar_1 /\ 1 <= i295' /\ 1 <= ar_2 /\ ar_2 - 1 = i286' ]
(Comp: 1, Cost: 29) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_1, ar_1 - 1, ar_0, 1)) [ 0 <= i13' /\ 0 <= static'1 /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ 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_ConstantStackPush_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_690) = V_2 + V_3
Pol(main_ConstantStackPush_2) = V_1 + V_2
Pol(koat_start) = V_1 + V_2
orients all transitions weakly and the transition
main_Load_690(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_0, ar_2 - 1, ar_1, ar_3 + 1)) [ ar_3 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_0 /\ 1 <= ar_3 /\ 2 <= i295' /\ 0 <= ar_1 /\ 1 <= i295' /\ 1 <= ar_2 /\ ar_2 - 1 = i286' ]
strictly and produces the following problem:
3: T:
(Comp: ar_0 + ar_1, Cost: 12) main_Load_690(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_0, ar_2 - 1, ar_1, ar_3 + 1)) [ ar_3 + 1 = i295' /\ 0 <= i286' /\ 0 < ar_2 /\ 1 <= ar_0 /\ 1 <= ar_3 /\ 2 <= i295' /\ 0 <= ar_1 /\ 1 <= i295' /\ 1 <= ar_2 /\ ar_2 - 1 = i286' ]
(Comp: 1, Cost: 29) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_690(ar_1, ar_1 - 1, ar_0, 1)) [ 0 <= i13' /\ 0 <= static'1 /\ 1 <= ar_1 /\ ar_1 - 1 = i13' /\ 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_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 12*ar_0 + 12*ar_1 + 29

Time: 0.159 sec (SMT: 0.151 sec)

(0) Obligation:

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

(2) Obligation:

(3) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(12)) 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) koat Proof (EQUIVALENT transformation)

(26) BOUNDS(CONSTANT, 30 + 12 * |#0| + 12 * |#1|)

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

(33) WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(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, 29 + 12 * |#0| + 12 * |#1|)