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

(0) Obligation:

Need to prove time_complexity of the following program:

/**
 * Abstract class to provide some additional mathematical functions
 * which are not provided by java.lang.Math.
 *
 * @author fuhs
 */
public abstract class AProVEMath {

  /**
   * Returns <code>base<sup>exponent</sup></code>.
   * Works considerably faster than java.lang.Math.pow(double, double).
   *
   * @param base base of the power
   * @param exponent non-negative exponent of the power
   * @return base<sup>exponent</sup>
   */
  public static int power (int base, int exponent) {
    if (exponent == 0) {
      return 1;
    }
    else if (exponent == 1) {
      return base;
    }
    else if (base == 2) {
      return base << (exponent-1);
    }
    else {
      int result = 1;
      while (exponent > 0) {
        if (exponent % 2 == 1) {
          result *= base;
        }
        base *= base;
        exponent /= 2;
      }
      return result;
    }
  }

}

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

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
AProVEMath.power(II)I: Graph of 115 nodes with 1 SCC.

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

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

(4) Obligation:

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

• Used field analysis yielded the following read fields:
  

Considered paths: all paths from start

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

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

(6) Obligation:

IntTrs with 69 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
power_Load_1(i2, i3, env, static) -{0,0}> power_Load_4(i2, i3, env, static) :|: 0 >= 0
power_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(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_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(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_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(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_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> power_Load_45(i2, i3, env, static) :|: 0 >= 0
power_Load_45(i2, i3, env, static) -{0,0}> power_Load_46(i2, i3, env, static) :|: 0 >= 0
power_Load_46(i2, i3, env, static) -{0,0}> power_Load_49(i2, i3, env, static) :|: 0 <= static
power_Load_49(i2, i3, env, static) -{0,0}> power_Load_50(i2, i3, env, static) :|: 0 >= 0
power_Load_50(i2, i3, env, static) -{0,0}> power_Load_51(i2, i3, env, static) :|: 0 >= 0
power_Load_51(i2, i3, env, static) -{1,1}> power_NE_52(i2, i3, env, static) :|: 0 >= 0
power_NE_52(i2, i8, env, static) -{0,0}> power_NE_54(i2, i8, env, static) :|: 0 >= 0
power_NE_54(i2, i8, env, static) -{1,1}> power_Load_56(i2, i8, env, static) :|: !(i8 = 0)
power_Load_56(i2, i8, env, static) -{1,1}> power_ConstantStackPush_59(i2, i8, env, static) :|: 0 >= 0
power_ConstantStackPush_59(i2, i8, env, static) -{1,1}> power_NE_70(i2, i8, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i16, iconst_1, env, static) -{0,0}> power_NE_76(i2, i16, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i16
power_NE_76(i2, i16, iconst_1, env, static) -{1,1}> power_Load_117(i2, i16, env, static) :|: iconst_1 = 1 && iconst_1 < i16 && 2 <= i16
power_Load_117(i2, i16, env, static) -{1,1}> power_ConstantStackPush_124(i2, i16, env, static) :|: 2 <= i16
power_ConstantStackPush_124(i2, i16, env, static) -{1,1}> power_NE_146(i2, i16, iconst_2, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_146(i37, i16, iconst_2, env, static) -{0,0}> power_NE_151(i37, i16, iconst_2, env, static) :|: i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_146(i38, i16, iconst_2, env, static) -{0,0}> power_NE_153(i38, i16, iconst_2, env, static) :|: 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_NE_151(i37, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_181(i37, i16, env, static) :|: i37 < iconst_2 && i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_153(i38, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_201(i38, i16, env, static) :|: iconst_2 < i38 && 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_181(i37, i16, env, static) -{1,1}> power_Store_217(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_ConstantStackPush_201(i38, i16, env, static) -{1,1}> power_Store_225(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Store_217(i37, i16, iconst_1, env, static) -{1,1}> power_Load_237(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Store_225(i38, i16, iconst_1, env, static) -{1,1}> power_Load_240(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Load_237(i37, i16, iconst_1, env, static) -{0,0}> power_Load_511(i37, i16, i37, i16, iconst_1, env, static) :|: iconst_1 <= 1 && 1 <= i16 && iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_240(i38, i16, iconst_1, env, static) -{0,0}> power_Load_646(i38, i16, i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 0 <= i16 && 3 <= i38 && 2 <= i16
power_Load_511(i37, i16, i100, i108, i80, env, static) -{0,0}> power_Load_646(i37, i16, i100, i108, i80, env, static) :|: i80 <= 1 && 1 <= i108 && 0 <= i108 && i37 <= 1 && 2 <= i16
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{0,0}> power_LE_659(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && 0 <= i226
power_LE_659(i206, i16, i226, i207, i209, env, static) -{1,1}> power_Load_665(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 0 < i226 && 2 <= i16
power_Load_665(i206, i16, i207, i226, i209, env, static) -{1,1}> power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) -{1,1}> power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) -{1,1}> power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) :|: i231 < iconst_2 && 1 <= i226 && 0 <= i231 && i231 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) -{1,1}> power_NE_686(i206, i16, i231, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && iconst_1 = 1 && i231 <= 1 && 2 <= i16
power_NE_686(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) :|: 0 <= iconst_0 && 1 <= i226 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_686(i206, i16, iconst_1, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1 && 2 <= i16
power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_705(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_719(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && 2 <= i16
power_Load_705(i206, i16, i207, i226, i209, env, static) -{0,0}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_719(i206, i16, i207, i226, i209, env, static) -{1,1}> power_Load_740(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_740(i206, i16, i209, i207, i226, env, static) -{1,1}> power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) -{1,1}> power_Store_784(i206, i16, i258, i207, i226, env, static) :|: 1 <= i226 && i209 * i207 = i258 && 2 <= i16
power_Store_784(i206, i16, i258, i207, i226, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_795(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Load_797(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_797(i206, i16, i207, i226, i258, env, static) -{1,1}> power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Store_803(i206, i16, i267, i226, i258, env, static) :|: i207 * i207 = i267 && 1 <= i226 && 2 <= i16
power_Store_803(i206, i16, i267, i226, i258, env, static) -{1,1}> power_Load_805(i206, i16, i267, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_805(i206, i16, i267, i226, i258, env, static) -{1,1}> power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) -{1,1}> power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) -{1,1}> power_Store_843(i206, i16, i268, i267, i258, env, static) :|: i268 < i226 && 0 <= i268 && 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_Store_843(i206, i16, i268, i267, i258, env, static) -{1,1}> power_JMP_845(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_JMP_845(i206, i16, i267, i268, i258, env, static) -{1,1}> power_Load_851(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_Load_851(i206, i16, i267, i268, i258, env, static) -{0,0}> power_Load_646(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16

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

obtained
power_Load_1(i2, i3, env, static) -{22,22}> power_NE_146(i2, i3, 2, env, static'1) :|: !(i3 = 0) && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
by chaining
power_Load_1(i2, i3, env, static) -{0,0}> power_Load_4(i2, i3, env, static) :|: 0 >= 0
power_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(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_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(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_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(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_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> power_Load_45(i2, i3, env, static) :|: 0 >= 0
power_Load_45(i2, i3, env, static) -{0,0}> power_Load_46(i2, i3, env, static) :|: 0 >= 0
power_Load_46(i2, i3, env, static) -{0,0}> power_Load_49(i2, i3, env, static) :|: 0 <= static
power_Load_49(i2, i3, env, static) -{0,0}> power_Load_50(i2, i3, env, static) :|: 0 >= 0
power_Load_50(i2, i3, env, static) -{0,0}> power_Load_51(i2, i3, env, static) :|: 0 >= 0
power_Load_51(i2, i3, env, static) -{1,1}> power_NE_52(i2, i3, env, static) :|: 0 >= 0
power_NE_52(i2, i8, env, static) -{0,0}> power_NE_54(i2, i8, env, static) :|: 0 >= 0
power_NE_54(i2, i8, env, static) -{1,1}> power_Load_56(i2, i8, env, static) :|: !(i8 = 0)
power_Load_56(i2, i8, env, static) -{1,1}> power_ConstantStackPush_59(i2, i8, env, static) :|: 0 >= 0
power_ConstantStackPush_59(i2, i8, env, static) -{1,1}> power_NE_70(i2, i8, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i16, iconst_1, env, static) -{0,0}> power_NE_76(i2, i16, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i16
power_NE_76(i2, i16, iconst_1, env, static) -{1,1}> power_Load_117(i2, i16, env, static) :|: iconst_1 = 1 && iconst_1 < i16 && 2 <= i16
power_Load_117(i2, i16, env, static) -{1,1}> power_ConstantStackPush_124(i2, i16, env, static) :|: 2 <= i16
power_ConstantStackPush_124(i2, i16, env, static) -{1,1}> power_NE_146(i2, i16, iconst_2, env, static) :|: 2 <= i16 && iconst_2 = 2

obtained
power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
by chaining
power_NE_146(i38, i16, iconst_2, env, static) -{0,0}> power_NE_153(i38, i16, iconst_2, env, static) :|: 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_NE_153(i38, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_201(i38, i16, env, static) :|: iconst_2 < i38 && 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_201(i38, i16, env, static) -{1,1}> power_Store_225(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Store_225(i38, i16, iconst_1, env, static) -{1,1}> power_Load_240(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Load_240(i38, i16, iconst_1, env, static) -{0,0}> power_Load_646(i38, i16, i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 0 <= i16 && 3 <= i38 && 2 <= i16

obtained
power_Load_646(i206, i16, i207, i208, i209, env, static) -{6,6}> power_NE_686(i206, i16, i231', 1, i207, i208, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
by chaining
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{0,0}> power_LE_659(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && 0 <= i226
power_LE_659(i206, i16, i226, i207, i209, env, static) -{1,1}> power_Load_665(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 0 < i226 && 2 <= i16
power_Load_665(i206, i16, i207, i226, i209, env, static) -{1,1}> power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) -{1,1}> power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) -{1,1}> power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) :|: i231 < iconst_2 && 1 <= i226 && 0 <= i231 && i231 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) -{1,1}> power_NE_686(i206, i16, i231, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && iconst_1 = 1 && i231 <= 1 && 2 <= i16

obtained
power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
by chaining
power_NE_686(i206, i16, iconst_1, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1 && 2 <= i16
power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_719(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && 2 <= i16
power_Load_719(i206, i16, i207, i226, i209, env, static) -{1,1}> power_Load_740(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_740(i206, i16, i209, i207, i226, env, static) -{1,1}> power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) -{1,1}> power_Store_784(i206, i16, i258, i207, i226, env, static) :|: 1 <= i226 && i209 * i207 = i258 && 2 <= i16
power_Store_784(i206, i16, i258, i207, i226, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16

obtained
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
by chaining
power_Load_795(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Load_797(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_797(i206, i16, i207, i226, i258, env, static) -{1,1}> power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Store_803(i206, i16, i267, i226, i258, env, static) :|: i207 * i207 = i267 && 1 <= i226 && 2 <= i16
power_Store_803(i206, i16, i267, i226, i258, env, static) -{1,1}> power_Load_805(i206, i16, i267, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_805(i206, i16, i267, i226, i258, env, static) -{1,1}> power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) -{1,1}> power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) -{1,1}> power_Store_843(i206, i16, i268, i267, i258, env, static) :|: i268 < i226 && 0 <= i268 && 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_Store_843(i206, i16, i268, i267, i258, env, static) -{1,1}> power_JMP_845(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_JMP_845(i206, i16, i267, i268, i258, env, static) -{1,1}> power_Load_851(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_Load_851(i206, i16, i267, i268, i258, env, static) -{0,0}> power_Load_646(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16

obtained
power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
by chaining
power_NE_686(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) :|: 0 <= iconst_0 && 1 <= i226 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_705(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_Load_705(i206, i16, i207, i226, i209, env, static) -{0,0}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16

obtained
power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
by chaining
power_NE_146(i37, i16, iconst_2, env, static) -{0,0}> power_NE_151(i37, i16, iconst_2, env, static) :|: i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_151(i37, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_181(i37, i16, env, static) :|: i37 < iconst_2 && i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_181(i37, i16, env, static) -{1,1}> power_Store_217(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Store_217(i37, i16, iconst_1, env, static) -{1,1}> power_Load_237(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_237(i37, i16, iconst_1, env, static) -{0,0}> power_Load_511(i37, i16, i37, i16, iconst_1, env, static) :|: iconst_1 <= 1 && 1 <= i16 && iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_511(i37, i16, i100, i108, i80, env, static) -{0,0}> power_Load_646(i37, i16, i100, i108, i80, env, static) :|: i80 <= 1 && 1 <= i108 && 0 <= i108 && i37 <= 1 && 2 <= i16

(8) Obligation:

IntTrs with 7 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: all paths from start
Rules:
power_Load_1(i2, i3, env, static) -{22,22}> power_NE_146(i2, i3, 2, env, static'1) :|: !(i3 = 0) && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_Load_646(i206, i16, i207, i208, i209, env, static) -{6,6}> power_NE_686(i206, i16, i231', 1, i207, i208, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2

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

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

power_Load_1(x1, x2, x3, x4) → power_Load_1(x1, x2, x4)
power_NE_146(x1, x2, x3, x4, x5) → power_NE_146(x1, x2)
power_Load_646(x1, x2, x3, x4, x5, x6, x7) → power_Load_646(x2, x3, x4, x5)
power_NE_686(x1, x2, x3, x4, x5, x6, x7, x8, x9) → power_NE_686(x2, x3, x5, x6, x7)
power_Load_795(x1, x2, x3, x4, x5, x6, x7) → power_Load_795(x2, x3, x4, x5)

(10) Obligation:

IntTrs with 7 rules
Start term: power_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: !(i3 = 0) && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_NE_146(i38, i16) -{3,3}> power_Load_646(i16, i38, i16, 1) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
power_NE_686(i16, 1, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i258') :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i267', i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_686(i16, 0, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2

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

Moved arithmethic from lhss to constraints.

power_NE_686(i16, 1, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i258') :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
was transformed to
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i258') :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1

power_NE_686(i16, 0, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
was transformed to
power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0

(12) Obligation:

IntTrs with 7 rules
Start term: power_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
power_NE_146(i38, i16) -{3,3}> power_Load_646(i16, i38, i16, 1) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i258') :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1
power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0
power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: !(i3 = 0) && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i267', i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

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

Removed div and mod.

power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: !(i3 = 0) && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 < 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 > 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2

(14) Obligation:

IntTrs with 8 rules
Start term: power_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
power_NE_146(i38, i16) -{3,3}> power_Load_646(i16, i38, i16, 1) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 < 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i258') :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1
power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 > 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i267', i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

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

Moved arithmethic from constraints to rhss.

power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i258') :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1
was transformed to
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i209 * i207) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1

power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i267', i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
was transformed to
power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i207 * i207, i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

(16) Obligation:

IntTrs with 8 rules
Start term: power_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 < 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_NE_146(i38, i16) -{3,3}> power_Load_646(i16, i38, i16, 1) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i209 * i207) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1
power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 > 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i207 * i207, i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

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

Simplified expressions.

power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 < 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 < 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0
was transformed to
power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 1 <= i226 && 2 <= i16 && x = 0

power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
was transformed to
power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && i37 <= 1 && 0 <= i16 && i37 < 2

power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i208 && 1 <= i208 && 0 < i208
was transformed to
power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 1 <= i208 && 0 < i208

power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 > 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 >= 0 && 0 < 2
was transformed to
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: 0 < i3 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1

power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i209 * i207) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1
was transformed to
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i209 * i207) :|: 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && x = 1

(18) Obligation:

IntTrs with 8 rules
Start term: power_Load_1(#0, #1, static)
Considered paths: all paths from start
Rules:
power_Load_646(i16, i207, i208, i209) -{6,6}> power_NE_686(i16, i231', i207, i208, i209) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 1 <= i208 && 0 < i208
power_NE_146(i38, i16) -{3,3}> power_Load_646(i16, i38, i16, 1) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_NE_686(i16, x, i207, i226, i209) -{1,1}> power_Load_795(i16, i207, i226, i209) :|: 1 <= i226 && 2 <= i16 && x = 0
power_NE_146(i37, i16) -{3,3}> power_Load_646(i16, i37, i16, 1) :|: 1 <= i16 && 2 <= i16 && i37 <= 1 && 0 <= i16 && i37 < 2
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: i3 < 0 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
power_Load_1(i2, i3, static) -{22,22}> power_NE_146(i2, i3) :|: 0 < i3 && 2 <= i3 && static'1 <= static''' + 1 && 1 < i3 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
power_NE_686(i16, x, i207, i226, i209) -{5,5}> power_Load_795(i16, i207, i226, i209 * i207) :|: 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && x = 1
power_Load_795(i16, i207, i226, i258) -{9,9}> power_Load_646(i16, i207 * i207, i268', i258) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

(19) koat Proof (EQUIVALENT transformation)

YES(?, 63*ar_1 + 28)

Initial complexity problem:
1: T:
(Comp: ?, Cost: 6) power_Load_646(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_686(ar_0, i231', ar_1, ar_2, ar_3)) [ i231' < 2 /\ 2 <= ar_0 /\ 0 <= i231' /\ i231' <= 1 /\ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: ?, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 2 < ar_0 /\ 2 <= ar_1 /\ 3 <= ar_0 /\ 0 <= ar_1 ]
(Comp: ?, Cost: 1) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_1 /\ ar_0 <= 1 /\ 0 <= ar_1 /\ ar_0 < 2 ]
(Comp: ?, Cost: 22) power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_146(ar_0, ar_1, arityPad, arityPad, arityPad)) [ ar_1 < 0 /\ 2 <= ar_1 /\ static'1 <= static''' + 1 /\ 1 < ar_1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 22) power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_146(ar_0, ar_1, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ 2 <= ar_1 /\ static'1 <= static''' + 1 /\ 1 < ar_1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: ?, Cost: 5) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_2*ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_2*ar_4 = i258' /\ ar_1 = 1 ]
(Comp: ?, Cost: 9) power_Load_795(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_0, ar_1^2, i268', ar_3, arityPad)) [ i268' < ar_2 /\ 0 <= i268' /\ 2 <= ar_0 /\ 1 <= ar_2 /\ ar_1^2 = i267' ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Testing for reachability in the complexity graph removes the following transition from problem 1:
power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_146(ar_0, ar_1, arityPad, arityPad, arityPad)) [ ar_1 < 0 /\ 2 <= ar_1 /\ static'1 <= static''' + 1 /\ 1 < ar_1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
We thus obtain the following problem:
2: T:
(Comp: ?, Cost: 9) power_Load_795(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_0, ar_1^2, i268', ar_3, arityPad)) [ i268' < ar_2 /\ 0 <= i268' /\ 2 <= ar_0 /\ 1 <= ar_2 /\ ar_1^2 = i267' ]
(Comp: ?, Cost: 5) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_2*ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_2*ar_4 = i258' /\ ar_1 = 1 ]
(Comp: ?, Cost: 1) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 6) power_Load_646(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_686(ar_0, i231', ar_1, ar_2, ar_3)) [ i231' < 2 /\ 2 <= ar_0 /\ 0 <= i231' /\ i231' <= 1 /\ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: ?, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_1 /\ ar_0 <= 1 /\ 0 <= ar_1 /\ ar_0 < 2 ]
(Comp: ?, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 2 < ar_0 /\ 2 <= ar_1 /\ 3 <= ar_0 /\ 0 <= ar_1 ]
(Comp: ?, Cost: 22) power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_146(ar_0, ar_1, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ 2 <= ar_1 /\ static'1 <= static''' + 1 /\ 1 < ar_1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Repeatedly propagating knowledge in problem 2 produces the following problem:
3: T:
(Comp: ?, Cost: 9) power_Load_795(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_0, ar_1^2, i268', ar_3, arityPad)) [ i268' < ar_2 /\ 0 <= i268' /\ 2 <= ar_0 /\ 1 <= ar_2 /\ ar_1^2 = i267' ]
(Comp: ?, Cost: 5) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_2*ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_2*ar_4 = i258' /\ ar_1 = 1 ]
(Comp: ?, Cost: 1) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_1 = 0 ]
(Comp: ?, Cost: 6) power_Load_646(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_686(ar_0, i231', ar_1, ar_2, ar_3)) [ i231' < 2 /\ 2 <= ar_0 /\ 0 <= i231' /\ i231' <= 1 /\ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: 1, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_1 /\ ar_0 <= 1 /\ 0 <= ar_1 /\ ar_0 < 2 ]
(Comp: 1, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 2 < ar_0 /\ 2 <= ar_1 /\ 3 <= ar_0 /\ 0 <= ar_1 ]
(Comp: 1, Cost: 22) power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_146(ar_0, ar_1, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ 2 <= ar_1 /\ static'1 <= static''' + 1 /\ 1 < ar_1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

A polynomial rank function with
Pol(power_Load_795) = 3*V_3 - 2
Pol(power_Load_646) = 3*V_3
Pol(power_NE_686) = 3*V_4 - 1
Pol(power_NE_146) = 3*V_2
Pol(power_Load_1) = 3*V_2
Pol(koat_start) = 3*V_2
orients all transitions weakly and the transitions
power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_2*ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_2*ar_4 = i258' /\ ar_1 = 1 ]
power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_1 = 0 ]
power_Load_795(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_0, ar_1^2, i268', ar_3, arityPad)) [ i268' < ar_2 /\ 0 <= i268' /\ 2 <= ar_0 /\ 1 <= ar_2 /\ ar_1^2 = i267' ]
power_Load_646(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_686(ar_0, i231', ar_1, ar_2, ar_3)) [ i231' < 2 /\ 2 <= ar_0 /\ 0 <= i231' /\ i231' <= 1 /\ 1 <= ar_2 /\ 0 < ar_2 ]
strictly and produces the following problem:
4: T:
(Comp: 3*ar_1, Cost: 9) power_Load_795(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_0, ar_1^2, i268', ar_3, arityPad)) [ i268' < ar_2 /\ 0 <= i268' /\ 2 <= ar_0 /\ 1 <= ar_2 /\ ar_1^2 = i267' ]
(Comp: 3*ar_1, Cost: 5) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_2*ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_2*ar_4 = i258' /\ ar_1 = 1 ]
(Comp: 3*ar_1, Cost: 1) power_NE_686(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_795(ar_0, ar_2, ar_3, ar_4, arityPad)) [ 1 <= ar_3 /\ 2 <= ar_0 /\ ar_1 = 0 ]
(Comp: 3*ar_1, Cost: 6) power_Load_646(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_686(ar_0, i231', ar_1, ar_2, ar_3)) [ i231' < 2 /\ 2 <= ar_0 /\ 0 <= i231' /\ i231' <= 1 /\ 1 <= ar_2 /\ 0 < ar_2 ]
(Comp: 1, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 1 <= ar_1 /\ 2 <= ar_1 /\ ar_0 <= 1 /\ 0 <= ar_1 /\ ar_0 < 2 ]
(Comp: 1, Cost: 3) power_NE_146(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_646(ar_1, ar_0, ar_1, 1, arityPad)) [ 2 < ar_0 /\ 2 <= ar_1 /\ 3 <= ar_0 /\ 0 <= ar_1 ]
(Comp: 1, Cost: 22) power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_NE_146(ar_0, ar_1, arityPad, arityPad, arityPad)) [ 0 < ar_1 /\ 2 <= ar_1 /\ static'1 <= static''' + 1 /\ 1 < ar_1 /\ 0 <= static''' /\ static''' <= ar_2 + 2 /\ 0 <= ar_2 /\ 0 <= static'1 ]
(Comp: 1, Cost: 0) koat_start(ar_0, ar_1, ar_2, ar_3, ar_4) -> Com_1(power_Load_1(ar_0, ar_1, ar_2, ar_3, ar_4)) [ 0 <= 0 ]
start location: koat_start
leaf cost: 0

Complexity upper bound 63*ar_1 + 28

Time: 0.136 sec (SMT: 0.119 sec)

(20) BOUNDS(CONSTANT, 28 + 63 * |#1|)

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

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

(22) Obligation:

Set of 80 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

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

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

(24) Obligation:

IntTrs with 80 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_1(i2, i3, env, static) -{0,0}> power_Load_4(i2, i3, env, static) :|: 0 >= 0
power_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(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_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(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_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(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_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> power_Load_45(i2, i3, env, static) :|: 0 >= 0
power_Load_45(i2, i3, env, static) -{0,0}> power_Load_46(i2, i3, env, static) :|: 0 >= 0
power_Load_46(i2, i3, env, static) -{0,0}> power_Load_49(i2, i3, env, static) :|: 0 <= static
power_Load_49(i2, i3, env, static) -{0,0}> power_Load_50(i2, i3, env, static) :|: 0 >= 0
power_Load_50(i2, i3, env, static) -{0,0}> power_Load_51(i2, i3, env, static) :|: 0 >= 0
power_Load_51(i2, i3, env, static) -{1,1}> power_NE_52(i2, i3, env, static) :|: 0 >= 0
power_NE_52(i2, i8, env, static) -{0,0}> power_NE_54(i2, i8, env, static) :|: 0 >= 0
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_54(i2, i8, env, static) -{1,1}> power_Load_56(i2, i8, env, static) :|: !(i8 = 0)
power_Load_56(i2, i8, env, static) -{1,1}> power_ConstantStackPush_59(i2, i8, env, static) :|: 0 >= 0
power_ConstantStackPush_59(i2, i8, env, static) -{1,1}> power_NE_70(i2, i8, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i15, iconst_1, env, static) -{0,0}> power_NE_74(i2, i15, iconst_1, env, static) :|: i15 <= -1 && iconst_1 = 1
power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i16, iconst_1, env, static) -{0,0}> power_NE_76(i2, i16, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i16
power_NE_74(i2, i15, iconst_1, env, static) -{1,1}> power_Load_91(i2, i15, env, static) :|: i15 <= -1 && iconst_1 = 1 && i15 < iconst_1
power_NE_76(i2, i16, iconst_1, env, static) -{1,1}> power_Load_117(i2, i16, env, static) :|: iconst_1 = 1 && iconst_1 < i16 && 2 <= i16
power_Load_91(i2, i15, env, static) -{1,1}> power_ConstantStackPush_119(i2, i15, env, static) :|: i15 <= -1
power_Load_117(i2, i16, env, static) -{1,1}> power_ConstantStackPush_124(i2, i16, env, static) :|: 2 <= i16
power_ConstantStackPush_119(i2, i15, env, static) -{1,1}> power_NE_136(i2, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2
power_ConstantStackPush_124(i2, i16, env, static) -{1,1}> power_NE_146(i2, i16, iconst_2, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_146(i37, i16, iconst_2, env, static) -{0,0}> power_NE_151(i37, i16, iconst_2, env, static) :|: i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_146(i38, i16, iconst_2, env, static) -{0,0}> power_NE_153(i38, i16, iconst_2, env, static) :|: 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_NE_151(i37, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_181(i37, i16, env, static) :|: i37 < iconst_2 && i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_153(i38, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_201(i38, i16, env, static) :|: iconst_2 < i38 && 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_181(i37, i16, env, static) -{1,1}> power_Store_217(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_ConstantStackPush_201(i38, i16, env, static) -{1,1}> power_Store_225(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Store_217(i37, i16, iconst_1, env, static) -{1,1}> power_Load_237(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Store_225(i38, i16, iconst_1, env, static) -{1,1}> power_Load_240(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Load_237(i37, i16, iconst_1, env, static) -{0,0}> power_Load_511(i37, i16, i37, i16, iconst_1, env, static) :|: iconst_1 <= 1 && 1 <= i16 && iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_240(i38, i16, iconst_1, env, static) -{0,0}> power_Load_646(i38, i16, i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 0 <= i16 && 3 <= i38 && 2 <= i16
power_Load_511(i37, i16, i100, i108, i80, env, static) -{0,0}> power_Load_646(i37, i16, i100, i108, i80, env, static) :|: i80 <= 1 && 1 <= i108 && 0 <= i108 && i37 <= 1 && 2 <= i16
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{0,0}> power_LE_659(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && 0 <= i226
power_LE_659(i206, i16, i226, i207, i209, env, static) -{1,1}> power_Load_665(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 0 < i226 && 2 <= i16
power_Load_665(i206, i16, i207, i226, i209, env, static) -{1,1}> power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) -{1,1}> power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) -{1,1}> power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) :|: i231 < iconst_2 && 1 <= i226 && 0 <= i231 && i231 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) -{1,1}> power_NE_686(i206, i16, i231, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && iconst_1 = 1 && i231 <= 1 && 2 <= i16
power_NE_686(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) :|: 0 <= iconst_0 && 1 <= i226 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_686(i206, i16, iconst_1, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1 && 2 <= i16
power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_705(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_719(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && 2 <= i16
power_Load_705(i206, i16, i207, i226, i209, env, static) -{0,0}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_719(i206, i16, i207, i226, i209, env, static) -{1,1}> power_Load_740(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_740(i206, i16, i209, i207, i226, env, static) -{1,1}> power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) -{1,1}> power_Store_784(i206, i16, i258, i207, i226, env, static) :|: 1 <= i226 && i209 * i207 = i258 && 2 <= i16
power_Store_784(i206, i16, i258, i207, i226, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_795(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Load_797(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_797(i206, i16, i207, i226, i258, env, static) -{1,1}> power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Store_803(i206, i16, i267, i226, i258, env, static) :|: i207 * i207 = i267 && 1 <= i226 && 2 <= i16
power_Store_803(i206, i16, i267, i226, i258, env, static) -{1,1}> power_Load_805(i206, i16, i267, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_805(i206, i16, i267, i226, i258, env, static) -{1,1}> power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) -{1,1}> power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) -{1,1}> power_Store_843(i206, i16, i268, i267, i258, env, static) :|: i268 < i226 && 0 <= i268 && 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_Store_843(i206, i16, i268, i267, i258, env, static) -{1,1}> power_JMP_845(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_JMP_845(i206, i16, i267, i268, i258, env, static) -{1,1}> power_Load_851(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_Load_851(i206, i16, i267, i268, i258, env, static) -{0,0}> power_Load_646(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16

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

obtained
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
power_Load_1(i2, i3, env, static) -{0,0}> power_Load_4(i2, i3, env, static) :|: 0 >= 0
power_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(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_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(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_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(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_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> power_Load_45(i2, i3, env, static) :|: 0 >= 0
power_Load_45(i2, i3, env, static) -{0,0}> power_Load_46(i2, i3, env, static) :|: 0 >= 0
power_Load_46(i2, i3, env, static) -{0,0}> power_Load_49(i2, i3, env, static) :|: 0 <= static
power_Load_49(i2, i3, env, static) -{0,0}> power_Load_50(i2, i3, env, static) :|: 0 >= 0
power_Load_50(i2, i3, env, static) -{0,0}> power_Load_51(i2, i3, env, static) :|: 0 >= 0
power_Load_51(i2, i3, env, static) -{1,1}> power_NE_52(i2, i3, env, static) :|: 0 >= 0

obtained
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
by chaining
power_NE_52(i2, i8, env, static) -{0,0}> power_NE_54(i2, i8, env, static) :|: 0 >= 0
power_NE_54(i2, i8, env, static) -{1,1}> power_Load_56(i2, i8, env, static) :|: !(i8 = 0)
power_Load_56(i2, i8, env, static) -{1,1}> power_ConstantStackPush_59(i2, i8, env, static) :|: 0 >= 0
power_ConstantStackPush_59(i2, i8, env, static) -{1,1}> power_NE_70(i2, i8, iconst_1, env, static) :|: iconst_1 = 1

obtained
power_NE_70(i2, i16, 1, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16
by chaining
power_NE_70(i2, i16, iconst_1, env, static) -{0,0}> power_NE_76(i2, i16, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i16
power_NE_76(i2, i16, iconst_1, env, static) -{1,1}> power_Load_117(i2, i16, env, static) :|: iconst_1 = 1 && iconst_1 < i16 && 2 <= i16
power_Load_117(i2, i16, env, static) -{1,1}> power_ConstantStackPush_124(i2, i16, env, static) :|: 2 <= i16
power_ConstantStackPush_124(i2, i16, env, static) -{1,1}> power_NE_146(i2, i16, iconst_2, env, static) :|: 2 <= i16 && iconst_2 = 2

obtained
power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
by chaining
power_NE_146(i38, i16, iconst_2, env, static) -{0,0}> power_NE_153(i38, i16, iconst_2, env, static) :|: 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_NE_153(i38, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_201(i38, i16, env, static) :|: iconst_2 < i38 && 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_201(i38, i16, env, static) -{1,1}> power_Store_225(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Store_225(i38, i16, iconst_1, env, static) -{1,1}> power_Load_240(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Load_240(i38, i16, iconst_1, env, static) -{0,0}> power_Load_646(i38, i16, i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 0 <= i16 && 3 <= i38 && 2 <= i16

obtained
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
by chaining
power_LE_656(i206, i16, i226, i207, i209, env, static) -{0,0}> power_LE_659(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && 0 <= i226
power_LE_659(i206, i16, i226, i207, i209, env, static) -{1,1}> power_Load_665(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 0 < i226 && 2 <= i16
power_Load_665(i206, i16, i207, i226, i209, env, static) -{1,1}> power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) -{1,1}> power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) -{1,1}> power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) :|: i231 < iconst_2 && 1 <= i226 && 0 <= i231 && i231 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) -{1,1}> power_NE_686(i206, i16, i231, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && iconst_1 = 1 && i231 <= 1 && 2 <= i16

obtained
power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
by chaining
power_NE_686(i206, i16, iconst_1, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1 && 2 <= i16
power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_719(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && 2 <= i16
power_Load_719(i206, i16, i207, i226, i209, env, static) -{1,1}> power_Load_740(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_740(i206, i16, i209, i207, i226, env, static) -{1,1}> power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) -{1,1}> power_Store_784(i206, i16, i258, i207, i226, env, static) :|: 1 <= i226 && i209 * i207 = i258 && 2 <= i16
power_Store_784(i206, i16, i258, i207, i226, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16

obtained
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
by chaining
power_Load_795(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Load_797(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_797(i206, i16, i207, i226, i258, env, static) -{1,1}> power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Store_803(i206, i16, i267, i226, i258, env, static) :|: i207 * i207 = i267 && 1 <= i226 && 2 <= i16
power_Store_803(i206, i16, i267, i226, i258, env, static) -{1,1}> power_Load_805(i206, i16, i267, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_805(i206, i16, i267, i226, i258, env, static) -{1,1}> power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) -{1,1}> power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) -{1,1}> power_Store_843(i206, i16, i268, i267, i258, env, static) :|: i268 < i226 && 0 <= i268 && 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_Store_843(i206, i16, i268, i267, i258, env, static) -{1,1}> power_JMP_845(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_JMP_845(i206, i16, i267, i268, i258, env, static) -{1,1}> power_Load_851(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_Load_851(i206, i16, i267, i268, i258, env, static) -{0,0}> power_Load_646(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16

obtained
power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
by chaining
power_NE_686(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) :|: 0 <= iconst_0 && 1 <= i226 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_705(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_Load_705(i206, i16, i207, i226, i209, env, static) -{0,0}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16

obtained
power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
by chaining
power_NE_146(i37, i16, iconst_2, env, static) -{0,0}> power_NE_151(i37, i16, iconst_2, env, static) :|: i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_151(i37, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_181(i37, i16, env, static) :|: i37 < iconst_2 && i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_181(i37, i16, env, static) -{1,1}> power_Store_217(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Store_217(i37, i16, iconst_1, env, static) -{1,1}> power_Load_237(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_237(i37, i16, iconst_1, env, static) -{0,0}> power_Load_511(i37, i16, i37, i16, iconst_1, env, static) :|: iconst_1 <= 1 && 1 <= i16 && iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_511(i37, i16, i100, i108, i80, env, static) -{0,0}> power_Load_646(i37, i16, i100, i108, i80, env, static) :|: i80 <= 1 && 1 <= i108 && 0 <= i108 && i37 <= 1 && 2 <= i16

obtained
power_NE_70(i2, i15, 1, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1
by chaining
power_NE_70(i2, i15, iconst_1, env, static) -{0,0}> power_NE_74(i2, i15, iconst_1, env, static) :|: i15 <= -1 && iconst_1 = 1
power_NE_74(i2, i15, iconst_1, env, static) -{1,1}> power_Load_91(i2, i15, env, static) :|: i15 <= -1 && iconst_1 = 1 && i15 < iconst_1
power_Load_91(i2, i15, env, static) -{1,1}> power_ConstantStackPush_119(i2, i15, env, static) :|: i15 <= -1
power_ConstantStackPush_119(i2, i15, env, static) -{1,1}> power_NE_136(i2, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2

(26) Obligation:

IntTrs with 18 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i16, 1, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16
power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
power_NE_70(i2, i15, 1, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36

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

Moved arithmethic from lhss to constraints.

power_NE_70(i2, i15, 1, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1
was transformed to
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1

power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1

power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
was transformed to
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2

power_NE_70(i2, i16, 1, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16
was transformed to
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1

power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
was transformed to
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2

power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1

(28) Obligation:

IntTrs with 18 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1

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

Linearized lhss.

power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
was transformed to
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1

power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
was transformed to
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2

power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
was transformed to
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2

(30) Obligation:

IntTrs with 18 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36

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

Removed div and mod.

power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
was transformed to
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0

(32) Obligation:

IntTrs with 19 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0

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

Moved arithmethic from constraints to rhss.

power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1
was transformed to
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, 1, env, static) :|: iconst_1 = 1 && x = iconst_1

power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
was transformed to
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, 2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2

power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1

power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
was transformed to
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, 0, env, static) :|: iconst_0 = 0

power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
was transformed to
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2

power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
was transformed to
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, 0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16

power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
was transformed to
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
was transformed to
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2

power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
was transformed to
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, 2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36

(34) Obligation:

IntTrs with 19 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, 1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, 2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, 0, env, static) :|: iconst_0 = 0
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, 0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, 2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0

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

Simplified expressions.

power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16 && x = 0 && x' = 1

power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
was transformed to
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: i8 < 0

power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && x = 1 && x' = 1

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

power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 0 <= i226 && 1 <= i226 && 0 < i226
was transformed to
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 1 <= i226 && 0 < i226

power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
was transformed to
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2

power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0
was transformed to
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 < i8

(36) Obligation:

IntTrs with 19 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, 2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, 1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && x = 1 && x' = 1
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, 0, env, static) :|: iconst_0 = 0
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i231' < 2 && 2 <= i16 && 0 <= i231' && i231' <= 1 && 1 <= i226 && 0 < i226
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, 2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16 && x = 0 && x' = 1
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: i8 < 0
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i268' < i226 && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 < i8
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, 0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16

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

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

(38) Obligation:

IntTrs with 80 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_1(i2, i3, env, static) -{0,0}> power_Load_4(i2, i3, env, static) :|: 0 >= 0
power_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(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_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(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_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(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_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> power_Load_45(i2, i3, env, static) :|: 0 >= 0
power_Load_45(i2, i3, env, static) -{0,0}> power_Load_46(i2, i3, env, static) :|: 0 >= 0
power_Load_46(i2, i3, env, static) -{0,0}> power_Load_49(i2, i3, env, static) :|: 0 <= static
power_Load_49(i2, i3, env, static) -{0,0}> power_Load_50(i2, i3, env, static) :|: 0 >= 0
power_Load_50(i2, i3, env, static) -{0,0}> power_Load_51(i2, i3, env, static) :|: 0 >= 0
power_Load_51(i2, i3, env, static) -{1,1}> power_NE_52(i2, i3, env, static) :|: 0 >= 0
power_NE_52(i2, i8, env, static) -{0,0}> power_NE_54(i2, i8, env, static) :|: 0 >= 0
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_54(i2, i8, env, static) -{1,1}> power_Load_56(i2, i8, env, static) :|: !(i8 = 0)
power_Load_56(i2, i8, env, static) -{1,1}> power_ConstantStackPush_59(i2, i8, env, static) :|: 0 >= 0
power_ConstantStackPush_59(i2, i8, env, static) -{1,1}> power_NE_70(i2, i8, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i15, iconst_1, env, static) -{0,0}> power_NE_74(i2, i15, iconst_1, env, static) :|: i15 <= -1 && iconst_1 = 1
power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i16, iconst_1, env, static) -{0,0}> power_NE_76(i2, i16, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i16
power_NE_74(i2, i15, iconst_1, env, static) -{1,1}> power_Load_91(i2, i15, env, static) :|: i15 <= -1 && iconst_1 = 1 && i15 < iconst_1
power_NE_76(i2, i16, iconst_1, env, static) -{1,1}> power_Load_117(i2, i16, env, static) :|: iconst_1 = 1 && iconst_1 < i16 && 2 <= i16
power_Load_91(i2, i15, env, static) -{1,1}> power_ConstantStackPush_119(i2, i15, env, static) :|: i15 <= -1
power_Load_117(i2, i16, env, static) -{1,1}> power_ConstantStackPush_124(i2, i16, env, static) :|: 2 <= i16
power_ConstantStackPush_119(i2, i15, env, static) -{1,1}> power_NE_136(i2, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2
power_ConstantStackPush_124(i2, i16, env, static) -{1,1}> power_NE_146(i2, i16, iconst_2, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_146(i37, i16, iconst_2, env, static) -{0,0}> power_NE_151(i37, i16, iconst_2, env, static) :|: i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_146(i38, i16, iconst_2, env, static) -{0,0}> power_NE_153(i38, i16, iconst_2, env, static) :|: 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_NE_151(i37, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_181(i37, i16, env, static) :|: i37 < iconst_2 && i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_153(i38, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_201(i38, i16, env, static) :|: iconst_2 < i38 && 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_181(i37, i16, env, static) -{1,1}> power_Store_217(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_ConstantStackPush_201(i38, i16, env, static) -{1,1}> power_Store_225(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Store_217(i37, i16, iconst_1, env, static) -{1,1}> power_Load_237(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Store_225(i38, i16, iconst_1, env, static) -{1,1}> power_Load_240(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Load_237(i37, i16, iconst_1, env, static) -{0,0}> power_Load_511(i37, i16, i37, i16, iconst_1, env, static) :|: iconst_1 <= 1 && 1 <= i16 && iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_240(i38, i16, iconst_1, env, static) -{0,0}> power_Load_646(i38, i16, i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 0 <= i16 && 3 <= i38 && 2 <= i16
power_Load_511(i37, i16, i100, i108, i80, env, static) -{0,0}> power_Load_646(i37, i16, i100, i108, i80, env, static) :|: i80 <= 1 && 1 <= i108 && 0 <= i108 && i37 <= 1 && 2 <= i16
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{0,0}> power_LE_659(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && 0 <= i226
power_LE_659(i206, i16, i226, i207, i209, env, static) -{1,1}> power_Load_665(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 0 < i226 && 2 <= i16
power_Load_665(i206, i16, i207, i226, i209, env, static) -{1,1}> power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) -{1,1}> power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) -{1,1}> power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && i231 <= 1 && 2 <= i16 && i226 % iconst_2 = i231 && iconst_2 = 2
power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) -{1,1}> power_NE_686(i206, i16, i231, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && iconst_1 = 1 && i231 <= 1 && 2 <= i16
power_NE_686(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) :|: 0 <= iconst_0 && 1 <= i226 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_686(i206, i16, iconst_1, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1 && 2 <= i16
power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_705(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_719(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && 2 <= i16
power_Load_705(i206, i16, i207, i226, i209, env, static) -{0,0}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_719(i206, i16, i207, i226, i209, env, static) -{1,1}> power_Load_740(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_740(i206, i16, i209, i207, i226, env, static) -{1,1}> power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) -{1,1}> power_Store_784(i206, i16, i258, i207, i226, env, static) :|: 1 <= i226 && i209 * i207 = i258 && 2 <= i16
power_Store_784(i206, i16, i258, i207, i226, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_795(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Load_797(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_797(i206, i16, i207, i226, i258, env, static) -{1,1}> power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Store_803(i206, i16, i267, i226, i258, env, static) :|: i207 * i207 = i267 && 1 <= i226 && 2 <= i16
power_Store_803(i206, i16, i267, i226, i258, env, static) -{1,1}> power_Load_805(i206, i16, i267, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_805(i206, i16, i267, i226, i258, env, static) -{1,1}> power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) -{1,1}> power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) -{1,1}> power_Store_843(i206, i16, i268, i267, i258, env, static) :|: 0 <= i268 && 1 <= i226 && i226 / iconst_2 = i268 && 2 <= i16 && iconst_2 = 2
power_Store_843(i206, i16, i268, i267, i258, env, static) -{1,1}> power_JMP_845(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_JMP_845(i206, i16, i267, i268, i258, env, static) -{1,1}> power_Load_851(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_Load_851(i206, i16, i267, i268, i258, env, static) -{0,0}> power_Load_646(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16

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

obtained
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
by chaining
power_Load_1(i2, i3, env, static) -{0,0}> power_Load_4(i2, i3, env, static) :|: 0 >= 0
power_Load_4(i2, i3, env, static) -{0,0}> langle_clinit_rangle_ConstantStackPush_6(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_ConstantStackPush_6(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_14(a2, i2, i3, iconst_0, env, static) :|: a2 = 2 && iconst_0 = 0 && 0 < a2
langle_clinit_rangle_FieldAccess_14(a2, i2, i3, iconst_0, env, static) -{1,1}> langle_clinit_rangle_New_16(i2, i3, env, static') :|: 0 <= a2 && iconst_0 = 0 && static' <= static + a2 && 0 <= static && 0 < a2
langle_clinit_rangle_New_16(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_18(i2, i3, env, static) :|: 0 >= 0
langle_clinit_rangle_New_18(i2, i3, env, static) -{0,0}> langle_clinit_rangle_New_19(i2, i3, env, static) :|: 0 <= static
langle_clinit_rangle_New_19(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_22(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_ConstantStackPush_22(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_25(o2, i2, i3, env, static) :|: NULL = 0 && 0 < o2
langle_init_rangle_Load_25(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_27(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Load_29(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Load_29(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_InvokeMethod_31(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_34(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_34(o2, i2, i3, env, static) -{1,1}> langle_init_rangle_Return_36(o2, i2, i3, env, static) :|: 0 < o2
langle_init_rangle_Return_36(o2, i2, i3, env, static) -{1,1}> langle_clinit_rangle_FieldAccess_39(o2, i2, i3, env, static) :|: 0 < o2
langle_clinit_rangle_FieldAccess_39(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}> power_Load_45(i2, i3, env, static) :|: 0 >= 0
power_Load_45(i2, i3, env, static) -{0,0}> power_Load_46(i2, i3, env, static) :|: 0 >= 0
power_Load_46(i2, i3, env, static) -{0,0}> power_Load_49(i2, i3, env, static) :|: 0 <= static
power_Load_49(i2, i3, env, static) -{0,0}> power_Load_50(i2, i3, env, static) :|: 0 >= 0
power_Load_50(i2, i3, env, static) -{0,0}> power_Load_51(i2, i3, env, static) :|: 0 >= 0
power_Load_51(i2, i3, env, static) -{1,1}> power_NE_52(i2, i3, env, static) :|: 0 >= 0

obtained
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
by chaining
power_NE_52(i2, i8, env, static) -{0,0}> power_NE_54(i2, i8, env, static) :|: 0 >= 0
power_NE_54(i2, i8, env, static) -{1,1}> power_Load_56(i2, i8, env, static) :|: !(i8 = 0)
power_Load_56(i2, i8, env, static) -{1,1}> power_ConstantStackPush_59(i2, i8, env, static) :|: 0 >= 0
power_ConstantStackPush_59(i2, i8, env, static) -{1,1}> power_NE_70(i2, i8, iconst_1, env, static) :|: iconst_1 = 1

obtained
power_NE_70(i2, i16, 1, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16
by chaining
power_NE_70(i2, i16, iconst_1, env, static) -{0,0}> power_NE_76(i2, i16, iconst_1, env, static) :|: iconst_1 = 1 && 2 <= i16
power_NE_76(i2, i16, iconst_1, env, static) -{1,1}> power_Load_117(i2, i16, env, static) :|: iconst_1 = 1 && iconst_1 < i16 && 2 <= i16
power_Load_117(i2, i16, env, static) -{1,1}> power_ConstantStackPush_124(i2, i16, env, static) :|: 2 <= i16
power_ConstantStackPush_124(i2, i16, env, static) -{1,1}> power_NE_146(i2, i16, iconst_2, env, static) :|: 2 <= i16 && iconst_2 = 2

obtained
power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
by chaining
power_NE_146(i38, i16, iconst_2, env, static) -{0,0}> power_NE_153(i38, i16, iconst_2, env, static) :|: 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_NE_153(i38, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_201(i38, i16, env, static) :|: iconst_2 < i38 && 3 <= i38 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_201(i38, i16, env, static) -{1,1}> power_Store_225(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Store_225(i38, i16, iconst_1, env, static) -{1,1}> power_Load_240(i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 3 <= i38 && 2 <= i16
power_Load_240(i38, i16, iconst_1, env, static) -{0,0}> power_Load_646(i38, i16, i38, i16, iconst_1, env, static) :|: iconst_1 = 1 && 0 <= i16 && 3 <= i38 && 2 <= i16

obtained
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 % 2 = i231' && 0 < i226
by chaining
power_LE_656(i206, i16, i226, i207, i209, env, static) -{0,0}> power_LE_659(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && 0 <= i226
power_LE_659(i206, i16, i226, i207, i209, env, static) -{1,1}> power_Load_665(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 0 < i226 && 2 <= i16
power_Load_665(i206, i16, i207, i226, i209, env, static) -{1,1}> power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_671(i206, i16, i226, i207, i209, env, static) -{1,1}> power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_675(i206, i16, i226, iconst_2, i207, i209, env, static) -{1,1}> power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && i231 <= 1 && 2 <= i16 && i226 % iconst_2 = i231 && iconst_2 = 2
power_ConstantStackPush_677(i206, i16, i231, i207, i226, i209, env, static) -{1,1}> power_NE_686(i206, i16, i231, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && 0 <= i231 && iconst_1 = 1 && i231 <= 1 && 2 <= i16

obtained
power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
by chaining
power_NE_686(i206, i16, iconst_1, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 <= 1 && 0 <= iconst_1 && iconst_1 = 1 && 2 <= i16
power_NE_695(i206, i16, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_719(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && 2 <= i16
power_Load_719(i206, i16, i207, i226, i209, env, static) -{1,1}> power_Load_740(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_740(i206, i16, i209, i207, i226, env, static) -{1,1}> power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_780(i206, i16, i209, i207, i226, env, static) -{1,1}> power_Store_784(i206, i16, i258, i207, i226, env, static) :|: 1 <= i226 && i209 * i207 = i258 && 2 <= i16
power_Store_784(i206, i16, i258, i207, i226, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16

obtained
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 / 2 = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
by chaining
power_Load_795(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Load_797(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_797(i206, i16, i207, i226, i258, env, static) -{1,1}> power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_IntArithmetic_800(i206, i16, i207, i226, i258, env, static) -{1,1}> power_Store_803(i206, i16, i267, i226, i258, env, static) :|: i207 * i207 = i267 && 1 <= i226 && 2 <= i16
power_Store_803(i206, i16, i267, i226, i258, env, static) -{1,1}> power_Load_805(i206, i16, i267, i226, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_Load_805(i206, i16, i267, i226, i258, env, static) -{1,1}> power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16
power_ConstantStackPush_807(i206, i16, i226, i267, i258, env, static) -{1,1}> power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) :|: 1 <= i226 && 2 <= i16 && iconst_2 = 2
power_IntArithmetic_809(i206, i16, i226, iconst_2, i267, i258, env, static) -{1,1}> power_Store_843(i206, i16, i268, i267, i258, env, static) :|: 0 <= i268 && 1 <= i226 && i226 / iconst_2 = i268 && 2 <= i16 && iconst_2 = 2
power_Store_843(i206, i16, i268, i267, i258, env, static) -{1,1}> power_JMP_845(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_JMP_845(i206, i16, i267, i268, i258, env, static) -{1,1}> power_Load_851(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16
power_Load_851(i206, i16, i267, i268, i258, env, static) -{0,0}> power_Load_646(i206, i16, i267, i268, i258, env, static) :|: 0 <= i268 && 2 <= i16

obtained
power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
by chaining
power_NE_686(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{0,0}> power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) :|: 0 <= iconst_0 && 1 <= i226 && iconst_0 <= 1 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_NE_694(i206, i16, iconst_0, iconst_1, i207, i226, i209, env, static) -{1,1}> power_Load_705(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && iconst_1 = 1 && iconst_0 = 0 && 2 <= i16
power_Load_705(i206, i16, i207, i226, i209, env, static) -{0,0}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16

obtained
power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
by chaining
power_NE_146(i37, i16, iconst_2, env, static) -{0,0}> power_NE_151(i37, i16, iconst_2, env, static) :|: i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_NE_151(i37, i16, iconst_2, env, static) -{1,1}> power_ConstantStackPush_181(i37, i16, env, static) :|: i37 < iconst_2 && i37 <= 1 && 2 <= i16 && iconst_2 = 2
power_ConstantStackPush_181(i37, i16, env, static) -{1,1}> power_Store_217(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Store_217(i37, i16, iconst_1, env, static) -{1,1}> power_Load_237(i37, i16, iconst_1, env, static) :|: iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_237(i37, i16, iconst_1, env, static) -{0,0}> power_Load_511(i37, i16, i37, i16, iconst_1, env, static) :|: iconst_1 <= 1 && 1 <= i16 && iconst_1 = 1 && i37 <= 1 && 2 <= i16
power_Load_511(i37, i16, i100, i108, i80, env, static) -{0,0}> power_Load_646(i37, i16, i100, i108, i80, env, static) :|: i80 <= 1 && 1 <= i108 && 0 <= i108 && i37 <= 1 && 2 <= i16

obtained
power_NE_70(i2, i15, 1, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1
by chaining
power_NE_70(i2, i15, iconst_1, env, static) -{0,0}> power_NE_74(i2, i15, iconst_1, env, static) :|: i15 <= -1 && iconst_1 = 1
power_NE_74(i2, i15, iconst_1, env, static) -{1,1}> power_Load_91(i2, i15, env, static) :|: i15 <= -1 && iconst_1 = 1 && i15 < iconst_1
power_Load_91(i2, i15, env, static) -{1,1}> power_ConstantStackPush_119(i2, i15, env, static) :|: i15 <= -1
power_ConstantStackPush_119(i2, i15, env, static) -{1,1}> power_NE_136(i2, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2

(40) Obligation:

IntTrs with 18 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
power_NE_70(i2, i16, 1, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16
power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 % 2 = i231' && 0 < i226
power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 / 2 = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
power_NE_70(i2, i15, 1, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36

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

Moved arithmethic from lhss to constraints.

power_NE_70(i2, i15, 1, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1
was transformed to
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1

power_NE_686(i206, i16, 1, 1, i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1

power_NE_146(i38, i16, 2, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16
was transformed to
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2

power_NE_70(i2, i16, 1, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16
was transformed to
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1

power_NE_146(i37, i16, 2, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2
was transformed to
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2

power_NE_686(i206, i16, 0, 1, i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1

(42) Obligation:

IntTrs with 18 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 / 2 = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 % 2 = i231' && 0 < i226
power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1

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

Linearized lhss.

power_NE_70(i2, iconst_1, iconst_1, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1
was transformed to
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1

power_NE_146(iconst_2, i16, iconst_2, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2
was transformed to
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2

power_NE_136(iconst_2, i15, iconst_2, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2
was transformed to
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2

(44) Obligation:

IntTrs with 18 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 / 2 = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 % 2 = i231' && 0 < i226
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36

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

Removed div and mod.

power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && !(i8 = 0)
was transformed to
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0

power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 / 2 = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
was transformed to
power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_795'(i206, i16, i207, i226, i258, env, static) :|: div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 % 2 = i231' && 0 < i226
was transformed to
power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_LE_656'(i206, i16, i226, i207, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226

(46) Obligation:

IntTrs with 21 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_LE_656'(i206, i16, i226, i207, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_795'(i206, i16, i207, i226, i258, env, static) :|: div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0

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

Moved arithmethic from constraints to rhss.

power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i267', i268', i258, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
was transformed to
power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, iconst_1, env, static) :|: iconst_1 = 1 && x = iconst_1
was transformed to
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, 1, env, static) :|: iconst_1 = 1 && x = iconst_1

power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, iconst_2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
was transformed to
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, 2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2

power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i258', env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1

power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, iconst_0, env, static) :|: iconst_0 = 0
was transformed to
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, 0, env, static) :|: iconst_0 = 0

power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i231', 1, i207, i226, i209, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
was transformed to
power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i226 - 2 * div, 1, i207, i226, i209, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226

power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(iconst_2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
was transformed to
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2

power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, iconst_0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
was transformed to
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, 0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16

power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(iconst_2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
was transformed to
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2

power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, iconst_2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
was transformed to
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, 2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36

(48) Obligation:

IntTrs with 21 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, 1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, 2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_LE_656'(i206, i16, i226, i207, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: 0 >= 0 && static'1 <= static''' + 1 && 0 <= 2 && 0 <= static''' && static''' <= static + 2 && 0 < 1 && 0 <= 1 && 0 <= static && 0 <= static'1 && 0 < 2
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, 0, env, static) :|: iconst_0 = 0
power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i226 - 2 * div, 1, i207, i226, i209, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, 0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_795'(i206, i16, i207, i226, i258, env, static) :|: div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, 2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0

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

Simplified expressions.

power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i226 - 2 * div, 1, i207, i226, i209, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
was transformed to
power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i226 + -2 * div, 1, i207, i226, i209, env, static) :|: i226 + -2 * div < 2 && 0 < i226 + -2 * div + 2 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 1 <= i226 && i226 + -2 * div = i231' && 0 < i226

power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 0 <= 0 && 1 <= i226 && 2 <= i16 && 0 <= 1 && x = 0 && x' = 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16 && x = 0 && x' = 1

power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i226 - 2 * div < 2 && i226 - 2 * div + 2 > 0 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
was transformed to
power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i226 + -2 * div < 2 && 0 < i226 + -2 * div + 2 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'

power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 < 0
was transformed to
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: i8 < 0

power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_LE_656'(i206, i16, i226, i207, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 0 <= i226 && 1 <= i226 && i226 - 2 * div = i231' && 0 < i226
was transformed to
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_LE_656'(i206, i16, i226, i207, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 1 <= i226 && i226 + -2 * div = i231' && 0 < i226

power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 0 <= 1 && 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && 1 <= 1 && x = 1 && x' = 1
was transformed to
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && x = 1 && x' = 1

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

power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && 1 <= 1 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
was transformed to
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2

power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 >= 0 && i8 > 0
was transformed to
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 < i8

(50) Obligation:

IntTrs with 21 rules
Start term: power_Load_1(#0, #1, env, static)
Considered paths: nonterm paths and paths from start to sinks
Rules:
power_NE_146(iconst_2, i16, x, env, static) -{0,0}> power_NE_152(2, i16, env, static) :|: 2 <= i16 && iconst_2 = 2 && x = iconst_2
power_Load_1(i2, i3, env, static) -{16,16}> power_NE_52(i2, i3, env, static'1) :|: static'1 <= static''' + 1 && 0 <= static''' && static''' <= static + 2 && 0 <= static && 0 <= static'1
power_Load_646(i206, i16, i207, i208, i209, env, static) -{1,1}> power_LE_656(i206, i16, i208, i207, i209, env, static) :|: 0 <= i208 && 2 <= i16
power_NE_136(i36, i15, iconst_2, env, static) -{0,0}> power_NE_150(i36, i15, 2, env, static) :|: i15 <= -1 && iconst_2 = 2 && 3 <= i36
power_Load_795'(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_646(i206, i16, i207 * i207, i268', i258, env, static) :|: i226 + -2 * div < 2 && 0 < i226 + -2 * div + 2 && div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_70(i2, iconst_1, x, env, static) -{0,0}> power_NE_75(i2, 1, env, static) :|: iconst_1 = 1 && x = iconst_1
power_NE_146(i37, i16, x, env, static) -{3,3}> power_Load_646(i37, i16, i37, i16, 1, env, static) :|: 1 <= i16 && 2 <= i16 && i37 <= 1 && 0 <= i16 && i37 < 2 && x = 2
power_NE_136(iconst_2, i15, x, env, static) -{0,0}> power_NE_148(2, i15, env, static) :|: i15 <= -1 && iconst_2 = 2 && x = iconst_2
power_LE_656'(i206, i16, i226, i207, i209, env, static) -{5,5}> power_NE_686(i206, i16, i226 + -2 * div, 1, i207, i226, i209, env, static) :|: i226 + -2 * div < 2 && 0 < i226 + -2 * div + 2 && 0 <= i231' && 2 <= i16 && i231' <= 1 && 1 <= i226 && i226 + -2 * div = i231' && 0 < i226
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{5,5}> power_Load_795(i206, i16, i207, i226, i209 * i207, env, static) :|: 1 <= i226 && 2 <= i16 && i209 * i207 = i258' && x = 1 && x' = 1
power_NE_70(i2, i16, x, env, static) -{3,3}> power_NE_146(i2, i16, 2, env, static) :|: 2 <= i16 && 1 < i16 && x = 1
power_NE_52(i2, iconst_0, env, static) -{0,0}> power_NE_55(i2, 0, env, static) :|: iconst_0 = 0
power_NE_136(i35, i15, iconst_2, env, static) -{0,0}> power_NE_147(i35, i15, 2, env, static) :|: i15 <= -1 && i35 <= 1 && iconst_2 = 2
power_NE_70(i2, i15, x, env, static) -{3,3}> power_NE_136(i2, i15, 2, env, static) :|: i15 <= -1 && i15 < 1 && x = 1
power_NE_146(i38, i16, x, env, static) -{3,3}> power_Load_646(i38, i16, i38, i16, 1, env, static) :|: 2 < i38 && 2 <= i16 && 3 <= i38 && 0 <= i16 && x = 2
power_Load_795(i206, i16, i207, i226, i258, env, static) -{9,9}> power_Load_795'(i206, i16, i207, i226, i258, env, static) :|: div = i268' && 0 <= i268' && 2 <= i16 && 1 <= i226 && i207 * i207 = i267'
power_NE_686(i206, i16, x, x', i207, i226, i209, env, static) -{1,1}> power_Load_795(i206, i16, i207, i226, i209, env, static) :|: 1 <= i226 && 2 <= i16 && x = 0 && x' = 1
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: i8 < 0
power_NE_52(i2, i8, env, static) -{3,3}> power_NE_70(i2, i8, 1, env, static) :|: 0 < i8
power_LE_656(i206, i16, iconst_0, i207, i209, env, static) -{0,0}> power_LE_658(i206, i16, 0, i207, i209, env, static) :|: 0 <= iconst_0 && iconst_0 = 0 && 2 <= i16
power_LE_656(i206, i16, i226, i207, i209, env, static) -{5,5}> power_LE_656'(i206, i16, i226, i207, i209, env, static) :|: 0 <= i231' && 2 <= i16 && i231' <= 1 && 1 <= i226 && i226 + -2 * div = i231' && 0 < i226