(0) Obligation:

Need to prove time_complexity of the following program:
public class AG313 {
  public static void main(String[] args) {
    int x, y;
    x = args[0].length();
    y = args[1].length() + 1;
    quot(x,y);

  }


  public static int quot(int x, int y) {
    int i = 0;
    if(x==0) return 0;
    while (x > 0 && y > 0) {
      i += 1;
      x = (x - 1)- (y - 1);

    }
    return i;
  }
}


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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
AG313.main([Ljava/lang/String;)V: Graph of 171 nodes with 1 SCC.


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

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

(4) Obligation:

Set of 73 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: nonterm paths and paths from start to sinks

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

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

(6) Obligation:

IntTrs with 73 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114

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

obtained
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5

obtained
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
by chaining
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6

obtained
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
by chaining
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8

obtained
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
by chaining
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6

obtained
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
by chaining
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8

obtained
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
by chaining
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95

obtained
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
by chaining
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114

(8) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

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

Moved arithmethic from lhss to constraints.

main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0

quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0

main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1

(10) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1

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

Linearized lhss.

main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

(12) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

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

Moved arithmethic from constraints to rhss.

main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
was transformed to
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6

quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
was transformed to
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8

main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23

(14) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23

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

Simplified expressions.

main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1

main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
was transformed to
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12

main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0

quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0

main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23

main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1

quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

(16) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0

(17) CESProof (EQUIVALENT transformation)

proved upper bound 21 + 14 * args using cofloco

(18) BOUNDS(CONSTANT, 21 + 14 * args)

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

Transformed 73 jbc graph edges to a weighted ITS with 73 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 73 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114

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

obtained
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
by chaining
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5

obtained
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
by chaining
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6

obtained
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
by chaining
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8

obtained
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
by chaining
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6

obtained
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
by chaining
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8

obtained
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
by chaining
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95

obtained
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
by chaining
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114

(22) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

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

Moved arithmethic from lhss to constraints.

main_ArrayAccess_57(a6, 0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0

quot_NE_195(i20, i16, 0, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0

main_ArrayAccess_90(a6, 1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20'
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1

(24) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1

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

Linearized lhss.

main_ArrayAccess_57(a6, iconst_0, iconst_0, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

quot_NE_195(iconst_0, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_ArrayAccess_90(a6, iconst_1, i8, iconst_1, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

(26) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

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

Moved arithmethic from constraints to rhss.

main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, iconst_1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
was transformed to
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1

quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(iconst_0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, iconst_0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
was transformed to
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0

main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, NULL, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
was transformed to
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6

quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, NULL, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
was transformed to
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8

main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i16', 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23

(28) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23

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

Simplified expressions.

main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 <= 2 && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 < 1 && 0 <= 1 && 0 <= static'1 && 0 < 2
was transformed to
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1

main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 <= o12 && 0 < a6 && 1 <= i6 && 0 < o12
was transformed to
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12

main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 0 <= i6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
was transformed to
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0

quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 0 <= i20 && 0 <= 0 && 2 <= i12 && 0 <= 2 && 1 <= i16 && 0 < i20 && 0 <= 1 && x = 0
was transformed to
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0

main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && 0 <= o23 && i15' <= o23
was transformed to
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23

main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: 1 <= i12 && o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
was transformed to
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1

quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 - 1 - i16 - 1, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' - i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

(30) Obligation:

IntTrs with 14 rules
Start term: main_Load_2(args, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
main_InvokeMethod_64(a6, o12, i6, env, static) -{4,4}> main_ArrayAccess_90(a6, 1, i8', i6, env, static) :|: i8' <= o12 && 0 <= i8' && 0 < a6 && 1 <= i6 && 0 < o12
main_ArrayAccess_90(a6, x, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20', i8, i12, env, static) :|: o20' < a6 && 0 <= i8 && 0 < a6 && 2 <= i12 && 1 < i12 && 0 <= o20' && x = 1
main_ArrayAccess_57(a6, x, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8', i6, env, static) :|: 0 < a6 && 1 <= i6 && o8' < a6 && 0 <= o8' && 0 < i6 && x = 0
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
main_ArrayAccess_57(a6, iconst_0, x, env, static) -{0,0}> main_ArrayAccess_58(a6, 0, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 0 < a6 && x = iconst_0
main_InvokeMethod_64(a6, NULL, i6, env, static) -{0,0}> main_InvokeMethod_67(a6, 0, i6, env, static) :|: NULL = 0 && 1 <= i6 && 0 <= NULL && 0 < a6
quot_LE_536(i109, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_538(i109, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && i109 <= 0 && 2 <= i12 && 1 <= i16
main_ArrayAccess_90(a6, iconst_1, i8, x, env, static) -{0,0}> main_ArrayAccess_96(a6, 1, i8, env, static) :|: 1 <= iconst_1 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && x = iconst_1
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{13,13}> quot_Load_531(i110 + -1 * i16, i16, i98 + 1, a103, i12, env, static) :|: 0 < i110 && 1 <= i114' && i16 - 1 = i119' && 0 <= i114' && 1 <= i110 && 1 <= i16 && 0 <= i116' && 0 < a103 && 2 <= i12 && i110 - 1 = i116' && i116' + -1 * i119' = i120' && 0 <= i98 && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, env, static) -{17,17}> main_ArrayAccess_57(o2, 0, i5', env, static'1) :|: static'1 <= static''' + 1 && 0 <= i5' && 0 < o2 && static''' <= static + 2 && i5' < o2 && 0 <= static''' && 0 <= static && 0 <= static'1
main_InvokeMethod_111(a6, NULL, i8, i12, env, static) -{0,0}> main_InvokeMethod_114(a6, 0, i8, i12, env, static) :|: NULL = 0 && 2 <= i12 && 0 <= NULL && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, x, a6, i12, env, static) -{1,1}> quot_Load_531(i20, i16, 0, a6, i12, env, static) :|: 1 <= i20 && 0 < a6 && 2 <= i12 && 1 <= i16 && 0 < i20 && x = 0
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{10,10}> quot_NE_195(i8, i15' + 1, 0, a6, i12, env, static) :|: i15' + 1 = i16' && 0 <= i8 && 0 < o23 && 0 < a6 && 1 <= i16' && 2 <= i12 && 0 <= i15' && i15' <= o23
quot_NE_195(iconst_0, i16, x, a6, i12, env, static) -{0,0}> quot_NE_205(0, i16, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && x = iconst_0

(31) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(94)) transformation)

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

(32) Obligation:

Set of 67 edges based on JBC Program.
Performed SCC analyses:
  • Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(34) Obligation:

IntTrs with 67 rules
Start term: main_Load_2(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114

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

obtained
main_Load_2(o2, env, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5', env, static'1) :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
by chaining
main_Load_2(o2, env, static) -{0,0}> main_Load_4(o2, env, static) :|: 0 < o2
main_Load_4(o2, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(o2, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_6(o2, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) :|: 0 < o2 && iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) :|: a2 = 2 && 0 < o2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_19(a2, o2, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_21(o2, env, static') :|: 0 <= a2 && 0 < o2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_21(o2, env, static) -{0,0}> langle_clinit_rangle_New_23(o2, env, static) :|: 0 < o2
langle_clinit_rangle_New_23(o2, env, static) -{0,0}> langle_clinit_rangle_New_24(o2, env, static) :|: 0 < o2 && 0 <= static
langle_clinit_rangle_New_24(o2, env, static) -{1,1}> langle_clinit_rangle_Duplicate_26(o4, o2, env, static) :|: o4 = 1 && 0 < o2 && 0 < o4
langle_clinit_rangle_Duplicate_26(o4, o2, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_ConstantStackPush_29(o4, o2, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_clinit_rangle_InvokeMethod_32(o4, NULL, o2, env, static) -{1,1}> langle_init_rangle_Load_33(o4, o2, env, static) :|: NULL = 0 && 0 < o2 && 0 < o4
langle_init_rangle_Load_33(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_35(o4, o2, env, static) -{1,1}> langle_init_rangle_Load_37(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Load_37(o4, o2, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_InvokeMethod_40(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_42(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_42(o4, o2, env, static) -{1,1}> langle_init_rangle_Return_43(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_init_rangle_Return_43(o4, o2, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) :|: 0 < o2 && 0 < o4
langle_clinit_rangle_FieldAccess_44(o4, o2, env, static) -{1,1}> langle_clinit_rangle_Return_45(o2, env, static') :|: 0 < o2 && 0 <= o4 && 0 < o4 && 0 <= static && static' <= static + o4
langle_clinit_rangle_Return_45(o2, env, static) -{1,1}> main_Load_47(o2, env, static) :|: 0 < o2
main_Load_47(o2, env, static) -{0,0}> main_Load_48(o2, env, static) :|: 0 < o2
main_Load_48(o2, env, static) -{0,0}> main_Load_49(o2, env, static) :|: 0 < o2 && 0 <= static
main_Load_49(o2, env, static) -{0,0}> main_Load_50(o2, env, static) :|: 0 < o2
main_Load_50(o2, env, static) -{0,0}> main_Load_53(o2, env, static) :|: 0 < o2
main_Load_53(o2, env, static) -{1,1}> main_ConstantStackPush_54(o2, env, static) :|: 0 < o2
main_ConstantStackPush_54(o2, env, static) -{1,1}> main_ArrayAccess_56(o2, iconst_0, env, static) :|: 0 < o2 && iconst_0 = 0
main_ArrayAccess_56(a6, iconst_0, env, static) -{0,0}> main_ArrayAccess_57(a6, iconst_0, i5, env, static) :|: i5 < a6 && iconst_0 = 0 && 0 < a6 && 0 <= i5
main_ArrayAccess_57(a6, iconst_0, i6, env, static) -{0,0}> main_ArrayAccess_59(a6, iconst_0, i6, env, static) :|: 0 <= i6 && 1 <= i6 && iconst_0 = 0 && 0 < a6
main_ArrayAccess_59(a6, iconst_0, i6, env, static) -{1,1}> main_InvokeMethod_64(a6, o8, i6, env, static) :|: 1 <= i6 && iconst_0 < i6 && 0 <= o8 && o8 < a6 && iconst_0 = 0 && 0 < a6
main_InvokeMethod_64(a6, o12, i6, env, static) -{0,0}> main_InvokeMethod_66(a6, o12, i6, env, static) :|: 1 <= i6 && 0 <= o12 && 0 < o12 && 0 < a6
main_InvokeMethod_66(a6, o12, i6, env, static) -{1,1}> main_Store_71(a6, i8, i6, env, static) :|: 1 <= i6 && i8 <= o12 && 0 < o12 && 0 < a6 && 0 <= i8
main_Store_71(a6, i8, i6, env, static) -{1,1}> main_Load_79(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_Load_79(a6, i8, i6, env, static) -{1,1}> main_ConstantStackPush_83(a6, i8, i6, env, static) :|: 1 <= i6 && 0 < a6 && 0 <= i8
main_ConstantStackPush_83(a6, i8, i6, env, static) -{1,1}> main_ArrayAccess_90(a6, iconst_1, i8, i6, env, static) :|: 1 <= i6 && iconst_1 = 1 && 0 < a6 && 0 <= i8
main_ArrayAccess_90(a6, iconst_1, i8, i12, env, static) -{0,0}> main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i8 && 1 <= i12
main_ArrayAccess_108(a6, iconst_1, i8, i12, env, static) -{1,1}> main_InvokeMethod_111(a6, o20, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 <= o20 && iconst_1 < i12 && 0 < a6 && 0 <= i8 && o20 < a6
main_InvokeMethod_111(a6, o23, i8, i12, env, static) -{0,0}> main_InvokeMethod_113(a6, o23, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i8 && 0 <= o23
main_InvokeMethod_113(a6, o23, i8, i12, env, static) -{1,1}> main_ConstantStackPush_125(a6, i15, i8, i12, env, static) :|: 0 < o23 && 2 <= i12 && 0 < a6 && 0 <= i15 && 0 <= i8 && i15 <= o23
main_ConstantStackPush_125(a6, i15, i8, i12, env, static) -{1,1}> main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) :|: 2 <= i12 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_IntArithmetic_133(a6, i15, iconst_1, i8, i12, env, static) -{1,1}> main_Store_140(a6, i16, i8, i12, env, static) :|: i15 + iconst_1 = i16 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 0 < a6 && 0 <= i15 && 0 <= i8
main_Store_140(a6, i16, i8, i12, env, static) -{1,1}> main_Load_149(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_149(a6, i8, i16, i12, env, static) -{1,1}> main_Load_158(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_Load_158(a6, i8, i16, i12, env, static) -{1,1}> main_InvokeMethod_161(a6, i8, i16, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
main_InvokeMethod_161(a6, i8, i16, i12, env, static) -{1,1}> quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && 0 < a6 && 0 <= i8
quot_ConstantStackPush_165(i8, i16, a6, i12, env, static) -{1,1}> quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Store_173(iconst_0, i8, i16, a6, i12, env, static) -{1,1}> quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_Load_185(i8, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_NE_195(i8, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 0 <= i8
quot_NE_195(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= i20 && 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_NE_204(i20, i16, iconst_0, a6, i12, env, static) -{1,1}> quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) :|: 2 <= i12 && 1 <= i16 && iconst_0 = 0 && 0 < i20 && 0 < a6 && 1 <= i20
quot_Load_222(i20, i16, iconst_0, a6, i12, env, static) -{0,0}> quot_Load_397(i20, i16, iconst_0, a6, i12, env, static) :|: 0 <= iconst_0 && 2 <= i12 && 1 <= i16 && iconst_0 <= 1 && iconst_0 = 0 && 0 < a6 && 1 <= i20
quot_Load_397(i40, i16, i41, a87, i12, env, static) -{0,0}> quot_Load_471(i40, i16, i41, a87, i12, env, static) :|: 0 <= i41 && 2 <= i12 && 1 <= i16 && 0 < a87 && i41 <= 2 && i41 <= 1
quot_Load_471(i71, i16, i72, a95, i12, env, static) -{0,0}> quot_Load_531(i71, i16, i72, a95, i12, env, static) :|: 2 <= i12 && 1 <= i16 && i72 <= 2 && 0 <= i72 && 0 < a95

obtained
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
by chaining
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_536(i97, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i16
quot_LE_536(i110, i16, i98, a103, i12, env, static) -{0,0}> quot_LE_539(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 2 <= i12 && 1 <= i110 && 1 <= i16
quot_LE_539(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_544(i110, i16, i98, a103, i12, env, static) :|: 0 < i110 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_Load_544(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_LE_548(i16, i110, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16
quot_LE_548(i16, i110, i98, a103, i12, env, static) -{1,1}> quot_Inc_556(i110, i16, i98, a103, i12, env, static) :|: 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 0 < i16
quot_Inc_556(i110, i16, i98, a103, i12, env, static) -{1,1}> quot_Load_560(i110, i16, i114, a103, i12, env, static) :|: i98 + 1 = i114 && 0 <= i98 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_560(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_563(i110, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) :|: 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_565(i110, iconst_1, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_567(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 1 <= i110 && 2 <= i12 && 1 <= i16 && i110 - iconst_1 = i116 && iconst_1 = 1 && 1 <= i114
quot_Load_567(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_ConstantStackPush_569(i116, i16, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && 1 <= i114
quot_IntArithmetic_571(i116, i16, iconst_1, i114, a103, i12, env, static) -{1,1}> quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && iconst_1 = 1 && i16 - iconst_1 = i119 && 0 <= i119 && 1 <= i114
quot_IntArithmetic_574(i116, i119, i16, i114, a103, i12, env, static) -{1,1}> quot_Store_576(i120, i16, i114, a103, i12, env, static) :|: 0 <= i116 && 0 < a103 && 2 <= i12 && 1 <= i16 && i116 - i119 = i120 && 0 <= i119 && 1 <= i114
quot_Store_576(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_JMP_579(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_JMP_579(i120, i16, i114, a103, i12, env, static) -{1,1}> quot_Load_584(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 1 <= i114
quot_Load_584(i120, i16, i114, a103, i12, env, static) -{0,0}> quot_Load_531(i120, i16, i114, a103, i12, env, static) :|: 0 < a103 && 2 <= i12 && 1 <= i16 && 0 <= i114 && 1 <= i114

(36) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, env, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, env, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5', env, static'1) :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12, env, static) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12, env, static) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

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

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

main_Load_2(x1, x2, x3) → main_Load_2(x1, x3)
quot_Load_531(x1, x2, x3, x4, x5, x6, x7) → quot_Load_531(x1, x2, x3, x4, x5)

(38) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

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

Moved arithmethic from constraints to rhss.

quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i120', i16, i114', a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' - i16 - 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i16', 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
was transformed to
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1

(40) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' - i16 - 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1

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

Simplified expressions.

quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' - i16 - 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' - i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
was transformed to
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' + -1 * i16 + 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' + -1 * i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'

main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && 0 <= 0 && o20' < o2 && 0 <= 2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 < 2 && 0 <= static'1 && 0 <= i8' && 0 <= o8' && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= i5' && 0 < 1 && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1 && 1 <= i5' && 0 <= o20' && 0 <= 1
was transformed to
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && o20' < o2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 <= static'1 && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1

(42) Obligation:

IntTrs with 2 rules
Start term: main_Load_2(args, static)
Considered paths: all paths from start
Rules:
quot_Load_531(i97, i16, i98, a103, i12) -{14,14}> quot_Load_531(i116' + -1 * i16 + 1, i16, i98 + 1, a103, i12) :|: 0 < i97 && 1 <= i114' && 1 <= i97 && 0 <= i114' && i16 - 1 = i119' && 1 <= i16 && 0 <= i98 && 0 < a103 && 2 <= i12 && 0 <= i116' && i116' + -1 * i119' = i120' && i97 - 1 = i116' && 0 <= i119' && 0 < i16 && i98 + 1 = i114'
main_Load_2(o2, static) -{34,34}> quot_Load_531(i8', i15' + 1, 0, o2, i5') :|: 1 <= i8' && 0 < o2 && i15' <= o20' && o20' < o2 && 0 <= i15' && 2 <= i5' && 1 <= i16' && 0 <= static'1 && i15' + 1 = i16' && 0 < o20' && 1 < i5' && 0 <= static && 0 < i5' && 0 <= static''' && i5' < o2 && i8' <= o8' && o8' < o2 && 0 < o8' && static''' <= static + 2 && 0 < i8' && static'1 <= static''' + 1