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

(0) Obligation:

Need to prove time_complexity of the following program:

public class GCD3 {
  public static int mod(int a, int b) {
    if(b == 0) {
      return b;
    }
    if(b < 0) {
      a = -a;
    }
    if(a > 0) {
      while(a>=b) {
        a -= b;
      }
      return a;
    } else {
      while(a < 0) {
        a -= b;
      }
      return a;
    }
  }

  public static int gcd(int a, int b) {
    int tmp;
    while(b > 0 && a > 0) {
      tmp = b;
      b = mod(a, b);
      a = tmp;
    }
    return a;
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
GCD3.gcd(II)I: Graph of 69 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 64 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 64 jbc graph edges to a weighted ITS with 64 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 64 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_3(i1, i4, env, static) :|: 0 >= 0
gcd_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_22(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_22(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_24(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_24(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_26(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_26(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_46(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i1, i4, env, static) -{1,1}> gcd_Load_48(i1, i4, env, static) :|: 0 >= 0
gcd_Load_48(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 >= 0
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_52(i1, i4, env, static) :|: 0 <= static
gcd_Load_52(i1, i4, env, static) -{0,0}> gcd_Load_54(i1, i4, env, static) :|: 0 >= 0
gcd_Load_54(i1, i4, env, static) -{0,0}> gcd_Load_56(i1, i4, env, static) :|: 0 >= 0
gcd_Load_56(i1, i4, env, static) -{1,1}> gcd_LE_60(i1, i4, env, static) :|: 0 >= 0
gcd_LE_60(i1, i4, env, static) -{0,0}> gcd_LE_176(i1, i4, i4, i1, env, static) :|: 0 >= 0
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{0,0}> gcd_LE_187(i32, i33, i45, i34, env, static) :|: 1 <= i45
gcd_LE_187(i32, i33, i45, i34, env, static) -{1,1}> gcd_Load_191(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_Load_191(i32, i33, i34, i45, env, static) -{1,1}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{0,0}> gcd_LE_198(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_LE_198(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_207(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
gcd_Load_207(i32, i33, i52, i45, env, static) -{1,1}> gcd_Store_213(i32, i33, i45, i52, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Store_213(i32, i33, i45, i52, env, static) -{1,1}> gcd_Load_215(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_215(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_216(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_216(i32, i33, i52, i45, env, static) -{1,1}> gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) -{1,1}> mod_Load_218(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_Load_218(i52, i45, i32, i33, env, static) -{1,1}> mod_NE_219(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_NE_219(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_220(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45 && 0 < i45
mod_Load_220(i52, i45, i32, i33, env, static) -{1,1}> mod_GE_221(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_GE_221(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_223(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 <= i45 && 1 <= i45
mod_Load_223(i52, i45, i32, i33, env, static) -{1,1}> mod_LE_225(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_LE_225(i52, i45, i32, i33, env, static) -{1,1}> mod_Load_227(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
mod_Load_227(i52, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i52 && 1 <= i52 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_281(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_281(i56, i45, i32, i33, env, static) -{1,1}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_296(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_297(i56, i45, i32, i33, env, static) :|: 0 <= i56 && i45 <= i56 && 1 <= i45
mod_LT_296(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_299(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_297(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_301(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i56 && i45 <= i56 && 1 <= i45
mod_Load_299(i56, i32, i33, i45, env, static) -{1,1}> mod_Return_302(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_301(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_303(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_Return_302(i56, i32, i33, i45, env, static) -{1,1}> gcd_Store_304(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_303(i56, i45, i32, i33, env, static) -{1,1}> mod_IntArithmetic_305(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
gcd_Store_304(i32, i33, i56, i45, env, static) -{1,1}> gcd_Load_306(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_IntArithmetic_305(i56, i45, i32, i33, env, static) -{1,1}> mod_Store_307(i59, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59 && 1 <= i45 && i56 - i45 = i59
gcd_Load_306(i32, i33, i56, i45, env, static) -{1,1}> gcd_Store_309(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_Store_307(i59, i45, i32, i33, env, static) -{1,1}> mod_JMP_310(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_Store_309(i32, i33, i45, i56, env, static) -{1,1}> gcd_JMP_313(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_JMP_310(i59, i45, i32, i33, env, static) -{1,1}> mod_Load_314(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_JMP_313(i32, i33, i45, i56, env, static) -{1,1}> gcd_Load_315(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_314(i59, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_Load_315(i32, i33, i45, i56, env, static) -{1,1}> gcd_LE_320(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_LE_320(i32, i33, i56, i45, env, static) -{0,0}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45

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

obtained
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_3(i1, i4, env, static) :|: 0 >= 0
gcd_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_22(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_22(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_24(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_24(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_26(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_26(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_46(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i1, i4, env, static) -{1,1}> gcd_Load_48(i1, i4, env, static) :|: 0 >= 0
gcd_Load_48(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 >= 0
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_52(i1, i4, env, static) :|: 0 <= static
gcd_Load_52(i1, i4, env, static) -{0,0}> gcd_Load_54(i1, i4, env, static) :|: 0 >= 0
gcd_Load_54(i1, i4, env, static) -{0,0}> gcd_Load_56(i1, i4, env, static) :|: 0 >= 0
gcd_Load_56(i1, i4, env, static) -{1,1}> gcd_LE_60(i1, i4, env, static) :|: 0 >= 0
gcd_LE_60(i1, i4, env, static) -{0,0}> gcd_LE_176(i1, i4, i4, i1, env, static) :|: 0 >= 0

obtained
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
by chaining
gcd_LE_176(i32, i33, i45, i34, env, static) -{0,0}> gcd_LE_187(i32, i33, i45, i34, env, static) :|: 1 <= i45
gcd_LE_187(i32, i33, i45, i34, env, static) -{1,1}> gcd_Load_191(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_Load_191(i32, i33, i34, i45, env, static) -{1,1}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45

obtained
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
by chaining
gcd_LE_193(i32, i33, i52, i45, env, static) -{0,0}> gcd_LE_198(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_LE_198(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_207(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
gcd_Load_207(i32, i33, i52, i45, env, static) -{1,1}> gcd_Store_213(i32, i33, i45, i52, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Store_213(i32, i33, i45, i52, env, static) -{1,1}> gcd_Load_215(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_215(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_216(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_216(i32, i33, i52, i45, env, static) -{1,1}> gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) -{1,1}> mod_Load_218(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_Load_218(i52, i45, i32, i33, env, static) -{1,1}> mod_NE_219(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_NE_219(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_220(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45 && 0 < i45
mod_Load_220(i52, i45, i32, i33, env, static) -{1,1}> mod_GE_221(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_GE_221(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_223(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 <= i45 && 1 <= i45
mod_Load_223(i52, i45, i32, i33, env, static) -{1,1}> mod_LE_225(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_LE_225(i52, i45, i32, i33, env, static) -{1,1}> mod_Load_227(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
mod_Load_227(i52, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i52 && 1 <= i52 && 1 <= i45

obtained
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
by chaining
mod_Load_277(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_281(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_281(i56, i45, i32, i33, env, static) -{1,1}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45

obtained
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
by chaining
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_297(i56, i45, i32, i33, env, static) :|: 0 <= i56 && i45 <= i56 && 1 <= i45
mod_LT_297(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_301(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i56 && i45 <= i56 && 1 <= i45
mod_Load_301(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_303(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_Load_303(i56, i45, i32, i33, env, static) -{1,1}> mod_IntArithmetic_305(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_IntArithmetic_305(i56, i45, i32, i33, env, static) -{1,1}> mod_Store_307(i59, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59 && 1 <= i45 && i56 - i45 = i59
mod_Store_307(i59, i45, i32, i33, env, static) -{1,1}> mod_JMP_310(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
mod_JMP_310(i59, i45, i32, i33, env, static) -{1,1}> mod_Load_314(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
mod_Load_314(i59, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45

obtained
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45
by chaining
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_296(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_296(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_299(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_Load_299(i56, i32, i33, i45, env, static) -{1,1}> mod_Return_302(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Return_302(i56, i32, i33, i45, env, static) -{1,1}> gcd_Store_304(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Store_304(i32, i33, i56, i45, env, static) -{1,1}> gcd_Load_306(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_306(i32, i33, i56, i45, env, static) -{1,1}> gcd_Store_309(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Store_309(i32, i33, i45, i56, env, static) -{1,1}> gcd_JMP_313(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_JMP_313(i32, i33, i45, i56, env, static) -{1,1}> gcd_Load_315(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_315(i32, i33, i45, i56, env, static) -{1,1}> gcd_LE_320(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_LE_320(i32, i33, i56, i45, env, static) -{0,0}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45

(8) Obligation:

IntTrs with 8 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45

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

Moved arithmethic from constraints to rhss.

mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
was transformed to
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 - i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'

(10) Obligation:

IntTrs with 8 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 - i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45

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

Simplified expressions.

gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
was transformed to
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 1 <= i45 && 1 <= i52 && 0 < i52 && 0 < i45

mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 - i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
was transformed to
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 + -1 * i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 + -1 * i45 = i59'

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

(12) Obligation:

IntTrs with 8 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 + -1 * i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 + -1 * i45 = i59'
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 1 <= i45 && 1 <= i52 && 0 < i52 && 0 < i45

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

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

(14) Obligation:

IntTrs with 64 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_3(i1, i4, env, static) :|: 0 >= 0
gcd_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_22(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_22(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_24(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_24(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_26(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_26(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_46(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i1, i4, env, static) -{1,1}> gcd_Load_48(i1, i4, env, static) :|: 0 >= 0
gcd_Load_48(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 >= 0
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_52(i1, i4, env, static) :|: 0 <= static
gcd_Load_52(i1, i4, env, static) -{0,0}> gcd_Load_54(i1, i4, env, static) :|: 0 >= 0
gcd_Load_54(i1, i4, env, static) -{0,0}> gcd_Load_56(i1, i4, env, static) :|: 0 >= 0
gcd_Load_56(i1, i4, env, static) -{1,1}> gcd_LE_60(i1, i4, env, static) :|: 0 >= 0
gcd_LE_60(i1, i4, env, static) -{0,0}> gcd_LE_176(i1, i4, i4, i1, env, static) :|: 0 >= 0
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{0,0}> gcd_LE_187(i32, i33, i45, i34, env, static) :|: 1 <= i45
gcd_LE_187(i32, i33, i45, i34, env, static) -{1,1}> gcd_Load_191(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_Load_191(i32, i33, i34, i45, env, static) -{1,1}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{0,0}> gcd_LE_198(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_LE_198(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_207(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
gcd_Load_207(i32, i33, i52, i45, env, static) -{1,1}> gcd_Store_213(i32, i33, i45, i52, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Store_213(i32, i33, i45, i52, env, static) -{1,1}> gcd_Load_215(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_215(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_216(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_216(i32, i33, i52, i45, env, static) -{1,1}> gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) -{1,1}> mod_Load_218(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_Load_218(i52, i45, i32, i33, env, static) -{1,1}> mod_NE_219(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_NE_219(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_220(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45 && 0 < i45
mod_Load_220(i52, i45, i32, i33, env, static) -{1,1}> mod_GE_221(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_GE_221(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_223(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 <= i45 && 1 <= i45
mod_Load_223(i52, i45, i32, i33, env, static) -{1,1}> mod_LE_225(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_LE_225(i52, i45, i32, i33, env, static) -{1,1}> mod_Load_227(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
mod_Load_227(i52, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i52 && 1 <= i52 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_281(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_281(i56, i45, i32, i33, env, static) -{1,1}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_296(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_297(i56, i45, i32, i33, env, static) :|: 0 <= i56 && i45 <= i56 && 1 <= i45
mod_LT_296(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_299(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_297(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_301(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i56 && i45 <= i56 && 1 <= i45
mod_Load_299(i56, i32, i33, i45, env, static) -{1,1}> mod_Return_302(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_301(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_303(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_Return_302(i56, i32, i33, i45, env, static) -{1,1}> gcd_Store_304(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_303(i56, i45, i32, i33, env, static) -{1,1}> mod_IntArithmetic_305(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
gcd_Store_304(i32, i33, i56, i45, env, static) -{1,1}> gcd_Load_306(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_IntArithmetic_305(i56, i45, i32, i33, env, static) -{1,1}> mod_Store_307(i59, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59 && 1 <= i45 && i56 - i45 = i59
gcd_Load_306(i32, i33, i56, i45, env, static) -{1,1}> gcd_Store_309(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_Store_307(i59, i45, i32, i33, env, static) -{1,1}> mod_JMP_310(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_Store_309(i32, i33, i45, i56, env, static) -{1,1}> gcd_JMP_313(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_JMP_310(i59, i45, i32, i33, env, static) -{1,1}> mod_Load_314(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_JMP_313(i32, i33, i45, i56, env, static) -{1,1}> gcd_Load_315(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_314(i59, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_Load_315(i32, i33, i45, i56, env, static) -{1,1}> gcd_LE_320(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_LE_320(i32, i33, i56, i45, env, static) -{0,0}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45

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

obtained
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_3(i1, i4, env, static) :|: 0 >= 0
gcd_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_22(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_22(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_24(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_24(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_26(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_26(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_46(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i1, i4, env, static) -{1,1}> gcd_Load_48(i1, i4, env, static) :|: 0 >= 0
gcd_Load_48(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 >= 0
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_52(i1, i4, env, static) :|: 0 <= static
gcd_Load_52(i1, i4, env, static) -{0,0}> gcd_Load_54(i1, i4, env, static) :|: 0 >= 0
gcd_Load_54(i1, i4, env, static) -{0,0}> gcd_Load_56(i1, i4, env, static) :|: 0 >= 0
gcd_Load_56(i1, i4, env, static) -{1,1}> gcd_LE_60(i1, i4, env, static) :|: 0 >= 0
gcd_LE_60(i1, i4, env, static) -{0,0}> gcd_LE_176(i1, i4, i4, i1, env, static) :|: 0 >= 0

obtained
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
by chaining
gcd_LE_176(i32, i33, i45, i34, env, static) -{0,0}> gcd_LE_187(i32, i33, i45, i34, env, static) :|: 1 <= i45
gcd_LE_187(i32, i33, i45, i34, env, static) -{1,1}> gcd_Load_191(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_Load_191(i32, i33, i34, i45, env, static) -{1,1}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45

obtained
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
by chaining
gcd_LE_193(i32, i33, i52, i45, env, static) -{0,0}> gcd_LE_198(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_LE_198(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_207(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
gcd_Load_207(i32, i33, i52, i45, env, static) -{1,1}> gcd_Store_213(i32, i33, i45, i52, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Store_213(i32, i33, i45, i52, env, static) -{1,1}> gcd_Load_215(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_215(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_216(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_216(i32, i33, i52, i45, env, static) -{1,1}> gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) -{1,1}> mod_Load_218(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_Load_218(i52, i45, i32, i33, env, static) -{1,1}> mod_NE_219(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_NE_219(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_220(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45 && 0 < i45
mod_Load_220(i52, i45, i32, i33, env, static) -{1,1}> mod_GE_221(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_GE_221(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_223(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 <= i45 && 1 <= i45
mod_Load_223(i52, i45, i32, i33, env, static) -{1,1}> mod_LE_225(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_LE_225(i52, i45, i32, i33, env, static) -{1,1}> mod_Load_227(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
mod_Load_227(i52, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i52 && 1 <= i52 && 1 <= i45

obtained
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
by chaining
mod_Load_277(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_281(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_281(i56, i45, i32, i33, env, static) -{1,1}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45

obtained
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
by chaining
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_297(i56, i45, i32, i33, env, static) :|: 0 <= i56 && i45 <= i56 && 1 <= i45
mod_LT_297(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_301(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i56 && i45 <= i56 && 1 <= i45
mod_Load_301(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_303(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_Load_303(i56, i45, i32, i33, env, static) -{1,1}> mod_IntArithmetic_305(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_IntArithmetic_305(i56, i45, i32, i33, env, static) -{1,1}> mod_Store_307(i59, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59 && 1 <= i45 && i56 - i45 = i59
mod_Store_307(i59, i45, i32, i33, env, static) -{1,1}> mod_JMP_310(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
mod_JMP_310(i59, i45, i32, i33, env, static) -{1,1}> mod_Load_314(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
mod_Load_314(i59, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45

obtained
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45
by chaining
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_296(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_296(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_299(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_Load_299(i56, i32, i33, i45, env, static) -{1,1}> mod_Return_302(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Return_302(i56, i32, i33, i45, env, static) -{1,1}> gcd_Store_304(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Store_304(i32, i33, i56, i45, env, static) -{1,1}> gcd_Load_306(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_306(i32, i33, i56, i45, env, static) -{1,1}> gcd_Store_309(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Store_309(i32, i33, i45, i56, env, static) -{1,1}> gcd_JMP_313(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_JMP_313(i32, i33, i45, i56, env, static) -{1,1}> gcd_Load_315(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_315(i32, i33, i45, i56, env, static) -{1,1}> gcd_LE_320(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_LE_320(i32, i33, i56, i45, env, static) -{0,0}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45

(16) Obligation:

IntTrs with 8 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45

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

Moved arithmethic from constraints to rhss.

mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
was transformed to
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 - i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'

(18) Obligation:

IntTrs with 8 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 - i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45

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

Simplified expressions.

gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i52 && 0 <= i52 && 0 < i52 && 0 < i45
was transformed to
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 1 <= i45 && 1 <= i52 && 0 < i52 && 0 < i45

mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 - i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
was transformed to
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 + -1 * i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 + -1 * i45 = i59'

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

(20) Obligation:

IntTrs with 8 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_LE_176(i32, i33, i44, i34, env, static) -{0,0}> gcd_LE_186(i32, i33, i44, i34, env, static) :|: i44 <= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{2,2}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_LE_193(i32, i33, i51, i45, env, static) -{0,0}> gcd_LE_197(i32, i33, i51, i45, env, static) :|: i51 <= 0 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i56 + -1 * i45, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 + -1 * i45 = i59'
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{12,12}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 1 <= i45 && 1 <= i52 && 0 < i52 && 0 < i45

(21) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)) transformation)

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

(22) Obligation:

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

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

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

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

(24) Obligation:

IntTrs with 62 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_3(i1, i4, env, static) :|: 0 >= 0
gcd_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_22(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_22(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_24(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_24(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_26(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_26(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_46(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i1, i4, env, static) -{1,1}> gcd_Load_48(i1, i4, env, static) :|: 0 >= 0
gcd_Load_48(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 >= 0
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_52(i1, i4, env, static) :|: 0 <= static
gcd_Load_52(i1, i4, env, static) -{0,0}> gcd_Load_54(i1, i4, env, static) :|: 0 >= 0
gcd_Load_54(i1, i4, env, static) -{0,0}> gcd_Load_56(i1, i4, env, static) :|: 0 >= 0
gcd_Load_56(i1, i4, env, static) -{1,1}> gcd_LE_60(i1, i4, env, static) :|: 0 >= 0
gcd_LE_60(i1, i4, env, static) -{0,0}> gcd_LE_176(i1, i4, i4, i1, env, static) :|: 0 >= 0
gcd_LE_176(i32, i33, i45, i34, env, static) -{0,0}> gcd_LE_187(i32, i33, i45, i34, env, static) :|: 1 <= i45
gcd_LE_187(i32, i33, i45, i34, env, static) -{1,1}> gcd_Load_191(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_Load_191(i32, i33, i34, i45, env, static) -{1,1}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{0,0}> gcd_LE_198(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_LE_198(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_207(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
gcd_Load_207(i32, i33, i52, i45, env, static) -{1,1}> gcd_Store_213(i32, i33, i45, i52, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Store_213(i32, i33, i45, i52, env, static) -{1,1}> gcd_Load_215(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_215(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_216(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_216(i32, i33, i52, i45, env, static) -{1,1}> gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) -{1,1}> mod_Load_218(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_Load_218(i52, i45, i32, i33, env, static) -{1,1}> mod_NE_219(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_NE_219(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_220(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45 && 0 < i45
mod_Load_220(i52, i45, i32, i33, env, static) -{1,1}> mod_GE_221(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_GE_221(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_223(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 <= i45 && 1 <= i45
mod_Load_223(i52, i45, i32, i33, env, static) -{1,1}> mod_LE_225(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_LE_225(i52, i45, i32, i33, env, static) -{1,1}> mod_Load_227(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
mod_Load_227(i52, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i52 && 1 <= i52 && 1 <= i45
mod_Load_277(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_281(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_281(i56, i45, i32, i33, env, static) -{1,1}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_296(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_297(i56, i45, i32, i33, env, static) :|: 0 <= i56 && i45 <= i56 && 1 <= i45
mod_LT_296(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_299(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_297(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_301(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i56 && i45 <= i56 && 1 <= i45
mod_Load_299(i56, i32, i33, i45, env, static) -{1,1}> mod_Return_302(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_301(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_303(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_Return_302(i56, i32, i33, i45, env, static) -{1,1}> gcd_Store_304(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_303(i56, i45, i32, i33, env, static) -{1,1}> mod_IntArithmetic_305(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
gcd_Store_304(i32, i33, i56, i45, env, static) -{1,1}> gcd_Load_306(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_IntArithmetic_305(i56, i45, i32, i33, env, static) -{1,1}> mod_Store_307(i59, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59 && 1 <= i45 && i56 - i45 = i59
gcd_Load_306(i32, i33, i56, i45, env, static) -{1,1}> gcd_Store_309(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_Store_307(i59, i45, i32, i33, env, static) -{1,1}> mod_JMP_310(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_Store_309(i32, i33, i45, i56, env, static) -{1,1}> gcd_JMP_313(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_JMP_310(i59, i45, i32, i33, env, static) -{1,1}> mod_Load_314(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_JMP_313(i32, i33, i45, i56, env, static) -{1,1}> gcd_Load_315(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_314(i59, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
gcd_Load_315(i32, i33, i45, i56, env, static) -{1,1}> gcd_LE_320(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_LE_320(i32, i33, i56, i45, env, static) -{0,0}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45

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

obtained
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
by chaining
gcd_Load_2(i1, i4, env, static) -{0,0}> gcd_Load_3(i1, i4, env, static) :|: 0 >= 0
gcd_Load_3(i1, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_17(iconst_0, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_20(a2, i1, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_22(i1, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_22(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_24(i1, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_24(i1, i4, env, static) -{0,0}> langle_clinit_rangle_New_26(i1, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_26(i1, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_28(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_31(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_32(o2, NULL, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i1, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_33(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_37(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Load_38(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_38(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_40(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_41(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_41(o2, i1, i4, env, static) -{1,1}> langle_init_rangle_Return_42(o2, i1, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_42(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_43(o2, i1, i4, env, static) -{1,1}> langle_clinit_rangle_Return_46(i1, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_46(i1, i4, env, static) -{1,1}> gcd_Load_48(i1, i4, env, static) :|: 0 >= 0
gcd_Load_48(i1, i4, env, static) -{0,0}> gcd_Load_49(i1, i4, env, static) :|: 0 >= 0
gcd_Load_49(i1, i4, env, static) -{0,0}> gcd_Load_52(i1, i4, env, static) :|: 0 <= static
gcd_Load_52(i1, i4, env, static) -{0,0}> gcd_Load_54(i1, i4, env, static) :|: 0 >= 0
gcd_Load_54(i1, i4, env, static) -{0,0}> gcd_Load_56(i1, i4, env, static) :|: 0 >= 0
gcd_Load_56(i1, i4, env, static) -{1,1}> gcd_LE_60(i1, i4, env, static) :|: 0 >= 0
gcd_LE_60(i1, i4, env, static) -{0,0}> gcd_LE_176(i1, i4, i4, i1, env, static) :|: 0 >= 0

obtained
gcd_LE_176(i32, i33, i45, i34, env, static) -{14,14}> mod_Load_277(i34, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i34 && 0 <= i34 && 0 < i34 && 0 < i45
by chaining
gcd_LE_176(i32, i33, i45, i34, env, static) -{0,0}> gcd_LE_187(i32, i33, i45, i34, env, static) :|: 1 <= i45
gcd_LE_187(i32, i33, i45, i34, env, static) -{1,1}> gcd_Load_191(i32, i33, i34, i45, env, static) :|: 1 <= i45 && 0 < i45
gcd_Load_191(i32, i33, i34, i45, env, static) -{1,1}> gcd_LE_193(i32, i33, i34, i45, env, static) :|: 1 <= i45
gcd_LE_193(i32, i33, i52, i45, env, static) -{0,0}> gcd_LE_198(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_LE_198(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_207(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
gcd_Load_207(i32, i33, i52, i45, env, static) -{1,1}> gcd_Store_213(i32, i33, i45, i52, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Store_213(i32, i33, i45, i52, env, static) -{1,1}> gcd_Load_215(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_215(i32, i33, i52, i45, env, static) -{1,1}> gcd_Load_216(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_Load_216(i32, i33, i52, i45, env, static) -{1,1}> gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) :|: 1 <= i52 && 1 <= i45
gcd_InvokeMethod_217(i32, i33, i52, i45, env, static) -{1,1}> mod_Load_218(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_Load_218(i52, i45, i32, i33, env, static) -{1,1}> mod_NE_219(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_NE_219(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_220(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45 && 0 < i45
mod_Load_220(i52, i45, i32, i33, env, static) -{1,1}> mod_GE_221(i45, i52, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_GE_221(i45, i52, i32, i33, env, static) -{1,1}> mod_Load_223(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 <= i45 && 1 <= i45
mod_Load_223(i52, i45, i32, i33, env, static) -{1,1}> mod_LE_225(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 1 <= i45
mod_LE_225(i52, i45, i32, i33, env, static) -{1,1}> mod_Load_227(i52, i45, i32, i33, env, static) :|: 1 <= i52 && 0 < i52 && 1 <= i45
mod_Load_227(i52, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i52, i45, i32, i33, env, static) :|: 0 <= i52 && 1 <= i52 && 1 <= i45

obtained
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
by chaining
mod_Load_277(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_281(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_Load_281(i56, i45, i32, i33, env, static) -{1,1}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45

obtained
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
by chaining
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_297(i56, i45, i32, i33, env, static) :|: 0 <= i56 && i45 <= i56 && 1 <= i45
mod_LT_297(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_301(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i56 && i45 <= i56 && 1 <= i45
mod_Load_301(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_303(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_Load_303(i56, i45, i32, i33, env, static) -{1,1}> mod_IntArithmetic_305(i56, i45, i32, i33, env, static) :|: 1 <= i56 && 1 <= i45
mod_IntArithmetic_305(i56, i45, i32, i33, env, static) -{1,1}> mod_Store_307(i59, i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59 && 1 <= i45 && i56 - i45 = i59
mod_Store_307(i59, i45, i32, i33, env, static) -{1,1}> mod_JMP_310(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
mod_JMP_310(i59, i45, i32, i33, env, static) -{1,1}> mod_Load_314(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45
mod_Load_314(i59, i45, i32, i33, env, static) -{0,0}> mod_Load_277(i59, i45, i32, i33, env, static) :|: 0 <= i59 && 1 <= i45

obtained
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45
by chaining
mod_LT_289(i56, i45, i32, i33, env, static) -{0,0}> mod_LT_296(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_LT_296(i56, i45, i32, i33, env, static) -{1,1}> mod_Load_299(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45 && i56 < i45
mod_Load_299(i56, i32, i33, i45, env, static) -{1,1}> mod_Return_302(i56, i32, i33, i45, env, static) :|: 0 <= i56 && 1 <= i45
mod_Return_302(i56, i32, i33, i45, env, static) -{1,1}> gcd_Store_304(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Store_304(i32, i33, i56, i45, env, static) -{1,1}> gcd_Load_306(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_306(i32, i33, i56, i45, env, static) -{1,1}> gcd_Store_309(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Store_309(i32, i33, i45, i56, env, static) -{1,1}> gcd_JMP_313(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_JMP_313(i32, i33, i45, i56, env, static) -{1,1}> gcd_Load_315(i32, i33, i45, i56, env, static) :|: 0 <= i56 && 1 <= i45
gcd_Load_315(i32, i33, i45, i56, env, static) -{1,1}> gcd_LE_320(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45
gcd_LE_320(i32, i33, i56, i45, env, static) -{0,0}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: 0 <= i56 && 1 <= i45

(26) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, env, static) -{16,16}> gcd_LE_176(i1, i4, i4, i1, env, static'1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
gcd_LE_176(i32, i33, i45, i34, env, static) -{14,14}> mod_Load_277(i34, i45, i32, i33, env, static) :|: 0 <= i45 && 1 <= i45 && 1 <= i34 && 0 <= i34 && 0 < i34 && 0 < i45
mod_Load_277(i56, i45, i32, i33, env, static) -{2,2}> mod_LT_289(i56, i45, i32, i33, env, static) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45, i32, i33, env, static) -{6,6}> mod_Load_277(i59', i45, i32, i33, env, static) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
mod_LT_289(i56, i45, i32, i33, env, static) -{8,8}> gcd_LE_176(i32, i33, i56, i45, env, static) :|: i56 < i45 && 0 <= i56 && 1 <= i45

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

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

gcd_Load_2(x1, x2, x3, x4) → gcd_Load_2(x1, x2, x4)
gcd_LE_176(x1, x2, x3, x4, x5, x6) → gcd_LE_176(x3, x4)
mod_Load_277(x1, x2, x3, x4, x5, x6) → mod_Load_277(x1, x2)
mod_LT_289(x1, x2, x3, x4, x5, x6) → mod_LT_289(x1, x2)

(28) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, static) -{16,16}> gcd_LE_176(i4, i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
gcd_LE_176(i45, i34) -{14,14}> mod_Load_277(i34, i45) :|: 0 <= i45 && 1 <= i45 && 1 <= i34 && 0 <= i34 && 0 < i34 && 0 < i45
mod_Load_277(i56, i45) -{2,2}> mod_LT_289(i56, i45) :|: 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i59', i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
mod_LT_289(i56, i45) -{8,8}> gcd_LE_176(i56, i45) :|: i56 < i45 && 0 <= i56 && 1 <= i45

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

Moved arithmethic from constraints to rhss.

mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i59', i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
was transformed to
mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i56 - i45, i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'

(30) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, static) -{16,16}> gcd_LE_176(i4, i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
mod_LT_289(i56, i45) -{8,8}> gcd_LE_176(i56, i45) :|: i56 < i45 && 0 <= i56 && 1 <= i45
mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i56 - i45, i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
mod_Load_277(i56, i45) -{2,2}> mod_LT_289(i56, i45) :|: 0 <= i56 && 1 <= i45
gcd_LE_176(i45, i34) -{14,14}> mod_Load_277(i34, i45) :|: 0 <= i45 && 1 <= i45 && 1 <= i34 && 0 <= i34 && 0 < i34 && 0 < i45

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

Simplified expressions.

mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i56 - i45, i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 - i45 = i59'
was transformed to
mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i56 + -1 * i45, i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 + -1 * i45 = i59'

gcd_Load_2(i1, i4, static) -{16,16}> gcd_LE_176(i4, i1) :|: 0 >= 0 && 0 < 2 && 0 <= static'1 && 0 <= static && 0 <= 1 && 0 < 1 && static''' <= static + 2 && 0 <= static''' && 0 <= 2 && static'1 <= static''' + 1
was transformed to
gcd_Load_2(i1, i4, static) -{16,16}> gcd_LE_176(i4, i1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

gcd_LE_176(i45, i34) -{14,14}> mod_Load_277(i34, i45) :|: 0 <= i45 && 1 <= i45 && 1 <= i34 && 0 <= i34 && 0 < i34 && 0 < i45
was transformed to
gcd_LE_176(i45, i34) -{14,14}> mod_Load_277(i34, i45) :|: 1 <= i45 && 1 <= i34 && 0 < i34 && 0 < i45

(32) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i4, static) -{16,16}> gcd_LE_176(i4, i1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_LT_289(i56, i45) -{6,6}> mod_Load_277(i56 + -1 * i45, i45) :|: 1 <= i56 && 0 <= i59' && 1 <= i45 && 0 <= i56 && i45 <= i56 && i56 + -1 * i45 = i59'
mod_LT_289(i56, i45) -{8,8}> gcd_LE_176(i56, i45) :|: i56 < i45 && 0 <= i56 && 1 <= i45
mod_Load_277(i56, i45) -{2,2}> mod_LT_289(i56, i45) :|: 0 <= i56 && 1 <= i45
gcd_LE_176(i45, i34) -{14,14}> mod_Load_277(i34, i45) :|: 1 <= i45 && 1 <= i34 && 0 < i34 && 0 < i45

(33) koat Proof (EQUIVALENT transformation)

YES(?, 60*ar_0 + 150*ar_1 + 16)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_0 - ar_1, ar_1, arityPad)) [ 1 <= ar_0 /\ 0 <= i59' /\ 1 <= ar_1 /\ 0 <= ar_0 /\ ar_1 <= ar_0 /\ ar_0 - ar_1 = i59' ]
(Comp: ?, Cost: 8) mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_Load_277(ar_0, ar_1, ar_2) -> Com_1(mod_LT_289(ar_0, ar_1, arityPad)) [ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 14) gcd_LE_176(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 1 produces the following problem:
2: T:
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 6) mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_0 - ar_1, ar_1, arityPad)) [ 1 <= ar_0 /\ 0 <= i59' /\ 1 <= ar_1 /\ 0 <= ar_0 /\ ar_1 <= ar_0 /\ ar_0 - ar_1 = i59' ]
(Comp: ?, Cost: 8) mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 2) mod_Load_277(ar_0, ar_1, ar_2) -> Com_1(mod_LT_289(ar_0, ar_1, arityPad)) [ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 14) gcd_LE_176(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(gcd_Load_2) = 2*V_1 + 5*V_2
Pol(gcd_LE_176) = 5*V_1 + 2*V_2
Pol(mod_LT_289) = 2*V_1 + 5*V_2 - 2
Pol(mod_Load_277) = 2*V_1 + 5*V_2 - 1
Pol(koat_start) = 2*V_1 + 5*V_2
orients all transitions weakly and the transitions
mod_Load_277(ar_0, ar_1, ar_2) -> Com_1(mod_LT_289(ar_0, ar_1, arityPad)) [ 0 <= ar_0 /\ 1 <= ar_1 ]
mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_0 - ar_1, ar_1, arityPad)) [ 1 <= ar_0 /\ 0 <= i59' /\ 1 <= ar_1 /\ 0 <= ar_0 /\ ar_1 <= ar_0 /\ ar_0 - ar_1 = i59' ]
mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
gcd_LE_176(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 0 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 6) mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_0 - ar_1, ar_1, arityPad)) [ 1 <= ar_0 /\ 0 <= i59' /\ 1 <= ar_1 /\ 0 <= ar_0 /\ ar_1 <= ar_0 /\ ar_0 - ar_1 = i59' ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 8) mod_LT_289(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_176(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 2) mod_Load_277(ar_0, ar_1, ar_2) -> Com_1(mod_LT_289(ar_0, ar_1, arityPad)) [ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 14) gcd_LE_176(ar_0, ar_1, ar_2) -> Com_1(mod_Load_277(ar_1, ar_0, arityPad)) [ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_1 /\ 0 < ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 60*ar_0 + 150*ar_1 + 16

Time: 0.080 sec (SMT: 0.071 sec)

(34) BOUNDS(CONSTANT, 16 + 60 * |#0| + 150 * |#1|)