Termination proof of /tmp/tmppSSxen/Nim.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 3251 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 7 ms)

        ↳7 intTRS

        ↳8 LinearRankingProcessor (⇔, 7 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 81 ms)

        ↳12 intTRS

        ↳13 LinearRankingProcessor (⇔, 0 ms)

        ↳14 YES

    ↳15 JBCTerminationSCC

        ↳16 SCCToIntTRSProof (⇒, 418 ms)

        ↳17 intTRS

        ↳18 PolynomialOrderProcessor (⇒, 0 ms)

        ↳19 intTRS

        ↳20 PolynomialOrderProcessor (⇔, 8 ms)

        ↳21 YES

    ↳22 JBCTerminationSCC

        ↳23 SCCToIntTRSProof (⇒, 105 ms)

        ↳24 intTRS

        ↳25 PolynomialOrderProcessor (⇔, 8 ms)

        ↳26 YES

    ↳27 JBCTerminationSCC

        ↳28 SCCToIntTRSProof (⇒, 602 ms)

        ↳29 intTRS

        ↳30 PolynomialOrderProcessor (⇔, 0 ms)

        ↳31 YES

    ↳32 JBCTerminationSCC

        ↳33 SCCToIntTRSProof (⇒, 54 ms)

        ↳34 intTRS

        ↳35 LinearRankingProcessor (⇔, 0 ms)

        ↳36 YES

    ↳37 JBCTerminationSCC

        ↳38 SCCToIntTRSProof (⇒, 185 ms)

        ↳39 intTRS

        ↳40 PolynomialOrderProcessor (⇔, 3 ms)

        ↳41 YES

    ↳42 JBCTerminationSCC

        ↳43 SCCToIntTRSProof (⇒, 676 ms)

        ↳44 intTRS

        ↳45 PolynomialOrderProcessor (⇔, 0 ms)

        ↳46 YES

    ↳47 JBCTerminationSCC

        ↳48 SCCToIntTRSProof (⇒, 92 ms)

        ↳49 intTRS

        ↳50 LinearRankingProcessor (⇔, 0 ms)

        ↳51 YES

    ↳52 JBCTerminationSCC

        ↳53 SCCToIntTRSProof (⇒, 9 ms)

        ↳54 intTRS

        ↳55 PolynomialOrderProcessor (⇔, 0 ms)

        ↳56 YES

    ↳57 JBCTerminationSCC

        ↳58 SCCToIntTRSProof (⇒, 1949 ms)

        ↳59 intTRS

        ↳60 PolynomialOrderProcessor (⇒, 0 ms)

        ↳61 intTRS

        ↳62 PolynomialOrderProcessor (⇔, 0 ms)

        ↳63 YES

(0) Obligation:

JBC Problem based on JBC Program:

public class Nim {

  public static int binaryToDecimal(
                          int[] binaryRepresentation) {
    int n = 0;
    int p2 = 1;
    for (int i=0; i < binaryRepresentation.length; i++) {
      n = n + binaryRepresentation[i] * p2;
      p2 = p2 * 2;
    }
    return n;
  }

  public static void decimalToBinaryAux(int n, int i,
      int[] binaryRepresentation) {
    if (n > 0) {
      binaryRepresentation[i] = n % 2;
      decimalToBinaryAux(n/2, i+1, binaryRepresentation);
    }
  }

  public static int[] decimalToBinary(int n, int k) {
    int[] binaryRepresentation = new int[k];
    decimalToBinaryAux(n, 0, binaryRepresentation);
    return binaryRepresentation;
  }

  public static int getBinaryLength(int[] decimalTab) {
    // search the largest value
    int max = decimalTab[0];
    for (int i = 1; i < decimalTab.length; i++) {
      if (decimalTab[i] > max) {
        max = decimalTab[i];
      }
    }
    int k = 0;
    int p = 1;
    while (p <= max) {
      ++k;
      p *= 2;
    }
    return k;
  }

  public static int[][] decomposition(int[] decimalTab) {
    int k = getBinaryLength(decimalTab);
    int[][] binaryTab = new int[decimalTab.length][];
    for (int i = 0; i < decimalTab.length; i++) {
      binaryTab[i] = decimalToBinary(decimalTab[i], k);
    }
    return binaryTab;
  }

  public static int[] binaryGrundy(int[][] binaryTab) {
    int k = binaryTab[0].length;
    int[] grundyBinaire = new int[k];
    for (int j = 0; j < k; j++) {
      for (int i = 0; i < binaryTab.length; i++) {
        grundyBinaire[j] =
          (grundyBinaire[j] + binaryTab[i][j]) % 2;
      }
    }
    return grundyBinaire;
  }

  public static int Grundy(int[] decimalTab) {
    int[][] binaryTab = decomposition(decimalTab);
    return binaryToDecimal(binaryGrundy(binaryTab));
  }

  public static int[] loserPick(int[] decimalTab) {
    int i = 0;
    while (decimalTab[i] == 0) {
      i++;
    }
    int[] play = { i, 1 };
    return play;
  }

  public static int[] pick(int[] decimalTab) {
    int[][] binaryTab = decomposition(decimalTab);
    int k = binaryTab[0].length;
    int[] grundyBin = binaryGrundy(binaryTab);

    if (binaryToDecimal(grundyBin) == 0) {
      return loserPick(decimalTab);
    }
    int j = k - 1;
    while (grundyBin[j] == 0) {
      j--;
    }
    int i = 0;
    while (binaryTab[i][j] == 0) {
      i++;
    }
    for (int h = 0; h < grundyBin.length; h++) {
      if (grundyBin[h] == 1) {
        binaryTab[i][h] = 1 - binaryTab[i][h];
      }
    }
    int[] play = new int[2];
    play[0] = i;
    play[1] = decimalTab[i] -
         binaryToDecimal(binaryTab[i]);
    return play;
  }

  public static void main(String[] args) {
      Random.args = args;
      if (args.length < 4)  return;
      int[] game = new int[4]; // = { 6, 9, 1, 2 };
      game[0] = Random.random();
      game[1] = Random.random();
      game[2] = Random.random();
      game[3] = Random.random();
      for (int n = 0; n < 20; n++) {
	  int tt = 0;
	  //System.out.println();
	  for (int i = 0; i < game.length; ++i) {
	    //System.out.print(game[i] + " ");
	      tt += game[i];
	  }
	  //System.out.println();
	  if ( tt <= 0 )
	      break;
	  //System.out.println(Grundy(game));
	  int[] play = pick(game);
	  //System.out.println(play[0] + " " + play[1]);
	  game[play[0]] -= play[1];
      } 
  }
}


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

  public static int random() {
      if (index >= args.length)
	  return 0;

      String string = args[index];
      index++;
      return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
Nim.main([Ljava/lang/String;)V: Graph of 336 nodes with 1 SCC.

Nim.pick([I)[I: Graph of 427 nodes with 3 SCCs.

Nim.decomposition([I)[[I: Graph of 107 nodes with 3 SCCs.

Nim.decimalToBinaryAux(II[I)V: Graph of 58 nodes with 0 SCCs.

Nim.binaryGrundy([[I)[I: Graph of 177 nodes with 1 SCC.

Nim.binaryToDecimal([I)I: Graph of 83 nodes with 1 SCC.

Nim.loserPick([I)[I: Graph of 54 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 11 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.loserPick([I)[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 9 IRules

P rules:
f3675_0_loserPick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i797, java.lang.Object(ARRAY(matching3))) → f3679_0_loserPick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i797, java.lang.Object(ARRAY(4)), i797) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f3679_0_loserPick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i802, java.lang.Object(ARRAY(matching3)), i802) → f3682_0_loserPick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i802, java.lang.Object(ARRAY(4)), i802) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f3682_0_loserPick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i802, java.lang.Object(ARRAY(matching3)), i802) → f3686_0_loserPick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i802, i804) | &&(&&(&&(<(i802, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f3686_0_loserPick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i802, matching3) → f3691_0_loserPick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i802, 0) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 0))
f3691_0_loserPick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i802, matching3) → f3696_0_loserPick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i802) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 0))
f3696_0_loserPick_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i802) → f3705_0_loserPick_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), +(i802, 1)) | &&(&&(>=(i802, 0), =(matching1, 4)), =(matching2, 4))
f3705_0_loserPick_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i810) → f3710_0_loserPick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i810) | &&(=(matching1, 4), =(matching2, 4))
f3710_0_loserPick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i810) → f3671_0_loserPick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i810) | &&(=(matching1, 4), =(matching2, 4))
f3671_0_loserPick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i797) → f3675_0_loserPick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i797, java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 4))

Combined rules. Obtained 1 IRules

P rules:
f3675_0_loserPick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(4))) → f3675_0_loserPick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), +(x2, 1), java.lang.Object(ARRAY(4))) | &&(<(x2, 4), >(+(x2, 1), 0))

Filtered ground terms:

f3675_0_loserPick_Load(x1, x2, x3, x4, x5) → f3675_0_loserPick_Load(x4)
Cond_f3675_0_loserPick_Load(x1, x2, x3, x4, x5, x6) → Cond_f3675_0_loserPick_Load(x1, x5)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY

Prepared 1 rules for path length conversion:

P rules:
f3675_0_loserPick_Load(x2) → f3675_0_loserPick_Load(+(x2, 1)) | &&(<(x2, 4), >(+(x2, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f3675_0_loserPick_Load(x0) → f3675_0_loserPick_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(7) Obligation:

Rules:
f3675_0_loserPick_Load(x0) → f3675_0_loserPick_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f3675_0_loserPick_Load(x)] = (-1)·x₁

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f3675_0_loserPick_Load(x0) → f3675_0_loserPick_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.binaryToDecimal([I)I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 23 IRules

P rules:
f11631_0_binaryToDecimal_Load(EOS, o2810, o2810, i3070, i3070) → f11632_0_binaryToDecimal_ArrayLength(EOS, o2810, o2810, i3070, i3070, o2810)
f11632_0_binaryToDecimal_ArrayLength(EOS, java.lang.Object(o2821put), java.lang.Object(o2821put), i3070, i3070, java.lang.Object(o2821put)) → f11633_0_binaryToDecimal_ArrayLength(EOS, java.lang.Object(o2821put), java.lang.Object(o2821put), i3070, i3070, java.lang.Object(o2821put))
f11633_0_binaryToDecimal_ArrayLength(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, java.lang.Object(ARRAY(i3083))) → f11636_0_binaryToDecimal_ArrayLength(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, java.lang.Object(ARRAY(i3083))) | >=(i3083, 0)
f11636_0_binaryToDecimal_ArrayLength(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, java.lang.Object(ARRAY(i3083))) → f11640_0_binaryToDecimal_GE(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, i3083) | >=(i3083, 0)
f11640_0_binaryToDecimal_GE(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, i3083) → f11647_0_binaryToDecimal_GE(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, i3083)
f11647_0_binaryToDecimal_GE(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, i3070, i3083) → f11653_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) | <(i3070, i3083)
f11653_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11660_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11660_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11682_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, java.lang.Object(ARRAY(i3083)))
f11682_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, java.lang.Object(ARRAY(i3083))) → f11705_0_binaryToDecimal_ArrayAccess(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, java.lang.Object(ARRAY(i3083)), i3070)
f11705_0_binaryToDecimal_ArrayAccess(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, java.lang.Object(ARRAY(i3083)), i3070) → f11716_0_binaryToDecimal_ArrayAccess(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, java.lang.Object(ARRAY(i3083)), i3070)
f11716_0_binaryToDecimal_ArrayAccess(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070, java.lang.Object(ARRAY(i3083)), i3070) → f11723_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) | <(i3070, i3083)
f11723_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11742_0_binaryToDecimal_IntArithmetic(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11742_0_binaryToDecimal_IntArithmetic(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11749_0_binaryToDecimal_IntArithmetic(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11749_0_binaryToDecimal_IntArithmetic(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11759_0_binaryToDecimal_Store(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11759_0_binaryToDecimal_Store(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11767_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11767_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11774_0_binaryToDecimal_ConstantStackPush(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11774_0_binaryToDecimal_ConstantStackPush(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11783_0_binaryToDecimal_IntArithmetic(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11783_0_binaryToDecimal_IntArithmetic(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11791_0_binaryToDecimal_Store(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11791_0_binaryToDecimal_Store(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11798_0_binaryToDecimal_Inc(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070)
f11798_0_binaryToDecimal_Inc(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3070) → f11810_0_binaryToDecimal_JMP(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), +(i3070, 1)) | >=(i3070, 0)
f11810_0_binaryToDecimal_JMP(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3126) → f11820_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3126)
f11820_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3126) → f11610_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(i3083)), java.lang.Object(ARRAY(i3083)), i3126)
f11610_0_binaryToDecimal_Load(EOS, o2810, o2810, i3070) → f11631_0_binaryToDecimal_Load(EOS, o2810, o2810, i3070, i3070)

Combined rules. Obtained 1 IRules

P rules:
f11631_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), x1, x1) → f11631_0_binaryToDecimal_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(ARRAY(x0)), +(x1, 1), +(x1, 1)) | &&(&&(>(+(x1, 1), 0), <(x1, x0)), >(+(x0, 1), 0))

Filtered ground terms:

f11631_0_binaryToDecimal_Load(x1, x2, x3, x4, x5) → f11631_0_binaryToDecimal_Load(x2, x3, x4, x5)
Cond_f11631_0_binaryToDecimal_Load(x1, x2, x3, x4, x5, x6) → Cond_f11631_0_binaryToDecimal_Load(x1, x3, x4, x5, x6)

Filtered duplicate terms:

f11631_0_binaryToDecimal_Load(x1, x2, x3, x4) → f11631_0_binaryToDecimal_Load(x2, x4)
Cond_f11631_0_binaryToDecimal_Load(x1, x2, x3, x4, x5) → Cond_f11631_0_binaryToDecimal_Load(x1, x3, x5)

Prepared 1 rules for path length conversion:

P rules:
f11631_0_binaryToDecimal_Load(java.lang.Object(ARRAY(x0)), x1, x0) → f11631_0_binaryToDecimal_Load(java.lang.Object(ARRAY(x0)), +(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), <(x1, x0)), >(+(x0, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f11631_0_binaryToDecimal_Load(v5, x1, x0) → f11631_0_binaryToDecimal_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(12) Obligation:

Rules:
f11631_0_binaryToDecimal_Load(v5, x1, x0) → f11631_0_binaryToDecimal_Load(v6, +(x1, 1), x0) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x0)), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(13) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f11631_0_binaryToDecimal_Load(x)] = (-1)·x₂ + 1·x₃

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f11631_0_binaryToDecimal_Load(x0, x1, x2) → f11631_0_binaryToDecimal_Load(x3, +(x1, 1), x2) | &&(&&(&&(&&(&&(>(x1, -1), <(x1, x2)), >(x2, -1)), >(+(x3, 1), 1)), <=(x3, x0)), >(+(x0, 1), 1))

(14) YES

(15) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.binaryGrundy([[I)[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(16) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 42 IRules

P rules:
f11680_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3090) → f11684_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3090, i945) | &&(=(matching1, 4), =(matching2, 4))
f11684_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3090, i945) → f11686_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3090, i945) | &&(=(matching1, 4), =(matching2, 4))
f11686_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3090, i945) → f11703_0_binaryGrundy_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090) | &&(&&(<(i3090, i945), =(matching1, 4)), =(matching2, 4))
f11703_0_binaryGrundy_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090) → f11714_0_binaryGrundy_Store(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, 0) | &&(=(matching1, 4), =(matching2, 4))
f11714_0_binaryGrundy_Store(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, matching3) → f11721_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, 0) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 0))
f11721_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, matching3) → f11944_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, 0) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 0))
f11944_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3172) → f12060_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3172) | &&(=(matching1, 4), =(matching2, 4))
f12060_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3219) → f12135_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3219) | &&(=(matching1, 4), =(matching2, 4))
f12135_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3227) → f12223_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3227) | &&(=(matching1, 4), =(matching2, 4))
f12223_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3236) → f12226_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3236, i3236) | &&(=(matching1, 4), =(matching2, 4))
f12226_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3236, i3236) → f12228_0_binaryGrundy_ArrayLength(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3236, i3236, java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 4))
f12228_0_binaryGrundy_ArrayLength(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3236, i3236, java.lang.Object(ARRAY(matching3))) → f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3236, i3236, 4) | &&(&&(&&(>=(4, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, i3240, matching3) → f12232_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, i3240, 4) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3241, i3241, matching3) → f12233_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3241, i3241, 4) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f12232_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, i3240, matching3) → f12235_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240) | &&(&&(&&(<(i3240, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f12235_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240) → f12238_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945))) | &&(=(matching1, 4), =(matching2, 4))
f12238_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945))) → f12242_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12242_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12248_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i945))) | &&(=(matching1, 4), =(matching2, 4))
f12248_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i945))) → f12250_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12250_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i945)), i3090) → f12251_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12251_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i945)), i3090) → f12254_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(&&(<(i3090, i945), =(matching1, 4)), =(matching2, 4))
f12254_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12256_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 4))
f12256_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(matching3))) → f12258_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(4)), i3240) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f12258_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(matching3)), i3240) → f12262_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, o2981) | &&(&&(&&(<(i3240, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f12262_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, o2981) → f12265_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, o2981, i3090) | &&(=(matching1, 4), =(matching2, 4))
f12265_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(o2983put), i3090) → f12267_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(o2983put), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12267_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i3246)), i3090) → f12270_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i3246)), i3090) | &&(&&(>=(i3246, 0), =(matching1, 4)), =(matching2, 4))
f12270_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i3246)), i3090) → f12275_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i3246)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12275_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090, java.lang.Object(ARRAY(i3246)), i3090) → f12280_0_binaryGrundy_IntArithmetic(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(&&(<(i3090, i3246), =(matching1, 4)), =(matching2, 4))
f12280_0_binaryGrundy_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12285_0_binaryGrundy_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12285_0_binaryGrundy_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12292_0_binaryGrundy_IntArithmetic(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12292_0_binaryGrundy_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12299_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12299_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12305_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) | &&(=(matching1, 4), =(matching2, 4))
f12305_0_binaryGrundy_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240, java.lang.Object(ARRAY(i945)), i3090) → f12313_0_binaryGrundy_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240) | &&(&&(<(i3090, i945), =(matching1, 4)), =(matching2, 4))
f12313_0_binaryGrundy_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3240) → f12321_0_binaryGrundy_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, +(i3240, 1)) | &&(&&(>=(i3240, 0), =(matching1, 4)), =(matching2, 4))
f12321_0_binaryGrundy_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3250) → f12330_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3250) | &&(=(matching1, 4), =(matching2, 4))
f12330_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3250) → f12223_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3250) | &&(=(matching1, 4), =(matching2, 4))
f12233_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090, i3241, i3241, matching3) → f12237_0_binaryGrundy_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090) | &&(&&(&&(>=(i3241, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f12237_0_binaryGrundy_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090) → f12241_0_binaryGrundy_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), +(i3090, 1)) | &&(&&(>=(i3090, 0), =(matching1, 4)), =(matching2, 4))
f12241_0_binaryGrundy_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3243) → f12247_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3243) | &&(=(matching1, 4), =(matching2, 4))
f12247_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3243) → f11674_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3243) | &&(=(matching1, 4), =(matching2, 4))
f11674_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i945, java.lang.Object(ARRAY(i945)), i3090) → f11680_0_binaryGrundy_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i945, java.lang.Object(ARRAY(i945)), i3090, i3090) | &&(=(matching1, 4), =(matching2, 4))

Combined rules. Obtained 2 IRules

P rules:
f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(x2)), x3, x4, x4, 4) → f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(x2)), x3, +(x4, 1), +(x4, 1), 4) | &&(&&(>(+(x4, 1), 0), <(x4, 4)), <(x3, x2))
f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(x2)), x3, x4, x4, 4) → f12230_0_binaryGrundy_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(x2)), +(x3, 1), 0, 0, 4) | &&(&&(>(+(x4, 1), 4), <(+(x3, 1), x2)), >(+(x3, 1), 0))

Filtered ground terms:

f12230_0_binaryGrundy_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f12230_0_binaryGrundy_GE(x4, x5, x6, x7, x8)
Cond_f12230_0_binaryGrundy_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f12230_0_binaryGrundy_GE(x1, x5, x6, x7, x8, x9)
Cond_f12230_0_binaryGrundy_GE1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f12230_0_binaryGrundy_GE1(x1, x5, x6, x7, x8, x9)

Filtered duplicate terms:

f12230_0_binaryGrundy_GE(x1, x2, x3, x4, x5) → f12230_0_binaryGrundy_GE(x2, x3, x5)
Cond_f12230_0_binaryGrundy_GE(x1, x2, x3, x4, x5, x6) → Cond_f12230_0_binaryGrundy_GE(x1, x3, x4, x6)
Cond_f12230_0_binaryGrundy_GE1(x1, x2, x3, x4, x5, x6) → Cond_f12230_0_binaryGrundy_GE1(x1, x3, x4, x6)

Filtered unneeded terms:

Cond_f12230_0_binaryGrundy_GE1(x1, x2, x3, x4) → Cond_f12230_0_binaryGrundy_GE1(x1, x2, x3)

Prepared 2 rules for path length conversion:

P rules:
f12230_0_binaryGrundy_GE(java.lang.Object(ARRAY(x2)), x3, x4, x2) → f12230_0_binaryGrundy_GE(java.lang.Object(ARRAY(x2)), x3, +(x4, 1), x2) | &&(&&(>(+(x4, 1), 0), <(x4, 4)), <(x3, x2))
f12230_0_binaryGrundy_GE(java.lang.Object(ARRAY(x2)), x3, x4, x2) → f12230_0_binaryGrundy_GE(java.lang.Object(ARRAY(x2)), +(x3, 1), 0, x2) | &&(&&(>(+(x4, 1), 4), <(+(x3, 1), x2)), >(+(x3, 1), 0))

Finished conversion. Obtained 2 rules.

P rules:
f12230_0_binaryGrundy_GE(v10, x1, x2, x0) → f12230_0_binaryGrundy_GE(v11, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 4)), <(x1, x0)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f12230_0_binaryGrundy_GE(v12, x4, x5, x3) → f12230_0_binaryGrundy_GE(v13, +(x4, 1), 0, x3) | &&(&&(&&(&&(&&(>(x5, 3), >(x4, -1)), <(+(x4, 1), x3)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(17) Obligation:

Rules:
f12230_0_binaryGrundy_GE(v10, x1, x2, x0) → f12230_0_binaryGrundy_GE(v11, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 4)), <(x1, x0)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f12230_0_binaryGrundy_GE(v12, x4, x5, x3) → f12230_0_binaryGrundy_GE(v13, +(x4, 1), 0, x3) | &&(&&(&&(&&(&&(>(x5, 3), >(x4, -1)), <(+(x4, 1), x3)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(18) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f12230_0_binaryGrundy_GE(x11, x13, x15, x17)] = -2 - x13 + 2·x17

Therefore the following rule(s) have been dropped:

f12230_0_binaryGrundy_GE(x5, x6, x7, x8) → f12230_0_binaryGrundy_GE(x9, +(x6, 1), 0, x8) | &&(&&(&&(&&(&&(>(x7, 3), >(x6, -1)), <(+(x6, 1), x8)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1))

(19) Obligation:

Rules:
f12230_0_binaryGrundy_GE(x0, x1, x2, x3) → f12230_0_binaryGrundy_GE(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 4)), <(x1, x3)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f12230_0_binaryGrundy_GE(x6, x8, x10, x12)] = 3 - x10

Therefore the following rule(s) have been dropped:

f12230_0_binaryGrundy_GE(x0, x1, x2, x3) → f12230_0_binaryGrundy_GE(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, 4)), <(x1, x3)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))

(21) YES

(22) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.decimalToBinaryAux(II[I)V
SCC calls the following helper methods: Nim.decimalToBinaryAux(II[I)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(23) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f2467_0_decimalToBinaryAux_LE(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), i370) → f2470_0_decimalToBinaryAux_LE(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), i370)
f2470_0_decimalToBinaryAux_LE(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), i370) → f2473_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291))) | >(i370, 0)
f2473_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291))) → f2476_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)))
f2476_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291))) → f2508_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360)
f2508_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360) → f2511_0_decimalToBinaryAux_ConstantStackPush(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360, i370)
f2511_0_decimalToBinaryAux_ConstantStackPush(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360, i370) → f2514_0_decimalToBinaryAux_IntArithmetic(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360, i370)
f2514_0_decimalToBinaryAux_IntArithmetic(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360, i370) → f2519_0_decimalToBinaryAux_ArrayAccess(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360)
f2519_0_decimalToBinaryAux_ArrayAccess(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360) → f2523_0_decimalToBinaryAux_ArrayAccess(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360)
f2523_0_decimalToBinaryAux_ArrayAccess(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i360) → f2534_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291))) | <(i360, i291)
f2534_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i370, i360, java.lang.Object(ARRAY(i291))) → f2577_0_decimalToBinaryAux_ConstantStackPush(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i360, java.lang.Object(ARRAY(i291)), i370)
f2577_0_decimalToBinaryAux_ConstantStackPush(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i360, java.lang.Object(ARRAY(i291)), i370) → f2583_0_decimalToBinaryAux_IntArithmetic(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i360, java.lang.Object(ARRAY(i291)), i370, 2)
f2583_0_decimalToBinaryAux_IntArithmetic(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i360, java.lang.Object(ARRAY(i291)), i370, matching1) → f2593_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i360, java.lang.Object(ARRAY(i291)), /(i370, 2)) | &&(>=(i370, 1), =(matching1, 2))
f2593_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i360, java.lang.Object(ARRAY(i291)), i399) → f2601_0_decimalToBinaryAux_ConstantStackPush(EOS, i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i399, i360)
f2601_0_decimalToBinaryAux_ConstantStackPush(EOS, i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i399, i360) → f2607_0_decimalToBinaryAux_IntArithmetic(EOS, i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i399, i360, 1)
f2607_0_decimalToBinaryAux_IntArithmetic(EOS, i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i399, i360, matching1) → f2615_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i399, +(i360, 1)) | &&(>=(i360, 0), =(matching1, 1))
f2615_0_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), java.lang.Object(ARRAY(i291)), i399, i402) → f2652_0_decimalToBinaryAux_InvokeMethod(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291)))
f2652_0_decimalToBinaryAux_InvokeMethod(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291))) → f2661_0_decimalToBinaryAux_Load(EOS, i399, i402, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291)))
f2652_0_decimalToBinaryAux_InvokeMethod(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291))) → f2661_1_decimalToBinaryAux_Load(EOS, i370, i360, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291)))
f2661_0_decimalToBinaryAux_Load(EOS, i399, i402, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291))) → f2673_0_decimalToBinaryAux_Load(EOS, i399, i402, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291)))
f2673_0_decimalToBinaryAux_Load(EOS, i399, i402, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291))) → f2457_0_decimalToBinaryAux_Load(EOS, i399, i402, java.lang.Object(ARRAY(i291)), i399, i402, java.lang.Object(ARRAY(i291)))
f2457_0_decimalToBinaryAux_Load(EOS, i359, i360, java.lang.Object(ARRAY(i291)), i359, i360, java.lang.Object(ARRAY(i291))) → f2467_0_decimalToBinaryAux_LE(EOS, i359, i360, java.lang.Object(ARRAY(i291)), i359, i360, java.lang.Object(ARRAY(i291)), i359)

Combined rules. Obtained 2 IRules

P rules:
f2467_0_decimalToBinaryAux_LE(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x0) → f2661_1_decimalToBinaryAux_Load(EOS, x0, x1, java.lang.Object(ARRAY(x2)), /(x0, 2), +(x1, 1), java.lang.Object(ARRAY(x2)), /(x0, 2), +(x1, 1), java.lang.Object(ARRAY(x2))) | &&(&&(>(x2, x1), >(+(x0, 1), 1)), >(+(x1, 1), 0))
f2467_0_decimalToBinaryAux_LE(EOS, x0, x1, java.lang.Object(ARRAY(x2)), x0, x1, java.lang.Object(ARRAY(x2)), x0) → f2467_0_decimalToBinaryAux_LE(EOS, /(x0, 2), +(x1, 1), java.lang.Object(ARRAY(x2)), /(x0, 2), +(x1, 1), java.lang.Object(ARRAY(x2)), /(x0, 2)) | &&(&&(>(x2, x1), >(+(x0, 1), 1)), >(+(x1, 1), 0))

Filtered ground terms:

f2467_0_decimalToBinaryAux_LE(x1, x2, x3, x4, x5, x6, x7, x8) → f2467_0_decimalToBinaryAux_LE(x2, x3, x4, x5, x6, x7, x8)
Cond_f2467_0_decimalToBinaryAux_LE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f2467_0_decimalToBinaryAux_LE(x1, x3, x4, x5, x6, x7, x8, x9)
f2661_1_decimalToBinaryAux_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → f2661_1_decimalToBinaryAux_Load(x2, x3, x4, x5, x6, x7, x8, x9, x10)
Cond_f2467_0_decimalToBinaryAux_LE1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f2467_0_decimalToBinaryAux_LE1(x1, x3, x4, x5, x6, x7, x8, x9)

Filtered duplicate terms:

f2467_0_decimalToBinaryAux_LE(x1, x2, x3, x4, x5, x6, x7) → f2467_0_decimalToBinaryAux_LE(x5, x6, x7)
Cond_f2467_0_decimalToBinaryAux_LE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2467_0_decimalToBinaryAux_LE(x1, x6, x7, x8)
f2661_1_decimalToBinaryAux_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → f2661_1_decimalToBinaryAux_Load(x7, x8, x9)
Cond_f2467_0_decimalToBinaryAux_LE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2467_0_decimalToBinaryAux_LE1(x1, x6, x7, x8)

Filtered unneeded terms:

Cond_f2467_0_decimalToBinaryAux_LE(x1, x2, x3, x4) → Cond_f2467_0_decimalToBinaryAux_LE(x1)

Prepared 2 rules for path length conversion:

P rules:
f2467_0_decimalToBinaryAux_LE(x1, java.lang.Object(ARRAY(x2)), x0, x2) → f2661_1_decimalToBinaryAux_Load(/(x0, 2), +(x1, 1), java.lang.Object(ARRAY(x2))) | &&(&&(>(x2, x1), >(+(x0, 1), 1)), >(+(x1, 1), 0))
f2467_0_decimalToBinaryAux_LE(x1, java.lang.Object(ARRAY(x2)), x0, x2) → f2467_0_decimalToBinaryAux_LE(+(x1, 1), java.lang.Object(ARRAY(x2)), /(x0, 2), x2) | &&(&&(>(x2, x1), >(+(x0, 1), 1)), >(+(x1, 1), 0))

Finished conversion. Obtained 2 rules.

P rules:
f2467_0_decimalToBinaryAux_LE(x3, v10, x5, x4) → f2467_0_decimalToBinaryAux_LE'(x3, v10, x5, x4) | &&(&&(&&(&&(&&(>(x5, 0), >(x4, x3)), >(x3, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f2467_0_decimalToBinaryAux_LE'(x3, v10, x5, x4) → f2467_0_decimalToBinaryAux_LE(+(x3, 1), v11, arith1, x4) | &&(&&(&&(&&(&&(&&(&&(>(x5, 0), >=(-(x5, *(2, arith1)), 0)), <(-(x5, *(2, arith1)), 2)), >(x4, x3)), >(x3, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(24) Obligation:

Rules:
f2467_0_decimalToBinaryAux_LE(x3, v10, x5, x4) → f2467_0_decimalToBinaryAux_LE'(x3, v10, x5, x4) | &&(&&(&&(&&(&&(>(x5, 0), >(x4, x3)), >(x3, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f2467_0_decimalToBinaryAux_LE'(x3, v10, x5, x4) → f2467_0_decimalToBinaryAux_LE(+(x3, 1), v11, arith1, x4) | &&(&&(&&(&&(&&(&&(&&(>(x5, 0), >=(-(x5, *(2, arith1)), 0)), <(-(x5, *(2, arith1)), 2)), >(x4, x3)), >(x3, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))

(25) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2467_0_decimalToBinaryAux_LE(x12, x14, x16, x18)] = 1 - 2·x12 + 2·x18
[f2467_0_decimalToBinaryAux_LE'(x21, x23, x25, x27)] = -2·x21 + 2·x27

Therefore the following rule(s) have been dropped:

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

(26) YES

(27) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.decomposition([I)[[I
SCC calls the following helper methods: Nim.decimalToBinaryAux(II[I)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(28) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 32 IRules

P rules:
f2579_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i385, i385) → f2581_0_decomposition_ArrayLength(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i385, i385, java.lang.Object(ARRAY(4))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f2581_0_decomposition_ArrayLength(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i385, i385, java.lang.Object(ARRAY(matching4))) → f2585_0_decomposition_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i385, i385, 4) | &&(&&(&&(&&(>=(4, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2585_0_decomposition_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, i397, matching4) → f2590_0_decomposition_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, i397, 4) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2590_0_decomposition_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, i397, matching4) → f2595_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397) | &&(&&(&&(&&(<(i397, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2595_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397) → f2603_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f2603_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4))) → f2609_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2609_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397) → f2617_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2617_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, java.lang.Object(ARRAY(matching5))) → f2654_0_decomposition_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f2654_0_decomposition_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, java.lang.Object(ARRAY(matching5)), i397) → f2658_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418) | &&(&&(&&(&&(&&(<(i397, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f2658_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418) → f2663_0_decomposition_InvokeMethod(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2663_0_decomposition_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384) → f2668_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, i418, i384) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2668_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, i418, i384) → f2679_0_decimalToBinary_ArrayCreate(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, i418, i384) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2679_0_decimalToBinary_ArrayCreate(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, i418, i384) → f2683_0_decimalToBinary_Store(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, i418, java.lang.Object(ARRAY(i384))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2683_0_decimalToBinary_Store(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, i418, java.lang.Object(ARRAY(i384))) → f2686_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, i418, java.lang.Object(ARRAY(i384))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2686_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, i418, java.lang.Object(ARRAY(i384))) → f2688_0_decimalToBinary_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2688_0_decimalToBinary_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418) → f2691_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418, 0) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2691_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418, matching5) → f2694_0_decimalToBinary_InvokeMethod(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418, 0, java.lang.Object(ARRAY(i384))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0))
f2694_0_decimalToBinary_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418, matching5, java.lang.Object(ARRAY(i384))) → f2697_0_decimalToBinaryAux_Load(EOS, i418, 0, java.lang.Object(ARRAY(i384)), i418, 0, java.lang.Object(ARRAY(i384))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0))
f2694_0_decimalToBinary_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418, matching5, java.lang.Object(ARRAY(i384))) → f2697_1_decimalToBinaryAux_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i418, i384, java.lang.Object(ARRAY(i384)), i418, 0, java.lang.Object(ARRAY(i384)), i418, 0, java.lang.Object(ARRAY(i384))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0))
f2697_0_decimalToBinaryAux_Load(EOS, i418, matching1, java.lang.Object(ARRAY(i384)), i418, matching2, java.lang.Object(ARRAY(i384))) → f2700_0_decimalToBinaryAux_Load(EOS, i418, 0, java.lang.Object(ARRAY(i384)), i418, 0, java.lang.Object(ARRAY(i384))) | &&(=(matching1, 0), =(matching2, 0))
f2761_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i446, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i448, i446, java.lang.Object(ARRAY(i446)), i448, matching5, java.lang.Object(ARRAY(i446))) → f2776_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i446, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i448, i446, java.lang.Object(ARRAY(i446)), i448, 0, java.lang.Object(ARRAY(i446))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0))
f2776_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i475, i476, java.lang.Object(ARRAY(i474)), i475, matching5, java.lang.Object(ARRAY(i474))) → f2782_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i475, i476, java.lang.Object(ARRAY(i474))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0))
f2782_0_decimalToBinary_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i475, i476, java.lang.Object(ARRAY(i474))) → f2784_0_decimalToBinary_Return(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i475, i476, java.lang.Object(ARRAY(i474))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2784_0_decimalToBinary_Return(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i475, i476, java.lang.Object(ARRAY(i474))) → f2787_0_decomposition_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(i474))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2787_0_decomposition_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, java.lang.Object(ARRAY(i474))) → f2797_0_decomposition_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), i397) | &&(&&(&&(&&(<(i397, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f2797_0_decomposition_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i397) → f2800_0_decomposition_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), +(i397, 1)) | &&(&&(&&(>=(i397, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f2800_0_decomposition_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i489) → f2804_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), i489) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f2804_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i476, java.lang.Object(ARRAY(matching3)), i489) → f2573_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i476, java.lang.Object(ARRAY(4)), i489) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f2573_0_decomposition_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i385) → f2579_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i385, i385) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f2827_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i510, i384, java.lang.Object(ARRAY(i505)), i510, matching5, java.lang.Object(ARRAY(i505))) → f2776_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i510, i384, java.lang.Object(ARRAY(i505)), i510, 0, java.lang.Object(ARRAY(i505))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0))
f2697_1_decimalToBinaryAux_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i446, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i448, i446, java.lang.Object(ARRAY(i446)), i448, matching5, java.lang.Object(ARRAY(i446)), i448, matching6, java.lang.Object(ARRAY(i446))) → f2761_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i446, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i448, i446, java.lang.Object(ARRAY(i446)), i448, 0, java.lang.Object(ARRAY(i446))) | &&(&&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0)), =(matching6, 0))
f2697_1_decimalToBinaryAux_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), i384, java.lang.Object(ARRAY(matching3)), i397, java.lang.Object(ARRAY(matching4)), i397, i510, i384, java.lang.Object(ARRAY(i384)), i510, matching5, java.lang.Object(ARRAY(i384)), i510, matching6, java.lang.Object(ARRAY(i384))) → f2827_0_decimalToBinaryAux_Return(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i384, java.lang.Object(ARRAY(4)), i397, java.lang.Object(ARRAY(4)), i397, i510, i384, java.lang.Object(ARRAY(i505)), i510, 0, java.lang.Object(ARRAY(i505))) | &&(&&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 0)), =(matching6, 0))

Combined rules. Obtained 2 IRules

P rules:
f2579_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(4)), x4, x4) → f2700_0_decimalToBinaryAux_Load(EOS, x5, 0, java.lang.Object(ARRAY(x2)), x5, 0, java.lang.Object(ARRAY(x2))) | <(x4, 4)
f2579_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(4)), x4, x4) → f2579_0_decomposition_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x2, java.lang.Object(ARRAY(4)), +(x4, 1), +(x4, 1)) | &&(>(+(x4, 1), 0), <(x4, 4))

Filtered ground terms:

f2579_0_decomposition_Load(x1, x2, x3, x4, x5, x6, x7) → f2579_0_decomposition_Load(x4, x6, x7)
Cond_f2579_0_decomposition_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f2579_0_decomposition_Load(x1, x5, x7, x8, x9)
f2700_0_decimalToBinaryAux_Load(x1, x2, x3, x4, x5, x6, x7) → f2700_0_decimalToBinaryAux_Load(x2, x4, x5, x7)
Cond_f2579_0_decomposition_Load1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2579_0_decomposition_Load1(x1, x5, x7, x8)

Filtered duplicate terms:

f2579_0_decomposition_Load(x1, x2, x3) → f2579_0_decomposition_Load(x1, x3)
Cond_f2579_0_decomposition_Load(x1, x2, x3, x4, x5) → Cond_f2579_0_decomposition_Load(x1, x2, x4, x5)
f2700_0_decimalToBinaryAux_Load(x1, x2, x3, x4) → f2700_0_decimalToBinaryAux_Load(x3, x4)
Cond_f2579_0_decomposition_Load1(x1, x2, x3, x4) → Cond_f2579_0_decomposition_Load1(x1, x2, x4)

Filtered unneeded terms:

Cond_f2579_0_decomposition_Load(x1, x2, x3, x4) → Cond_f2579_0_decomposition_Load(x1)
Cond_f2579_0_decomposition_Load1(x1, x2, x3) → Cond_f2579_0_decomposition_Load1(x1, x3)
f2579_0_decomposition_Load(x1, x2) → f2579_0_decomposition_Load(x2)

Prepared 2 rules for path length conversion:

P rules:
f2579_0_decomposition_Load(x4) → f2700_0_decimalToBinaryAux_Load(x5, java.lang.Object(ARRAY(x2))) | <(x4, 4)
f2579_0_decomposition_Load(x4) → f2579_0_decomposition_Load(+(x4, 1)) | &&(>(+(x4, 1), 0), <(x4, 4))

Finished conversion. Obtained 1 rules.

P rules:
f2579_0_decomposition_Load(x3) → f2579_0_decomposition_Load(+(x3, 1)) | &&(<(x3, 4), >(x3, -1))

(29) Obligation:

Rules:
f2579_0_decomposition_Load(x3) → f2579_0_decomposition_Load(+(x3, 1)) | &&(<(x3, 4), >(x3, -1))

(30) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2579_0_decomposition_Load(x2)] = 3 - x2

Therefore the following rule(s) have been dropped:

f2579_0_decomposition_Load(x0) → f2579_0_decomposition_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(31) YES

(32) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.decomposition([I)[[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(33) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 11 IRules

P rules:
f1987_0_getBinaryLength_Load(EOS, i218, i245, i245) → f1989_0_getBinaryLength_GT(EOS, i218, i245, i245, i218)
f1989_0_getBinaryLength_GT(EOS, i218, i245, i245, i218) → f1992_0_getBinaryLength_GT(EOS, i218, i245, i245, i218)
f1992_0_getBinaryLength_GT(EOS, i218, i245, i245, i218) → f1995_0_getBinaryLength_Inc(EOS, i218, i245) | <=(i245, i218)
f1995_0_getBinaryLength_Inc(EOS, i218, i245) → f1998_0_getBinaryLength_Load(EOS, i218, i245)
f1998_0_getBinaryLength_Load(EOS, i218, i245) → f2001_0_getBinaryLength_ConstantStackPush(EOS, i218, i245)
f2001_0_getBinaryLength_ConstantStackPush(EOS, i218, i245) → f2003_0_getBinaryLength_IntArithmetic(EOS, i218, i245, 2)
f2003_0_getBinaryLength_IntArithmetic(EOS, i218, i245, matching1) → f2005_0_getBinaryLength_Store(EOS, i218, *(i245, 2)) | &&(>=(i245, 1), =(matching1, 2))
f2005_0_getBinaryLength_Store(EOS, i218, i249) → f2007_0_getBinaryLength_JMP(EOS, i218, i249)
f2007_0_getBinaryLength_JMP(EOS, i218, i249) → f2009_0_getBinaryLength_Load(EOS, i218, i249)
f2009_0_getBinaryLength_Load(EOS, i218, i249) → f1984_0_getBinaryLength_Load(EOS, i218, i249)
f1984_0_getBinaryLength_Load(EOS, i218, i245) → f1987_0_getBinaryLength_Load(EOS, i218, i245, i245)

Combined rules. Obtained 1 IRules

P rules:
f1987_0_getBinaryLength_Load(EOS, x0, x1, x1) → f1987_0_getBinaryLength_Load(EOS, x0, *(x1, 2), *(x1, 2)) | &&(<=(x1, x0), >(+(x1, 1), 1))

Filtered ground terms:

f1987_0_getBinaryLength_Load(x1, x2, x3, x4) → f1987_0_getBinaryLength_Load(x2, x3, x4)
Cond_f1987_0_getBinaryLength_Load(x1, x2, x3, x4, x5) → Cond_f1987_0_getBinaryLength_Load(x1, x3, x4, x5)

Filtered duplicate terms:

f1987_0_getBinaryLength_Load(x1, x2, x3) → f1987_0_getBinaryLength_Load(x1, x3)
Cond_f1987_0_getBinaryLength_Load(x1, x2, x3, x4) → Cond_f1987_0_getBinaryLength_Load(x1, x2, x4)

Prepared 1 rules for path length conversion:

P rules:
f1987_0_getBinaryLength_Load(x0, x1) → f1987_0_getBinaryLength_Load(x0, *(x1, 2)) | &&(<=(x1, x0), >(+(x1, 1), 1))

Finished conversion. Obtained 1 rules.

P rules:
f1987_0_getBinaryLength_Load(x0, x1) → f1987_0_getBinaryLength_Load(x0, *(2, x1)) | &&(<=(x1, x0), >(x1, 0))

(34) Obligation:

Rules:
f1987_0_getBinaryLength_Load(x0, x1) → f1987_0_getBinaryLength_Load(x0, *(2, x1)) | &&(<=(x1, x0), >(x1, 0))

(35) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f1987_0_getBinaryLength_Load(x)] = 1·x₁ + (-1)·x₂

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f1987_0_getBinaryLength_Load(x0, x1) → f1987_0_getBinaryLength_Load(x0, *(2, x1)) | &&(<=(x1, x0), >(x1, 0))

(36) YES

(37) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.decomposition([I)[[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(38) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 21 IRules

P rules:
f1679_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i192, i192) → f1681_0_getBinaryLength_ArrayLength(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i192, i192, java.lang.Object(ARRAY(4))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1681_0_getBinaryLength_ArrayLength(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i192, i192, java.lang.Object(ARRAY(matching5))) → f1683_0_getBinaryLength_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i192, i192, 4) | &&(&&(&&(&&(&&(>=(4, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1683_0_getBinaryLength_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i198, matching5) → f1686_0_getBinaryLength_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, i198, 4) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1686_0_getBinaryLength_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i198, matching5) → f1689_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198) | &&(&&(&&(&&(&&(<(i198, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1689_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198) → f1692_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, java.lang.Object(ARRAY(4))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1692_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, java.lang.Object(ARRAY(matching5))) → f1695_0_getBinaryLength_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, java.lang.Object(ARRAY(4)), i198) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1695_0_getBinaryLength_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, java.lang.Object(ARRAY(matching5)), i198) → f1699_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, i200) | &&(&&(&&(&&(&&(<(i198, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1699_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i200) → f1703_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, i200, i191) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1703_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i200, i191) → f1707_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, i200, i191) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1703_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i200, i191) → f1708_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198, i200, i191) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1707_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i200, i191) → f1712_0_getBinaryLength_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198) | &&(&&(&&(&&(<=(i200, i191), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1712_0_getBinaryLength_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198) → f1779_0_getBinaryLength_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i198) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1779_0_getBinaryLength_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i207, i198) → f1785_0_getBinaryLength_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i207, +(i198, 1)) | &&(&&(&&(&&(>(i198, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1785_0_getBinaryLength_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i207, i209) → f1812_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i207, i209) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1812_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i207, i209) → f1675_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i207, i209) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1675_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i192) → f1679_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i191, i192, i192) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1708_0_getBinaryLength_LE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i191, i198, i200, i191) → f1713_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i198) | &&(&&(&&(&&(>(i200, i191), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1713_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i198) → f1719_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i198, java.lang.Object(ARRAY(4))) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f1719_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i198, java.lang.Object(ARRAY(matching5))) → f1748_0_getBinaryLength_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i198, java.lang.Object(ARRAY(4)), i198) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1748_0_getBinaryLength_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i198, java.lang.Object(ARRAY(matching5)), i198) → f1753_0_getBinaryLength_Store(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i198, i207) | &&(&&(&&(&&(&&(<(i198, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 4))
f1753_0_getBinaryLength_Store(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i198, i207) → f1779_0_getBinaryLength_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i207, i198) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))

Combined rules. Obtained 2 IRules

P rules:
f1679_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x4, x5, x5) → f1679_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x4, +(x5, 1), +(x5, 1)) | &&(>(x5, 0), <(x5, 4))
f1679_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x4, x5, x5) → f1679_0_getBinaryLength_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x6, +(x5, 1), +(x5, 1)) | &&(>(x5, 0), <(x5, 4))

Filtered ground terms:

f1679_0_getBinaryLength_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f1679_0_getBinaryLength_Load(x6, x7, x8)
Cond_f1679_0_getBinaryLength_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f1679_0_getBinaryLength_Load(x1, x7, x8, x9)
Cond_f1679_0_getBinaryLength_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_f1679_0_getBinaryLength_Load1(x1, x7, x8, x9, x10)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY

Filtered duplicate terms:

f1679_0_getBinaryLength_Load(x1, x2, x3) → f1679_0_getBinaryLength_Load(x1, x3)
Cond_f1679_0_getBinaryLength_Load(x1, x2, x3, x4) → Cond_f1679_0_getBinaryLength_Load(x1, x2, x4)
Cond_f1679_0_getBinaryLength_Load1(x1, x2, x3, x4, x5) → Cond_f1679_0_getBinaryLength_Load1(x1, x2, x4, x5)

Filtered unneeded terms:

Cond_f1679_0_getBinaryLength_Load(x1, x2, x3) → Cond_f1679_0_getBinaryLength_Load(x1, x3)
Cond_f1679_0_getBinaryLength_Load1(x1, x2, x3, x4) → Cond_f1679_0_getBinaryLength_Load1(x1, x3)
f1679_0_getBinaryLength_Load(x1, x2) → f1679_0_getBinaryLength_Load(x2)

Prepared 1 rules for path length conversion:

P rules:
f1679_0_getBinaryLength_Load(x5) → f1679_0_getBinaryLength_Load(+(x5, 1)) | &&(>(x5, 0), <(x5, 4))

Finished conversion. Obtained 1 rules.

P rules:
f1679_0_getBinaryLength_Load(x0) → f1679_0_getBinaryLength_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, 0))

(39) Obligation:

Rules:
f1679_0_getBinaryLength_Load(x0) → f1679_0_getBinaryLength_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, 0))

(40) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f1679_0_getBinaryLength_Load(x2)] = 3 - x2

Therefore the following rule(s) have been dropped:

f1679_0_getBinaryLength_Load(x0) → f1679_0_getBinaryLength_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, 0))

(41) YES

(42) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.pick([I)[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(43) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 39 IRules

P rules:
f8903_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432) → f8904_0_pick_ArrayLength(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432, java.lang.Object(ARRAY(i2034))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8904_0_pick_ArrayLength(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432, java.lang.Object(ARRAY(i2034))) → f8907_0_pick_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432, i2034) | &&(&&(&&(>=(i2034, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f8907_0_pick_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432, i2034) → f8913_0_pick_GE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432, i2034) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8913_0_pick_GE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432, i2034) → f8920_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(&&(<(i2432, i2034), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f8920_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432) → f8927_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2034))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8927_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2034))) → f8935_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2034)), i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8935_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2034)), i2432) → f8938_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2034)), i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8938_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2034)), i2432) → f8943_0_pick_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2437) | &&(&&(&&(<(i2432, i2034), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f8943_0_pick_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2437) → f8953_0_pick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2437, 1) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8953_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2442, matching4) → f8966_0_pick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2442, 1) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 1))
f8953_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, matching4, matching5) → f8967_0_pick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, 1, 1) | &&(&&(&&(&&(&&(=(i2437, 1), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 1)), =(matching5, 1))
f8953_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2443, matching4) → f8968_0_pick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2443, 1) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 1))
f8966_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2442, matching4) → f8982_0_pick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(&&(&&(<(i2442, 1), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 1))
f8982_0_pick_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432) → f8995_0_pick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8995_0_pick_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432) → f9329_0_pick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9329_0_pick_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432) → f9404_0_pick_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, +(i2432, 1)) | &&(&&(&&(>=(i2432, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f9404_0_pick_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2523) → f9455_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2523) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9455_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2523) → f8895_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2523) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8895_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432) → f8903_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f8967_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, matching4, matching5) → f8985_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 1)), =(matching5, 1))
f8985_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432) → f9008_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(4))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9008_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(matching4))) → f9024_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(4)), i1837) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f9024_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(matching4)), i1837) → f9052_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681) | &&(&&(&&(&&(<(i1837, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f9052_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681) → f9061_0_pick_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9061_0_pick_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) → f9075_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9075_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) → f9108_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(4))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9108_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(matching4))) → f9118_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(4)), i1837) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f9118_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(matching4)), i1837) → f9131_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, o1697) | &&(&&(&&(&&(<(i1837, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f9131_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, o1697) → f9150_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, o1697, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9150_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(o1711put), i2432) → f9160_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(o1711put), i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9160_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(i2479)), i2432) → f9167_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(i2479)), i2432) | &&(&&(&&(>=(i2479, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f9167_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(i2479)), i2432) → f9182_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(i2479)), i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9182_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432, java.lang.Object(ARRAY(i2479)), i2432) → f9196_0_pick_IntArithmetic(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) | &&(&&(&&(<(i2432, i2479), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f9196_0_pick_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) → f9205_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, o1681, i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9205_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(o1770put), i2432) → f9232_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(o1770put), i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9232_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2500)), i2432) → f9269_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2500)), i2432) | &&(&&(&&(>=(i2500, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f9269_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2500)), i2432) → f9284_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2500)), i2432) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f9284_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, java.lang.Object(ARRAY(i2500)), i2432) → f9329_0_pick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(&&(<(i2432, i2500), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f8968_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(i2034)), i1837, i2432, i2443, matching4) → f8995_0_pick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(i2034)), i1837, i2432) | &&(&&(&&(&&(>(i2443, 1), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 1))

Combined rules. Obtained 2 IRules

P rules:
f8903_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(x3)), x4, x5, x5) → f8903_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(x3)), x4, +(x5, 1), +(x5, 1)) | &&(&&(>(+(x5, 1), 0), <(x5, x3)), >(+(x3, 1), 0))
f8903_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(x3)), x4, x5, x5) → f8903_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(x3)), x4, +(x5, 1), +(x5, 1)) | &&(&&(&&(>(+(x5, 1), 0), <(x5, x3)), <(x4, 4)), >(+(x3, 1), 0))

Filtered ground terms:

f8903_0_pick_Load(x1, x2, x3, x4, x5, x6, x7, x8) → f8903_0_pick_Load(x5, x6, x7, x8)
Cond_f8903_0_pick_Load(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f8903_0_pick_Load(x1, x6, x7, x8, x9)
Cond_f8903_0_pick_Load1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f8903_0_pick_Load1(x1, x6, x7, x8, x9)

Filtered duplicate terms:

f8903_0_pick_Load(x1, x2, x3, x4) → f8903_0_pick_Load(x1, x2, x4)
Cond_f8903_0_pick_Load(x1, x2, x3, x4, x5) → Cond_f8903_0_pick_Load(x1, x2, x3, x5)
Cond_f8903_0_pick_Load1(x1, x2, x3, x4, x5) → Cond_f8903_0_pick_Load1(x1, x2, x3, x5)

Prepared 2 rules for path length conversion:

P rules:
f8903_0_pick_Load(java.lang.Object(ARRAY(x3)), x4, x5, x3) → f8903_0_pick_Load(java.lang.Object(ARRAY(x3)), x4, +(x5, 1), x3) | &&(&&(>(+(x5, 1), 0), <(x5, x3)), >(+(x3, 1), 0))
f8903_0_pick_Load(java.lang.Object(ARRAY(x3)), x4, x5, x3) → f8903_0_pick_Load(java.lang.Object(ARRAY(x3)), x4, +(x5, 1), x3) | &&(&&(&&(>(+(x5, 1), 0), <(x5, x3)), <(x4, 4)), >(+(x3, 1), 0))

Finished conversion. Obtained 2 rules.

P rules:
f8903_0_pick_Load(v10, x1, x2, x0) → f8903_0_pick_Load(v11, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, x0)), >(x0, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f8903_0_pick_Load(v12, x4, x5, x3) → f8903_0_pick_Load(v13, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(&&(>(x5, -1), <(x5, x3)), <(x4, 4)), >(x3, -1)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(44) Obligation:

Rules:
f8903_0_pick_Load(v10, x1, x2, x0) → f8903_0_pick_Load(v11, x1, +(x2, 1), x0) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, x0)), >(x0, -1)), >(+(v11, 1), 1)), <=(v11, v10)), >(+(v10, 1), 1))
f8903_0_pick_Load(v12, x4, x5, x3) → f8903_0_pick_Load(v13, x4, +(x5, 1), x3) | &&(&&(&&(&&(&&(&&(>(x5, -1), <(x5, x3)), <(x4, 4)), >(x3, -1)), >(+(v13, 1), 1)), <=(v13, v12)), >(+(v12, 1), 1))

(45) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f8903_0_pick_Load(x11, x13, x15, x17)] = -x15 + x17

Therefore the following rule(s) have been dropped:

f8903_0_pick_Load(x0, x1, x2, x3) → f8903_0_pick_Load(x4, x1, +(x2, 1), x3) | &&(&&(&&(&&(&&(>(x2, -1), <(x2, x3)), >(x3, -1)), >(+(x4, 1), 1)), <=(x4, x0)), >(+(x0, 1), 1))
f8903_0_pick_Load(x5, x6, x7, x8) → f8903_0_pick_Load(x9, x6, +(x7, 1), x8) | &&(&&(&&(&&(&&(&&(>(x7, -1), <(x7, x8)), <(x6, 4)), >(x8, -1)), >(+(x9, 1), 1)), <=(x9, x5)), >(+(x5, 1), 1))

(46) YES

(47) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.pick([I)[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(48) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 14 IRules

P rules:
f7075_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1827, java.lang.Object(ARRAY(matching4))) → f7081_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1827, java.lang.Object(ARRAY(4)), i1827) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f7081_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, java.lang.Object(ARRAY(matching4)), i1837) → f7086_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, java.lang.Object(ARRAY(4)), i1837) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f7086_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, java.lang.Object(ARRAY(matching4)), i1837) → f7099_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, o1099) | &&(&&(&&(&&(<(i1837, 4), =(matching1, 4)), =(matching2, 4)), =(matching3, 4)), =(matching4, 4))
f7099_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, o1099) → f7110_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, o1099, i1251) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f7110_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, java.lang.Object(o1106put), i1251) → f7118_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, java.lang.Object(o1106put), i1251) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f7118_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, java.lang.Object(ARRAY(i1872)), i1251) → f7140_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, java.lang.Object(ARRAY(i1872)), i1251) | &&(&&(&&(>=(i1872, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f7140_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, java.lang.Object(ARRAY(i1872)), i1251) → f7164_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, java.lang.Object(ARRAY(i1872)), i1251) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f7164_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, java.lang.Object(ARRAY(i1872)), i1251) → f7199_0_pick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, i1922) | &&(&&(&&(<(i1251, i1872), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f7199_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, matching4) → f7235_0_pick_NE(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837, 0) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 0))
f7235_0_pick_NE(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837, matching4) → f7261_0_pick_Inc(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1837) | &&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 0))
f7261_0_pick_Inc(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1837) → f7277_0_pick_JMP(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, +(i1837, 1)) | &&(&&(&&(>=(i1837, 0), =(matching1, 4)), =(matching2, 4)), =(matching3, 4))
f7277_0_pick_JMP(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1934) → f7324_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1934) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f7324_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1934) → f7053_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1934) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f7053_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i1251, i1827) → f7075_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i1251, i1827, java.lang.Object(ARRAY(4))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))

Combined rules. Obtained 1 IRules

P rules:
f7075_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x3, x4, java.lang.Object(ARRAY(4))) → f7075_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), x3, +(x4, 1), java.lang.Object(ARRAY(4))) | &&(<(x4, 4), >(+(x4, 1), 0))

Filtered ground terms:

f7075_0_pick_Load(x1, x2, x3, x4, x5, x6, x7) → f7075_0_pick_Load(x5, x6)
Cond_f7075_0_pick_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f7075_0_pick_Load(x1, x6, x7)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY

Filtered unneeded terms:

Cond_f7075_0_pick_Load(x1, x2, x3) → Cond_f7075_0_pick_Load(x1, x3)
f7075_0_pick_Load(x1, x2) → f7075_0_pick_Load(x2)

Prepared 1 rules for path length conversion:

P rules:
f7075_0_pick_Load(x4) → f7075_0_pick_Load(+(x4, 1)) | &&(<(x4, 4), >(+(x4, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f7075_0_pick_Load(x0) → f7075_0_pick_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(49) Obligation:

Rules:
f7075_0_pick_Load(x0) → f7075_0_pick_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(50) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f7075_0_pick_Load(x)] = (-1)·x₁

where x = (x₁, ... ,x_n).

Therefore the following rule(s) have been dropped:

f7075_0_pick_Load(x0) → f7075_0_pick_Load(+(x0, 1)) | &&(<(x0, 4), >(x0, -1))

(51) YES

(52) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.pick([I)[I
SCC calls the following helper methods:
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(53) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 10 IRules

P rules:
f4953_0_pick_Load(EOS, java.lang.Object(ARRAY(i1189)), i1207, java.lang.Object(ARRAY(i1189))) → f4980_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(i1189)), i1207, java.lang.Object(ARRAY(i1189)), i1207)
f4980_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(i1189)), i1251, java.lang.Object(ARRAY(i1189)), i1251) → f4998_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(i1189)), i1251, java.lang.Object(ARRAY(i1189)), i1251)
f4998_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(i1189)), i1251, java.lang.Object(ARRAY(i1189)), i1251) → f5031_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(i1189)), i1251, java.lang.Object(ARRAY(i1189)), i1251)
f5031_0_pick_ArrayAccess(EOS, java.lang.Object(ARRAY(i1189)), i1251, java.lang.Object(ARRAY(i1189)), i1251) → f5045_0_pick_NE(EOS, java.lang.Object(ARRAY(i1189)), i1251, i1262) | <(i1251, i1189)
f5045_0_pick_NE(EOS, java.lang.Object(ARRAY(i1189)), i1251, matching1) → f5059_0_pick_NE(EOS, java.lang.Object(ARRAY(i1189)), i1251, 0) | =(matching1, 0)
f5059_0_pick_NE(EOS, java.lang.Object(ARRAY(i1189)), i1251, matching1) → f5094_0_pick_Inc(EOS, java.lang.Object(ARRAY(i1189)), i1251) | =(matching1, 0)
f5094_0_pick_Inc(EOS, java.lang.Object(ARRAY(i1189)), i1251) → f5142_0_pick_JMP(EOS, java.lang.Object(ARRAY(i1189)), +(i1251, -1)) | >=(i1251, 0)
f5142_0_pick_JMP(EOS, java.lang.Object(ARRAY(i1189)), i1278) → f5208_0_pick_Load(EOS, java.lang.Object(ARRAY(i1189)), i1278)
f5208_0_pick_Load(EOS, java.lang.Object(ARRAY(i1189)), i1278) → f4948_0_pick_Load(EOS, java.lang.Object(ARRAY(i1189)), i1278)
f4948_0_pick_Load(EOS, java.lang.Object(ARRAY(i1189)), i1207) → f4953_0_pick_Load(EOS, java.lang.Object(ARRAY(i1189)), i1207, java.lang.Object(ARRAY(i1189)))

Combined rules. Obtained 1 IRules

P rules:
f4953_0_pick_Load(EOS, java.lang.Object(ARRAY(x0)), x1, java.lang.Object(ARRAY(x0))) → f4953_0_pick_Load(EOS, java.lang.Object(ARRAY(x0)), -(x1, 1), java.lang.Object(ARRAY(x0))) | &&(<(x1, x0), >(+(x1, 1), 0))

Filtered ground terms:

f4953_0_pick_Load(x1, x2, x3, x4) → f4953_0_pick_Load(x2, x3, x4)
Cond_f4953_0_pick_Load(x1, x2, x3, x4, x5) → Cond_f4953_0_pick_Load(x1, x3, x4, x5)

Filtered duplicate terms:

f4953_0_pick_Load(x1, x2, x3) → f4953_0_pick_Load(x2, x3)
Cond_f4953_0_pick_Load(x1, x2, x3, x4) → Cond_f4953_0_pick_Load(x1, x3, x4)

Prepared 1 rules for path length conversion:

P rules:
f4953_0_pick_Load(x1, java.lang.Object(ARRAY(x0)), x0) → f4953_0_pick_Load(-(x1, 1), java.lang.Object(ARRAY(x0)), x0) | &&(<(x1, x0), >(+(x1, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f4953_0_pick_Load(x0, v5, x1) → f4953_0_pick_Load(-(x0, 1), v6, x1) | &&(&&(&&(&&(>(x1, x0), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(54) Obligation:

Rules:
f4953_0_pick_Load(x0, v5, x1) → f4953_0_pick_Load(-(x0, 1), v6, x1) | &&(&&(&&(&&(>(x1, x0), >(x0, -1)), >(+(v6, 1), 1)), <=(v6, v5)), >(+(v5, 1), 1))

(55) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f4953_0_pick_Load(x5, x7, x9)] = x5

Therefore the following rule(s) have been dropped:

f4953_0_pick_Load(x0, x1, x2) → f4953_0_pick_Load(-(x0, 1), x3, x2) | &&(&&(&&(&&(>(x2, x0), >(x0, -1)), >(+(x3, 1), 1)), <=(x3, x1)), >(+(x1, 1), 1))

(56) YES

(57) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: Nim.main([Ljava/lang/String;)V
SCC calls the following helper methods: Nim.pick([I)[I, Nim.decomposition([I)[[I, Nim.binaryGrundy([[I)[I, Nim.binaryToDecimal([I)I, Nim.loserPick([I)[I, Nim.decimalToBinaryAux(II[I)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
Marker field analysis yielded the following relations that could be markers:

(58) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 56 IRules

P rules:
f7318_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i1937, i1937) → f7322_0_main_GE(EOS, java.lang.Object(ARRAY(4)), i1937, i1937, 20) | =(matching1, 4)
f7322_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i1946, i1946, matching2) → f7325_0_main_GE(EOS, java.lang.Object(ARRAY(4)), i1946, i1946, 20) | &&(=(matching1, 4), =(matching2, 20))
f7325_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i1946, i1946, matching2) → f7328_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), i1946) | &&(&&(<(i1946, 20), =(matching1, 4)), =(matching2, 20))
f7328_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i1946) → f7335_0_main_Store(EOS, java.lang.Object(ARRAY(4)), i1946, 0) | =(matching1, 4)
f7335_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i1946, matching2) → f7352_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), i1946, 0) | &&(=(matching1, 4), =(matching2, 0))
f7352_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i1946, matching2) → f7356_0_main_Store(EOS, java.lang.Object(ARRAY(4)), i1946, 0, 0) | &&(=(matching1, 4), =(matching2, 0))
f7356_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i1946, matching2, matching3) → f7358_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, 0, 0) | &&(&&(=(matching1, 4), =(matching2, 0)), =(matching3, 0))
f7358_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, matching2, matching3) → f7417_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, 0, 0) | &&(&&(=(matching1, 4), =(matching2, 0)), =(matching3, 0))
f7417_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i1960, i1961) → f7504_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i1960, i1961) | =(matching1, 4)
f7504_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i1974, i1975) → f7605_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i1974, i1975) | =(matching1, 4)
f7605_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i1998, i1999) → f7722_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i1998, i1999) | =(matching1, 4)
f7722_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2017) → f7732_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2016, i2017, i2017) | =(matching1, 4)
f7732_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2017, i2017) → f7739_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(4)), i1946, i2016, i2017, i2017, java.lang.Object(ARRAY(4))) | =(matching1, 4)
f7739_0_main_ArrayLength(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2017, i2017, java.lang.Object(ARRAY(matching2))) → f7744_0_main_GE(EOS, java.lang.Object(ARRAY(4)), i1946, i2016, i2017, i2017, 4) | &&(&&(>=(4, 0), =(matching1, 4)), =(matching2, 4))
f7744_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2024, i2024, matching2) → f7751_0_main_GE(EOS, java.lang.Object(ARRAY(4)), i1946, i2016, i2024, i2024, 4) | &&(=(matching1, 4), =(matching2, 4))
f7744_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2025, i2025, matching2) → f7752_0_main_GE(EOS, java.lang.Object(ARRAY(4)), i1946, i2016, i2025, i2025, 4) | &&(=(matching1, 4), =(matching2, 4))
f7751_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2024, i2024, matching2) → f7755_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2016, i2024) | &&(&&(<(i2024, 4), =(matching1, 4)), =(matching2, 4))
f7755_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2024) → f7780_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2024, i2016) | =(matching1, 4)
f7780_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2024, i2016) → f7791_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2024, i2016, java.lang.Object(ARRAY(4))) | =(matching1, 4)
f7791_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2024, i2016, java.lang.Object(ARRAY(matching2))) → f7823_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), i1946, i2024, i2016, java.lang.Object(ARRAY(4)), i2024) | &&(=(matching1, 4), =(matching2, 4))
f7823_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2024, i2016, java.lang.Object(ARRAY(matching2)), i2024) → f7853_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(4)), i1946, i2024, i2016, i2044) | &&(&&(<(i2024, 4), =(matching1, 4)), =(matching2, 4))
f7853_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2024, i2016, i2044) → f7866_0_main_Store(EOS, java.lang.Object(ARRAY(4)), i1946, i2024, +(i2016, i2044)) | =(matching1, 4)
f7866_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2024, i2045) → f7901_0_main_Inc(EOS, java.lang.Object(ARRAY(4)), i1946, i2045, i2024) | =(matching1, 4)
f7901_0_main_Inc(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2045, i2024) → f7920_0_main_JMP(EOS, java.lang.Object(ARRAY(4)), i1946, i2045, +(i2024, 1)) | &&(>=(i2024, 0), =(matching1, 4))
f7920_0_main_JMP(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2045, i2055) → f7943_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2045, i2055) | =(matching1, 4)
f7943_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2045, i2055) → f7722_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2045, i2055) | =(matching1, 4)
f7752_0_main_GE(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016, i2025, i2025, matching2) → f7770_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, i2016) | &&(&&(>=(i2025, 4), =(matching1, 4)), =(matching2, 4))
f7770_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2016) → f7786_0_main_GT(EOS, java.lang.Object(ARRAY(4)), i1946, i2016) | =(matching1, 4)
f7786_0_main_GT(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2033) → f7797_0_main_GT(EOS, java.lang.Object(ARRAY(4)), i1946, i2033) | =(matching1, 4)
f7797_0_main_GT(EOS, java.lang.Object(ARRAY(matching1)), i1946, i2033) → f7843_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946) | &&(>(i2033, 0), =(matching1, 4))
f7843_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946) → f7860_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4))) | =(matching1, 4)
f7860_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2))) → f7889_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 4))
f7860_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2))) → f7889_1_pick_Load(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 4))
f7889_0_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), java.lang.Object(ARRAY(matching2))) → f7906_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 4))
f8232_0_pick_Return(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), i2091, java.lang.Object(ARRAY(i2097)), java.lang.Object(ARRAY(matching5))) → f8315_0_main_Store(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2))) | &&(&&(&&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4)), =(matching4, 4)), =(matching5, 2))
f8315_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2))) → f9752_0_main_Store(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2))) | &&(=(matching1, 4), =(matching2, 2))
f9752_0_main_Store(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2))) → f9765_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2))) | &&(=(matching1, 4), =(matching2, 2))
f9765_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2))) → f9781_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2)), java.lang.Object(ARRAY(4))) | &&(=(matching1, 4), =(matching2, 2))
f9781_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3))) → f9792_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(2))) | &&(&&(=(matching1, 4), =(matching2, 2)), =(matching3, 4))
f9792_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4))) → f9815_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(2)), 0) | &&(&&(&&(=(matching1, 4), =(matching2, 2)), =(matching3, 4)), =(matching4, 2))
f9815_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), java.lang.Object(ARRAY(matching4)), matching5) → f9857_0_main_Duplicate(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2)), java.lang.Object(ARRAY(4)), i2573) | &&(&&(&&(&&(&&(<(0, 2), =(matching1, 4)), =(matching2, 2)), =(matching3, 4)), =(matching4, 2)), =(matching5, 0))
f9857_0_main_Duplicate(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i2573) → f9869_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2)), java.lang.Object(ARRAY(4)), i2573, java.lang.Object(ARRAY(4)), i2573) | &&(&&(=(matching1, 4), =(matching2, 2)), =(matching3, 4))
f9869_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i2573, java.lang.Object(ARRAY(matching4)), i2573) → f9892_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2)), java.lang.Object(ARRAY(4)), i2573) | &&(&&(&&(&&(<(i2573, 4), =(matching1, 4)), =(matching2, 2)), =(matching3, 4)), =(matching4, 4))
f9892_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3)), i2573) → f9900_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), i2573, java.lang.Object(ARRAY(2))) | &&(&&(=(matching1, 4), =(matching2, 2)), =(matching3, 4))
f9900_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), i2573, java.lang.Object(ARRAY(matching3))) → f9903_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), i2573, java.lang.Object(ARRAY(2)), 1) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 2))
f9903_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), i2573, java.lang.Object(ARRAY(matching3)), matching4) → f9927_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), i2573, i2574) | &&(&&(&&(&&(<(1, 2), =(matching1, 4)), =(matching2, 4)), =(matching3, 2)), =(matching4, 1))
f9927_0_main_IntArithmetic(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), i2573, i2574) → f9947_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), i2573) | &&(=(matching1, 4), =(matching2, 4))
f9947_0_main_ArrayAccess(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), i2573) → f9955_0_main_Inc(EOS, java.lang.Object(ARRAY(4)), i1946) | &&(&&(<(i2573, 4), =(matching1, 4)), =(matching2, 4))
f9955_0_main_Inc(EOS, java.lang.Object(ARRAY(matching1)), i1946) → f9959_0_main_JMP(EOS, java.lang.Object(ARRAY(4)), +(i1946, 1)) | &&(>=(i1946, 0), =(matching1, 4))
f9959_0_main_JMP(EOS, java.lang.Object(ARRAY(matching1)), i2631) → f9982_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i2631) | =(matching1, 4)
f9982_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i2631) → f7307_0_main_Load(EOS, java.lang.Object(ARRAY(4)), i2631) | =(matching1, 4)
f7307_0_main_Load(EOS, java.lang.Object(ARRAY(matching1)), i1937) → f7318_0_main_ConstantStackPush(EOS, java.lang.Object(ARRAY(4)), i1937, i1937) | =(matching1, 4)
f10263_0_pick_Return(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3))) → f9725_0_pick_Return(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(2))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 2))
f9725_0_pick_Return(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3))) → f9752_0_main_Store(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(2))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 2))
f7889_1_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3))) → f8232_0_pick_Return(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4)), i2091, java.lang.Object(ARRAY(i2097)), java.lang.Object(ARRAY(2))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))
f7889_1_pick_Load(EOS, java.lang.Object(ARRAY(matching1)), i1946, java.lang.Object(ARRAY(matching2)), java.lang.Object(ARRAY(matching3))) → f10263_0_pick_Return(EOS, java.lang.Object(ARRAY(4)), i1946, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(2))) | &&(&&(=(matching1, 4), =(matching2, 4)), =(matching3, 4))

Combined rules. Obtained 3 IRules

P rules:
f7744_0_main_GE(EOS, java.lang.Object(ARRAY(4)), x1, x2, x3, x3, 4) → f7744_0_main_GE(EOS, java.lang.Object(ARRAY(4)), x1, +(x2, x5), +(x3, 1), +(x3, 1), 4) | &&(>(+(x3, 1), 0), <(x3, 4))
f7744_0_main_GE(EOS, java.lang.Object(ARRAY(4)), x1, x2, x3, x3, 4) → f7906_0_pick_Load(EOS, java.lang.Object(ARRAY(4)), java.lang.Object(ARRAY(4))) | &&(>(x2, 0), >(+(x3, 1), 4))
f7744_0_main_GE(EOS, java.lang.Object(ARRAY(4)), x1, x2, x3, x3, 4) → f7744_0_main_GE(EOS, java.lang.Object(ARRAY(4)), +(x1, 1), 0, 0, 0, 4) | &&(&&(&&(>(+(x3, 1), 4), >(x2, 0)), <(x1, 19)), >(+(x1, 1), 0))

Filtered ground terms:

f7744_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → f7744_0_main_GE(x3, x4, x5, x6)
Cond_f7744_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f7744_0_main_GE(x1, x4, x5, x6, x7, x9)
Cond_f7744_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f7744_0_main_GE1(x1, x4, x5, x6, x7)
f7906_0_pick_Load(x1, x2, x3) → f7906_0_pick_Load
Cond_f7744_0_main_GE2(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f7744_0_main_GE2(x1, x4, x5, x6, x7)
java.lang.Object(x1) → java.lang.Object
ARRAY(x1) → ARRAY

Filtered duplicate terms:

f7744_0_main_GE(x1, x2, x3, x4) → f7744_0_main_GE(x1, x2, x4)
Cond_f7744_0_main_GE(x1, x2, x3, x4, x5, x6) → Cond_f7744_0_main_GE(x1, x2, x3, x5, x6)
Cond_f7744_0_main_GE1(x1, x2, x3, x4, x5) → Cond_f7744_0_main_GE1(x1, x2, x3, x5)
Cond_f7744_0_main_GE2(x1, x2, x3, x4, x5) → Cond_f7744_0_main_GE2(x1, x2, x3, x5)

Filtered unneeded terms:

Cond_f7744_0_main_GE1(x1, x2, x3, x4) → Cond_f7744_0_main_GE1(x1)
Cond_f7744_0_main_GE2(x1, x2, x3, x4) → Cond_f7744_0_main_GE2(x1, x2)

Prepared 3 rules for path length conversion:

P rules:
f7744_0_main_GE(x1, x2, x3) → f7744_0_main_GE(x1, +(x2, x5), +(x3, 1)) | &&(>(+(x3, 1), 0), <(x3, 4))
f7744_0_main_GE(x1, x2, x3) → f7906_0_pick_Load | &&(>(x2, 0), >(+(x3, 1), 4))
f7744_0_main_GE(x1, x2, x3) → f7744_0_main_GE(+(x1, 1), 0, 0) | &&(&&(&&(>(+(x3, 1), 4), >(x2, 0)), <(x1, 19)), >(+(x1, 1), 0))

Finished conversion. Obtained 2 rules.

P rules:
f7744_0_main_GE(x0, x1, x2) → f7744_0_main_GE(x0, +(x1, x3), +(x2, 1)) | &&(<(x2, 4), >(x2, -1))
f7744_0_main_GE(x7, x8, x9) → f7744_0_main_GE(+(x7, 1), 0, 0) | &&(&&(&&(>(x9, 3), >(x8, 0)), <(x7, 19)), >(x7, -1))

(59) Obligation:

Rules:
f7744_0_main_GE(x0, x1, x2) → f7744_0_main_GE(x0, +(x1, x3), +(x2, 1)) | &&(<(x2, 4), >(x2, -1))
f7744_0_main_GE(x7, x8, x9) → f7744_0_main_GE(+(x7, 1), 0, 0) | &&(&&(&&(>(x9, 3), >(x8, 0)), <(x7, 19)), >(x7, -1))

(60) PolynomialOrderProcessor (SOUND transformation)

Found the following polynomial interpretation:

[f7744_0_main_GE(x8, x10, x12)] = 18 - x8

Therefore the following rule(s) have been dropped:

f7744_0_main_GE(x4, x5, x6) → f7744_0_main_GE(+(x4, 1), 0, 0) | &&(&&(&&(>(x6, 3), >(x5, 0)), <(x4, 19)), >(x4, -1))

(61) Obligation:

Rules:
f7744_0_main_GE(x0, x1, x2) → f7744_0_main_GE(x0, +(x1, x3), +(x2, 1)) | &&(<(x2, 4), >(x2, -1))

(62) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f7744_0_main_GE(x5, x7, x9)] = 3 - x9

Therefore the following rule(s) have been dropped:

f7744_0_main_GE(x0, x1, x2) → f7744_0_main_GE(x0, +(x1, x3), +(x2, 1)) | &&(<(x2, 4), >(x2, -1))

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIntTRSProof (SOUND transformation)

(7) Obligation:

(8) LinearRankingProcessor (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) SCCToIntTRSProof (SOUND transformation)

(12) Obligation:

(13) LinearRankingProcessor (EQUIVALENT transformation)

(14) YES

(15) Obligation:

(16) SCCToIntTRSProof (SOUND transformation)

(17) Obligation:

(18) PolynomialOrderProcessor (SOUND transformation)

(19) Obligation:

(20) PolynomialOrderProcessor (EQUIVALENT transformation)

(21) YES

(22) Obligation:

(23) SCCToIntTRSProof (SOUND transformation)

(24) Obligation:

(25) PolynomialOrderProcessor (EQUIVALENT transformation)

(26) YES

(27) Obligation:

(28) SCCToIntTRSProof (SOUND transformation)

(29) Obligation:

(30) PolynomialOrderProcessor (EQUIVALENT transformation)

(31) YES

(32) Obligation:

(33) SCCToIntTRSProof (SOUND transformation)

(34) Obligation:

(35) LinearRankingProcessor (EQUIVALENT transformation)

(36) YES

(37) Obligation:

(38) SCCToIntTRSProof (SOUND transformation)

(39) Obligation:

(40) PolynomialOrderProcessor (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) SCCToIntTRSProof (SOUND transformation)

(44) Obligation:

(45) PolynomialOrderProcessor (EQUIVALENT transformation)

(46) YES

(47) Obligation:

(48) SCCToIntTRSProof (SOUND transformation)

(49) Obligation:

(50) LinearRankingProcessor (EQUIVALENT transformation)

(51) YES

(52) Obligation:

(53) SCCToIntTRSProof (SOUND transformation)

(54) Obligation:

(55) PolynomialOrderProcessor (EQUIVALENT transformation)

(56) YES

(57) Obligation:

(58) SCCToIntTRSProof (SOUND transformation)

(59) Obligation:

(60) PolynomialOrderProcessor (SOUND transformation)

(61) Obligation:

(62) PolynomialOrderProcessor (EQUIVALENT transformation)

(63) YES