time complexity proof of /tmp/tmpQcyF6o/GCD2.jar

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

0 JBC problem

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

↳2 JBCTerminationGraph

↳3 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)), 4 ms)

↳4 JBCComplexityEdges

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

    ↳6 WeightedIntTrs

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

        ↳8 WeightedIntTrs

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

        ↳10 WeightedIntTrs

        ↳11 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳12 WeightedIntTrs

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

        ↳14 WeightedIntTrs

        ↳15 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 6 ms)

        ↳16 WeightedIntTrs

    ↳17 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 82 ms)

    ↳18 WeightedIntTrs

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

        ↳20 WeightedIntTrs

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

        ↳22 WeightedIntTrs

        ↳23 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

        ↳24 WeightedIntTrs

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

        ↳26 WeightedIntTrs

        ↳27 ExpressionSimplificationProof (BOTH CONCRETE BOUNDS(ID, ID), 10 ms)

        ↳28 WeightedIntTrs

↳29 TerminationGraphToComplexityProof (BOTH CONCRETE BOUNDS(ID, ADD(9)), 7 ms)

↳30 JBCComplexityEdges

    ↳31 JBCGraphEdgesToCpxIntTrsProof (CONCRETE UPPER BOUND(ID), 105 ms)

    ↳32 WeightedIntTrs

    ↳33 StraightLineCodeCompressionProof (BOTH CONCRETE BOUNDS(ID, ID), 20 ms)

    ↳34 WeightedIntTrs

    ↳35 WeightedIntTrsUnneededArgumentFilterProof (CONCRETE UPPER BOUND(ID), 22 ms)

    ↳36 WeightedIntTrs

    ↳37 LinearizedLhssProof (BOTH CONCRETE BOUNDS(ID, ID), 0 ms)

    ↳38 WeightedIntTrs

    ↳39 RemoveDivModProof (CONCRETE UPPER BOUND(ID), 0 ms)

    ↳40 WeightedIntTrs

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

    ↳42 WeightedIntTrs

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

    ↳44 WeightedIntTrs

    ↳45 koat Proof (⇔, 353 ms)

    ↳46 BOUNDS(CONSTANT, 57 + 34 * |#0| + 34 * |#1|)

(0) Obligation:

Need to prove time_complexity of the following program:

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

  public static int gcd(int a, int b) {
    int tmp;
    while(b != 0 && a >= 0 && b >= 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:
GCD2.gcd(II)I: Graph of 82 nodes with 1 SCC.

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

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

(4) Obligation:

Set of 75 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 75 jbc graph edges to a weighted ITS with 75 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 75 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, i3, env, static) -{0,0}> gcd_Load_3(i2, i3, env, static) :|: 0 >= 0
gcd_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_18(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> gcd_Load_41(i2, i3, env, static) :|: 0 >= 0
gcd_Load_41(i2, i3, env, static) -{0,0}> gcd_Load_42(i2, i3, env, static) :|: 0 >= 0
gcd_Load_42(i2, i3, env, static) -{0,0}> gcd_Load_43(i2, i3, env, static) :|: 0 <= static
gcd_Load_43(i2, i3, env, static) -{0,0}> gcd_Load_45(i2, i3, env, static) :|: 0 >= 0
gcd_Load_45(i2, i3, env, static) -{0,0}> gcd_Load_48(i2, i3, env, static) :|: 0 >= 0
gcd_Load_48(i2, i3, env, static) -{0,0}> gcd_Load_329(i2, i3, i2, i3, env, static) :|: 0 >= 0
gcd_Load_329(i79, i80, i81, i82, env, static) -{1,1}> gcd_EQ_330(i79, i80, i82, i81, env, static) :|: 0 >= 0
gcd_EQ_330(i79, i80, i93, i81, env, static) -{0,0}> gcd_EQ_331(i79, i80, i93, i81, env, static) :|: 0 >= 0
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, iconst_0, i81, env, static) :|: iconst_0 = 0
gcd_EQ_331(i79, i80, i93, i81, env, static) -{1,1}> gcd_Load_333(i79, i80, i81, i93, env, static) :|: !(i93 = 0)
gcd_Load_333(i79, i80, i81, i93, env, static) -{1,1}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1
gcd_LT_335(i79, i80, i99, i93, env, static) -{0,0}> gcd_LT_341(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_LT_341(i79, i80, i99, i93, env, static) -{1,1}> gcd_Load_346(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_Load_346(i79, i80, i99, i93, env, static) -{1,1}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_LT_348(i79, i80, i105, i99, env, static) -{0,0}> gcd_LT_351(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_LT_351(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_355(i79, i80, i99, i105, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_Load_355(i79, i80, i99, i105, env, static) -{1,1}> gcd_Store_357(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Store_357(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_361(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_361(i79, i80, i99, i105, env, static) -{1,1}> gcd_Load_363(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_363(i79, i80, i99, i105, env, static) -{1,1}> gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) -{1,1}> mod_Load_366(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_366(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_367(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_367(i99, i105, i79, i80, env, static) -{1,1}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{0,0}> mod_NE_372(i99, i105, i79, i80, env, static) :|: 0 <= i99 && !(i99 = i105) && 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{0,0}> mod_NE_373(i105, i79, i80, env, static) :|: i99 = i105 && 0 <= i99 && 1 <= i105
mod_NE_372(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_374(i99, i105, i79, i80, env, static) :|: 0 <= i99 && !(i99 = i105) && 1 <= i105
mod_NE_373(i105, i79, i80, env, static) -{1,1}> mod_ConstantStackPush_377(i79, i80, i105, env, static) :|: i105 = i105 && 1 <= i105
mod_Load_374(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_379(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_ConstantStackPush_377(i79, i80, i105, env, static) -{1,1}> mod_Return_380(iconst_0, i79, i80, i105, env, static) :|: iconst_0 = 0 && 1 <= i105
mod_Load_379(i99, i105, i79, i80, env, static) -{1,1}> mod_LE_389(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Return_380(iconst_0, i79, i80, i105, env, static) -{1,1}> gcd_Store_391(i79, i80, iconst_0, i105, env, static) :|: iconst_0 = 0 && 1 <= i105
mod_LE_389(i99, i105, i79, i80, env, static) -{0,0}> mod_LE_460(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Store_391(i79, i80, iconst_0, i105, env, static) -{0,0}> gcd_Store_415(i79, i80, iconst_0, i105, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i105
gcd_Store_415(i79, i80, i99, i105, env, static) -{0,0}> gcd_Store_479(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{0,0}> mod_LE_463(i116, i105, i79, i80, env, static) :|: i116 <= i105 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{0,0}> mod_LE_464(i116, i105, i79, i80, env, static) :|: i105 < i116 && 1 <= i105
mod_LE_463(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_465(i116, i79, i80, i105, env, static) :|: i116 <= i105 && 1 <= i105
mod_LE_464(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_468(i116, i105, i79, i80, env, static) :|: i105 < i116 && 2 <= i116 && 1 <= i105
mod_Load_465(i116, i79, i80, i105, env, static) -{1,1}> mod_Return_471(i116, i79, i80, i105, env, static) :|: 1 <= i105
mod_Load_468(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_472(i116, i105, i79, i80, env, static) :|: 2 <= i116 && 1 <= i105
mod_Return_471(i116, i79, i80, i105, env, static) -{1,1}> gcd_Store_478(i79, i80, i116, i105, env, static) :|: 1 <= i105
mod_Load_472(i116, i105, i79, i80, env, static) -{1,1}> mod_IntArithmetic_481(i116, i105, i79, i80, env, static) :|: 2 <= i116 && 1 <= i105
gcd_Store_478(i79, i80, i116, i105, env, static) -{0,0}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105
gcd_Store_479(i79, i80, i118, i105, env, static) -{1,1}> gcd_Load_482(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_IntArithmetic_481(i116, i105, i79, i80, env, static) -{1,1}> mod_Store_487(i120, i105, i79, i80, env, static) :|: 1 <= i120 && i116 - i105 = i120 && 2 <= i116 && 1 <= i105
gcd_Load_482(i79, i80, i118, i105, env, static) -{1,1}> gcd_Store_488(i79, i80, i105, i118, env, static) :|: 1 <= i105
mod_Store_487(i120, i105, i79, i80, env, static) -{1,1}> mod_JMP_489(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_Store_488(i79, i80, i105, i118, env, static) -{1,1}> gcd_JMP_490(i79, i80, i105, i118, env, static) :|: 1 <= i105
mod_JMP_489(i120, i105, i79, i80, env, static) -{1,1}> mod_Load_493(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_JMP_490(i79, i80, i105, i118, env, static) -{1,1}> gcd_Load_495(i79, i80, i105, i118, env, static) :|: 1 <= i105
mod_Load_493(i120, i105, i79, i80, env, static) -{1,1}> mod_Load_496(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_Load_495(i79, i80, i105, i118, env, static) -{1,1}> gcd_EQ_502(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_Load_496(i120, i105, i79, i80, env, static) -{1,1}> mod_LE_505(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_EQ_502(i79, i80, i118, i105, env, static) -{0,0}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_LE_505(i120, i105, i79, i80, env, static) -{0,0}> mod_LE_460(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105

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

obtained
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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, i3, env, static) -{0,0}> gcd_Load_3(i2, i3, env, static) :|: 0 >= 0
gcd_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_18(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> gcd_Load_41(i2, i3, env, static) :|: 0 >= 0
gcd_Load_41(i2, i3, env, static) -{0,0}> gcd_Load_42(i2, i3, env, static) :|: 0 >= 0
gcd_Load_42(i2, i3, env, static) -{0,0}> gcd_Load_43(i2, i3, env, static) :|: 0 <= static
gcd_Load_43(i2, i3, env, static) -{0,0}> gcd_Load_45(i2, i3, env, static) :|: 0 >= 0
gcd_Load_45(i2, i3, env, static) -{0,0}> gcd_Load_48(i2, i3, env, static) :|: 0 >= 0
gcd_Load_48(i2, i3, env, static) -{0,0}> gcd_Load_329(i2, i3, i2, i3, env, static) :|: 0 >= 0
gcd_Load_329(i79, i80, i81, i82, env, static) -{1,1}> gcd_EQ_330(i79, i80, i82, i81, env, static) :|: 0 >= 0

obtained
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && !(i93 = 0)
by chaining
gcd_EQ_330(i79, i80, i93, i81, env, static) -{0,0}> gcd_EQ_331(i79, i80, i93, i81, env, static) :|: 0 >= 0
gcd_EQ_331(i79, i80, i93, i81, env, static) -{1,1}> gcd_Load_333(i79, i80, i81, i93, env, static) :|: !(i93 = 0)
gcd_Load_333(i79, i80, i81, i93, env, static) -{1,1}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0

obtained
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
by chaining
gcd_LT_335(i79, i80, i99, i93, env, static) -{0,0}> gcd_LT_341(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_LT_341(i79, i80, i99, i93, env, static) -{1,1}> gcd_Load_346(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_Load_346(i79, i80, i99, i93, env, static) -{1,1}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99

obtained
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
by chaining
gcd_LT_348(i79, i80, i105, i99, env, static) -{0,0}> gcd_LT_351(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_LT_351(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_355(i79, i80, i99, i105, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_Load_355(i79, i80, i99, i105, env, static) -{1,1}> gcd_Store_357(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Store_357(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_361(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_361(i79, i80, i99, i105, env, static) -{1,1}> gcd_Load_363(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_363(i79, i80, i99, i105, env, static) -{1,1}> gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) -{1,1}> mod_Load_366(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_366(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_367(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_367(i99, i105, i79, i80, env, static) -{1,1}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105

obtained
mod_NE_371(i99, i99, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99
by chaining
mod_NE_371(i99, i105, i79, i80, env, static) -{0,0}> mod_NE_373(i105, i79, i80, env, static) :|: i99 = i105 && 0 <= i99 && 1 <= i105
mod_NE_373(i105, i79, i80, env, static) -{1,1}> mod_ConstantStackPush_377(i79, i80, i105, env, static) :|: i105 = i105 && 1 <= i105
mod_ConstantStackPush_377(i79, i80, i105, env, static) -{1,1}> mod_Return_380(iconst_0, i79, i80, i105, env, static) :|: iconst_0 = 0 && 1 <= i105
mod_Return_380(iconst_0, i79, i80, i105, env, static) -{1,1}> gcd_Store_391(i79, i80, iconst_0, i105, env, static) :|: iconst_0 = 0 && 1 <= i105
gcd_Store_391(i79, i80, iconst_0, i105, env, static) -{0,0}> gcd_Store_415(i79, i80, iconst_0, i105, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i105
gcd_Store_415(i79, i80, i99, i105, env, static) -{0,0}> gcd_Store_479(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105

obtained
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
by chaining
gcd_Store_479(i79, i80, i118, i105, env, static) -{1,1}> gcd_Load_482(i79, i80, i118, i105, env, static) :|: 1 <= i105
gcd_Load_482(i79, i80, i118, i105, env, static) -{1,1}> gcd_Store_488(i79, i80, i105, i118, env, static) :|: 1 <= i105
gcd_Store_488(i79, i80, i105, i118, env, static) -{1,1}> gcd_JMP_490(i79, i80, i105, i118, env, static) :|: 1 <= i105
gcd_JMP_490(i79, i80, i105, i118, env, static) -{1,1}> gcd_Load_495(i79, i80, i105, i118, env, static) :|: 1 <= i105
gcd_Load_495(i79, i80, i105, i118, env, static) -{1,1}> gcd_EQ_502(i79, i80, i118, i105, env, static) :|: 1 <= i105
gcd_EQ_502(i79, i80, i118, i105, env, static) -{0,0}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105

obtained
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
by chaining
mod_NE_371(i99, i105, i79, i80, env, static) -{0,0}> mod_NE_372(i99, i105, i79, i80, env, static) :|: 0 <= i99 && !(i99 = i105) && 1 <= i105
mod_NE_372(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_374(i99, i105, i79, i80, env, static) :|: 0 <= i99 && !(i99 = i105) && 1 <= i105
mod_Load_374(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_379(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_379(i99, i105, i79, i80, env, static) -{1,1}> mod_LE_389(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_LE_389(i99, i105, i79, i80, env, static) -{0,0}> mod_LE_460(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105

obtained
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i120', i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
by chaining
mod_LE_460(i116, i105, i79, i80, env, static) -{0,0}> mod_LE_464(i116, i105, i79, i80, env, static) :|: i105 < i116 && 1 <= i105
mod_LE_464(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_468(i116, i105, i79, i80, env, static) :|: i105 < i116 && 2 <= i116 && 1 <= i105
mod_Load_468(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_472(i116, i105, i79, i80, env, static) :|: 2 <= i116 && 1 <= i105
mod_Load_472(i116, i105, i79, i80, env, static) -{1,1}> mod_IntArithmetic_481(i116, i105, i79, i80, env, static) :|: 2 <= i116 && 1 <= i105
mod_IntArithmetic_481(i116, i105, i79, i80, env, static) -{1,1}> mod_Store_487(i120, i105, i79, i80, env, static) :|: 1 <= i120 && i116 - i105 = i120 && 2 <= i116 && 1 <= i105
mod_Store_487(i120, i105, i79, i80, env, static) -{1,1}> mod_JMP_489(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
mod_JMP_489(i120, i105, i79, i80, env, static) -{1,1}> mod_Load_493(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
mod_Load_493(i120, i105, i79, i80, env, static) -{1,1}> mod_Load_496(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
mod_Load_496(i120, i105, i79, i80, env, static) -{1,1}> mod_LE_505(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
mod_LE_505(i120, i105, i79, i80, env, static) -{0,0}> mod_LE_460(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105

obtained
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105
by chaining
mod_LE_460(i116, i105, i79, i80, env, static) -{0,0}> mod_LE_463(i116, i105, i79, i80, env, static) :|: i116 <= i105 && 1 <= i105
mod_LE_463(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_465(i116, i79, i80, i105, env, static) :|: i116 <= i105 && 1 <= i105
mod_Load_465(i116, i79, i80, i105, env, static) -{1,1}> mod_Return_471(i116, i79, i80, i105, env, static) :|: 1 <= i105
mod_Return_471(i116, i79, i80, i105, env, static) -{1,1}> gcd_Store_478(i79, i80, i116, i105, env, static) :|: 1 <= i105
gcd_Store_478(i79, i80, i116, i105, env, static) -{0,0}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105

(8) Obligation:

IntTrs with 12 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, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, iconst_0, i81, env, static) :|: iconst_0 = 0
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && !(i93 = 0)
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i99, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i120', i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105

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

Linearized lhss.

mod_NE_371(i99, i99, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99
was transformed to
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99

(10) Obligation:

IntTrs with 12 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, iconst_0, i81, env, static) :|: iconst_0 = 0
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i120', i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && !(i93 = 0)
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1

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

Removed div and mod.

mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
was transformed to
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 > i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 < i105 && 0 <= i99 && 1 <= i105

gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && !(i93 = 0)
was transformed to
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 < 0
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 > 0

(12) Obligation:

IntTrs with 14 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i120', i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 > 0
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 < i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, iconst_0, i81, env, static) :|: iconst_0 = 0
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 > i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 < 0
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99

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

Moved arithmethic from constraints to rhss.

mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i120', i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
was transformed to
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i116 - i105, i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, iconst_0, i81, env, static) :|: iconst_0 = 0
was transformed to
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, 0, i81, env, static) :|: iconst_0 = 0

(14) Obligation:

IntTrs with 14 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i116 - i105, i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 > 0
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 < i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, 0, i81, env, static) :|: iconst_0 = 0
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 > i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 < 0
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99

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

Simplified expressions.

gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 > 0
was transformed to
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 < i93

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

mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i116 - i105, i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
was transformed to
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i116 + -1 * i105, i105, i79, i80, env, static) :|: i116 + -1 * i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 > i105 && 0 <= i99 && 1 <= i105
was transformed to
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i105 < i99 && 0 <= i99 && 1 <= i105

gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 < 0
was transformed to
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: i93 < 0

mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99
was transformed to
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 1 <= i99 && 0 <= i99 && x = i99

(16) Obligation:

IntTrs with 14 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 1 <= i99 && 0 <= i99 && x = i99
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, i2, env, static'1) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 < i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i105 < i99 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 < i93
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: i93 < 0
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, 0, i81, env, static) :|: iconst_0 = 0
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i116 + -1 * i105, i105, i79, i80, env, static) :|: i116 + -1 * i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

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

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

(18) Obligation:

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

(20) Obligation:

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

Linearized lhss.

(22) Obligation:

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

Removed div and mod.

(24) Obligation:

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

Moved arithmethic from constraints to rhss.

(26) Obligation:

IntTrs with 14 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i116 - i105, i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105
gcd_LT_348(i79, i80, i104, i99, env, static) -{0,0}> gcd_LT_350(i79, i80, i104, i99, env, static) :|: i104 <= -1 && 0 <= i99
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 > 0
gcd_LT_335(i79, i80, i98, i93, env, static) -{0,0}> gcd_LT_339(i79, i80, i98, i93, env, static) :|: i98 <= -1
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 < i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, iconst_0, i81, env, static) -{0,0}> gcd_EQ_332(i79, i80, 0, i81, env, static) :|: iconst_0 = 0
gcd_LT_348(i79, i80, i105, i99, env, static) -{8,8}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_LT_335(i79, i80, i99, i93, env, static) -{2,2}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: i99 > i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i79, i80, i93, i81, env, static) -{2,2}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0 && i93 < 0
mod_NE_371(i99, x, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99

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

Simplified expressions.

(28) Obligation:

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

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

(30) Obligation:

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

Used field analysis yielded the following read fields:

Considered paths: all paths from start

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

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

(32) Obligation:

IntTrs with 72 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i2, i3, env, static) -{0,0}> gcd_Load_3(i2, i3, env, static) :|: 0 >= 0
gcd_Load_3(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_5(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_5(i2, i3, env, static) -{1,1}> langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) :|: iconst_0 = 0
langle_clinit_rangle_ArrayCreate_12(iconst_0, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_13(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_15(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_15(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_16(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_18(i2, i3, env, static) -{1,1}> langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) :|: 0 < o2 && o2 = 1
langle_clinit_rangle_Duplicate_20(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_21(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_clinit_rangle_InvokeMethod_23(o2, NULL, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_24(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_24(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_26(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_28(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_28(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_30(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_32(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_32(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_35(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_35(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_37(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_37(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_Return_40(i2, i3, env, static') :|: 0 < o2 && 0 <= o2 && 0 <= static && static' <= static + o2
langle_clinit_rangle_Return_40(i2, i3, env, static) -{1,1}> gcd_Load_41(i2, i3, env, static) :|: 0 >= 0
gcd_Load_41(i2, i3, env, static) -{0,0}> gcd_Load_42(i2, i3, env, static) :|: 0 >= 0
gcd_Load_42(i2, i3, env, static) -{0,0}> gcd_Load_43(i2, i3, env, static) :|: 0 <= static
gcd_Load_43(i2, i3, env, static) -{0,0}> gcd_Load_45(i2, i3, env, static) :|: 0 >= 0
gcd_Load_45(i2, i3, env, static) -{0,0}> gcd_Load_48(i2, i3, env, static) :|: 0 >= 0
gcd_Load_48(i2, i3, env, static) -{0,0}> gcd_Load_329(i2, i3, i2, i3, env, static) :|: 0 >= 0
gcd_Load_329(i79, i80, i81, i82, env, static) -{1,1}> gcd_EQ_330(i79, i80, i82, i81, env, static) :|: 0 >= 0
gcd_EQ_330(i79, i80, i93, i81, env, static) -{0,0}> gcd_EQ_331(i79, i80, i93, i81, env, static) :|: 0 >= 0
gcd_EQ_331(i79, i80, i93, i81, env, static) -{1,1}> gcd_Load_333(i79, i80, i81, i93, env, static) :|: !(i93 = 0)
gcd_Load_333(i79, i80, i81, i93, env, static) -{1,1}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0
gcd_LT_335(i79, i80, i99, i93, env, static) -{0,0}> gcd_LT_341(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_LT_341(i79, i80, i99, i93, env, static) -{1,1}> gcd_Load_346(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_Load_346(i79, i80, i99, i93, env, static) -{1,1}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_LT_348(i79, i80, i105, i99, env, static) -{0,0}> gcd_LT_351(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_LT_351(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_355(i79, i80, i99, i105, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_Load_355(i79, i80, i99, i105, env, static) -{1,1}> gcd_Store_357(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Store_357(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_361(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_361(i79, i80, i99, i105, env, static) -{1,1}> gcd_Load_363(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_363(i79, i80, i99, i105, env, static) -{1,1}> gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) -{1,1}> mod_Load_366(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_366(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_367(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_367(i99, i105, i79, i80, env, static) -{1,1}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{0,0}> mod_NE_372(i99, i105, i79, i80, env, static) :|: 0 <= i99 && !(i99 = i105) && 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{0,0}> mod_NE_373(i105, i79, i80, env, static) :|: i99 = i105 && 0 <= i99 && 1 <= i105
mod_NE_372(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_374(i99, i105, i79, i80, env, static) :|: 0 <= i99 && !(i99 = i105) && 1 <= i105
mod_NE_373(i105, i79, i80, env, static) -{1,1}> mod_ConstantStackPush_377(i79, i80, i105, env, static) :|: i105 = i105 && 1 <= i105
mod_Load_374(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_379(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_ConstantStackPush_377(i79, i80, i105, env, static) -{1,1}> mod_Return_380(iconst_0, i79, i80, i105, env, static) :|: iconst_0 = 0 && 1 <= i105
mod_Load_379(i99, i105, i79, i80, env, static) -{1,1}> mod_LE_389(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Return_380(iconst_0, i79, i80, i105, env, static) -{1,1}> gcd_Store_391(i79, i80, iconst_0, i105, env, static) :|: iconst_0 = 0 && 1 <= i105
mod_LE_389(i99, i105, i79, i80, env, static) -{0,0}> mod_LE_460(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Store_391(i79, i80, iconst_0, i105, env, static) -{0,0}> gcd_Store_415(i79, i80, iconst_0, i105, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 1 <= i105
gcd_Store_415(i79, i80, i99, i105, env, static) -{0,0}> gcd_Store_479(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{0,0}> mod_LE_463(i116, i105, i79, i80, env, static) :|: i116 <= i105 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{0,0}> mod_LE_464(i116, i105, i79, i80, env, static) :|: i105 < i116 && 1 <= i105
mod_LE_463(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_465(i116, i79, i80, i105, env, static) :|: i116 <= i105 && 1 <= i105
mod_LE_464(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_468(i116, i105, i79, i80, env, static) :|: i105 < i116 && 2 <= i116 && 1 <= i105
mod_Load_465(i116, i79, i80, i105, env, static) -{1,1}> mod_Return_471(i116, i79, i80, i105, env, static) :|: 1 <= i105
mod_Load_468(i116, i105, i79, i80, env, static) -{1,1}> mod_Load_472(i116, i105, i79, i80, env, static) :|: 2 <= i116 && 1 <= i105
mod_Return_471(i116, i79, i80, i105, env, static) -{1,1}> gcd_Store_478(i79, i80, i116, i105, env, static) :|: 1 <= i105
mod_Load_472(i116, i105, i79, i80, env, static) -{1,1}> mod_IntArithmetic_481(i116, i105, i79, i80, env, static) :|: 2 <= i116 && 1 <= i105
gcd_Store_478(i79, i80, i116, i105, env, static) -{0,0}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105
gcd_Store_479(i79, i80, i118, i105, env, static) -{1,1}> gcd_Load_482(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_IntArithmetic_481(i116, i105, i79, i80, env, static) -{1,1}> mod_Store_487(i120, i105, i79, i80, env, static) :|: 1 <= i120 && i116 - i105 = i120 && 2 <= i116 && 1 <= i105
gcd_Load_482(i79, i80, i118, i105, env, static) -{1,1}> gcd_Store_488(i79, i80, i105, i118, env, static) :|: 1 <= i105
mod_Store_487(i120, i105, i79, i80, env, static) -{1,1}> mod_JMP_489(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_Store_488(i79, i80, i105, i118, env, static) -{1,1}> gcd_JMP_490(i79, i80, i105, i118, env, static) :|: 1 <= i105
mod_JMP_489(i120, i105, i79, i80, env, static) -{1,1}> mod_Load_493(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_JMP_490(i79, i80, i105, i118, env, static) -{1,1}> gcd_Load_495(i79, i80, i105, i118, env, static) :|: 1 <= i105
mod_Load_493(i120, i105, i79, i80, env, static) -{1,1}> mod_Load_496(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_Load_495(i79, i80, i105, i118, env, static) -{1,1}> gcd_EQ_502(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_Load_496(i120, i105, i79, i80, env, static) -{1,1}> mod_LE_505(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105
gcd_EQ_502(i79, i80, i118, i105, env, static) -{0,0}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_LE_505(i120, i105, i79, i80, env, static) -{0,0}> mod_LE_460(i120, i105, i79, i80, env, static) :|: 1 <= i120 && 1 <= i105

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

obtained
gcd_EQ_330(i79, i80, i93, i81, env, static) -{12,12}> mod_NE_371(i81, i93, i79, i80, env, static) :|: !(i93 = 0) && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
by chaining
gcd_EQ_330(i79, i80, i93, i81, env, static) -{0,0}> gcd_EQ_331(i79, i80, i93, i81, env, static) :|: 0 >= 0
gcd_EQ_331(i79, i80, i93, i81, env, static) -{1,1}> gcd_Load_333(i79, i80, i81, i93, env, static) :|: !(i93 = 0)
gcd_Load_333(i79, i80, i81, i93, env, static) -{1,1}> gcd_LT_335(i79, i80, i81, i93, env, static) :|: 0 >= 0
gcd_LT_335(i79, i80, i99, i93, env, static) -{0,0}> gcd_LT_341(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_LT_341(i79, i80, i99, i93, env, static) -{1,1}> gcd_Load_346(i79, i80, i99, i93, env, static) :|: 0 <= i99
gcd_Load_346(i79, i80, i99, i93, env, static) -{1,1}> gcd_LT_348(i79, i80, i93, i99, env, static) :|: 0 <= i99
gcd_LT_348(i79, i80, i105, i99, env, static) -{0,0}> gcd_LT_351(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_LT_351(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_355(i79, i80, i99, i105, env, static) :|: 0 <= i105 && 0 <= i99 && 1 <= i105
gcd_Load_355(i79, i80, i99, i105, env, static) -{1,1}> gcd_Store_357(i79, i80, i105, i99, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Store_357(i79, i80, i105, i99, env, static) -{1,1}> gcd_Load_361(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_361(i79, i80, i99, i105, env, static) -{1,1}> gcd_Load_363(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_Load_363(i79, i80, i99, i105, env, static) -{1,1}> gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) :|: 0 <= i99 && 1 <= i105
gcd_InvokeMethod_365(i79, i80, i99, i105, env, static) -{1,1}> mod_Load_366(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_366(i99, i105, i79, i80, env, static) -{1,1}> mod_Load_367(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105
mod_Load_367(i99, i105, i79, i80, env, static) -{1,1}> mod_NE_371(i99, i105, i79, i80, env, static) :|: 0 <= i99 && 1 <= i105

(34) Obligation:

IntTrs with 7 rules
Start term: gcd_Load_2(#0, #1, env, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i2, i3, env, static) -{16,16}> gcd_EQ_330(i2, i3, i3, 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_EQ_330(i79, i80, i93, i81, env, static) -{12,12}> mod_NE_371(i81, i93, i79, i80, env, static) :|: !(i93 = 0) && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
mod_NE_371(i99, i99, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, 0, i99, env, static) :|: 0 <= 0 && 1 <= i99 && 0 <= i99
gcd_Store_479(i79, i80, i118, i105, env, static) -{5,5}> gcd_EQ_330(i79, i80, i118, i105, env, static) :|: 1 <= i105
mod_NE_371(i99, i105, i79, i80, env, static) -{3,3}> mod_LE_460(i99, i105, i79, i80, env, static) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105, i79, i80, env, static) -{8,8}> mod_LE_460(i120', i105, i79, i80, env, static) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
mod_LE_460(i116, i105, i79, i80, env, static) -{3,3}> gcd_Store_479(i79, i80, i116, i105, env, static) :|: 1 <= i105 && i116 <= i105

(35) 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_EQ_330(x1, x2, x3, x4, x5, x6) → gcd_EQ_330(x3, x4)
mod_NE_371(x1, x2, x3, x4, x5, x6) → mod_NE_371(x1, x2)
gcd_Store_479(x1, x2, x3, x4, x5, x6) → gcd_Store_479(x3, x4)
mod_LE_460(x1, x2, x3, x4, x5, x6) → mod_LE_460(x1, x2)

(36) Obligation:

IntTrs with 7 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Load_2(i2, i3, static) -{16,16}> gcd_EQ_330(i3, 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_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: !(i93 = 0) && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
mod_NE_371(i99, i99) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99
gcd_Store_479(i118, i105) -{5,5}> gcd_EQ_330(i118, i105) :|: 1 <= i105
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i120', i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
mod_LE_460(i116, i105) -{3,3}> gcd_Store_479(i116, i105) :|: 1 <= i105 && i116 <= i105

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

Linearized lhss.

mod_NE_371(i99, i99) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99
was transformed to
mod_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99

(38) Obligation:

IntTrs with 7 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Store_479(i118, i105) -{5,5}> gcd_EQ_330(i118, i105) :|: 1 <= i105
gcd_Load_2(i2, i3, static) -{16,16}> gcd_EQ_330(i3, 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_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99
mod_LE_460(i116, i105) -{3,3}> gcd_Store_479(i116, i105) :|: 1 <= i105 && i116 <= i105
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i120', i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: !(i93 = 0) && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0

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

Removed div and mod.

mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: !(i99 = i105) && 0 <= i99 && 1 <= i105
was transformed to
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 < i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 > i105 && 0 <= i99 && 1 <= i105

gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: !(i93 = 0) && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
was transformed to
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 < 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 > 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0

(40) Obligation:

IntTrs with 9 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Store_479(i118, i105) -{5,5}> gcd_EQ_330(i118, i105) :|: 1 <= i105
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 < 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
gcd_Load_2(i2, i3, static) -{16,16}> gcd_EQ_330(i3, 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_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 < i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 > i105 && 0 <= i99 && 1 <= i105
mod_LE_460(i116, i105) -{3,3}> gcd_Store_479(i116, i105) :|: 1 <= i105 && i116 <= i105
mod_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 > 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i120', i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

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

Moved arithmethic from constraints to rhss.

mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i120', i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
was transformed to
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i116 - i105, i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

(42) Obligation:

IntTrs with 9 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 < 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
gcd_Store_479(i118, i105) -{5,5}> gcd_EQ_330(i118, i105) :|: 1 <= i105
gcd_Load_2(i2, i3, static) -{16,16}> gcd_EQ_330(i3, 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_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 < i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 > i105 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 > 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
mod_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99
mod_LE_460(i116, i105) -{3,3}> gcd_Store_479(i116, i105) :|: 1 <= i105 && i116 <= i105
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i116 - i105, i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

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

Simplified expressions.

gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 < 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
was transformed to
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 < 0 && 0 <= i81 && 1 <= i93 && 0 <= i93

mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i116 - i105, i105) :|: i116 - i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
was transformed to
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i116 + -1 * i105, i105) :|: i116 + -1 * i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116

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

mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 > i105 && 0 <= i99 && 1 <= i105
was transformed to
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i105 < i99 && 0 <= i99 && 1 <= i105

mod_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 0 <= 0 && 1 <= i99 && 0 <= i99 && x = i99
was transformed to
mod_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 1 <= i99 && 0 <= i99 && x = i99

gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 > 0 && 0 <= i81 && 1 <= i93 && 0 <= i93 && 0 >= 0
was transformed to
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: 0 < i93 && 0 <= i81 && 1 <= i93

(44) Obligation:

IntTrs with 9 rules
Start term: gcd_Load_2(#0, #1, static)
Considered paths: all paths from start
Rules:
gcd_Store_479(i118, i105) -{5,5}> gcd_EQ_330(i118, i105) :|: 1 <= i105
mod_LE_460(i116, i105) -{8,8}> mod_LE_460(i116 + -1 * i105, i105) :|: i116 + -1 * i105 = i120' && 1 <= i120' && 1 <= i105 && 2 <= i116 && i105 < i116
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: 0 < i93 && 0 <= i81 && 1 <= i93
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i99 < i105 && 0 <= i99 && 1 <= i105
mod_NE_371(i99, i105) -{3,3}> mod_LE_460(i99, i105) :|: i105 < i99 && 0 <= i99 && 1 <= i105
gcd_EQ_330(i93, i81) -{12,12}> mod_NE_371(i81, i93) :|: i93 < 0 && 0 <= i81 && 1 <= i93 && 0 <= i93
mod_LE_460(i116, i105) -{3,3}> gcd_Store_479(i116, i105) :|: 1 <= i105 && i116 <= i105
gcd_Load_2(i2, i3, static) -{16,16}> gcd_EQ_330(i3, i2) :|: 0 <= static'1 && 0 <= static && static''' <= static + 2 && 0 <= static''' && static'1 <= static''' + 1
mod_NE_371(i99, x) -{3,3}> gcd_Store_479(0, i99) :|: 1 <= i99 && 0 <= i99 && x = i99

(45) koat Proof (EQUIVALENT transformation)

YES(?, 34*ar_0 + 34*ar_1 + 57)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: ?, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ ar_0 < 0 /\ 0 <= ar_1 /\ 1 <= ar_0 /\ 0 <= ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ?, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 1:
gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ ar_0 < 0 /\ 0 <= ar_1 /\ 1 <= ar_0 /\ 0 <= ar_0 ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: ?, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(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 2 produces the following problem:
3: T:
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: ?, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(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(gcd_Store_479) = V_1 + V_2
Pol(gcd_EQ_330) = V_1 + V_2
Pol(mod_LE_460) = V_1 + V_2
Pol(mod_NE_371) = V_1 + V_2
Pol(gcd_Load_2) = V_1 + V_2
Pol(koat_start) = V_1 + V_2
orients all transitions weakly and the transitions
mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
strictly and produces the following problem:
4: T:
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ 1 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(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

Applied AI with 'oct' on problem 4 to obtain the following invariants:
For symbol gcd_Store_479: X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ -X_1 + X_2 >= 0
For symbol mod_LE_460: X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0
For symbol mod_NE_371: X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ X_1 >= 0

This yielded the following problem:
5: T:
(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 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 ]
start location: koat_start
leaf cost: 0

By chaining the transition koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_Load_2(ar_0, ar_1, ar_2)) [ 0 <= 0 ] with all transitions in problem 5, the following new transition is obtained:
koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= 0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
We thus obtain the following problem:
6: T:
(Comp: 1, Cost: 16) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= 0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: 1, Cost: 16) gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 6:
gcd_Load_2(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
We thus obtain the following problem:
7: T:
(Comp: ?, Cost: 5) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 16) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= 0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
start location: koat_start
leaf cost: 0

By chaining the transition gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 ] with all transitions in problem 7, the following new transition is obtained:
gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
We thus obtain the following problem:
8: T:
(Comp: ?, Cost: 17) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ar_0 + ar_1, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ?, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: ?, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 16) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= 0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 8 produces the following problem:
9: T:
(Comp: ar_0 + ar_1 + 1, Cost: 17) gcd_Store_479(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad')) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ -ar_0 + ar_1 >= 0 /\ 1 <= ar_1 /\ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: ar_0 + ar_1, Cost: 8) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0 - ar_1, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 - ar_1 = i120' /\ 1 <= i120' /\ 1 <= ar_1 /\ 2 <= ar_0 /\ ar_1 < ar_0 ]
(Comp: ar_0 + ar_1 + 1, Cost: 3) mod_LE_460(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ 1 <= ar_1 /\ ar_0 <= ar_1 ]
(Comp: ar_0 + ar_1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(gcd_Store_479(0, ar_0, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ 1 <= ar_0 /\ 0 <= ar_0 /\ ar_1 = ar_0 ]
(Comp: ar_0 + ar_1 + 2, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_1 < ar_0 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 3) mod_NE_371(ar_0, ar_1, ar_2) -> Com_1(mod_LE_460(ar_0, ar_1, arityPad)) [ ar_1 - 1 >= 0 /\ ar_0 + ar_1 - 1 >= 0 /\ ar_0 >= 0 /\ ar_0 < ar_1 /\ 0 <= ar_0 /\ 1 <= ar_1 ]
(Comp: 1, Cost: 12) gcd_EQ_330(ar_0, ar_1, ar_2) -> Com_1(mod_NE_371(ar_1, ar_0, arityPad)) [ 0 < ar_0 /\ 0 <= ar_1 /\ 1 <= ar_0 ]
(Comp: 1, Cost: 16) koat_start(ar_0, ar_1, ar_2) -> Com_1(gcd_EQ_330(ar_1, ar_0, arityPad)) [ 0 <= 0 /\ 0 <= static'1 /\ 0 <= ar_2 /\ static''' <= ar_2 + 2 /\ 0 <= static''' /\ static'1 <= static''' + 1 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 34*ar_0 + 34*ar_1 + 57

Time: 0.601 sec (SMT: 0.525 sec)

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

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

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

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

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

(45) koat Proof (EQUIVALENT transformation)

(46) BOUNDS(CONSTANT, 57 + 34 * |#0| + 34 * |#1|)