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

(0) Obligation:

Need to prove time_complexity of the following program:

public class MinusMin{

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

    if (x < y) return x;
    else return y;
  }


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



    while (min(x-1,y) == y) {

      y++;
      res++;

    }


  }

}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 61 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i1, i4, env, static) -{0,0}> main_ConstantStackPush_4(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i1, i4, env, static) -{0,0}> main_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, i4, env, static) -{0,0}> main_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, i4, env, static) -{0,0}> main_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, env, static) -{0,0}> main_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, i4, env, static) -{1,1}> main_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, i4, iconst_0, env, static) -{1,1}> main_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, i4, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(i1, i4, iconst_0, env, static) -{1,1}> main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) -{1,1}> main_Load_58(i1, i4, i6, iconst_0, env, static) :|: i1 - iconst_1 = i6 && iconst_1 = 1 && iconst_0 = 0
main_Load_58(i1, i4, i6, iconst_0, env, static) -{1,1}> main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) :|: iconst_0 = 0
main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) -{1,1}> min_Load_62(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_62(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_64(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_64(i6, i4, i1, iconst_0, env, static) -{1,1}> min_GE_69(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_77(i6, i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_GE_77(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_79(i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_Load_79(i4, i1, iconst_0, env, static) -{1,1}> min_Return_82(i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Return_82(i4, i1, iconst_0, env, static) -{1,1}> main_Load_84(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_84(i1, i4, iconst_0, env, static) -{1,1}> main_NE_99(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_NE_99(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_108(i1, i4, iconst_0, env, static) :|: i4 = i4 && iconst_0 = 0
main_Inc_108(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_113(i1, i4, i13, iconst_0, env, static) :|: i4 + 1 = i13 && iconst_0 = 0
main_Inc_113(i1, i4, i13, iconst_0, env, static) -{1,1}> main_JMP_116(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_116(i1, i4, i13, iconst_1, env, static) -{1,1}> main_Load_118(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1
main_Load_118(i1, i4, i13, iconst_1, env, static) -{0,0}> main_Load_228(i1, i4, i13, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_228(i1, i4, i70, i71, env, static) -{0,0}> main_Load_352(i1, i4, i70, i71, env, static) :|: i71 <= 3 && i71 <= 2 && 1 <= i71
main_Load_352(i1, i4, i132, i133, env, static) -{0,0}> main_Load_435(i1, i4, i132, i133, env, static) :|: 1 <= i133 && i133 <= 3
main_Load_435(i1, i4, i186, i187, env, static) -{1,1}> main_ConstantStackPush_437(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_ConstantStackPush_437(i1, i4, i186, i187, env, static) -{1,1}> main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1
main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) -{1,1}> main_Load_448(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1 && i1 - iconst_1 = i198
main_Load_448(i1, i4, i198, i186, i187, env, static) -{1,1}> main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187
main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) -{1,1}> min_Load_451(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_451(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_452(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_452(i198, i186, i1, i4, i187, env, static) -{1,1}> min_GE_477(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_489(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_GE_489(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_493(i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_Load_493(i186, i1, i4, i187, env, static) -{1,1}> min_Return_501(i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Return_501(i186, i1, i4, i187, env, static) -{1,1}> main_Load_507(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_Load_507(i1, i4, i186, i187, env, static) -{1,1}> main_NE_521(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_NE_521(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_571(i1, i4, i186, i187, env, static) :|: 1 <= i187 && i186 = i186
main_Inc_571(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_575(i1, i4, i241, i187, env, static) :|: i186 + 1 = i241 && 1 <= i187
main_Inc_575(i1, i4, i241, i187, env, static) -{1,1}> main_JMP_584(i1, i4, i241, i243, env, static) :|: 1 <= i187 && i187 + 1 = i243 && 2 <= i243
main_JMP_584(i1, i4, i241, i243, env, static) -{1,1}> main_Load_590(i1, i4, i241, i243, env, static) :|: 2 <= i243
main_Load_590(i1, i4, i241, i243, env, static) -{0,0}> main_Load_435(i1, i4, i241, i243, env, static) :|: 1 <= i243 && 2 <= i243

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

obtained
main_ConstantStackPush_2(i1, i4, env, static) -{32,32}> main_Load_435(i1, i4, i13', 1, env, static'1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2
by chaining
main_ConstantStackPush_2(i1, i4, env, static) -{0,0}> main_ConstantStackPush_4(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i1, i4, env, static) -{0,0}> main_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, i4, env, static) -{0,0}> main_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, i4, env, static) -{0,0}> main_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, env, static) -{0,0}> main_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, i4, env, static) -{1,1}> main_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, i4, iconst_0, env, static) -{1,1}> main_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, i4, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(i1, i4, iconst_0, env, static) -{1,1}> main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) -{1,1}> main_Load_58(i1, i4, i6, iconst_0, env, static) :|: i1 - iconst_1 = i6 && iconst_1 = 1 && iconst_0 = 0
main_Load_58(i1, i4, i6, iconst_0, env, static) -{1,1}> main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) :|: iconst_0 = 0
main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) -{1,1}> min_Load_62(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_62(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_64(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_64(i6, i4, i1, iconst_0, env, static) -{1,1}> min_GE_69(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_77(i6, i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_GE_77(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_79(i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_Load_79(i4, i1, iconst_0, env, static) -{1,1}> min_Return_82(i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Return_82(i4, i1, iconst_0, env, static) -{1,1}> main_Load_84(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_84(i1, i4, iconst_0, env, static) -{1,1}> main_NE_99(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_NE_99(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_108(i1, i4, iconst_0, env, static) :|: i4 = i4 && iconst_0 = 0
main_Inc_108(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_113(i1, i4, i13, iconst_0, env, static) :|: i4 + 1 = i13 && iconst_0 = 0
main_Inc_113(i1, i4, i13, iconst_0, env, static) -{1,1}> main_JMP_116(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_116(i1, i4, i13, iconst_1, env, static) -{1,1}> main_Load_118(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1
main_Load_118(i1, i4, i13, iconst_1, env, static) -{0,0}> main_Load_228(i1, i4, i13, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_228(i1, i4, i70, i71, env, static) -{0,0}> main_Load_352(i1, i4, i70, i71, env, static) :|: i71 <= 3 && i71 <= 2 && 1 <= i71
main_Load_352(i1, i4, i132, i133, env, static) -{0,0}> main_Load_435(i1, i4, i132, i133, env, static) :|: 1 <= i133 && i133 <= 3

obtained
main_Load_435(i1, i4, i186, i187, env, static) -{15,15}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'
by chaining
main_Load_435(i1, i4, i186, i187, env, static) -{1,1}> main_ConstantStackPush_437(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_ConstantStackPush_437(i1, i4, i186, i187, env, static) -{1,1}> main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1
main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) -{1,1}> main_Load_448(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1 && i1 - iconst_1 = i198
main_Load_448(i1, i4, i198, i186, i187, env, static) -{1,1}> main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187
main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) -{1,1}> min_Load_451(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_451(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_452(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_452(i198, i186, i1, i4, i187, env, static) -{1,1}> min_GE_477(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_489(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_GE_489(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_493(i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_Load_493(i186, i1, i4, i187, env, static) -{1,1}> min_Return_501(i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Return_501(i186, i1, i4, i187, env, static) -{1,1}> main_Load_507(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_Load_507(i1, i4, i186, i187, env, static) -{1,1}> main_NE_521(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_NE_521(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_571(i1, i4, i186, i187, env, static) :|: 1 <= i187 && i186 = i186
main_Inc_571(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_575(i1, i4, i241, i187, env, static) :|: i186 + 1 = i241 && 1 <= i187
main_Inc_575(i1, i4, i241, i187, env, static) -{1,1}> main_JMP_584(i1, i4, i241, i243, env, static) :|: 1 <= i187 && i187 + 1 = i243 && 2 <= i243
main_JMP_584(i1, i4, i241, i243, env, static) -{1,1}> main_Load_590(i1, i4, i241, i243, env, static) :|: 2 <= i243
main_Load_590(i1, i4, i241, i243, env, static) -{0,0}> main_Load_435(i1, i4, i241, i243, env, static) :|: 1 <= i243 && 2 <= i243

(8) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i1, i4, env, static) -{32,32}> main_Load_435(i1, i4, i13', 1, env, static'1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2
main_Load_435(i1, i4, i186, i187, env, static) -{15,15}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'

(9) 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_435(x1, x2, x3, x4, x5, x6) → main_Load_435(x1, x2, x3, x4)

(10) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i13', 1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2
main_Load_435(i1, i4, i186, i187) -{15,15}> main_Load_435(i1, i4, i241', i243') :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'

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

Moved arithmethic from constraints to rhss.

main_Load_435(i1, i4, i186, i187) -{15,15}> main_Load_435(i1, i4, i241', i243') :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'
was transformed to
main_Load_435(i1, i4, i186, i187) -{15,15}> main_Load_435(i1, i4, i186 + 1, i187 + 1) :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'

main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i13', 1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2
was transformed to
main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i4 + 1, 1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2

(12) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_Load_435(i1, i4, i186, i187) -{15,15}> main_Load_435(i1, i4, i186 + 1, i187 + 1) :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'
main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i4 + 1, 1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2

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

Simplified expressions.

main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i4 + 1, 1) :|: i4 <= i6' && 1 <= 1 && 1 <= 3 && 0 <= 2 && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 1 <= 2 && i4 + 1 = i13' && 0 < 2
was transformed to
main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i4 + 1, 1) :|: i4 <= i6' && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 + 1 = i13'

(14) Obligation:

IntTrs with 2 rules
Start term: main_ConstantStackPush_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_ConstantStackPush_2(i1, i4, static) -{32,32}> main_Load_435(i1, i4, i4 + 1, 1) :|: i4 <= i6' && static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1 && i4 + 1 = i13'
main_Load_435(i1, i4, i186, i187) -{15,15}> main_Load_435(i1, i4, i186 + 1, i187 + 1) :|: i186 <= i198' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i187 + 1 = i243' && i1 - 1 = i198' && i186 + 1 = i241'

(15) koat Proof (EQUIVALENT transformation)

YES(?, 15*ar_0 + 15*ar_1 + 32)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 32) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_1 + 1, 1)) [ ar_1 <= i6' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i6' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 + 1 = i13' ]
(Comp: ?, Cost: 15) main_Load_435(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_2 + 1, ar_3 + 1)) [ ar_2 <= i198' /\ 1 <= i243' /\ 2 <= i243' /\ 1 <= ar_3 /\ ar_3 + 1 = i243' /\ ar_0 - 1 = i198' /\ ar_2 + 1 = i241' ]
(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: 1, Cost: 32) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_1 + 1, 1)) [ ar_1 <= i6' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i6' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 + 1 = i13' ]
(Comp: ?, Cost: 15) main_Load_435(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_2 + 1, ar_3 + 1)) [ ar_2 <= i198' /\ 1 <= i243' /\ 2 <= i243' /\ 1 <= ar_3 /\ ar_3 + 1 = i243' /\ ar_0 - 1 = i198' /\ ar_2 + 1 = i241' ]
(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_ConstantStackPush_2) = V_1 - V_2
Pol(main_Load_435) = V_1 - V_3
Pol(koat_start) = V_1 - V_2
orients all transitions weakly and the transition
main_Load_435(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_2 + 1, ar_3 + 1)) [ ar_2 <= i198' /\ 1 <= i243' /\ 2 <= i243' /\ 1 <= ar_3 /\ ar_3 + 1 = i243' /\ ar_0 - 1 = i198' /\ ar_2 + 1 = i241' ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 32) main_ConstantStackPush_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_1 + 1, 1)) [ ar_1 <= i6' /\ static'1 <= static''' + 1 /\ ar_0 - 1 = i6' /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 /\ ar_1 + 1 = i13' ]
(Comp: ar_0 + ar_1, Cost: 15) main_Load_435(ar_0, ar_1, ar_2, ar_3) -> Com_1(main_Load_435(ar_0, ar_1, ar_2 + 1, ar_3 + 1)) [ ar_2 <= i198' /\ 1 <= i243' /\ 2 <= i243' /\ 1 <= ar_3 /\ ar_3 + 1 = i243' /\ ar_0 - 1 = i198' /\ ar_2 + 1 = i241' ]
(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 15*ar_0 + 15*ar_1 + 32

Time: 0.073 sec (SMT: 0.066 sec)

(16) BOUNDS(CONSTANT, 32 + 15 * |#0| + 15 * |#1|)

(17) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(11)) transformation)

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

(18) Obligation:

Set of 63 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

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

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

(20) Obligation:

IntTrs with 63 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(i1, i4, env, static) -{0,0}> main_ConstantStackPush_4(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i1, i4, env, static) -{0,0}> main_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, i4, env, static) -{0,0}> main_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, i4, env, static) -{0,0}> main_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, env, static) -{0,0}> main_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, i4, env, static) -{1,1}> main_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, i4, iconst_0, env, static) -{1,1}> main_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, i4, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(i1, i4, iconst_0, env, static) -{1,1}> main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) -{1,1}> main_Load_58(i1, i4, i6, iconst_0, env, static) :|: i1 - iconst_1 = i6 && iconst_1 = 1 && iconst_0 = 0
main_Load_58(i1, i4, i6, iconst_0, env, static) -{1,1}> main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) :|: iconst_0 = 0
main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) -{1,1}> min_Load_62(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_62(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_64(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_64(i6, i4, i1, iconst_0, env, static) -{1,1}> min_GE_69(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_77(i6, i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_77(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_79(i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_Load_79(i4, i1, iconst_0, env, static) -{1,1}> min_Return_82(i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Return_82(i4, i1, iconst_0, env, static) -{1,1}> main_Load_84(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_84(i1, i4, iconst_0, env, static) -{1,1}> main_NE_99(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_NE_99(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_108(i1, i4, iconst_0, env, static) :|: i4 = i4 && iconst_0 = 0
main_Inc_108(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_113(i1, i4, i13, iconst_0, env, static) :|: i4 + 1 = i13 && iconst_0 = 0
main_Inc_113(i1, i4, i13, iconst_0, env, static) -{1,1}> main_JMP_116(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_116(i1, i4, i13, iconst_1, env, static) -{1,1}> main_Load_118(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1
main_Load_118(i1, i4, i13, iconst_1, env, static) -{0,0}> main_Load_228(i1, i4, i13, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_228(i1, i4, i70, i71, env, static) -{0,0}> main_Load_352(i1, i4, i70, i71, env, static) :|: i71 <= 3 && i71 <= 2 && 1 <= i71
main_Load_352(i1, i4, i132, i133, env, static) -{0,0}> main_Load_435(i1, i4, i132, i133, env, static) :|: 1 <= i133 && i133 <= 3
main_Load_435(i1, i4, i186, i187, env, static) -{1,1}> main_ConstantStackPush_437(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_ConstantStackPush_437(i1, i4, i186, i187, env, static) -{1,1}> main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1
main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) -{1,1}> main_Load_448(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1 && i1 - iconst_1 = i198
main_Load_448(i1, i4, i198, i186, i187, env, static) -{1,1}> main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187
main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) -{1,1}> min_Load_451(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_451(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_452(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_452(i198, i186, i1, i4, i187, env, static) -{1,1}> min_GE_477(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_489(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186
min_GE_489(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_493(i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_Load_493(i186, i1, i4, i187, env, static) -{1,1}> min_Return_501(i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Return_501(i186, i1, i4, i187, env, static) -{1,1}> main_Load_507(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_Load_507(i1, i4, i186, i187, env, static) -{1,1}> main_NE_521(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_NE_521(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_571(i1, i4, i186, i187, env, static) :|: 1 <= i187 && i186 = i186
main_Inc_571(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_575(i1, i4, i241, i187, env, static) :|: i186 + 1 = i241 && 1 <= i187
main_Inc_575(i1, i4, i241, i187, env, static) -{1,1}> main_JMP_584(i1, i4, i241, i243, env, static) :|: 1 <= i187 && i187 + 1 = i243 && 2 <= i243
main_JMP_584(i1, i4, i241, i243, env, static) -{1,1}> main_Load_590(i1, i4, i241, i243, env, static) :|: 2 <= i243
main_Load_590(i1, i4, i241, i243, env, static) -{0,0}> main_Load_435(i1, i4, i241, i243, env, static) :|: 1 <= i243 && 2 <= i243

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

obtained
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
main_ConstantStackPush_2(i1, i4, env, static) -{0,0}> main_ConstantStackPush_4(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i1, i4, env, static) -{0,0}> main_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, i4, env, static) -{0,0}> main_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, i4, env, static) -{0,0}> main_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, env, static) -{0,0}> main_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, i4, env, static) -{1,1}> main_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, i4, iconst_0, env, static) -{1,1}> main_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, i4, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(i1, i4, iconst_0, env, static) -{1,1}> main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) -{1,1}> main_Load_58(i1, i4, i6, iconst_0, env, static) :|: i1 - iconst_1 = i6 && iconst_1 = 1 && iconst_0 = 0
main_Load_58(i1, i4, i6, iconst_0, env, static) -{1,1}> main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) :|: iconst_0 = 0
main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) -{1,1}> min_Load_62(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_62(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_64(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_64(i6, i4, i1, iconst_0, env, static) -{1,1}> min_GE_69(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0

obtained
min_GE_69(i6, i4, i1, 0, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2
by chaining
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_77(i6, i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_GE_77(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_79(i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_Load_79(i4, i1, iconst_0, env, static) -{1,1}> min_Return_82(i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Return_82(i4, i1, iconst_0, env, static) -{1,1}> main_Load_84(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_84(i1, i4, iconst_0, env, static) -{1,1}> main_NE_99(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_NE_99(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_108(i1, i4, iconst_0, env, static) :|: i4 = i4 && iconst_0 = 0
main_Inc_108(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_113(i1, i4, i13, iconst_0, env, static) :|: i4 + 1 = i13 && iconst_0 = 0
main_Inc_113(i1, i4, i13, iconst_0, env, static) -{1,1}> main_JMP_116(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_116(i1, i4, i13, iconst_1, env, static) -{1,1}> main_Load_118(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1
main_Load_118(i1, i4, i13, iconst_1, env, static) -{0,0}> main_Load_228(i1, i4, i13, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_228(i1, i4, i70, i71, env, static) -{0,0}> main_Load_352(i1, i4, i70, i71, env, static) :|: i71 <= 3 && i71 <= 2 && 1 <= i71
main_Load_352(i1, i4, i132, i133, env, static) -{0,0}> main_Load_435(i1, i4, i132, i133, env, static) :|: 1 <= i133 && i133 <= 3

obtained
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
by chaining
main_Load_435(i1, i4, i186, i187, env, static) -{1,1}> main_ConstantStackPush_437(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_ConstantStackPush_437(i1, i4, i186, i187, env, static) -{1,1}> main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1
main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) -{1,1}> main_Load_448(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1 && i1 - iconst_1 = i198
main_Load_448(i1, i4, i198, i186, i187, env, static) -{1,1}> main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187
main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) -{1,1}> min_Load_451(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_451(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_452(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_452(i198, i186, i1, i4, i187, env, static) -{1,1}> min_GE_477(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187

obtained
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
by chaining
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_489(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_GE_489(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_493(i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_Load_493(i186, i1, i4, i187, env, static) -{1,1}> min_Return_501(i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Return_501(i186, i1, i4, i187, env, static) -{1,1}> main_Load_507(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_Load_507(i1, i4, i186, i187, env, static) -{1,1}> main_NE_521(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_NE_521(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_571(i1, i4, i186, i187, env, static) :|: 1 <= i187 && i186 = i186
main_Inc_571(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_575(i1, i4, i241, i187, env, static) :|: i186 + 1 = i241 && 1 <= i187
main_Inc_575(i1, i4, i241, i187, env, static) -{1,1}> main_JMP_584(i1, i4, i241, i243, env, static) :|: 1 <= i187 && i187 + 1 = i243 && 2 <= i243
main_JMP_584(i1, i4, i241, i243, env, static) -{1,1}> main_Load_590(i1, i4, i241, i243, env, static) :|: 2 <= i243
main_Load_590(i1, i4, i241, i243, env, static) -{0,0}> main_Load_435(i1, i4, i241, i243, env, static) :|: 1 <= i243 && 2 <= i243

(22) 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(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_69(i6, i4, i1, 0, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'

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

Moved arithmethic from lhss to constraints.

min_GE_69(i6, i4, i1, 0, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2
was transformed to
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0

(24) 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:
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186

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

Moved arithmethic from constraints to rhss.

min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
was transformed to
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, 0, env, static) :|: iconst_0 = 0 && i6 < i4

min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
was transformed to
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0

main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
was transformed to
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i1 - 1, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'

main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2

min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
was transformed to
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i186 + 1, i187 + 1, env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'

(26) 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:
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, 0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i1 - 1, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i186 + 1, i187 + 1, env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'

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

Simplified expressions.

min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
was transformed to
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && i4 <= i6 && x = 0

main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(28) 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_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i1 - 1, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && i4 <= i6 && x = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, 0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i186 + 1, i187 + 1, env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186

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

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

(30) Obligation:

IntTrs with 63 rules
Start term: main_ConstantStackPush_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ConstantStackPush_2(i1, i4, env, static) -{0,0}> main_ConstantStackPush_4(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i1, i4, env, static) -{0,0}> main_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, i4, env, static) -{0,0}> main_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, i4, env, static) -{0,0}> main_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, env, static) -{0,0}> main_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, i4, env, static) -{1,1}> main_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, i4, iconst_0, env, static) -{1,1}> main_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, i4, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(i1, i4, iconst_0, env, static) -{1,1}> main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) -{1,1}> main_Load_58(i1, i4, i6, iconst_0, env, static) :|: i1 - iconst_1 = i6 && iconst_1 = 1 && iconst_0 = 0
main_Load_58(i1, i4, i6, iconst_0, env, static) -{1,1}> main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) :|: iconst_0 = 0
main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) -{1,1}> min_Load_62(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_62(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_64(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_64(i6, i4, i1, iconst_0, env, static) -{1,1}> min_GE_69(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_77(i6, i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_77(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_79(i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_Load_79(i4, i1, iconst_0, env, static) -{1,1}> min_Return_82(i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Return_82(i4, i1, iconst_0, env, static) -{1,1}> main_Load_84(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_84(i1, i4, iconst_0, env, static) -{1,1}> main_NE_99(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_NE_99(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_108(i1, i4, iconst_0, env, static) :|: i4 = i4 && iconst_0 = 0
main_Inc_108(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_113(i1, i4, i13, iconst_0, env, static) :|: i4 + 1 = i13 && iconst_0 = 0
main_Inc_113(i1, i4, i13, iconst_0, env, static) -{1,1}> main_JMP_116(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_116(i1, i4, i13, iconst_1, env, static) -{1,1}> main_Load_118(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1
main_Load_118(i1, i4, i13, iconst_1, env, static) -{0,0}> main_Load_228(i1, i4, i13, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_228(i1, i4, i70, i71, env, static) -{0,0}> main_Load_352(i1, i4, i70, i71, env, static) :|: i71 <= 3 && i71 <= 2 && 1 <= i71
main_Load_352(i1, i4, i132, i133, env, static) -{0,0}> main_Load_435(i1, i4, i132, i133, env, static) :|: 1 <= i133 && i133 <= 3
main_Load_435(i1, i4, i186, i187, env, static) -{1,1}> main_ConstantStackPush_437(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_ConstantStackPush_437(i1, i4, i186, i187, env, static) -{1,1}> main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1
main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) -{1,1}> main_Load_448(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1 && i1 - iconst_1 = i198
main_Load_448(i1, i4, i198, i186, i187, env, static) -{1,1}> main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187
main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) -{1,1}> min_Load_451(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_451(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_452(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_452(i198, i186, i1, i4, i187, env, static) -{1,1}> min_GE_477(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_489(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186
min_GE_489(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_493(i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_Load_493(i186, i1, i4, i187, env, static) -{1,1}> min_Return_501(i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Return_501(i186, i1, i4, i187, env, static) -{1,1}> main_Load_507(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_Load_507(i1, i4, i186, i187, env, static) -{1,1}> main_NE_521(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_NE_521(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_571(i1, i4, i186, i187, env, static) :|: 1 <= i187 && i186 = i186
main_Inc_571(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_575(i1, i4, i241, i187, env, static) :|: i186 + 1 = i241 && 1 <= i187
main_Inc_575(i1, i4, i241, i187, env, static) -{1,1}> main_JMP_584(i1, i4, i241, i243, env, static) :|: 1 <= i187 && i187 + 1 = i243 && 2 <= i243
main_JMP_584(i1, i4, i241, i243, env, static) -{1,1}> main_Load_590(i1, i4, i241, i243, env, static) :|: 2 <= i243
main_Load_590(i1, i4, i241, i243, env, static) -{0,0}> main_Load_435(i1, i4, i241, i243, env, static) :|: 1 <= i243 && 2 <= i243

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

obtained
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
main_ConstantStackPush_2(i1, i4, env, static) -{0,0}> main_ConstantStackPush_4(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_4(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_17(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_17(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_36(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_40(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i1, i4, env, static) -{1,1}> main_ConstantStackPush_47(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_47(i1, i4, env, static) -{0,0}> main_ConstantStackPush_49(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_49(i1, i4, env, static) -{0,0}> main_ConstantStackPush_50(i1, i4, env, static) :|: 0 <= static
main_ConstantStackPush_50(i1, i4, env, static) -{0,0}> main_ConstantStackPush_51(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_51(i1, i4, env, static) -{0,0}> main_ConstantStackPush_52(i1, i4, env, static) :|: 0 >= 0
main_ConstantStackPush_52(i1, i4, env, static) -{1,1}> main_Store_53(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Store_53(i1, i4, iconst_0, env, static) -{1,1}> main_Load_54(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_54(i1, i4, iconst_0, env, static) -{1,1}> main_ConstantStackPush_55(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_ConstantStackPush_55(i1, i4, iconst_0, env, static) -{1,1}> main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_IntArithmetic_56(i1, i4, iconst_1, iconst_0, env, static) -{1,1}> main_Load_58(i1, i4, i6, iconst_0, env, static) :|: i1 - iconst_1 = i6 && iconst_1 = 1 && iconst_0 = 0
main_Load_58(i1, i4, i6, iconst_0, env, static) -{1,1}> main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) :|: iconst_0 = 0
main_InvokeMethod_60(i1, i4, i6, iconst_0, env, static) -{1,1}> min_Load_62(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_62(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_64(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Load_64(i6, i4, i1, iconst_0, env, static) -{1,1}> min_GE_69(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0

obtained
min_GE_69(i6, i4, i1, 0, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2
by chaining
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_77(i6, i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_GE_77(i6, i4, i1, iconst_0, env, static) -{1,1}> min_Load_79(i4, i1, iconst_0, env, static) :|: i4 <= i6 && iconst_0 = 0
min_Load_79(i4, i1, iconst_0, env, static) -{1,1}> min_Return_82(i4, i1, iconst_0, env, static) :|: iconst_0 = 0
min_Return_82(i4, i1, iconst_0, env, static) -{1,1}> main_Load_84(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_Load_84(i1, i4, iconst_0, env, static) -{1,1}> main_NE_99(i1, i4, iconst_0, env, static) :|: iconst_0 = 0
main_NE_99(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_108(i1, i4, iconst_0, env, static) :|: i4 = i4 && iconst_0 = 0
main_Inc_108(i1, i4, iconst_0, env, static) -{1,1}> main_Inc_113(i1, i4, i13, iconst_0, env, static) :|: i4 + 1 = i13 && iconst_0 = 0
main_Inc_113(i1, i4, i13, iconst_0, env, static) -{1,1}> main_JMP_116(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1 && iconst_0 = 0
main_JMP_116(i1, i4, i13, iconst_1, env, static) -{1,1}> main_Load_118(i1, i4, i13, iconst_1, env, static) :|: iconst_1 = 1
main_Load_118(i1, i4, i13, iconst_1, env, static) -{0,0}> main_Load_228(i1, i4, i13, iconst_1, env, static) :|: iconst_1 <= 2 && 1 <= iconst_1 && iconst_1 = 1
main_Load_228(i1, i4, i70, i71, env, static) -{0,0}> main_Load_352(i1, i4, i70, i71, env, static) :|: i71 <= 3 && i71 <= 2 && 1 <= i71
main_Load_352(i1, i4, i132, i133, env, static) -{0,0}> main_Load_435(i1, i4, i132, i133, env, static) :|: 1 <= i133 && i133 <= 3

obtained
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
by chaining
main_Load_435(i1, i4, i186, i187, env, static) -{1,1}> main_ConstantStackPush_437(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_ConstantStackPush_437(i1, i4, i186, i187, env, static) -{1,1}> main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1
main_IntArithmetic_444(i1, i4, iconst_1, i186, i187, env, static) -{1,1}> main_Load_448(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187 && iconst_1 = 1 && i1 - iconst_1 = i198
main_Load_448(i1, i4, i198, i186, i187, env, static) -{1,1}> main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) :|: 1 <= i187
main_InvokeMethod_450(i1, i4, i198, i186, i187, env, static) -{1,1}> min_Load_451(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_451(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_452(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Load_452(i198, i186, i1, i4, i187, env, static) -{1,1}> min_GE_477(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187

obtained
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
by chaining
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_489(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_GE_489(i198, i186, i1, i4, i187, env, static) -{1,1}> min_Load_493(i186, i1, i4, i187, env, static) :|: 1 <= i187 && i186 <= i198
min_Load_493(i186, i1, i4, i187, env, static) -{1,1}> min_Return_501(i186, i1, i4, i187, env, static) :|: 1 <= i187
min_Return_501(i186, i1, i4, i187, env, static) -{1,1}> main_Load_507(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_Load_507(i1, i4, i186, i187, env, static) -{1,1}> main_NE_521(i1, i4, i186, i187, env, static) :|: 1 <= i187
main_NE_521(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_571(i1, i4, i186, i187, env, static) :|: 1 <= i187 && i186 = i186
main_Inc_571(i1, i4, i186, i187, env, static) -{1,1}> main_Inc_575(i1, i4, i241, i187, env, static) :|: i186 + 1 = i241 && 1 <= i187
main_Inc_575(i1, i4, i241, i187, env, static) -{1,1}> main_JMP_584(i1, i4, i241, i243, env, static) :|: 1 <= i187 && i187 + 1 = i243 && 2 <= i243
main_JMP_584(i1, i4, i241, i243, env, static) -{1,1}> main_Load_590(i1, i4, i241, i243, env, static) :|: 2 <= i243
main_Load_590(i1, i4, i241, i243, env, static) -{0,0}> main_Load_435(i1, i4, i241, i243, env, static) :|: 1 <= i243 && 2 <= i243

(32) 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(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_69(i6, i4, i1, 0, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'

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

Moved arithmethic from lhss to constraints.

min_GE_69(i6, i4, i1, 0, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2
was transformed to
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0

(34) 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:
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186

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

Moved arithmethic from constraints to rhss.

min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, iconst_0, env, static) :|: iconst_0 = 0 && i6 < i4
was transformed to
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, 0, env, static) :|: iconst_0 = 0 && i6 < i4

min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i13', 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
was transformed to
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0

main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i198', i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
was transformed to
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i1 - 1, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'

main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i6', i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2

min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i241', i243', env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
was transformed to
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i186 + 1, i187 + 1, env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'

(36) 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:
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, 0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
main_Load_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i1 - 1, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i186 + 1, i187 + 1, env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'

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

Simplified expressions.

min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && 1 <= 1 && 1 <= 3 && i4 <= i6 && 1 <= 2 && x = 0
was transformed to
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && i4 <= i6 && x = 0

main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= 2 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

(38) 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_435(i1, i4, i186, i187, env, static) -{7,7}> min_GE_477(i1 - 1, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i1 - 1 = i198'
min_GE_69(i6, i4, i1, x, env, static) -{8,8}> main_Load_435(i1, i4, i4 + 1, 1, env, static) :|: i4 + 1 = i13' && i4 <= i6 && x = 0
min_GE_69(i6, i4, i1, iconst_0, env, static) -{0,0}> min_GE_78(i6, i4, i1, 0, env, static) :|: iconst_0 = 0 && i6 < i4
min_GE_477(i198, i186, i1, i4, i187, env, static) -{8,8}> main_Load_435(i1, i4, i186 + 1, i187 + 1, env, static) :|: i186 + 1 = i241' && 1 <= i243' && 2 <= i243' && 1 <= i187 && i186 <= i198 && i187 + 1 = i243'
main_ConstantStackPush_2(i1, i4, env, static) -{24,24}> min_GE_69(i1 - 1, i4, i1, 0, env, static'1) :|: static'1 <= static''' + 1 && i1 - 1 = i6' && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
min_GE_477(i198, i186, i1, i4, i187, env, static) -{0,0}> min_GE_490(i198, i186, i1, i4, i187, env, static) :|: 1 <= i187 && i198 < i186