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

(0) Obligation:

Need to prove time_complexity of the following program:

public class IntRTA {
  // only wrap a primitive int
  private int val;

  // count up to the value
  // in "limit"
  public static void count(
      IntRTA orig, IntRTA limit) {

    if (orig == null
        || limit == null) {
      return;
    }

    // introduce sharing
    IntRTA copy = orig;

    while (orig.val < limit.val) {
      copy.val++;
    }
  }

    public static void main(int i, int j) {
    IntRTA x = new IntRTA();
    x.val = i;
    IntRTA y = new IntRTA();
    y.val = j;
    count(x, y);
  }
}

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

Constructed TerminationGraph.

(2) Obligation:

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

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

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

(4) Obligation:

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

• Used field analysis yielded the following read fields:
  
  • IntRTA: [val]

Considered paths: all paths from start

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

Transformed 67 jbc graph edges to a weighted ITS with 70 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 70 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, i3, env, static) -{0,0}> main_New_4(i2, i3, env, static) :|: 0 >= 0
main_New_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_47(i2, i3, env, static) :|: 0 >= 0
main_New_47(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 <= static
main_New_48(i2, i3, env, static) -{0,0}> main_New_49(i2, i3, env, static) :|: 0 >= 0
main_New_49(i2, i3, env, static) -{0,0}> main_New_50(i2, i3, env, static) :|: 0 >= 0
main_New_50(i2, i3, env, static) -{1,1}> main_Duplicate_51(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_51(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Store_58(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_58(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_62(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_62(i2, i3, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4, env, static) -{1,1}> main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && o6 = 1
main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Store_85(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Store_85(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_87(i2, i3, o4, o6, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_87(i2, i3, o4, o6, iconst_0, env, static) -{1,1}> main_Load_88(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_88(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{1,1}> main_Load_95(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_Load_95(i2, i3, o4, o6, env, static) -{1,1}> main_InvokeMethod_97(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_InvokeMethod_97(i2, i3, o4, o6, env, static) -{1,1}> count_Load_98(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_98(o4, o6, i2, i3, env, static) -{1,1}> count_NULL_101(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NULL_101(o4, o6, i2, i3, env, static) -{1,1}> count_Load_103(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_103(o4, o6, i2, i3, env, static) -{1,1}> count_NONNULL_106(o6, o4, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NONNULL_106(o6, o4, i2, i3, env, static) -{1,1}> count_Load_108(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_108(o4, o6, i2, i3, env, static) -{1,1}> count_Store_109(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Store_109(o4, o6, i2, i3, env, static) -{1,1}> count_Load_110(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_110(o4, o6, i2, i3, env, static) -{0,0}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Load_147(i8, o14, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_Load_147(i8, o14, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) -{1,1}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_166(i8, i3, o14, o15, i2, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_GE_166(i8, i3, o14, o15, i2, env, static) -{1,1}> count_Load_170(o14, o15, i2, i3, i8, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_Load_170(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Duplicate_172(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_Duplicate_172(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) -{1,1}> count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) -{1,1}> count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) :|: iconst_1 = 1 && 0 < o15 && 0 < o14
count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) :|: i8 + iconst_1 = i12 && iconst_1 = 1 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_182(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
count_Load_182(o14, o15, i2, i3, i12, env, static) -{0,0}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

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

obtained
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
main_New_2(i2, i3, env, static) -{0,0}> main_New_4(i2, i3, env, static) :|: 0 >= 0
main_New_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_47(i2, i3, env, static) :|: 0 >= 0
main_New_47(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 <= static
main_New_48(i2, i3, env, static) -{0,0}> main_New_49(i2, i3, env, static) :|: 0 >= 0
main_New_49(i2, i3, env, static) -{0,0}> main_New_50(i2, i3, env, static) :|: 0 >= 0
main_New_50(i2, i3, env, static) -{1,1}> main_Duplicate_51(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_51(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Store_58(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_58(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_62(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_62(i2, i3, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0

obtained
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
by chaining
main_New_68(i2, i3, o4, env, static) -{1,1}> main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && o6 = 1
main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Store_85(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Store_85(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_87(i2, i3, o4, o6, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_87(i2, i3, o4, o6, iconst_0, env, static) -{1,1}> main_Load_88(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_88(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0

obtained
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
by chaining
main_Load_92(i2, i3, o4, o6, env, static) -{1,1}> main_Load_95(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_Load_95(i2, i3, o4, o6, env, static) -{1,1}> main_InvokeMethod_97(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_InvokeMethod_97(i2, i3, o4, o6, env, static) -{1,1}> count_Load_98(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_98(o4, o6, i2, i3, env, static) -{1,1}> count_NULL_101(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NULL_101(o4, o6, i2, i3, env, static) -{1,1}> count_Load_103(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_103(o4, o6, i2, i3, env, static) -{1,1}> count_NONNULL_106(o6, o4, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NONNULL_106(o6, o4, i2, i3, env, static) -{1,1}> count_Load_108(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_108(o4, o6, i2, i3, env, static) -{1,1}> count_Store_109(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Store_109(o4, o6, i2, i3, env, static) -{1,1}> count_Load_110(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_110(o4, o6, i2, i3, env, static) -{0,0}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4

obtained
count_Load_145(o14, o15, i2, i3, i8, env, static) -{10,10}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
by chaining
count_Load_145(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Load_147(i8, o14, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_Load_147(i8, o14, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) -{1,1}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_166(i8, i3, o14, o15, i2, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_GE_166(i8, i3, o14, o15, i2, env, static) -{1,1}> count_Load_170(o14, o15, i2, i3, i8, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_Load_170(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Duplicate_172(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_Duplicate_172(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) -{1,1}> count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) -{1,1}> count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) :|: iconst_1 = 1 && 0 < o15 && 0 < o14
count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) :|: i8 + iconst_1 = i12 && iconst_1 = 1 && 0 < o15 && 0 < o14

obtained
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
by chaining
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_182(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
count_Load_182(o14, o15, i2, i3, i12, env, static) -{0,0}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

(8) Obligation:

IntTrs with 11 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i2, i3, i8, env, static) -{10,10}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

(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_New_2(x1, x2, x3, x4) → main_New_2(x1, x2, x4)
main_FieldAccess_66(x1, x2, x3, x4, x5, x6) → main_FieldAccess_66(x1, x2, x3, x4)
main_New_68(x1, x2, x3, x4, x5) → main_New_68(x1, x2, x3)
main_FieldAccess_91(x1, x2, x3, x4, x5, x6, x7) → main_FieldAccess_91(x1, x2, x3, x4, x5)
main_Load_92(x1, x2, x3, x4, x5, x6) → main_Load_92(x1, x2, x3, x4)
count_Load_145(x1, x2, x3, x4, x5, x6, x7) → count_Load_145(x1, x2, x4, x5)
count_FieldAccess_177(x1, x2, x3, x4, x5, x6, x7, x8) → count_FieldAccess_177(x1, x2, x3, x5)
count_JMP_178(x1, x2, x3, x4, x5, x6, x7) → count_JMP_178(x1, x2, x4, x5)

(10) Obligation:

IntTrs with 11 rules
Start term: main_New_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_New_2(i2, i3, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_FieldAccess_66(i2, i3, o4, iconst_0) -{1,1}> main_New_68(i2, i3, o4') :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0) -{1,1}> main_New_68(i2, i3, o4') :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0) :|: 0 < 1 && 0 < o4
main_FieldAccess_91(i2, i3, o6, o4, iconst_0) -{1,1}> main_Load_92(i2, i3, o4, o6') :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0) -{1,1}> main_Load_92(i2, i3, o4, o6') :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6) -{9,9}> count_Load_145(o4, o6, i3, i2) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i3, i8) -{10,10}> count_FieldAccess_177(o14, i12', o15, i3) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_FieldAccess_177(o14, i12, o15, i3) -{1,1}> count_JMP_178(o14', o15, i3, i12) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i3) -{1,1}> count_JMP_178(o14', o15, i3, i12) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i3, i12) -{1,1}> count_Load_145(o14, o15, i3, i12) :|: 0 < o15 && 0 < o14

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

Moved arithmethic from constraints to rhss.

count_Load_145(o14, o15, i3, i8) -{10,10}> count_FieldAccess_177(o14, i12', o15, i3) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
was transformed to
count_Load_145(o14, o15, i3, i8) -{10,10}> count_FieldAccess_177(o14, i8 + 1, o15, i3) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'

(12) Obligation:

IntTrs with 11 rules
Start term: main_New_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_FieldAccess_91(i2, i3, o6, o4, iconst_0) -{1,1}> main_Load_92(i2, i3, o4, o6') :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6) -{9,9}> count_Load_145(o4, o6, i3, i2) :|: 0 < o6 && 0 < o4
main_New_2(i2, i3, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_New_68(i2, i3, o4) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0) :|: 0 < 1 && 0 < o4
main_FieldAccess_66(i2, i3, o4, iconst_0) -{1,1}> main_New_68(i2, i3, o4') :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0) -{1,1}> main_Load_92(i2, i3, o4, o6') :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_66(i2, i3, o4, iconst_0) -{1,1}> main_New_68(i2, i3, o4') :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
count_FieldAccess_177(o14, i12, o15, i3) -{1,1}> count_JMP_178(o14', o15, i3, i12) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_Load_145(o14, o15, i3, i8) -{10,10}> count_FieldAccess_177(o14, i8 + 1, o15, i3) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_JMP_178(o14, o15, i3, i12) -{1,1}> count_Load_145(o14, o15, i3, i12) :|: 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i3) -{1,1}> count_JMP_178(o14', o15, i3, i12) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12

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

Simplified expressions.

main_New_2(i2, i3, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
main_New_2(i2, i3, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

main_New_68(i2, i3, o4) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0) :|: 0 < 1 && 0 < o4
was transformed to
main_New_68(i2, i3, o4) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0) :|: 0 < o4

(14) Obligation:

IntTrs with 11 rules
Start term: main_New_2(#0, #1, static)
Considered paths: all paths from start
Rules:
main_FieldAccess_91(i2, i3, o6, o4, iconst_0) -{1,1}> main_Load_92(i2, i3, o4, o6') :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_New_68(i2, i3, o4) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0) :|: 0 < o4
main_Load_92(i2, i3, o4, o6) -{9,9}> count_Load_145(o4, o6, i3, i2) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i3, i8) -{10,10}> count_FieldAccess_177(o14, i8 + 1, o15, i3) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
main_New_2(i2, i3, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_FieldAccess_66(i2, i3, o4, iconst_0) -{1,1}> main_New_68(i2, i3, o4') :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0) -{1,1}> main_New_68(i2, i3, o4') :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0) -{1,1}> main_Load_92(i2, i3, o4, o6') :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
count_FieldAccess_177(o14, i12, o15, i3) -{1,1}> count_JMP_178(o14', o15, i3, i12) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i3, i12) -{1,1}> count_Load_145(o14, o15, i3, i12) :|: 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i3) -{1,1}> count_JMP_178(o14', o15, i3, i12) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12

(15) koat Proof (EQUIVALENT transformation)

YES(?, 14*ar_0 + 14*ar_1 + 84)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 - ar_1 /\ 0 < ar_2 /\ ar_1 <= 0 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: ?, Cost: 9) main_New_68(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_91(ar_0, ar_1, 1, ar_2, 0)) [ 0 < ar_2 ]
(Comp: ?, Cost: 9) main_Load_92(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_2, ar_3, ar_1, ar_0, arityPad)) [ 0 < ar_3 /\ 0 < ar_2 ]
(Comp: ?, Cost: 10) count_Load_145(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_FieldAccess_177(ar_0, ar_3 + 1, ar_1, ar_2, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 /\ ar_3 < ar_2 /\ ar_3 + 1 = i12' ]
(Comp: ?, Cost: 24) main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_66(ar_0, ar_1, 1, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ ar_0 <= 0 /\ o4' <= ar_2 - ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: ?, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ o4' <= ar_2 + ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < ar_0 /\ 0 < o4' ]
(Comp: ?, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 + ar_1 /\ 0 < ar_1 /\ 0 < ar_2 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: ?, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ o14' <= ar_0 - ar_1 /\ 0 < o14' /\ ar_1 <= 0 /\ 0 < ar_2 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) count_JMP_178(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ 0 < ar_1 /\ 0 < o14' /\ 0 < ar_2 /\ 0 < ar_0 /\ o14' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 2, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 - ar_1 /\ 0 < ar_2 /\ ar_1 <= 0 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: 2, Cost: 9) main_New_68(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_91(ar_0, ar_1, 1, ar_2, 0)) [ 0 < ar_2 ]
(Comp: 4, Cost: 9) main_Load_92(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_2, ar_3, ar_1, ar_0, arityPad)) [ 0 < ar_3 /\ 0 < ar_2 ]
(Comp: ?, Cost: 10) count_Load_145(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_FieldAccess_177(ar_0, ar_3 + 1, ar_1, ar_2, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 /\ ar_3 < ar_2 /\ ar_3 + 1 = i12' ]
(Comp: 1, Cost: 24) main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_66(ar_0, ar_1, 1, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ ar_0 <= 0 /\ o4' <= ar_2 - ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: 1, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ o4' <= ar_2 + ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < ar_0 /\ 0 < o4' ]
(Comp: 2, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 + ar_1 /\ 0 < ar_1 /\ 0 < ar_2 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: ?, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ o14' <= ar_0 - ar_1 /\ 0 < o14' /\ ar_1 <= 0 /\ 0 < ar_2 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) count_JMP_178(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ 0 < ar_1 /\ 0 < o14' /\ 0 < ar_2 /\ 0 < ar_0 /\ o14' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(main_FieldAccess_91) = -V_1 + V_2
Pol(main_Load_92) = -V_1 + V_2
Pol(main_New_68) = -V_1 + V_2
Pol(count_Load_145) = V_3 - V_4
Pol(count_FieldAccess_177) = -V_2 + V_4
Pol(main_New_2) = -V_1 + V_2
Pol(main_FieldAccess_66) = -V_1 + V_2
Pol(count_JMP_178) = V_3 - V_4
Pol(koat_start) = -V_1 + V_2
orients all transitions weakly and the transition
count_Load_145(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_FieldAccess_177(ar_0, ar_3 + 1, ar_1, ar_2, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 /\ ar_3 < ar_2 /\ ar_3 + 1 = i12' ]
strictly and produces the following problem:
3: T:
(Comp: 2, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 - ar_1 /\ 0 < ar_2 /\ ar_1 <= 0 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: 2, Cost: 9) main_New_68(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_91(ar_0, ar_1, 1, ar_2, 0)) [ 0 < ar_2 ]
(Comp: 4, Cost: 9) main_Load_92(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_2, ar_3, ar_1, ar_0, arityPad)) [ 0 < ar_3 /\ 0 < ar_2 ]
(Comp: ar_0 + ar_1, Cost: 10) count_Load_145(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_FieldAccess_177(ar_0, ar_3 + 1, ar_1, ar_2, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 /\ ar_3 < ar_2 /\ ar_3 + 1 = i12' ]
(Comp: 1, Cost: 24) main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_66(ar_0, ar_1, 1, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ ar_0 <= 0 /\ o4' <= ar_2 - ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: 1, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ o4' <= ar_2 + ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < ar_0 /\ 0 < o4' ]
(Comp: 2, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 + ar_1 /\ 0 < ar_1 /\ 0 < ar_2 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: ?, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ o14' <= ar_0 - ar_1 /\ 0 < o14' /\ ar_1 <= 0 /\ 0 < ar_2 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) count_JMP_178(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ 0 < ar_1 /\ 0 < o14' /\ 0 < ar_2 /\ 0 < ar_0 /\ o14' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 3 produces the following problem:
4: T:
(Comp: 2, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 - ar_1 /\ 0 < ar_2 /\ ar_1 <= 0 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: 2, Cost: 9) main_New_68(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_91(ar_0, ar_1, 1, ar_2, 0)) [ 0 < ar_2 ]
(Comp: 4, Cost: 9) main_Load_92(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_2, ar_3, ar_1, ar_0, arityPad)) [ 0 < ar_3 /\ 0 < ar_2 ]
(Comp: ar_0 + ar_1, Cost: 10) count_Load_145(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_FieldAccess_177(ar_0, ar_3 + 1, ar_1, ar_2, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 /\ ar_3 < ar_2 /\ ar_3 + 1 = i12' ]
(Comp: 1, Cost: 24) main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_FieldAccess_66(ar_0, ar_1, 1, 0, arityPad)) [ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ ar_0 <= 0 /\ o4' <= ar_2 - ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < o4' ]
(Comp: 1, Cost: 1) main_FieldAccess_66(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_68(ar_0, ar_1, o4', arityPad, arityPad)) [ o4' <= ar_2 + ar_0 /\ 0 < ar_2 /\ ar_3 = 0 /\ 0 < ar_0 /\ 0 < o4' ]
(Comp: 2, Cost: 1) main_FieldAccess_91(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_Load_92(ar_0, ar_1, ar_3, o6', arityPad)) [ o6' <= ar_2 + ar_1 /\ 0 < ar_1 /\ 0 < ar_2 /\ 0 < ar_3 /\ ar_4 = 0 /\ 0 < o6' ]
(Comp: ar_0 + ar_1, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ o14' <= ar_0 - ar_1 /\ 0 < o14' /\ ar_1 <= 0 /\ 0 < ar_2 /\ 0 < ar_0 ]
(Comp: 2*ar_0 + 2*ar_1, Cost: 1) count_JMP_178(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_Load_145(ar_0, ar_1, ar_2, ar_3, arityPad)) [ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: ar_0 + ar_1, Cost: 1) count_FieldAccess_177(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(count_JMP_178(o14', ar_2, ar_3, ar_1, arityPad)) [ 0 < ar_1 /\ 0 < o14' /\ 0 < ar_2 /\ 0 < ar_0 /\ o14' <= ar_0 + ar_1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(main_New_2(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 14*ar_0 + 14*ar_1 + 84

Time: 0.453 sec (SMT: 0.396 sec)

(16) BOUNDS(CONSTANT, 84 + 14 * |#0| + 14 * |#1|)

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

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

(18) Obligation:

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

• Used field analysis yielded the following read fields:
  
  • IntRTA: [val]

Considered paths: nonterm paths and paths from start to sinks

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

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

(20) Obligation:

IntTrs with 71 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, i3, env, static) -{0,0}> main_New_4(i2, i3, env, static) :|: 0 >= 0
main_New_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_47(i2, i3, env, static) :|: 0 >= 0
main_New_47(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 <= static
main_New_48(i2, i3, env, static) -{0,0}> main_New_49(i2, i3, env, static) :|: 0 >= 0
main_New_49(i2, i3, env, static) -{0,0}> main_New_50(i2, i3, env, static) :|: 0 >= 0
main_New_50(i2, i3, env, static) -{1,1}> main_Duplicate_51(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_51(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Store_58(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_58(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_62(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_62(i2, i3, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4, env, static) -{1,1}> main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && o6 = 1
main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Store_85(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Store_85(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_87(i2, i3, o4, o6, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_87(i2, i3, o4, o6, iconst_0, env, static) -{1,1}> main_Load_88(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_88(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{1,1}> main_Load_95(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_Load_95(i2, i3, o4, o6, env, static) -{1,1}> main_InvokeMethod_97(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_InvokeMethod_97(i2, i3, o4, o6, env, static) -{1,1}> count_Load_98(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_98(o4, o6, i2, i3, env, static) -{1,1}> count_NULL_101(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NULL_101(o4, o6, i2, i3, env, static) -{1,1}> count_Load_103(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_103(o4, o6, i2, i3, env, static) -{1,1}> count_NONNULL_106(o6, o4, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NONNULL_106(o6, o4, i2, i3, env, static) -{1,1}> count_Load_108(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_108(o4, o6, i2, i3, env, static) -{1,1}> count_Store_109(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Store_109(o4, o6, i2, i3, env, static) -{1,1}> count_Load_110(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_110(o4, o6, i2, i3, env, static) -{0,0}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Load_147(i8, o14, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_Load_147(i8, o14, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) -{1,1}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_166(i8, i3, o14, o15, i2, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_GE_166(i8, i3, o14, o15, i2, env, static) -{1,1}> count_Load_170(o14, o15, i2, i3, i8, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_Load_170(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Duplicate_172(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_Duplicate_172(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) -{1,1}> count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) -{1,1}> count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) :|: iconst_1 = 1 && 0 < o15 && 0 < o14
count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) :|: i8 + iconst_1 = i12 && iconst_1 = 1 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_182(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
count_Load_182(o14, o15, i2, i3, i12, env, static) -{0,0}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

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

obtained
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
main_New_2(i2, i3, env, static) -{0,0}> main_New_4(i2, i3, env, static) :|: 0 >= 0
main_New_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_47(i2, i3, env, static) :|: 0 >= 0
main_New_47(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 <= static
main_New_48(i2, i3, env, static) -{0,0}> main_New_49(i2, i3, env, static) :|: 0 >= 0
main_New_49(i2, i3, env, static) -{0,0}> main_New_50(i2, i3, env, static) :|: 0 >= 0
main_New_50(i2, i3, env, static) -{1,1}> main_Duplicate_51(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_51(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Store_58(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_58(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_62(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_62(i2, i3, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0

obtained
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
by chaining
main_New_68(i2, i3, o4, env, static) -{1,1}> main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && o6 = 1
main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Store_85(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Store_85(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_87(i2, i3, o4, o6, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_87(i2, i3, o4, o6, iconst_0, env, static) -{1,1}> main_Load_88(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_88(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0

obtained
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
by chaining
main_Load_92(i2, i3, o4, o6, env, static) -{1,1}> main_Load_95(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_Load_95(i2, i3, o4, o6, env, static) -{1,1}> main_InvokeMethod_97(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_InvokeMethod_97(i2, i3, o4, o6, env, static) -{1,1}> count_Load_98(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_98(o4, o6, i2, i3, env, static) -{1,1}> count_NULL_101(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NULL_101(o4, o6, i2, i3, env, static) -{1,1}> count_Load_103(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_103(o4, o6, i2, i3, env, static) -{1,1}> count_NONNULL_106(o6, o4, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NONNULL_106(o6, o4, i2, i3, env, static) -{1,1}> count_Load_108(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_108(o4, o6, i2, i3, env, static) -{1,1}> count_Store_109(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Store_109(o4, o6, i2, i3, env, static) -{1,1}> count_Load_110(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_110(o4, o6, i2, i3, env, static) -{0,0}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4

obtained
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
by chaining
count_Load_145(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Load_147(i8, o14, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_Load_147(i8, o14, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) -{1,1}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14

obtained
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
by chaining
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_166(i8, i3, o14, o15, i2, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_GE_166(i8, i3, o14, o15, i2, env, static) -{1,1}> count_Load_170(o14, o15, i2, i3, i8, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_Load_170(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Duplicate_172(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_Duplicate_172(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) -{1,1}> count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) -{1,1}> count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) :|: iconst_1 = 1 && 0 < o15 && 0 < o14
count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) :|: i8 + iconst_1 = i12 && iconst_1 = 1 && 0 < o15 && 0 < o14

obtained
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
by chaining
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_182(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
count_Load_182(o14, o15, i2, i3, i12, env, static) -{0,0}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

(22) Obligation:

IntTrs with 13 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

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

Moved arithmethic from constraints to rhss.

count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
was transformed to
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i8 + 1, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'

(24) Obligation:

IntTrs with 13 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i8 + 1, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14

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

Simplified expressions.

main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
was transformed to
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < o4

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

(26) Obligation:

IntTrs with 13 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < o4
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i8 + 1, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'

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

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

(28) Obligation:

IntTrs with 71 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, i3, env, static) -{0,0}> main_New_4(i2, i3, env, static) :|: 0 >= 0
main_New_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_47(i2, i3, env, static) :|: 0 >= 0
main_New_47(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 <= static
main_New_48(i2, i3, env, static) -{0,0}> main_New_49(i2, i3, env, static) :|: 0 >= 0
main_New_49(i2, i3, env, static) -{0,0}> main_New_50(i2, i3, env, static) :|: 0 >= 0
main_New_50(i2, i3, env, static) -{1,1}> main_Duplicate_51(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_51(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Store_58(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_58(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_62(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_62(i2, i3, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4, env, static) -{1,1}> main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && o6 = 1
main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Store_85(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Store_85(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_87(i2, i3, o4, o6, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_87(i2, i3, o4, o6, iconst_0, env, static) -{1,1}> main_Load_88(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_88(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{1,1}> main_Load_95(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_Load_95(i2, i3, o4, o6, env, static) -{1,1}> main_InvokeMethod_97(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_InvokeMethod_97(i2, i3, o4, o6, env, static) -{1,1}> count_Load_98(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_98(o4, o6, i2, i3, env, static) -{1,1}> count_NULL_101(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NULL_101(o4, o6, i2, i3, env, static) -{1,1}> count_Load_103(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_103(o4, o6, i2, i3, env, static) -{1,1}> count_NONNULL_106(o6, o4, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NONNULL_106(o6, o4, i2, i3, env, static) -{1,1}> count_Load_108(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_108(o4, o6, i2, i3, env, static) -{1,1}> count_Store_109(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Store_109(o4, o6, i2, i3, env, static) -{1,1}> count_Load_110(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_110(o4, o6, i2, i3, env, static) -{0,0}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Load_147(i8, o14, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_Load_147(i8, o14, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) -{1,1}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_166(i8, i3, o14, o15, i2, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_GE_166(i8, i3, o14, o15, i2, env, static) -{1,1}> count_Load_170(o14, o15, i2, i3, i8, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_Load_170(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Duplicate_172(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_Duplicate_172(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) -{1,1}> count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) -{1,1}> count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) :|: iconst_1 = 1 && 0 < o15 && 0 < o14
count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) :|: i8 + iconst_1 = i12 && iconst_1 = 1 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_182(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
count_Load_182(o14, o15, i2, i3, i12, env, static) -{0,0}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

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

obtained
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
main_New_2(i2, i3, env, static) -{0,0}> main_New_4(i2, i3, env, static) :|: 0 >= 0
main_New_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> main_New_46(i2, i3, env, static) :|: 0 >= 0
main_New_46(i2, i3, env, static) -{0,0}> main_New_47(i2, i3, env, static) :|: 0 >= 0
main_New_47(i2, i3, env, static) -{0,0}> main_New_48(i2, i3, env, static) :|: 0 <= static
main_New_48(i2, i3, env, static) -{0,0}> main_New_49(i2, i3, env, static) :|: 0 >= 0
main_New_49(i2, i3, env, static) -{0,0}> main_New_50(i2, i3, env, static) :|: 0 >= 0
main_New_50(i2, i3, env, static) -{1,1}> main_Duplicate_51(i2, i3, o4, iconst_0, env, static) :|: o4 = 1 && 0 < o4 && iconst_0 = 0
main_Duplicate_51(i2, i3, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_InvokeMethod_52(i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_53(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_54(o4, i2, i3, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_55(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Store_58(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Store_58(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_60(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_60(i2, i3, o4, iconst_0, env, static) -{1,1}> main_Load_62(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0
main_Load_62(i2, i3, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) :|: 0 < o4 && iconst_0 = 0

obtained
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
by chaining
main_New_68(i2, i3, o4, env, static) -{1,1}> main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0 && o6 = 1
main_Duplicate_70(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_InvokeMethod_71(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Load_72(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_InvokeMethod_80(o6, i2, i3, o4, iconst_0, env, static) -{1,1}> langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
langle_init_rangle_Return_82(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Store_85(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Store_85(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_87(i2, i3, o4, o6, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_87(i2, i3, o4, o6, iconst_0, env, static) -{1,1}> main_Load_88(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0
main_Load_88(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) :|: 0 < o6 && 0 < o4 && iconst_0 = 0

obtained
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
by chaining
main_Load_92(i2, i3, o4, o6, env, static) -{1,1}> main_Load_95(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_Load_95(i2, i3, o4, o6, env, static) -{1,1}> main_InvokeMethod_97(i2, i3, o4, o6, env, static) :|: 0 < o6 && 0 < o4
main_InvokeMethod_97(i2, i3, o4, o6, env, static) -{1,1}> count_Load_98(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_98(o4, o6, i2, i3, env, static) -{1,1}> count_NULL_101(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NULL_101(o4, o6, i2, i3, env, static) -{1,1}> count_Load_103(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_103(o4, o6, i2, i3, env, static) -{1,1}> count_NONNULL_106(o6, o4, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_NONNULL_106(o6, o4, i2, i3, env, static) -{1,1}> count_Load_108(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_108(o4, o6, i2, i3, env, static) -{1,1}> count_Store_109(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Store_109(o4, o6, i2, i3, env, static) -{1,1}> count_Load_110(o4, o6, i2, i3, env, static) :|: 0 < o6 && 0 < o4
count_Load_110(o4, o6, i2, i3, env, static) -{0,0}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4

obtained
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
by chaining
count_Load_145(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_146(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Load_147(i8, o14, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_Load_147(i8, o14, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_148(i8, o15, o14, i2, i3, env, static) -{1,1}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14

obtained
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
by chaining
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_166(i8, i3, o14, o15, i2, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_GE_166(i8, i3, o14, o15, i2, env, static) -{1,1}> count_Load_170(o14, o15, i2, i3, i8, env, static) :|: i8 < i3 && 0 < o15 && 0 < o14
count_Load_170(o14, o15, i2, i3, i8, env, static) -{1,1}> count_Duplicate_172(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_Duplicate_172(o14, o15, i2, i3, i8, env, static) -{1,1}> count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_174(o14, o15, i2, i3, i8, env, static) -{1,1}> count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) :|: 0 < o15 && 0 < o14
count_ConstantStackPush_175(o14, i8, o15, i2, i3, env, static) -{1,1}> count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) :|: iconst_1 = 1 && 0 < o15 && 0 < o14
count_IntArithmetic_176(o14, i8, iconst_1, o15, i2, i3, env, static) -{1,1}> count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) :|: i8 + iconst_1 = i12 && iconst_1 = 1 && 0 < o15 && 0 < o14

obtained
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
by chaining
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_182(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
count_Load_182(o14, o15, i2, i3, i12, env, static) -{0,0}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

(30) Obligation:

IntTrs with 13 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14

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

Moved arithmethic from constraints to rhss.

count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i12', o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
was transformed to
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i8 + 1, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'

(32) Obligation:

IntTrs with 13 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i8 + 1, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: 0 <= 2 && 0 < 1 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14

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

Simplified expressions.

main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < 1 && 0 < o4
was transformed to
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < o4

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

(34) Obligation:

IntTrs with 13 rules
Start term: main_New_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
count_Load_145(o14, o15, i2, i3, i8, env, static) -{4,4}> count_GE_156(i8, i3, o14, o15, i2, env, static) :|: 0 < o15 && 0 < o14
count_JMP_178(o14, o15, i2, i3, i12, env, static) -{1,1}> count_Load_145(o14, o15, i2, i3, i12, env, static) :|: 0 < o15 && 0 < o14
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: i2 <= 0 && o4' <= o4 + -1 * i2 && 0 < o4 && iconst_0 = 0 && 0 < o4'
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + i3 && 0 < i3 && 0 < o6 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_New_2(i2, i3, env, static) -{24,24}> main_FieldAccess_66(i2, i3, 1, 0, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
main_FieldAccess_66(i2, i3, o4, iconst_0, env, static) -{1,1}> main_New_68(i2, i3, o4', env, static) :|: o4' <= o4 + i2 && 0 < o4 && iconst_0 = 0 && 0 < i2 && 0 < o4'
count_GE_156(i8, i3, o14, o15, i2, env, static) -{0,0}> count_GE_164(i8, i3, o14, o15, i2, env, static) :|: i3 <= i8 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: o14' <= o14 + -1 * i12 && 0 < o14' && i12 <= 0 && 0 < o15 && 0 < o14
count_FieldAccess_177(o14, i12, o15, i2, i3, i8, env, static) -{1,1}> count_JMP_178(o14', o15, i2, i3, i12, env, static) :|: 0 < i12 && 0 < o14' && 0 < o15 && 0 < o14 && o14' <= o14 + i12
main_FieldAccess_91(i2, i3, o6, o4, iconst_0, env, static) -{1,1}> main_Load_92(i2, i3, o4, o6', env, static) :|: o6' <= o6 + -1 * i3 && 0 < o6 && i3 <= 0 && 0 < o4 && iconst_0 = 0 && 0 < o6'
main_Load_92(i2, i3, o4, o6, env, static) -{9,9}> count_Load_145(o4, o6, i2, i3, i2, env, static) :|: 0 < o6 && 0 < o4
main_New_68(i2, i3, o4, env, static) -{9,9}> main_FieldAccess_91(i2, i3, 1, o4, 0, env, static) :|: 0 < o4
count_GE_156(i8, i3, o14, o15, i2, env, static) -{6,6}> count_FieldAccess_177(o14, i8 + 1, o15, i2, i3, i8, env, static) :|: 0 < o15 && 0 < o14 && i8 < i3 && i8 + 1 = i12'