time complexity proof of /tmp/tmproVAvr/GCD4.jar

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

0 JBC problem

↳1 JBCToGraph (BOTH CONCRETE BOUNDS(ID, ID), 296 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)), 0 ms)

↳4 JBCComplexityEdges

    ↳5 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 103 ms)

    ↳6 WeightedIntTrs

        ↳7 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 28 ms)

        ↳8 WeightedIntTrs

        ↳9 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳10 WeightedIntTrs

        ↳11 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳12 WeightedIntTrs

        ↳13 koat Proof (⇔, 93 ms)

        ↳14 BOUNDS(CONSTANT, 16 + 20 * |#0| + 78 * |#1|)

    ↳15 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 101 ms)

    ↳16 WeightedIntTrs

        ↳17 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 35 ms)

        ↳18 WeightedIntTrs

        ↳19 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳20 WeightedIntTrs

        ↳21 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

        ↳22 WeightedIntTrs

↳23 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(6)), 0 ms)

↳24 JBCComplexityEdges

    ↳25 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 91 ms)

    ↳26 WeightedIntTrs

    ↳27 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 30 ms)

    ↳28 WeightedIntTrs

    ↳29 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 26 ms)

    ↳30 WeightedIntTrs

    ↳31 MovedArithmeticFromConstraintsProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳32 WeightedIntTrs

    ↳33 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳34 WeightedIntTrs

    ↳35 koat Proof (⇔, 28 ms)

    ↳36 BOUNDS(CONSTANT, 16 + 52 * |#0| + 130 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

public class GCD4 {
  public static int mod(int a, int b) {
    while(a>=b && b > 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:
GCD4.gcd(II)I: Graph of 65 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 60 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 60 jbc graph edges to a weighted ITS with 60 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 60 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Load_2(i2, i4, env, static) -{0,0}> gcd_Load_3(i2, i4, env, static) :|: 0 >= 0
gcd_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_42(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i4, env, static) -{1,1}> gcd_Load_47(i2, i4, env, static) :|: 0 >= 0
gcd_Load_47(i2, i4, env, static) -{0,0}> gcd_Load_48(i2, i4, env, static) :|: 0 >= 0
gcd_Load_48(i2, i4, env, static) -{0,0}> gcd_Load_49(i2, i4, env, static) :|: 0 <= static
gcd_Load_49(i2, i4, env, static) -{0,0}> gcd_Load_50(i2, i4, env, static) :|: 0 >= 0
gcd_Load_50(i2, i4, env, static) -{0,0}> gcd_Load_52(i2, i4, env, static) :|: 0 >= 0
gcd_Load_52(i2, i4, env, static) -{1,1}> gcd_LE_53(i2, i4, env, static) :|: 0 >= 0
gcd_LE_53(i2, i4, env, static) -{0,0}> gcd_LE_135(i2, i4, i4, i2, env, static) :|: 0 >= 0
gcd_LE_135(i27, i28, i39, i29, env, static) -{0,0}> gcd_LE_140(i27, i28, i39, i29, env, static) :|: i39 <= 0
gcd_LE_135(i27, i28, i40, i29, env, static) -{0,0}> gcd_LE_141(i27, i28, i40, i29, env, static) :|: 1 <= i40
gcd_LE_141(i27, i28, i40, i29, env, static) -{1,1}> gcd_Load_145(i27, i28, i29, i40, env, static) :|: 0 < i40 && 1 <= i40
gcd_Load_145(i27, i28, i29, i40, env, static) -{1,1}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40
gcd_LE_151(i27, i28, i45, i40, env, static) -{0,0}> gcd_LE_155(i27, i28, i45, i40, env, static) :|: i45 <= 0 && 1 <= i40
gcd_LE_151(i27, i28, i46, i40, env, static) -{0,0}> gcd_LE_156(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_LE_156(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_160(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40 && 0 < i46
gcd_Load_160(i27, i28, i46, i40, env, static) -{1,1}> gcd_Store_162(i27, i28, i40, i46, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Store_162(i27, i28, i40, i46, env, static) -{1,1}> gcd_Load_164(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_164(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_165(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_165(i27, i28, i46, i40, env, static) -{1,1}> gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) -{1,1}> mod_Load_169(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 1 <= i40
mod_Load_169(i46, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 0 <= i46 && 1 <= i40
mod_Load_220(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_223(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_223(i50, i40, i27, i28, env, static) -{1,1}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{0,0}> mod_LT_242(i50, i40, i27, i28, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{0,0}> mod_LT_243(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50 && i40 <= i50
mod_LT_242(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_244(i50, i27, i28, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
mod_LT_243(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_245(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50 && 1 <= i50 && i40 <= i50
mod_Load_244(i50, i27, i28, i40, env, static) -{1,1}> mod_Return_246(i50, i27, i28, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_245(i50, i40, i27, i28, env, static) -{1,1}> mod_LE_249(i40, i50, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
mod_Return_246(i50, i27, i28, i40, env, static) -{1,1}> gcd_Store_250(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_LE_249(i40, i50, i27, i28, env, static) -{1,1}> mod_Load_252(i50, i40, i27, i28, env, static) :|: 0 < i40 && 1 <= i40 && 1 <= i50
gcd_Store_250(i27, i28, i50, i40, env, static) -{1,1}> gcd_Load_253(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_252(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_256(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
gcd_Load_253(i27, i28, i50, i40, env, static) -{1,1}> gcd_Store_258(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_256(i50, i40, i27, i28, env, static) -{1,1}> mod_IntArithmetic_259(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
gcd_Store_258(i27, i28, i40, i50, env, static) -{1,1}> gcd_JMP_260(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
mod_IntArithmetic_259(i50, i40, i27, i28, env, static) -{1,1}> mod_Store_262(i60, i40, i27, i28, env, static) :|: i50 - i40 = i60 && 1 <= i40 && 0 <= i60 && 1 <= i50
gcd_JMP_260(i27, i28, i40, i50, env, static) -{1,1}> gcd_Load_263(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
mod_Store_262(i60, i40, i27, i28, env, static) -{1,1}> mod_JMP_264(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60
gcd_Load_263(i27, i28, i40, i50, env, static) -{1,1}> gcd_LE_266(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_JMP_264(i60, i40, i27, i28, env, static) -{1,1}> mod_Load_268(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60
gcd_LE_266(i27, i28, i50, i40, env, static) -{0,0}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_268(i60, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60

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

obtained
gcd_Load_2(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, 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(i2, i4, env, static) -{0,0}> gcd_Load_3(i2, i4, env, static) :|: 0 >= 0
gcd_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_42(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i4, env, static) -{1,1}> gcd_Load_47(i2, i4, env, static) :|: 0 >= 0
gcd_Load_47(i2, i4, env, static) -{0,0}> gcd_Load_48(i2, i4, env, static) :|: 0 >= 0
gcd_Load_48(i2, i4, env, static) -{0,0}> gcd_Load_49(i2, i4, env, static) :|: 0 <= static
gcd_Load_49(i2, i4, env, static) -{0,0}> gcd_Load_50(i2, i4, env, static) :|: 0 >= 0
gcd_Load_50(i2, i4, env, static) -{0,0}> gcd_Load_52(i2, i4, env, static) :|: 0 >= 0
gcd_Load_52(i2, i4, env, static) -{1,1}> gcd_LE_53(i2, i4, env, static) :|: 0 >= 0
gcd_LE_53(i2, i4, env, static) -{0,0}> gcd_LE_135(i2, i4, i4, i2, env, static) :|: 0 >= 0

obtained
gcd_LE_135(i27, i28, i40, i29, env, static) -{2,2}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40 && 0 < i40
by chaining
gcd_LE_135(i27, i28, i40, i29, env, static) -{0,0}> gcd_LE_141(i27, i28, i40, i29, env, static) :|: 1 <= i40
gcd_LE_141(i27, i28, i40, i29, env, static) -{1,1}> gcd_Load_145(i27, i28, i29, i40, env, static) :|: 0 < i40 && 1 <= i40
gcd_Load_145(i27, i28, i29, i40, env, static) -{1,1}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40

obtained
gcd_LE_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46 && 0 <= i46
by chaining
gcd_LE_151(i27, i28, i46, i40, env, static) -{0,0}> gcd_LE_156(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_LE_156(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_160(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40 && 0 < i46
gcd_Load_160(i27, i28, i46, i40, env, static) -{1,1}> gcd_Store_162(i27, i28, i40, i46, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Store_162(i27, i28, i40, i46, env, static) -{1,1}> gcd_Load_164(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_164(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_165(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_165(i27, i28, i46, i40, env, static) -{1,1}> gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) -{1,1}> mod_Load_169(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 1 <= i40
mod_Load_169(i46, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 0 <= i46 && 1 <= i40

obtained
mod_Load_220(i50, i40, i27, i28, env, static) -{2,2}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
by chaining
mod_Load_220(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_223(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_223(i50, i40, i27, i28, env, static) -{1,1}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50

obtained
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i60', i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
by chaining
mod_LT_236(i50, i40, i27, i28, env, static) -{0,0}> mod_LT_243(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50 && i40 <= i50
mod_LT_243(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_245(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50 && 1 <= i50 && i40 <= i50
mod_Load_245(i50, i40, i27, i28, env, static) -{1,1}> mod_LE_249(i40, i50, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
mod_LE_249(i40, i50, i27, i28, env, static) -{1,1}> mod_Load_252(i50, i40, i27, i28, env, static) :|: 0 < i40 && 1 <= i40 && 1 <= i50
mod_Load_252(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_256(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
mod_Load_256(i50, i40, i27, i28, env, static) -{1,1}> mod_IntArithmetic_259(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
mod_IntArithmetic_259(i50, i40, i27, i28, env, static) -{1,1}> mod_Store_262(i60, i40, i27, i28, env, static) :|: i50 - i40 = i60 && 1 <= i40 && 0 <= i60 && 1 <= i50
mod_Store_262(i60, i40, i27, i28, env, static) -{1,1}> mod_JMP_264(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60
mod_JMP_264(i60, i40, i27, i28, env, static) -{1,1}> mod_Load_268(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60
mod_Load_268(i60, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60

obtained
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
by chaining
mod_LT_236(i50, i40, i27, i28, env, static) -{0,0}> mod_LT_242(i50, i40, i27, i28, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
mod_LT_242(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_244(i50, i27, i28, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
mod_Load_244(i50, i27, i28, i40, env, static) -{1,1}> mod_Return_246(i50, i27, i28, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Return_246(i50, i27, i28, i40, env, static) -{1,1}> gcd_Store_250(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
gcd_Store_250(i27, i28, i50, i40, env, static) -{1,1}> gcd_Load_253(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
gcd_Load_253(i27, i28, i50, i40, env, static) -{1,1}> gcd_Store_258(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
gcd_Store_258(i27, i28, i40, i50, env, static) -{1,1}> gcd_JMP_260(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
gcd_JMP_260(i27, i28, i40, i50, env, static) -{1,1}> gcd_Load_263(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
gcd_Load_263(i27, i28, i40, i50, env, static) -{1,1}> gcd_LE_266(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
gcd_LE_266(i27, i28, i50, i40, env, static) -{0,0}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50

(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(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, 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_135(i27, i28, i39, i29, env, static) -{0,0}> gcd_LE_140(i27, i28, i39, i29, env, static) :|: i39 <= 0
gcd_LE_135(i27, i28, i40, i29, env, static) -{2,2}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40 && 0 < i40
gcd_LE_151(i27, i28, i45, i40, env, static) -{0,0}> gcd_LE_155(i27, i28, i45, i40, env, static) :|: i45 <= 0 && 1 <= i40
gcd_LE_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46 && 0 <= i46
mod_Load_220(i50, i40, i27, i28, env, static) -{2,2}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i60', i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50

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

Moved arithmethic from constraints to rhss.

mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i60', i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
was transformed to
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i50 - i40, i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50

(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_Load_220(i50, i40, i27, i28, env, static) -{2,2}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
gcd_Load_2(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, 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_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46 && 0 <= i46
gcd_LE_151(i27, i28, i45, i40, env, static) -{0,0}> gcd_LE_155(i27, i28, i45, i40, env, static) :|: i45 <= 0 && 1 <= i40
gcd_LE_135(i27, i28, i40, i29, env, static) -{2,2}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40 && 0 < i40
gcd_LE_135(i27, i28, i39, i29, env, static) -{0,0}> gcd_LE_140(i27, i28, i39, i29, env, static) :|: i39 <= 0
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i50 - i40, i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50

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

Simplified expressions.

gcd_Load_2(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, 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(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

gcd_LE_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46 && 0 <= i46
was transformed to
gcd_LE_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46

mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i50 - i40, i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
was transformed to
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i50 + -1 * i40, i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 + -1 * i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50

(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:
mod_Load_220(i50, i40, i27, i28, env, static) -{2,2}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i50 + -1 * i40, i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 + -1 * i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
gcd_LE_151(i27, i28, i45, i40, env, static) -{0,0}> gcd_LE_155(i27, i28, i45, i40, env, static) :|: i45 <= 0 && 1 <= i40
gcd_LE_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46
gcd_LE_135(i27, i28, i39, i29, env, static) -{0,0}> gcd_LE_140(i27, i28, i39, i29, env, static) :|: i39 <= 0
gcd_LE_135(i27, i28, i40, i29, env, static) -{2,2}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40 && 0 < i40
gcd_Load_2(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50

(13) koat Proof (EQUIVALENT transformation)

YES(?, 78*ar_1 + 20*ar_0 + 16)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3, ar_4, ar_5)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 0) gcd_LE_151(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
(Comp: ?, Cost: 6) gcd_LE_151(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1, ar_4, ar_5)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 0) gcd_LE_135(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ ar_2 <= 0 ]
(Comp: ?, Cost: 2) gcd_LE_135(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2, ar_4, ar_5)) [ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: ?, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(gcd_LE_135(ar_0, ar_1, ar_1, ar_0, ar_2, static'1)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1, ar_4, ar_5)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2, ar_3, ar_4, ar_5)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Slicing away variables that do not contribute to conditions from problem 1 leaves variables [ar_0, ar_1, ar_2, ar_3].
We thus obtain the following problem:
2: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_0, ar_1, ar_1, ar_0)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: ?, Cost: 0) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 ]
(Comp: ?, Cost: 6) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 0) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_0, ar_1, ar_1, ar_0)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: ?, Cost: 0) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 ]
(Comp: ?, Cost: 6) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
(Comp: ?, Cost: 0) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 1
Pol(gcd_Load_2) = 1
Pol(mod_LT_236) = 1
Pol(gcd_LE_135) = 1
Pol(gcd_LE_151) = 1
Pol(gcd_LE_140) = 0
Pol(mod_Load_220) = 1
Pol(gcd_LE_155) = 0
orients all transitions weakly and the transitions
gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 ]
strictly and produces the following problem:
4: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_0, ar_1, ar_1, ar_0)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 2) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: 1, Cost: 0) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 ]
(Comp: ?, Cost: 6) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 3*V_2
Pol(gcd_Load_2) = 3*V_2
Pol(mod_LT_236) = 3*V_2 - 2
Pol(gcd_LE_135) = 3*V_3
Pol(gcd_LE_151) = 3*V_4 - 1
Pol(gcd_LE_140) = 3*V_3
Pol(mod_Load_220) = 3*V_2 - 2
Pol(gcd_LE_155) = 3*V_4 - 1
orients all transitions weakly and the transitions
mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 < ar_2 ]
strictly and produces the following problem:
5: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 3*ar_1, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_0, ar_1, ar_1, ar_0)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 3*ar_1, Cost: 2) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: 1, Cost: 0) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 ]
(Comp: 3*ar_1, Cost: 6) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(koat_start) = 2*V_1 + 3*V_2
Pol(gcd_Load_2) = 2*V_1 + 3*V_2
Pol(mod_LT_236) = 2*V_1 + 3*V_2 - 1
Pol(gcd_LE_135) = 3*V_3 + 2*V_4
Pol(gcd_LE_151) = 2*V_3 + 3*V_4
Pol(gcd_LE_140) = 3*V_3 + 2*V_4
Pol(mod_Load_220) = 2*V_1 + 3*V_2
Pol(gcd_LE_155) = 2*V_3 + 3*V_4
orients all transitions weakly and the transitions
mod_Load_220(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
strictly and produces the following problem:
6: T:
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2, ar_3)) [ 0 <= 0 ]
(Comp: 3*ar_1, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_2, ar_3, ar_0, ar_1)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_135(ar_0, ar_1, ar_1, ar_0)) [ 0 <= static'1 /\ 0 <= ar_3 /\ static''' <= ar_3 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 3*ar_1, Cost: 2) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_151(ar_0, ar_1, ar_3, ar_2)) [ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: 1, Cost: 0) gcd_LE_135(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_140(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 ]
(Comp: 3*ar_1, Cost: 6) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_2, ar_3, ar_0, ar_1)) [ 1 <= ar_3 /\ 0 < ar_2 /\ 1 <= ar_2 ]
(Comp: 1, Cost: 0) gcd_LE_151(ar_0, ar_1, ar_2, ar_3) -> Com_1(gcd_LE_155(ar_0, ar_1, ar_2, ar_3)) [ ar_2 <= 0 /\ 1 <= ar_3 ]
(Comp: 2*ar_0 + 3*ar_1, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, ar_2, ar_3)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 3*ar_1, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2, ar_3) -> Com_1(mod_LT_236(ar_0, ar_1, ar_2, ar_3)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 78*ar_1 + 20*ar_0 + 16

Time: 0.176 sec (SMT: 0.153 sec)

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

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

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

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

(18) Obligation:

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

Moved arithmethic from constraints to rhss.

(20) Obligation:

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

Simplified expressions.

(22) 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_Load_220(i50, i40, i27, i28, env, static) -{2,2}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i50 + -1 * i40, i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 + -1 * i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
gcd_LE_151(i27, i28, i45, i40, env, static) -{0,0}> gcd_LE_155(i27, i28, i45, i40, env, static) :|: i45 <= 0 && 1 <= i40
gcd_LE_151(i27, i28, i46, i40, env, static) -{6,6}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i40 && 0 < i46 && 1 <= i46
gcd_LE_135(i27, i28, i39, i29, env, static) -{0,0}> gcd_LE_140(i27, i28, i39, i29, env, static) :|: i39 <= 0
gcd_LE_135(i27, i28, i40, i29, env, static) -{2,2}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40 && 0 < i40
gcd_Load_2(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50

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

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

(24) Obligation:

Set of 58 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 58 jbc graph edges to a weighted ITS with 58 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 58 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i2, i4, env, static) -{0,0}> gcd_Load_3(i2, i4, env, static) :|: 0 >= 0
gcd_Load_3(i2, i4, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(i2, i4, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_14(iconst_0, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_16(a2, i2, i4, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_17(i2, i4, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_17(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i4, env, static) :|: 0 >= 0
langle_clinit_rangle_New_19(i2, i4, env, static) -{0,0}> langle_clinit_rangle_New_20(i2, i4, env, static) :|: 0 <= static
langle_clinit_rangle_New_20(i2, i4, env, static) -{1,1}> langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_22(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_25(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_25(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_27(o2, NULL, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i4, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_28(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Load_33(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Load_33(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_36(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_37(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_37(o2, i2, i4, env, static) -{1,1}> langle_init_rangle_Return_40(o2, i2, i4, env, static) :|: 0 < o2
langle_init_rangle_Return_40(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_42(o2, i2, i4, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_42(o2, i2, i4, env, static) -{1,1}> langle_clinit_rangle_Return_44(i2, i4, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_44(i2, i4, env, static) -{1,1}> gcd_Load_47(i2, i4, env, static) :|: 0 >= 0
gcd_Load_47(i2, i4, env, static) -{0,0}> gcd_Load_48(i2, i4, env, static) :|: 0 >= 0
gcd_Load_48(i2, i4, env, static) -{0,0}> gcd_Load_49(i2, i4, env, static) :|: 0 <= static
gcd_Load_49(i2, i4, env, static) -{0,0}> gcd_Load_50(i2, i4, env, static) :|: 0 >= 0
gcd_Load_50(i2, i4, env, static) -{0,0}> gcd_Load_52(i2, i4, env, static) :|: 0 >= 0
gcd_Load_52(i2, i4, env, static) -{1,1}> gcd_LE_53(i2, i4, env, static) :|: 0 >= 0
gcd_LE_53(i2, i4, env, static) -{0,0}> gcd_LE_135(i2, i4, i4, i2, env, static) :|: 0 >= 0
gcd_LE_135(i27, i28, i40, i29, env, static) -{0,0}> gcd_LE_141(i27, i28, i40, i29, env, static) :|: 1 <= i40
gcd_LE_141(i27, i28, i40, i29, env, static) -{1,1}> gcd_Load_145(i27, i28, i29, i40, env, static) :|: 0 < i40 && 1 <= i40
gcd_Load_145(i27, i28, i29, i40, env, static) -{1,1}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40
gcd_LE_151(i27, i28, i46, i40, env, static) -{0,0}> gcd_LE_156(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_LE_156(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_160(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40 && 0 < i46
gcd_Load_160(i27, i28, i46, i40, env, static) -{1,1}> gcd_Store_162(i27, i28, i40, i46, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Store_162(i27, i28, i40, i46, env, static) -{1,1}> gcd_Load_164(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_164(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_165(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_165(i27, i28, i46, i40, env, static) -{1,1}> gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) -{1,1}> mod_Load_169(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 1 <= i40
mod_Load_169(i46, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 0 <= i46 && 1 <= i40
mod_Load_220(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_223(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_223(i50, i40, i27, i28, env, static) -{1,1}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{0,0}> mod_LT_242(i50, i40, i27, i28, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{0,0}> mod_LT_243(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50 && i40 <= i50
mod_LT_242(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_244(i50, i27, i28, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50
mod_LT_243(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_245(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50 && 1 <= i50 && i40 <= i50
mod_Load_244(i50, i27, i28, i40, env, static) -{1,1}> mod_Return_246(i50, i27, i28, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_245(i50, i40, i27, i28, env, static) -{1,1}> mod_LE_249(i40, i50, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
mod_Return_246(i50, i27, i28, i40, env, static) -{1,1}> gcd_Store_250(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_LE_249(i40, i50, i27, i28, env, static) -{1,1}> mod_Load_252(i50, i40, i27, i28, env, static) :|: 0 < i40 && 1 <= i40 && 1 <= i50
gcd_Store_250(i27, i28, i50, i40, env, static) -{1,1}> gcd_Load_253(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_252(i50, i40, i27, i28, env, static) -{1,1}> mod_Load_256(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
gcd_Load_253(i27, i28, i50, i40, env, static) -{1,1}> gcd_Store_258(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_256(i50, i40, i27, i28, env, static) -{1,1}> mod_IntArithmetic_259(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 1 <= i50
gcd_Store_258(i27, i28, i40, i50, env, static) -{1,1}> gcd_JMP_260(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
mod_IntArithmetic_259(i50, i40, i27, i28, env, static) -{1,1}> mod_Store_262(i60, i40, i27, i28, env, static) :|: i50 - i40 = i60 && 1 <= i40 && 0 <= i60 && 1 <= i50
gcd_JMP_260(i27, i28, i40, i50, env, static) -{1,1}> gcd_Load_263(i27, i28, i40, i50, env, static) :|: 1 <= i40 && 0 <= i50
mod_Store_262(i60, i40, i27, i28, env, static) -{1,1}> mod_JMP_264(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60
gcd_Load_263(i27, i28, i40, i50, env, static) -{1,1}> gcd_LE_266(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_JMP_264(i60, i40, i27, i28, env, static) -{1,1}> mod_Load_268(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60
gcd_LE_266(i27, i28, i50, i40, env, static) -{0,0}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: 1 <= i40 && 0 <= i50
mod_Load_268(i60, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i60, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i60

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

obtained
gcd_LE_135(i27, i28, i40, i29, env, static) -{8,8}> mod_Load_220(i29, i40, i27, i28, env, static) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 <= i29 && 0 < i40
by chaining
gcd_LE_135(i27, i28, i40, i29, env, static) -{0,0}> gcd_LE_141(i27, i28, i40, i29, env, static) :|: 1 <= i40
gcd_LE_141(i27, i28, i40, i29, env, static) -{1,1}> gcd_Load_145(i27, i28, i29, i40, env, static) :|: 0 < i40 && 1 <= i40
gcd_Load_145(i27, i28, i29, i40, env, static) -{1,1}> gcd_LE_151(i27, i28, i29, i40, env, static) :|: 1 <= i40
gcd_LE_151(i27, i28, i46, i40, env, static) -{0,0}> gcd_LE_156(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_LE_156(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_160(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40 && 0 < i46
gcd_Load_160(i27, i28, i46, i40, env, static) -{1,1}> gcd_Store_162(i27, i28, i40, i46, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Store_162(i27, i28, i40, i46, env, static) -{1,1}> gcd_Load_164(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_164(i27, i28, i46, i40, env, static) -{1,1}> gcd_Load_165(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_Load_165(i27, i28, i46, i40, env, static) -{1,1}> gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) :|: 1 <= i46 && 1 <= i40
gcd_InvokeMethod_167(i27, i28, i46, i40, env, static) -{1,1}> mod_Load_169(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 1 <= i40
mod_Load_169(i46, i40, i27, i28, env, static) -{0,0}> mod_Load_220(i46, i40, i27, i28, env, static) :|: 1 <= i46 && 0 <= i46 && 1 <= i40

(28) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i2, i4, env, static) -{16,16}> gcd_LE_135(i2, i4, i4, i2, 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_135(i27, i28, i40, i29, env, static) -{8,8}> mod_Load_220(i29, i40, i27, i28, env, static) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 <= i29 && 0 < i40
mod_Load_220(i50, i40, i27, i28, env, static) -{2,2}> mod_LT_236(i50, i40, i27, i28, env, static) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> mod_Load_220(i60', i40, i27, i28, env, static) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
mod_LT_236(i50, i40, i27, i28, env, static) -{8,8}> gcd_LE_135(i27, i28, i50, i40, env, static) :|: i50 < i40 && 1 <= i40 && 0 <= i50

(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_135(x1, x2, x3, x4, x5, x6) → gcd_LE_135(x3, x4)
mod_Load_220(x1, x2, x3, x4, x5, x6) → mod_Load_220(x1, x2)
mod_LT_236(x1, x2, x3, x4, x5, x6) → mod_LT_236(x1, x2)

(30) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i2, i4, static) -{16,16}> gcd_LE_135(i4, i2) :|: 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_135(i40, i29) -{8,8}> mod_Load_220(i29, i40) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 <= i29 && 0 < i40
mod_Load_220(i50, i40) -{2,2}> mod_LT_236(i50, i40) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i60', i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
mod_LT_236(i50, i40) -{8,8}> gcd_LE_135(i50, i40) :|: i50 < i40 && 1 <= i40 && 0 <= i50

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

Moved arithmethic from constraints to rhss.

mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i60', i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
was transformed to
mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i50 - i40, i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50

(32) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_LE_135(i40, i29) -{8,8}> mod_Load_220(i29, i40) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 <= i29 && 0 < i40
mod_LT_236(i50, i40) -{8,8}> gcd_LE_135(i50, i40) :|: i50 < i40 && 1 <= i40 && 0 <= i50
gcd_Load_2(i2, i4, static) -{16,16}> gcd_LE_135(i4, i2) :|: 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_Load_220(i50, i40) -{2,2}> mod_LT_236(i50, i40) :|: 1 <= i40 && 0 <= i50
mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i50 - i40, i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50

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

Simplified expressions.

gcd_LE_135(i40, i29) -{8,8}> mod_Load_220(i29, i40) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 <= i29 && 0 < i40
was transformed to
gcd_LE_135(i40, i29) -{8,8}> mod_Load_220(i29, i40) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 < i40

gcd_Load_2(i2, i4, static) -{16,16}> gcd_LE_135(i4, i2) :|: 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(i2, i4, static) -{16,16}> gcd_LE_135(i4, i2) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i50 - i40, i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 - i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
was transformed to
mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i50 + -1 * i40, i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 + -1 * i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50

(34) Obligation:

IntTrs with 5 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
mod_LT_236(i50, i40) -{8,8}> mod_Load_220(i50 + -1 * i40, i40) :|: i40 <= i50 && 1 <= i40 && 0 <= i60' && i50 + -1 * i40 = i60' && 0 <= i50 && 0 < i40 && 1 <= i50
mod_LT_236(i50, i40) -{8,8}> gcd_LE_135(i50, i40) :|: i50 < i40 && 1 <= i40 && 0 <= i50
gcd_LE_135(i40, i29) -{8,8}> mod_Load_220(i29, i40) :|: 0 < i29 && 1 <= i40 && 1 <= i29 && 0 < i40
mod_Load_220(i50, i40) -{2,2}> mod_LT_236(i50, i40) :|: 1 <= i40 && 0 <= i50
gcd_Load_2(i2, i4, static) -{16,16}> gcd_LE_135(i4, i2) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1

(35) koat Proof (EQUIVALENT transformation)

YES(?, 52*ar_0 + 130*ar_1 + 16)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 8) gcd_LE_135(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_1, ar_0, arityPad)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2) -> Com_1(mod_LT_236(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 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: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 8) gcd_LE_135(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_1, ar_0, arityPad)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: ?, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2) -> Com_1(mod_LT_236(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 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(mod_LT_236) = 2*V_1 + 5*V_2 - 2
Pol(mod_Load_220) = 2*V_1 + 5*V_2 - 1
Pol(gcd_LE_135) = 5*V_1 + 2*V_2
Pol(gcd_Load_2) = 2*V_1 + 5*V_2
Pol(koat_start) = 2*V_1 + 5*V_2
orients all transitions weakly and the transitions
mod_Load_220(ar_0, ar_1, ar_2) -> Com_1(mod_LT_236(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
gcd_LE_135(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_1, ar_0, arityPad)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
strictly and produces the following problem:
3: T:
(Comp: 2*ar_0 + 5*ar_1, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 <= ar_0 /\ 1 <= ar_1 /\ 0 <= i60' /\ ar_0 - ar_1 = i60' /\ 0 <= ar_0 /\ 0 < ar_1 /\ 1 <= ar_0 ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 8) mod_LT_236(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 8) gcd_LE_135(ar_0, ar_1, ar_2) -> Com_1(mod_Load_220(ar_1, ar_0, arityPad)) [ 0 < ar_1 /\ 1 <= ar_0 /\ 1 <= ar_1 /\ 0 < ar_0 ]
(Comp: 2*ar_0 + 5*ar_1, Cost: 2) mod_Load_220(ar_0, ar_1, ar_2) -> Com_1(mod_LT_236(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ 0 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_LE_135(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 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 52*ar_0 + 130*ar_1 + 16

Time: 0.118 sec (SMT: 0.099 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

(13) koat Proof (EQUIVALENT transformation)

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

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

(35) koat Proof (EQUIVALENT transformation)

(36) BOUNDS(CONSTANT, 16 + 52 * |#0| + 130 * |#1|)