Termination of the given JBC could be proven:

0 JBC
↳1 JBCToGraph (⇒, 461 ms)
↳2 JBCTerminationGraph
↳3 TerminationGraphToSCCProof (⇒, 10 ms)
↳4 JBCTerminationSCC
↳5 SCCToIntTRSProof (⇒, 196 ms)
↳6 intTRS
↳7 TerminationGraphProcessor (⇒, 75 ms)
↳8 AND
    ↳9 intTRS
        ↳10 PolynomialOrderProcessor (⇔, 0 ms)
        ↳11 YES
    ↳12 intTRS
        ↳13 PolynomialOrderProcessor (⇔, 8 ms)
        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:
public class AProVEMathRecursive {
  public static void main(String[] args) {
    Random.args = args;
    int x = Random.random();
    int y = Random.random();
    power(x, y);
  }

  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 if (exponent % 2 == 1) {
      return base * power(base, exponent-1);
    } else {
      int halfPower = power(base, exponent/2);
      return halfPower * halfPower;
    }
  }
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    if (args.length <= index) {
      return 0;
    }
    String string = args[index];
    index++;
    if (string == null) {
      return 0;
    }
    return string.length();
  }
}


(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
AProVEMathRecursive.main([Ljava/lang/String;)V: Graph of 171 nodes with 0 SCCs.

AProVEMathRecursive.power(II)I: Graph of 125 nodes with 0 SCCs.


(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: AProVEMathRecursive.power(II)I
SCC calls the following helper methods: AProVEMathRecursive.power(II)I
Performed SCC analyses:
  • Used field analysis yielded the following read fields:
  • Marker field analysis yielded the following relations that could be markers:

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 63 IRules

P rules:
f516_0_power_GT(EOS, i83, i88, i83, i88, i88) → f519_0_power_GT(EOS, i83, i88, i83, i88, i88)
f519_0_power_GT(EOS, i83, i88, i83, i88, i88) → f524_0_power_Load(EOS, i83, i88, i83, i88) | >(i88, 0)
f524_0_power_Load(EOS, i83, i88, i83, i88) → f528_0_power_ConstantStackPush(EOS, i83, i88, i83, i88, i88)
f528_0_power_ConstantStackPush(EOS, i83, i88, i83, i88, i88) → f532_0_power_NE(EOS, i83, i88, i83, i88, i88, 1)
f532_0_power_NE(EOS, i83, i113, i83, i113, i113, matching1) → f604_0_power_NE(EOS, i83, i113, i83, i113, i113, 1) | =(matching1, 1)
f604_0_power_NE(EOS, i83, i113, i83, i113, i113, matching1) → f616_0_power_Load(EOS, i83, i113, i83, i113) | &&(>(i113, 1), =(matching1, 1))
f616_0_power_Load(EOS, i83, i113, i83, i113) → f628_0_power_ConstantStackPush(EOS, i83, i113, i83, i113, i83)
f628_0_power_ConstantStackPush(EOS, i83, i113, i83, i113, i83) → f635_0_power_NE(EOS, i83, i113, i83, i113, i83, 2)
f635_0_power_NE(EOS, i142, i113, i142, i113, i142, matching1) → f706_0_power_NE(EOS, i142, i113, i142, i113, i142, 2) | =(matching1, 2)
f635_0_power_NE(EOS, i144, i113, i144, i113, i144, matching1) → f709_0_power_NE(EOS, i144, i113, i144, i113, i144, 2) | =(matching1, 2)
f706_0_power_NE(EOS, i142, i113, i142, i113, i142, matching1) → f723_0_power_Load(EOS, i142, i113, i142, i113) | &&(<(i142, 2), =(matching1, 2))
f723_0_power_Load(EOS, i142, i113, i142, i113) → f746_0_power_ConstantStackPush(EOS, i142, i113, i142, i113, i113)
f746_0_power_ConstantStackPush(EOS, i142, i113, i142, i113, i113) → f767_0_power_IntArithmetic(EOS, i142, i113, i142, i113, i113, 2)
f767_0_power_IntArithmetic(EOS, i142, i113, i142, i113, i113, matching1) → f777_0_power_ConstantStackPush(EOS, i142, i113, i142, i113, %(i113, 2)) | =(matching1, 2)
f777_0_power_ConstantStackPush(EOS, i142, i113, i142, i113, i159) → f785_0_power_NE(EOS, i142, i113, i142, i113, i159, 1)
f785_0_power_NE(EOS, i142, i113, i142, i113, matching1, matching2) → f795_0_power_NE(EOS, i142, i113, i142, i113, 0, 1) | &&(&&(=(i159, 0), =(matching1, 0)), =(matching2, 1))
f785_0_power_NE(EOS, i142, i113, i142, i113, matching1, matching2) → f796_0_power_NE(EOS, i142, i113, i142, i113, 1, 1) | &&(&&(=(i159, 1), =(matching1, 1)), =(matching2, 1))
f795_0_power_NE(EOS, i142, i113, i142, i113, matching1, matching2) → f803_0_power_Load(EOS, i142, i113, i142, i113) | &&(=(matching1, 0), =(matching2, 1))
f803_0_power_Load(EOS, i142, i113, i142, i113) → f815_0_power_Load(EOS, i142, i113, i113, i142)
f815_0_power_Load(EOS, i142, i113, i113, i142) → f870_0_power_ConstantStackPush(EOS, i142, i113, i142, i113)
f870_0_power_ConstantStackPush(EOS, i142, i113, i142, i113) → f900_0_power_IntArithmetic(EOS, i142, i113, i142, i113, 2)
f900_0_power_IntArithmetic(EOS, i142, i113, i142, i113, matching1) → f911_0_power_InvokeMethod(EOS, i142, i113, i142, /(i113, 2)) | &&(>(i113, 1), =(matching1, 2))
f911_0_power_InvokeMethod(EOS, i142, i113, i142, i194) → f922_0_power_Load(EOS, i142, i194, i142, i194)
f911_0_power_InvokeMethod(EOS, i142, i113, i142, i194) → f922_1_power_Load(EOS, i142, i113, i142, i194, i142, i194)
f922_0_power_Load(EOS, i142, i194, i142, i194) → f931_0_power_Load(EOS, i142, i194, i142, i194)
f931_0_power_Load(EOS, i142, i194, i142, i194) → f512_0_power_Load(EOS, i142, i194, i142, i194)
f512_0_power_Load(EOS, i83, i84, i83, i84) → f516_0_power_GT(EOS, i83, i84, i83, i84, i84)
f796_0_power_NE(EOS, i142, i113, i142, i113, matching1, matching2) → f805_0_power_Load(EOS, i142, i113, i142, i113) | &&(=(matching1, 1), =(matching2, 1))
f805_0_power_Load(EOS, i142, i113, i142, i113) → f817_0_power_Load(EOS, i142, i113, i142, i113, i142)
f817_0_power_Load(EOS, i142, i113, i142, i113, i142) → f875_0_power_Load(EOS, i142, i113, i142, i113, i142, i142)
f875_0_power_Load(EOS, i142, i113, i142, i113, i142, i142) → f904_0_power_ConstantStackPush(EOS, i142, i113, i142, i113, i142, i142, i113)
f904_0_power_ConstantStackPush(EOS, i142, i113, i142, i113, i142, i142, i113) → f914_0_power_IntArithmetic(EOS, i142, i113, i142, i113, i142, i142, i113, 1)
f914_0_power_IntArithmetic(EOS, i142, i113, i142, i113, i142, i142, i113, matching1) → f924_0_power_InvokeMethod(EOS, i142, i113, i142, i113, i142, i142, -(i113, 1)) | &&(>(i113, 0), =(matching1, 1))
f924_0_power_InvokeMethod(EOS, i142, i113, i142, i113, i142, i142, i197) → f933_0_power_Load(EOS, i142, i197, i142, i197)
f924_0_power_InvokeMethod(EOS, i142, i113, i142, i113, i142, i142, i197) → f933_1_power_Load(EOS, i142, i113, i142, i113, i142, i142, i197, i142, i197)
f933_0_power_Load(EOS, i142, i197, i142, i197) → f939_0_power_Load(EOS, i142, i197, i142, i197)
f939_0_power_Load(EOS, i142, i197, i142, i197) → f512_0_power_Load(EOS, i142, i197, i142, i197)
f709_0_power_NE(EOS, i144, i113, i144, i113, i144, matching1) → f741_0_power_Load(EOS, i144, i113, i144, i113) | &&(>(i144, 2), =(matching1, 2))
f741_0_power_Load(EOS, i144, i113, i144, i113) → f761_0_power_ConstantStackPush(EOS, i144, i113, i144, i113, i113)
f761_0_power_ConstantStackPush(EOS, i144, i113, i144, i113, i113) → f775_0_power_IntArithmetic(EOS, i144, i113, i144, i113, i113, 2)
f775_0_power_IntArithmetic(EOS, i144, i113, i144, i113, i113, matching1) → f782_0_power_ConstantStackPush(EOS, i144, i113, i144, i113, %(i113, 2)) | =(matching1, 2)
f782_0_power_ConstantStackPush(EOS, i144, i113, i144, i113, i160) → f792_0_power_NE(EOS, i144, i113, i144, i113, i160, 1)
f792_0_power_NE(EOS, i144, i113, i144, i113, matching1, matching2) → f800_0_power_NE(EOS, i144, i113, i144, i113, 0, 1) | &&(&&(=(i160, 0), =(matching1, 0)), =(matching2, 1))
f792_0_power_NE(EOS, i144, i113, i144, i113, matching1, matching2) → f801_0_power_NE(EOS, i144, i113, i144, i113, 1, 1) | &&(&&(=(i160, 1), =(matching1, 1)), =(matching2, 1))
f800_0_power_NE(EOS, i144, i113, i144, i113, matching1, matching2) → f810_0_power_Load(EOS, i144, i113, i144, i113) | &&(=(matching1, 0), =(matching2, 1))
f810_0_power_Load(EOS, i144, i113, i144, i113) → f859_0_power_Load(EOS, i144, i113, i113, i144)
f859_0_power_Load(EOS, i144, i113, i113, i144) → f889_0_power_ConstantStackPush(EOS, i144, i113, i144, i113)
f889_0_power_ConstantStackPush(EOS, i144, i113, i144, i113) → f907_0_power_IntArithmetic(EOS, i144, i113, i144, i113, 2)
f907_0_power_IntArithmetic(EOS, i144, i113, i144, i113, matching1) → f916_0_power_InvokeMethod(EOS, i144, i113, i144, /(i113, 2)) | &&(>(i113, 1), =(matching1, 2))
f916_0_power_InvokeMethod(EOS, i144, i113, i144, i196) → f926_0_power_Load(EOS, i144, i196, i144, i196)
f916_0_power_InvokeMethod(EOS, i144, i113, i144, i196) → f926_1_power_Load(EOS, i144, i113, i144, i196, i144, i196)
f926_0_power_Load(EOS, i144, i196, i144, i196) → f935_0_power_Load(EOS, i144, i196, i144, i196)
f935_0_power_Load(EOS, i144, i196, i144, i196) → f512_0_power_Load(EOS, i144, i196, i144, i196)
f801_0_power_NE(EOS, i144, i113, i144, i113, matching1, matching2) → f813_0_power_Load(EOS, i144, i113, i144, i113) | &&(=(matching1, 1), =(matching2, 1))
f813_0_power_Load(EOS, i144, i113, i144, i113) → f867_0_power_Load(EOS, i144, i113, i144, i113, i144)
f867_0_power_Load(EOS, i144, i113, i144, i113, i144) → f893_0_power_Load(EOS, i144, i113, i144, i113, i144, i144)
f893_0_power_Load(EOS, i144, i113, i144, i113, i144, i144) → f909_0_power_ConstantStackPush(EOS, i144, i113, i144, i113, i144, i144, i113)
f909_0_power_ConstantStackPush(EOS, i144, i113, i144, i113, i144, i144, i113) → f920_0_power_IntArithmetic(EOS, i144, i113, i144, i113, i144, i144, i113, 1)
f920_0_power_IntArithmetic(EOS, i144, i113, i144, i113, i144, i144, i113, matching1) → f929_0_power_InvokeMethod(EOS, i144, i113, i144, i113, i144, i144, -(i113, 1)) | &&(>(i113, 0), =(matching1, 1))
f929_0_power_InvokeMethod(EOS, i144, i113, i144, i113, i144, i144, i198) → f937_0_power_Load(EOS, i144, i198, i144, i198)
f929_0_power_InvokeMethod(EOS, i144, i113, i144, i113, i144, i144, i198) → f937_1_power_Load(EOS, i144, i113, i144, i113, i144, i144, i198, i144, i198)
f937_0_power_Load(EOS, i144, i198, i144, i198) → f941_0_power_Load(EOS, i144, i198, i144, i198)
f941_0_power_Load(EOS, i144, i198, i144, i198) → f512_0_power_Load(EOS, i144, i198, i144, i198)

Combined rules. Obtained 8 IRules

P rules:
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f922_1_power_Load(EOS, x0, x1, x0, /(x1, 2), x0, /(x1, 2)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f516_0_power_GT(EOS, x0, /(x1, 2), x0, /(x1, 2), /(x1, 2)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f933_1_power_Load(EOS, x0, x1, x0, x1, x0, x0, -(x1, 1), x0, -(x1, 1)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 1))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f516_0_power_GT(EOS, x0, -(x1, 1), x0, -(x1, 1), -(x1, 1)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 1))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f926_1_power_Load(EOS, x0, x1, x0, /(x1, 2), x0, /(x1, 2)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f516_0_power_GT(EOS, x0, /(x1, 2), x0, /(x1, 2), /(x1, 2)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f937_1_power_Load(EOS, x0, x1, x0, x1, x0, x0, -(x1, 1), x0, -(x1, 1)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 1))
f516_0_power_GT(EOS, x0, x1, x0, x1, x1) → f516_0_power_GT(EOS, x0, -(x1, 1), x0, -(x1, 1), -(x1, 1)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 1))

Filtered ground terms:


f516_0_power_GT(x1, x2, x3, x4, x5, x6) → f516_0_power_GT(x2, x3, x4, x5, x6)
Cond_f516_0_power_GT(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT(x1, x3, x4, x5, x6, x7)
f922_1_power_Load(x1, x2, x3, x4, x5, x6, x7) → f922_1_power_Load(x2, x3, x4, x5, x6, x7)
Cond_f516_0_power_GT1(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT1(x1, x3, x4, x5, x6, x7)
Cond_f516_0_power_GT2(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT2(x1, x3, x4, x5, x6, x7)
f933_1_power_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f933_1_power_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f516_0_power_GT3(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT3(x1, x3, x4, x5, x6, x7)
Cond_f516_0_power_GT4(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT4(x1, x3, x4, x5, x6, x7)
f926_1_power_Load(x1, x2, x3, x4, x5, x6, x7) → f926_1_power_Load(x2, x3, x4, x5, x6, x7)
Cond_f516_0_power_GT5(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT5(x1, x3, x4, x5, x6, x7)
Cond_f516_0_power_GT6(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT6(x1, x3, x4, x5, x6, x7)
f937_1_power_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f937_1_power_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f516_0_power_GT7(x1, x2, x3, x4, x5, x6, x7) → Cond_f516_0_power_GT7(x1, x3, x4, x5, x6, x7)

Filtered duplicate terms:


f516_0_power_GT(x1, x2, x3, x4, x5) → f516_0_power_GT(x3, x5)
Cond_f516_0_power_GT(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT(x1, x4, x6)
f922_1_power_Load(x1, x2, x3, x4, x5, x6) → f922_1_power_Load(x5, x6)
Cond_f516_0_power_GT1(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT1(x1, x4, x6)
Cond_f516_0_power_GT2(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT2(x1, x4, x6)
f933_1_power_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f933_1_power_Load(x8, x9)
Cond_f516_0_power_GT3(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT3(x1, x4, x6)
Cond_f516_0_power_GT4(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT4(x1, x4, x6)
f926_1_power_Load(x1, x2, x3, x4, x5, x6) → f926_1_power_Load(x5, x6)
Cond_f516_0_power_GT5(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT5(x1, x4, x6)
Cond_f516_0_power_GT6(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT6(x1, x4, x6)
f937_1_power_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f937_1_power_Load(x8, x9)
Cond_f516_0_power_GT7(x1, x2, x3, x4, x5, x6) → Cond_f516_0_power_GT7(x1, x4, x6)

Filtered unneeded terms:


Cond_f516_0_power_GT(x1, x2, x3) → Cond_f516_0_power_GT(x1)
Cond_f516_0_power_GT2(x1, x2, x3) → Cond_f516_0_power_GT2(x1)
Cond_f516_0_power_GT4(x1, x2, x3) → Cond_f516_0_power_GT4(x1)
Cond_f516_0_power_GT6(x1, x2, x3) → Cond_f516_0_power_GT6(x1)

Prepared 8 rules for path length conversion:

P rules:
f516_0_power_GT(x0, x1) → f922_1_power_Load(x0, /(x1, 2)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(x0, x1) → f516_0_power_GT(x0, /(x1, 2)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(x0, x1) → f933_1_power_Load(x0, -(x1, 1)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 1))
f516_0_power_GT(x0, x1) → f516_0_power_GT(x0, -(x1, 1)) | &&(&&(>(x1, 1), <(x0, 2)), =(%(x1, 2), 1))
f516_0_power_GT(x0, x1) → f926_1_power_Load(x0, /(x1, 2)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(x0, x1) → f516_0_power_GT(x0, /(x1, 2)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 0))
f516_0_power_GT(x0, x1) → f937_1_power_Load(x0, -(x1, 1)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 1))
f516_0_power_GT(x0, x1) → f516_0_power_GT(x0, -(x1, 1)) | &&(&&(>(x1, 1), >(x0, 2)), =(%(x1, 2), 1))

Finished conversion. Obtained 8 rules.

P rules:
f516_0_power_GT(x2, x3) → f516_0_power_GT'(x2, x3) | &&(&&(>(x3, 1), <(x2, 2)), =(-(x3, *(2, div)), 0))
f516_0_power_GT'(x2, x3) → f516_0_power_GT(x2, arith) | &&(&&(&&(&&(&&(&&(>(x3, 1), >=(-(x3, *(2, div)), 0)), =(-(x3, *(2, div)), 0)), <(-(x3, *(2, div)), 2)), >=(-(x3, *(2, arith)), 0)), <(x2, 2)), <(-(x3, *(2, arith)), 2))
f516_0_power_GT(x6, x7) → f516_0_power_GT'(x6, x7) | &&(&&(>(x7, 1), <(x6, 2)), =(-(x7, *(2, div)), 1))
f516_0_power_GT'(x6, x7) → f516_0_power_GT(x6, -(x7, 1)) | &&(&&(&&(&&(>(x7, 1), >=(-(x7, *(2, div)), 0)), =(-(x7, *(2, div)), 1)), <(x6, 2)), <(-(x7, *(2, div)), 2))
f516_0_power_GT(x10, x11) → f516_0_power_GT'(x10, x11) | &&(&&(>(x11, 1), >(x10, 2)), =(-(x11, *(2, div)), 0))
f516_0_power_GT'(x10, x11) → f516_0_power_GT(x10, arith) | &&(&&(&&(&&(&&(&&(>(x11, 1), >=(-(x11, *(2, div)), 0)), =(-(x11, *(2, div)), 0)), <(-(x11, *(2, div)), 2)), >=(-(x11, *(2, arith)), 0)), >(x10, 2)), <(-(x11, *(2, arith)), 2))
f516_0_power_GT(x14, x15) → f516_0_power_GT'(x14, x15) | &&(&&(>(x15, 1), >(x14, 2)), =(-(x15, *(2, div)), 1))
f516_0_power_GT'(x14, x15) → f516_0_power_GT(x14, -(x15, 1)) | &&(&&(&&(&&(>(x15, 1), >=(-(x15, *(2, div)), 0)), =(-(x15, *(2, div)), 1)), >(x14, 2)), <(-(x15, *(2, div)), 2))

(6) Obligation:

Rules:
f516_0_power_GT(x2, x3) → f516_0_power_GT'(x2, x3) | &&(&&(>(x3, 1), <(x2, 2)), =(-(x3, *(2, div)), 0))
f516_0_power_GT'(x2, x3) → f516_0_power_GT(x2, arith) | &&(&&(&&(&&(&&(&&(>(x3, 1), >=(-(x3, *(2, div)), 0)), =(-(x3, *(2, div)), 0)), <(-(x3, *(2, div)), 2)), >=(-(x3, *(2, arith)), 0)), <(x2, 2)), <(-(x3, *(2, arith)), 2))
f516_0_power_GT(x6, x7) → f516_0_power_GT'(x6, x7) | &&(&&(>(x7, 1), <(x6, 2)), =(-(x7, *(2, div)), 1))
f516_0_power_GT'(x6, x7) → f516_0_power_GT(x6, -(x7, 1)) | &&(&&(&&(&&(>(x7, 1), >=(-(x7, *(2, div)), 0)), =(-(x7, *(2, div)), 1)), <(x6, 2)), <(-(x7, *(2, div)), 2))
f516_0_power_GT(x10, x11) → f516_0_power_GT'(x10, x11) | &&(&&(>(x11, 1), >(x10, 2)), =(-(x11, *(2, div)), 0))
f516_0_power_GT'(x10, x11) → f516_0_power_GT(x10, arith) | &&(&&(&&(&&(&&(&&(>(x11, 1), >=(-(x11, *(2, div)), 0)), =(-(x11, *(2, div)), 0)), <(-(x11, *(2, div)), 2)), >=(-(x11, *(2, arith)), 0)), >(x10, 2)), <(-(x11, *(2, arith)), 2))
f516_0_power_GT(x14, x15) → f516_0_power_GT'(x14, x15) | &&(&&(>(x15, 1), >(x14, 2)), =(-(x15, *(2, div)), 1))
f516_0_power_GT'(x14, x15) → f516_0_power_GT(x14, -(x15, 1)) | &&(&&(&&(&&(>(x15, 1), >=(-(x15, *(2, div)), 0)), =(-(x15, *(2, div)), 1)), >(x14, 2)), <(-(x15, *(2, div)), 2))

(7) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained 2 non-trivial SCCs.


(8) Complex Obligation (AND)

(9) Obligation:

Rules:
f516_0_power_GT(x13, x14) → f516_0_power_GT'(x13, x14) | &&(&&(>(x14, 1), >(x13, 2)), =(-(x14, *(2, x15)), 0))
f516_0_power_GT'(x16, x17) → f516_0_power_GT(x16, x18) | &&(&&(&&(&&(&&(&&(>(x17, 1), >=(-(x17, *(2, x19)), 0)), =(-(x17, *(2, x19)), 0)), <(-(x17, *(2, x19)), 2)), >=(-(x17, *(2, x18)), 0)), >(x16, 2)), <(-(x17, *(2, x18)), 2))
f516_0_power_GT'(x23, x24) → f516_0_power_GT(x23, -(x24, 1)) | &&(&&(&&(&&(>(x24, 1), >=(-(x24, *(2, x25)), 0)), =(-(x24, *(2, x25)), 1)), >(x23, 2)), <(-(x24, *(2, x25)), 2))
f516_0_power_GT(x20, x21) → f516_0_power_GT'(x20, x21) | &&(&&(>(x21, 1), >(x20, 2)), =(-(x21, *(2, x22)), 1))

(10) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f516_0_power_GT(x14, x16)] = 1 + 2·x16
[f516_0_power_GT'(x19, x21)] = 2·x21

Therefore the following rule(s) have been dropped:


f516_0_power_GT(x0, x1) → f516_0_power_GT'(x0, x1) | &&(&&(>(x1, 1), >(x0, 2)), =(-(x1, *(2, x2)), 0))
f516_0_power_GT'(x3, x4) → f516_0_power_GT(x3, x5) | &&(&&(&&(&&(&&(&&(>(x4, 1), >=(-(x4, *(2, x6)), 0)), =(-(x4, *(2, x6)), 0)), <(-(x4, *(2, x6)), 2)), >=(-(x4, *(2, x5)), 0)), >(x3, 2)), <(-(x4, *(2, x5)), 2))
f516_0_power_GT'(x7, x8) → f516_0_power_GT(x7, -(x8, 1)) | &&(&&(&&(&&(>(x8, 1), >=(-(x8, *(2, x9)), 0)), =(-(x8, *(2, x9)), 1)), >(x7, 2)), <(-(x8, *(2, x9)), 2))
f516_0_power_GT(x10, x11) → f516_0_power_GT'(x10, x11) | &&(&&(>(x11, 1), >(x10, 2)), =(-(x11, *(2, x12)), 1))

(11) YES

(12) Obligation:

Rules:
f516_0_power_GT(x0, x1) → f516_0_power_GT'(x0, x1) | &&(&&(>(x1, 1), <(x0, 2)), =(-(x1, *(2, x2)), 0))
f516_0_power_GT'(x3, x4) → f516_0_power_GT(x3, x5) | &&(&&(&&(&&(&&(&&(>(x4, 1), >=(-(x4, *(2, x6)), 0)), =(-(x4, *(2, x6)), 0)), <(-(x4, *(2, x6)), 2)), >=(-(x4, *(2, x5)), 0)), <(x3, 2)), <(-(x4, *(2, x5)), 2))
f516_0_power_GT'(x10, x11) → f516_0_power_GT(x10, -(x11, 1)) | &&(&&(&&(&&(>(x11, 1), >=(-(x11, *(2, x12)), 0)), =(-(x11, *(2, x12)), 1)), <(x10, 2)), <(-(x11, *(2, x12)), 2))
f516_0_power_GT(x7, x8) → f516_0_power_GT'(x7, x8) | &&(&&(>(x8, 1), <(x7, 2)), =(-(x8, *(2, x9)), 1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:


[f516_0_power_GT(x14, x16)] = 1 + 2·x16
[f516_0_power_GT'(x19, x21)] = 2·x21

Therefore the following rule(s) have been dropped:


f516_0_power_GT(x0, x1) → f516_0_power_GT'(x0, x1) | &&(&&(>(x1, 1), <(x0, 2)), =(-(x1, *(2, x2)), 0))
f516_0_power_GT'(x3, x4) → f516_0_power_GT(x3, x5) | &&(&&(&&(&&(&&(&&(>(x4, 1), >=(-(x4, *(2, x6)), 0)), =(-(x4, *(2, x6)), 0)), <(-(x4, *(2, x6)), 2)), >=(-(x4, *(2, x5)), 0)), <(x3, 2)), <(-(x4, *(2, x5)), 2))
f516_0_power_GT'(x7, x8) → f516_0_power_GT(x7, -(x8, 1)) | &&(&&(&&(&&(>(x8, 1), >=(-(x8, *(2, x9)), 0)), =(-(x8, *(2, x9)), 1)), <(x7, 2)), <(-(x8, *(2, x9)), 2))
f516_0_power_GT(x10, x11) → f516_0_power_GT'(x10, x11) | &&(&&(>(x11, 1), <(x10, 2)), =(-(x11, *(2, x12)), 1))

(14) YES