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

0 JBC problem
↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 176 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)), 0 ms)
↳4 JBCComplexityEdges
    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 131 ms)
    ↳6 WeightedIntTrs
        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 10 ms)
        ↳8 WeightedIntTrs
        ↳9 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)
        ↳10 WeightedIntTrs
        ↳11 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳12 WeightedIntTrs
        ↳13 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 10 ms)
        ↳14 WeightedIntTrs
    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 137 ms)
    ↳16 WeightedIntTrs
        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 18 ms)
        ↳18 WeightedIntTrs
        ↳19 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
        ↳20 WeightedIntTrs
        ↳21 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 13 ms)
        ↳22 WeightedIntTrs
↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)), 0 ms)
↳24 JBCComplexityEdges
    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 124 ms)
    ↳26 WeightedIntTrs
    ↳27 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 13 ms)
    ↳28 WeightedIntTrs
    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 23 ms)
    ↳30 WeightedIntTrs
    ↳31 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)
    ↳32 WeightedIntTrs
    ↳33 koat Proof (⇔, 32 ms)
    ↳34 BOUNDS(CONSTANT, 18 + 13 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:
public class GCD5 {
  public static int gcd(int a, int b) {
    int tmp;
    while(b > 0 && a > 0) {
      tmp = b;
      b = a % b;
      a = tmp;
    }
    return a;
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

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


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

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

(4) Obligation:

Set of 47 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 47 jbc graph edges to a weighted ITS with 47 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.

(6) Obligation:

IntTrs with 47 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, i3, env, static) -{0,0}> gcd_Load_4(i1, i3, env, static) :|: 0 >= 0
gcd_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, env, static) -{1,1}> gcd_Load_45(i1, i3, env, static) :|: 0 >= 0
gcd_Load_45(i1, i3, env, static) -{0,0}> gcd_Load_46(i1, i3, env, static) :|: 0 >= 0
gcd_Load_46(i1, i3, env, static) -{0,0}> gcd_Load_49(i1, i3, env, static) :|: 0 <= static
gcd_Load_49(i1, i3, env, static) -{0,0}> gcd_Load_50(i1, i3, env, static) :|: 0 >= 0
gcd_Load_50(i1, i3, env, static) -{0,0}> gcd_Load_51(i1, i3, env, static) :|: 0 >= 0
gcd_Load_51(i1, i3, env, static) -{1,1}> gcd_LE_52(i1, i3, env, static) :|: 0 >= 0
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_52(i1, i12, env, static) -{0,0}> gcd_LE_55(i1, i12, env, static) :|: 1 <= i12
gcd_LE_55(i1, i12, env, static) -{1,1}> gcd_Load_59(i1, i12, env, static) :|: 0 < i12 && 1 <= i12
gcd_Load_59(i1, i12, env, static) -{1,1}> gcd_LE_66(i1, i12, env, static) :|: 1 <= i12
gcd_LE_66(i1, i12, env, static) -{0,0}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_160(i41, i12, i54, i43, env, static) -{0,0}> gcd_LE_167(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_LE_167(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_172(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 0 < i54 && 1 <= i12
gcd_Load_172(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_178(i41, i12, i43, i54, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_178(i41, i12, i43, i54, env, static) -{1,1}> gcd_Load_181(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_181(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_183(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_183(i41, i12, i54, i43, env, static) -{1,1}> gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_188(i41, i12, i59, i43, env, static) :|: 0 <= i59 && i54 % i43 = i59 && 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_188(i41, i12, i59, i43, env, static) -{1,1}> gcd_Load_190(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_190(i41, i12, i59, i43, env, static) -{1,1}> gcd_Store_192(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Store_192(i41, i12, i43, i59, env, static) -{1,1}> gcd_JMP_194(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_JMP_194(i41, i12, i43, i59, env, static) -{1,1}> gcd_Load_198(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_198(i41, i12, i43, i59, env, static) -{1,1}> gcd_LE_205(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{0,0}> gcd_LE_209(i41, i12, i73, i43, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12 && 0 <= i73
gcd_LE_209(i41, i12, i73, i43, env, static) -{1,1}> gcd_Load_217(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 0 < i73 && 1 <= i43 && 1 <= i12
gcd_Load_217(i41, i12, i43, i73, env, static) -{1,1}> gcd_LE_231(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12
gcd_LE_231(i41, i12, i43, i73, env, static) -{0,0}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12

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

obtained
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
gcd_Load_2(i1, i3, env, static) -{0,0}> gcd_Load_4(i1, i3, env, static) :|: 0 >= 0
gcd_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, env, static) -{1,1}> gcd_Load_45(i1, i3, env, static) :|: 0 >= 0
gcd_Load_45(i1, i3, env, static) -{0,0}> gcd_Load_46(i1, i3, env, static) :|: 0 >= 0
gcd_Load_46(i1, i3, env, static) -{0,0}> gcd_Load_49(i1, i3, env, static) :|: 0 <= static
gcd_Load_49(i1, i3, env, static) -{0,0}> gcd_Load_50(i1, i3, env, static) :|: 0 >= 0
gcd_Load_50(i1, i3, env, static) -{0,0}> gcd_Load_51(i1, i3, env, static) :|: 0 >= 0
gcd_Load_51(i1, i3, env, static) -{1,1}> gcd_LE_52(i1, i3, env, static) :|: 0 >= 0

obtained
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
by chaining
gcd_LE_52(i1, i12, env, static) -{0,0}> gcd_LE_55(i1, i12, env, static) :|: 1 <= i12
gcd_LE_55(i1, i12, env, static) -{1,1}> gcd_Load_59(i1, i12, env, static) :|: 0 < i12 && 1 <= i12
gcd_Load_59(i1, i12, env, static) -{1,1}> gcd_LE_66(i1, i12, env, static) :|: 1 <= i12
gcd_LE_66(i1, i12, env, static) -{0,0}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12

obtained
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i54 % i43 = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
by chaining
gcd_LE_160(i41, i12, i54, i43, env, static) -{0,0}> gcd_LE_167(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_LE_167(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_172(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 0 < i54 && 1 <= i12
gcd_Load_172(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_178(i41, i12, i43, i54, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_178(i41, i12, i43, i54, env, static) -{1,1}> gcd_Load_181(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_181(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_183(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_183(i41, i12, i54, i43, env, static) -{1,1}> gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_188(i41, i12, i59, i43, env, static) :|: 0 <= i59 && i54 % i43 = i59 && 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_188(i41, i12, i59, i43, env, static) -{1,1}> gcd_Load_190(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_190(i41, i12, i59, i43, env, static) -{1,1}> gcd_Store_192(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Store_192(i41, i12, i43, i59, env, static) -{1,1}> gcd_JMP_194(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_JMP_194(i41, i12, i43, i59, env, static) -{1,1}> gcd_Load_198(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_198(i41, i12, i43, i59, env, static) -{1,1}> gcd_LE_205(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12

obtained
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
by chaining
gcd_LE_205(i41, i12, i73, i43, env, static) -{0,0}> gcd_LE_209(i41, i12, i73, i43, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12 && 0 <= i73
gcd_LE_209(i41, i12, i73, i43, env, static) -{1,1}> gcd_Load_217(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 0 < i73 && 1 <= i43 && 1 <= i12
gcd_Load_217(i41, i12, i43, i73, env, static) -{1,1}> gcd_LE_231(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12
gcd_LE_231(i41, i12, i43, i73, env, static) -{0,0}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12

(8) Obligation:

IntTrs with 7 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, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i54 % i43 = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73

(9) RemoveDivModProof (CONCRETE UPPER BOUND(ID) transformation)

Removed div and mod.

gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i54 % i43 = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
was transformed to
gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i54 - i43 * div < i43 && i54 - i43 * div + i43 > 0 && i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_160'(i41, i12, i54, i43, env, static) :|: i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

(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:
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i54 - i43 * div < i43 && i54 - i43 * div + i43 > 0 && i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_160'(i41, i12, i54, i43, env, static) :|: i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

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

Moved arithmethic from constraints to rhss.

gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
was transformed to
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, 0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12

gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i54 - i43 * div < i43 && i54 - i43 * div + i43 > 0 && i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
was transformed to
gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i54 - i43 * div, i43, env, static) :|: i54 - i43 * div < i43 && i54 - i43 * div + i43 > 0 && i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

(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_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, 0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i54 - i43 * div, i43, env, static) :|: i54 - i43 * div < i43 && i54 - i43 * div + i43 > 0 && i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_160'(i41, i12, i54, i43, env, static) :|: i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

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

Simplified expressions.

gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
was transformed to
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73

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

gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i54 - i43 * div, i43, env, static) :|: i54 - i43 * div < i43 && i54 - i43 * div + i43 > 0 && i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
was transformed to
gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i54 + -1 * i43 * div, i43, env, static) :|: i54 + -1 * i43 * div < i43 && 0 < i54 + -1 * i43 * div + i43 && i54 + -1 * i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_160'(i41, i12, i54, i43, env, static) :|: i54 - i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
was transformed to
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_160'(i41, i12, i54, i43, env, static) :|: i54 + -1 * i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

(14) 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_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_160'(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i54 + -1 * i43 * div, i43, env, static) :|: i54 + -1 * i43 * div < i43 && 0 < i54 + -1 * i43 * div + i43 && i54 + -1 * i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_160'(i41, i12, i54, i43, env, static) :|: i54 + -1 * i43 * div = i59' && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, 0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73

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

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

(16) Obligation:

IntTrs with 47 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, i3, env, static) -{0,0}> gcd_Load_4(i1, i3, env, static) :|: 0 >= 0
gcd_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, env, static) -{1,1}> gcd_Load_45(i1, i3, env, static) :|: 0 >= 0
gcd_Load_45(i1, i3, env, static) -{0,0}> gcd_Load_46(i1, i3, env, static) :|: 0 >= 0
gcd_Load_46(i1, i3, env, static) -{0,0}> gcd_Load_49(i1, i3, env, static) :|: 0 <= static
gcd_Load_49(i1, i3, env, static) -{0,0}> gcd_Load_50(i1, i3, env, static) :|: 0 >= 0
gcd_Load_50(i1, i3, env, static) -{0,0}> gcd_Load_51(i1, i3, env, static) :|: 0 >= 0
gcd_Load_51(i1, i3, env, static) -{1,1}> gcd_LE_52(i1, i3, env, static) :|: 0 >= 0
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_52(i1, i12, env, static) -{0,0}> gcd_LE_55(i1, i12, env, static) :|: 1 <= i12
gcd_LE_55(i1, i12, env, static) -{1,1}> gcd_Load_59(i1, i12, env, static) :|: 0 < i12 && 1 <= i12
gcd_Load_59(i1, i12, env, static) -{1,1}> gcd_LE_66(i1, i12, env, static) :|: 1 <= i12
gcd_LE_66(i1, i12, env, static) -{0,0}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_160(i41, i12, i54, i43, env, static) -{0,0}> gcd_LE_167(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_LE_167(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_172(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 0 < i54 && 1 <= i12
gcd_Load_172(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_178(i41, i12, i43, i54, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_178(i41, i12, i43, i54, env, static) -{1,1}> gcd_Load_181(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_181(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_183(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_183(i41, i12, i54, i43, env, static) -{1,1}> gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_188(i41, i12, i59, i43, env, static) :|: i59 < i43 && 0 <= i59 && 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_188(i41, i12, i59, i43, env, static) -{1,1}> gcd_Load_190(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_190(i41, i12, i59, i43, env, static) -{1,1}> gcd_Store_192(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Store_192(i41, i12, i43, i59, env, static) -{1,1}> gcd_JMP_194(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_JMP_194(i41, i12, i43, i59, env, static) -{1,1}> gcd_Load_198(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_198(i41, i12, i43, i59, env, static) -{1,1}> gcd_LE_205(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{0,0}> gcd_LE_209(i41, i12, i73, i43, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12 && 0 <= i73
gcd_LE_209(i41, i12, i73, i43, env, static) -{1,1}> gcd_Load_217(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 0 < i73 && 1 <= i43 && 1 <= i12
gcd_Load_217(i41, i12, i43, i73, env, static) -{1,1}> gcd_LE_231(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12
gcd_LE_231(i41, i12, i43, i73, env, static) -{0,0}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12

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

obtained
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
gcd_Load_2(i1, i3, env, static) -{0,0}> gcd_Load_4(i1, i3, env, static) :|: 0 >= 0
gcd_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, env, static) -{1,1}> gcd_Load_45(i1, i3, env, static) :|: 0 >= 0
gcd_Load_45(i1, i3, env, static) -{0,0}> gcd_Load_46(i1, i3, env, static) :|: 0 >= 0
gcd_Load_46(i1, i3, env, static) -{0,0}> gcd_Load_49(i1, i3, env, static) :|: 0 <= static
gcd_Load_49(i1, i3, env, static) -{0,0}> gcd_Load_50(i1, i3, env, static) :|: 0 >= 0
gcd_Load_50(i1, i3, env, static) -{0,0}> gcd_Load_51(i1, i3, env, static) :|: 0 >= 0
gcd_Load_51(i1, i3, env, static) -{1,1}> gcd_LE_52(i1, i3, env, static) :|: 0 >= 0

obtained
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
by chaining
gcd_LE_52(i1, i12, env, static) -{0,0}> gcd_LE_55(i1, i12, env, static) :|: 1 <= i12
gcd_LE_55(i1, i12, env, static) -{1,1}> gcd_Load_59(i1, i12, env, static) :|: 0 < i12 && 1 <= i12
gcd_Load_59(i1, i12, env, static) -{1,1}> gcd_LE_66(i1, i12, env, static) :|: 1 <= i12
gcd_LE_66(i1, i12, env, static) -{0,0}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12

obtained
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i59' < i43 && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
by chaining
gcd_LE_160(i41, i12, i54, i43, env, static) -{0,0}> gcd_LE_167(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_LE_167(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_172(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 0 < i54 && 1 <= i12
gcd_Load_172(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_178(i41, i12, i43, i54, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_178(i41, i12, i43, i54, env, static) -{1,1}> gcd_Load_181(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_181(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_183(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_183(i41, i12, i54, i43, env, static) -{1,1}> gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_188(i41, i12, i59, i43, env, static) :|: i59 < i43 && 0 <= i59 && 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_188(i41, i12, i59, i43, env, static) -{1,1}> gcd_Load_190(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_190(i41, i12, i59, i43, env, static) -{1,1}> gcd_Store_192(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Store_192(i41, i12, i43, i59, env, static) -{1,1}> gcd_JMP_194(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_JMP_194(i41, i12, i43, i59, env, static) -{1,1}> gcd_Load_198(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_198(i41, i12, i43, i59, env, static) -{1,1}> gcd_LE_205(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12

obtained
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
by chaining
gcd_LE_205(i41, i12, i73, i43, env, static) -{0,0}> gcd_LE_209(i41, i12, i73, i43, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12 && 0 <= i73
gcd_LE_209(i41, i12, i73, i43, env, static) -{1,1}> gcd_Load_217(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 0 < i73 && 1 <= i43 && 1 <= i12
gcd_Load_217(i41, i12, i43, i73, env, static) -{1,1}> gcd_LE_231(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12
gcd_LE_231(i41, i12, i43, i73, env, static) -{0,0}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12

(18) Obligation:

IntTrs with 7 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, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i59' < i43 && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73

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

Moved arithmethic from constraints to rhss.

gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, iconst_0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
was transformed to
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, 0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12

(20) Obligation:

IntTrs with 7 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, 0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i59' < i43 && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54

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

Simplified expressions.

gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 0 <= i73 && 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73
was transformed to
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73

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

(22) Obligation:

IntTrs with 7 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_LE_52(i1, i12, env, static) -{2,2}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12 && 0 < i12
gcd_LE_160(i41, i12, i53, i43, env, static) -{0,0}> gcd_LE_166(i41, i12, i53, i43, env, static) :|: 1 <= i43 && 1 <= i12 && i53 <= 0
gcd_LE_52(i1, i11, env, static) -{0,0}> gcd_LE_54(i1, i11, env, static) :|: i11 <= 0
gcd_LE_160(i41, i12, i54, i43, env, static) -{11,11}> gcd_LE_205(i41, i12, i59', i43, env, static) :|: i59' < i43 && 1 <= i12 && 1 <= i43 && 0 <= i59' && 1 <= i54 && 0 < i54
gcd_Load_2(i1, i3, env, static) -{16,16}> gcd_LE_52(i1, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
gcd_LE_205(i41, i12, iconst_0, i43, env, static) -{0,0}> gcd_LE_208(i41, i12, 0, i43, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{2,2}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i12 && 1 <= i43 && 1 <= i73 && 0 < i73

(23) TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)) transformation)

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

(24) Obligation:

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

Considered paths: all paths from start

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

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

(26) Obligation:

IntTrs with 44 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i3, env, static) -{0,0}> gcd_Load_4(i1, i3, env, static) :|: 0 >= 0
gcd_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, env, static) -{1,1}> gcd_Load_45(i1, i3, env, static) :|: 0 >= 0
gcd_Load_45(i1, i3, env, static) -{0,0}> gcd_Load_46(i1, i3, env, static) :|: 0 >= 0
gcd_Load_46(i1, i3, env, static) -{0,0}> gcd_Load_49(i1, i3, env, static) :|: 0 <= static
gcd_Load_49(i1, i3, env, static) -{0,0}> gcd_Load_50(i1, i3, env, static) :|: 0 >= 0
gcd_Load_50(i1, i3, env, static) -{0,0}> gcd_Load_51(i1, i3, env, static) :|: 0 >= 0
gcd_Load_51(i1, i3, env, static) -{1,1}> gcd_LE_52(i1, i3, env, static) :|: 0 >= 0
gcd_LE_52(i1, i12, env, static) -{0,0}> gcd_LE_55(i1, i12, env, static) :|: 1 <= i12
gcd_LE_55(i1, i12, env, static) -{1,1}> gcd_Load_59(i1, i12, env, static) :|: 0 < i12 && 1 <= i12
gcd_Load_59(i1, i12, env, static) -{1,1}> gcd_LE_66(i1, i12, env, static) :|: 1 <= i12
gcd_LE_66(i1, i12, env, static) -{0,0}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12
gcd_LE_160(i41, i12, i54, i43, env, static) -{0,0}> gcd_LE_167(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_LE_167(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_172(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 0 < i54 && 1 <= i12
gcd_Load_172(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_178(i41, i12, i43, i54, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_178(i41, i12, i43, i54, env, static) -{1,1}> gcd_Load_181(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_181(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_183(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_183(i41, i12, i54, i43, env, static) -{1,1}> gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_188(i41, i12, i59, i43, env, static) :|: i59 < i43 && 0 <= i59 && 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_188(i41, i12, i59, i43, env, static) -{1,1}> gcd_Load_190(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_190(i41, i12, i59, i43, env, static) -{1,1}> gcd_Store_192(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Store_192(i41, i12, i43, i59, env, static) -{1,1}> gcd_JMP_194(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_JMP_194(i41, i12, i43, i59, env, static) -{1,1}> gcd_Load_198(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_198(i41, i12, i43, i59, env, static) -{1,1}> gcd_LE_205(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{0,0}> gcd_LE_209(i41, i12, i73, i43, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12 && 0 <= i73
gcd_LE_209(i41, i12, i73, i43, env, static) -{1,1}> gcd_Load_217(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 0 < i73 && 1 <= i43 && 1 <= i12
gcd_Load_217(i41, i12, i43, i73, env, static) -{1,1}> gcd_LE_231(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12
gcd_LE_231(i41, i12, i43, i73, env, static) -{0,0}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12

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

obtained
gcd_Load_2(i1, i3, env, static) -{18,18}> gcd_LE_160(i1, i3, i1, i3, env, static'1) :|: 1 <= i3 && 0 < i3 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
gcd_Load_2(i1, i3, env, static) -{0,0}> gcd_Load_4(i1, i3, env, static) :|: 0 >= 0
gcd_Load_4(i1, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i1, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_13(iconst_0, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i1, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i1, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i1, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i1, i3, env, static) -{0,0}> langle_clinit_rangle_New_20(i1, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i1, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_24(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_26(o2, NULL, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i1, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Load_32(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_32(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_35(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i1, i3, env, static) -{1,1}> langle_init_rangle_Return_38(o2, i1, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_38(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(o2, i1, i3, env, static) -{1,1}> langle_clinit_rangle_Return_41(i1, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_41(i1, i3, env, static) -{1,1}> gcd_Load_45(i1, i3, env, static) :|: 0 >= 0
gcd_Load_45(i1, i3, env, static) -{0,0}> gcd_Load_46(i1, i3, env, static) :|: 0 >= 0
gcd_Load_46(i1, i3, env, static) -{0,0}> gcd_Load_49(i1, i3, env, static) :|: 0 <= static
gcd_Load_49(i1, i3, env, static) -{0,0}> gcd_Load_50(i1, i3, env, static) :|: 0 >= 0
gcd_Load_50(i1, i3, env, static) -{0,0}> gcd_Load_51(i1, i3, env, static) :|: 0 >= 0
gcd_Load_51(i1, i3, env, static) -{1,1}> gcd_LE_52(i1, i3, env, static) :|: 0 >= 0
gcd_LE_52(i1, i12, env, static) -{0,0}> gcd_LE_55(i1, i12, env, static) :|: 1 <= i12
gcd_LE_55(i1, i12, env, static) -{1,1}> gcd_Load_59(i1, i12, env, static) :|: 0 < i12 && 1 <= i12
gcd_Load_59(i1, i12, env, static) -{1,1}> gcd_LE_66(i1, i12, env, static) :|: 1 <= i12
gcd_LE_66(i1, i12, env, static) -{0,0}> gcd_LE_160(i1, i12, i1, i12, env, static) :|: 1 <= i12

obtained
gcd_LE_160(i41, i12, i54, i43, env, static) -{13,13}> gcd_LE_160(i41, i12, i43, i59', env, static) :|: i59' < i43 && 1 <= i12 && 0 < i59' && 1 <= i59' && 1 <= i43 && 1 <= i54 && 0 < i54 && 0 <= i59'
by chaining
gcd_LE_160(i41, i12, i54, i43, env, static) -{0,0}> gcd_LE_167(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_LE_167(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_172(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 0 < i54 && 1 <= i12
gcd_Load_172(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_178(i41, i12, i43, i54, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_178(i41, i12, i43, i54, env, static) -{1,1}> gcd_Load_181(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_181(i41, i12, i54, i43, env, static) -{1,1}> gcd_Load_183(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Load_183(i41, i12, i54, i43, env, static) -{1,1}> gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) :|: 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_IntArithmetic_185(i41, i12, i54, i43, env, static) -{1,1}> gcd_Store_188(i41, i12, i59, i43, env, static) :|: i59 < i43 && 0 <= i59 && 1 <= i54 && 1 <= i43 && 1 <= i12
gcd_Store_188(i41, i12, i59, i43, env, static) -{1,1}> gcd_Load_190(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_190(i41, i12, i59, i43, env, static) -{1,1}> gcd_Store_192(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Store_192(i41, i12, i43, i59, env, static) -{1,1}> gcd_JMP_194(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_JMP_194(i41, i12, i43, i59, env, static) -{1,1}> gcd_Load_198(i41, i12, i43, i59, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_Load_198(i41, i12, i43, i59, env, static) -{1,1}> gcd_LE_205(i41, i12, i59, i43, env, static) :|: 0 <= i59 && 1 <= i43 && 1 <= i12
gcd_LE_205(i41, i12, i73, i43, env, static) -{0,0}> gcd_LE_209(i41, i12, i73, i43, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12 && 0 <= i73
gcd_LE_209(i41, i12, i73, i43, env, static) -{1,1}> gcd_Load_217(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 0 < i73 && 1 <= i43 && 1 <= i12
gcd_Load_217(i41, i12, i43, i73, env, static) -{1,1}> gcd_LE_231(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12
gcd_LE_231(i41, i12, i43, i73, env, static) -{0,0}> gcd_LE_160(i41, i12, i43, i73, env, static) :|: 1 <= i73 && 1 <= i43 && 1 <= i12

(28) Obligation:

IntTrs with 2 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i3, env, static) -{18,18}> gcd_LE_160(i1, i3, i1, i3, env, static'1) :|: 1 <= i3 && 0 < i3 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_160(i41, i12, i54, i43, env, static) -{13,13}> gcd_LE_160(i41, i12, i43, i59', env, static) :|: i59' < i43 && 1 <= i12 && 0 < i59' && 1 <= i59' && 1 <= i43 && 1 <= i54 && 0 < i54 && 0 <= i59'

(29) 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_160(x1, x2, x3, x4, x5, x6) → gcd_LE_160(x2, x3, x4)

(30) Obligation:

IntTrs with 2 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i3, static) -{18,18}> gcd_LE_160(i3, i1, i3) :|: 1 <= i3 && 0 < i3 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
gcd_LE_160(i12, i54, i43) -{13,13}> gcd_LE_160(i12, i43, i59') :|: i59' < i43 && 1 <= i12 && 0 < i59' && 1 <= i59' && 1 <= i43 && 1 <= i54 && 0 < i54 && 0 <= i59'

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

Simplified expressions.

gcd_Load_2(i1, i3, static) -{18,18}> gcd_LE_160(i3, i1, i3) :|: 1 <= i3 && 0 < i3 && static'1 <= static''' + 1 && 0 >= 0 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
was transformed to
gcd_Load_2(i1, i3, static) -{18,18}> gcd_LE_160(i3, i1, i3) :|: 1 <= i3 && 0 < i3 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

gcd_LE_160(i12, i54, i43) -{13,13}> gcd_LE_160(i12, i43, i59') :|: i59' < i43 && 1 <= i12 && 0 < i59' && 1 <= i59' && 1 <= i43 && 1 <= i54 && 0 < i54 && 0 <= i59'
was transformed to
gcd_LE_160(i12, i54, i43) -{13,13}> gcd_LE_160(i12, i43, i59') :|: i59' < i43 && 1 <= i12 && 0 < i59' && 1 <= i59' && 1 <= i43 && 1 <= i54 && 0 < i54

(32) Obligation:

IntTrs with 2 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i1, i3, static) -{18,18}> gcd_LE_160(i3, i1, i3) :|: 1 <= i3 && 0 < i3 && static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
gcd_LE_160(i12, i54, i43) -{13,13}> gcd_LE_160(i12, i43, i59') :|: i59' < i43 && 1 <= i12 && 0 < i59' && 1 <= i59' && 1 <= i43 && 1 <= i54 && 0 < i54

(33) koat Proof (EQUIVALENT transformation)

YES(?, 13*ar_1 + 18)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 18) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_1, ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 13) gcd_LE_160(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_0, ar_2, i59')) [ i59' < ar_2 /\ 1 <= ar_0 /\ 0 < i59' /\ 1 <= i59' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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: 18) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_1, ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 13) gcd_LE_160(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_0, ar_2, i59')) [ i59' < ar_2 /\ 1 <= ar_0 /\ 0 < i59' /\ 1 <= i59' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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) = V_2
Pol(gcd_LE_160) = V_3
Pol(koat_start) = V_2
orients all transitions weakly and the transition
gcd_LE_160(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_0, ar_2, i59')) [ i59' < ar_2 /\ 1 <= ar_0 /\ 0 < i59' /\ 1 <= i59' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 ]
strictly and produces the following problem:
3: T:
(Comp: 1, Cost: 18) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_1, ar_0, ar_1)) [ 1 <= ar_1 /\ 0 < ar_1 /\ static'1 <= static''' + 1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ar_1, Cost: 13) gcd_LE_160(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_160(ar_0, ar_2, i59')) [ i59' < ar_2 /\ 1 <= ar_0 /\ 0 < i59' /\ 1 <= i59' /\ 1 <= ar_2 /\ 1 <= ar_1 /\ 0 < ar_1 ]
(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 13*ar_1 + 18

Time: 0.115 sec (SMT: 0.112 sec)

(34) BOUNDS(CONSTANT, 18 + 13 * |#1|)