Termination proof of /tmp/tmp_kUxlo/SearchTreeR.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1313 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 185 ms)

        ↳7 intTRS

        ↳8 PolynomialOrderProcessor (⇔, 0 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIntTRSProof (⇒, 204 ms)

        ↳12 intTRS

        ↳13 PolynomialOrderProcessor (⇔, 0 ms)

        ↳14 YES

(0) Obligation:

JBC Problem based on JBC Program:

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

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


package SearchTreeR;


public class SearchTreeR {
  public static void main(final String[] args) {
    Random.args = args;

    final Tree t = new Tree(Random.random());

    final int numberOfVals = Random.random();
    for (int i = 0; i < numberOfVals; i++) {
        t.insert(Random.random());
    }
  }
}


package SearchTreeR;

public class Tree {
    Tree left;
    Tree right;
    int value;

    public Tree(final int val) {
        this.value = val;
    }

    public void insert(final int v) {
        if (v <= this.value) {
            if (this.left == null) {
                this.left = new Tree(v);
            } else {
                this.left.insert(v);
            }
        } else {
            if (this.right == null) {
                this.right = new Tree(v);
            } else {
                this.right.insert(v);
            }
        }
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

SearchTreeR.Tree.insert(I)V: Graph of 72 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: SearchTreeR.Tree.insert(I)V
SCC calls the following helper methods: SearchTreeR.Tree.insert(I)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
- SearchTreeR.Tree: [value, right, left]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 30 IRules

P rules:
f2839_0_insert_Load(EOS, java.lang.Object(o1537sub), i923, java.lang.Object(o1537sub), i923, i923) → f2848_0_insert_FieldAccess(EOS, java.lang.Object(o1537sub), i923, java.lang.Object(o1537sub), i923, i923, java.lang.Object(o1537sub))
f2848_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555))) → f2855_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)))
f2855_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555))) → f2856_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930)
f2856_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930) → f2860_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930)
f2856_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930) → f2861_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930)
f2860_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930) → f2868_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923) | >(i923, i930)
f2868_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923) → f2883_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)))
f2883_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555))) → f2897_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, o1556)
f2897_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub)) → f2910_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub))
f2910_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub)) → f2926_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923)
f2926_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923) → f2948_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)))
f2948_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555))) → f2964_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, i923, java.lang.Object(o1611sub))
f2964_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, i923, java.lang.Object(o1611sub)) → f2978_0_insert_InvokeMethod(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub), i923)
f2978_0_insert_InvokeMethod(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub), i923) → f2991_0_insert_Load(EOS, java.lang.Object(o1611sub), i923, java.lang.Object(o1611sub), i923)
f2978_0_insert_InvokeMethod(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub), i923) → f2991_1_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, java.lang.Object(o1611sub), o1555)), i923, java.lang.Object(o1611sub), i923, java.lang.Object(o1611sub), i923)
f2991_0_insert_Load(EOS, java.lang.Object(o1611sub), i923, java.lang.Object(o1611sub), i923) → f3007_0_insert_Load(EOS, java.lang.Object(o1611sub), i923, java.lang.Object(o1611sub), i923)
f3007_0_insert_Load(EOS, java.lang.Object(o1611sub), i923, java.lang.Object(o1611sub), i923) → f2835_0_insert_Load(EOS, java.lang.Object(o1611sub), i923, java.lang.Object(o1611sub), i923)
f2835_0_insert_Load(EOS, java.lang.Object(o1537sub), i923, java.lang.Object(o1537sub), i923) → f2839_0_insert_Load(EOS, java.lang.Object(o1537sub), i923, java.lang.Object(o1537sub), i923, i923)
f2861_0_insert_GT(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, i923, i930) → f2875_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923) | <=(i923, i930)
f2875_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923) → f2889_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)))
f2889_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555))) → f2904_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, o1555)), i923, o1555)
f2904_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub)) → f2919_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub))
f2919_0_insert_NONNULL(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub)) → f2941_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923)
f2941_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923) → f2959_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))))
f2959_0_insert_FieldAccess(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, i923, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub)))) → f2970_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, i923, java.lang.Object(o1619sub))
f2970_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, i923, java.lang.Object(o1619sub)) → f2983_0_insert_InvokeMethod(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub), i923)
f2983_0_insert_InvokeMethod(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub), i923) → f2999_0_insert_Load(EOS, java.lang.Object(o1619sub), i923, java.lang.Object(o1619sub), i923)
f2983_0_insert_InvokeMethod(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub), i923) → f2999_1_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, i930, o1556, java.lang.Object(o1619sub))), i923, java.lang.Object(o1619sub), i923, java.lang.Object(o1619sub), i923)
f2999_0_insert_Load(EOS, java.lang.Object(o1619sub), i923, java.lang.Object(o1619sub), i923) → f3013_0_insert_Load(EOS, java.lang.Object(o1619sub), i923, java.lang.Object(o1619sub), i923)
f3013_0_insert_Load(EOS, java.lang.Object(o1619sub), i923, java.lang.Object(o1619sub), i923) → f2835_0_insert_Load(EOS, java.lang.Object(o1619sub), i923, java.lang.Object(o1619sub), i923)

Combined rules. Obtained 4 IRules

P rules:
f2839_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, x0, java.lang.Object(x1), x2)), x3, java.lang.Object(SearchTreeR.Tree(EOC, x0, java.lang.Object(x1), x2)), x3, x3) → f2991_1_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, x0, java.lang.Object(x1), x2)), x3, java.lang.Object(x1), x3, java.lang.Object(x1), x3) | >(x3, x0)
f2839_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, x0, java.lang.Object(x1), x2)), x3, java.lang.Object(SearchTreeR.Tree(EOC, x0, java.lang.Object(x1), x2)), x3, x3) → f2839_0_insert_Load(EOS, java.lang.Object(x1), x3, java.lang.Object(x1), x3, x3) | >(x3, x0)
f2839_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, x0, x1, java.lang.Object(x2))), x3, java.lang.Object(SearchTreeR.Tree(EOC, x0, x1, java.lang.Object(x2))), x3, x3) → f2999_1_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, x0, x1, java.lang.Object(x2))), x3, java.lang.Object(x2), x3, java.lang.Object(x2), x3) | <=(x3, x0)
f2839_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC, x0, x1, java.lang.Object(x2))), x3, java.lang.Object(SearchTreeR.Tree(EOC, x0, x1, java.lang.Object(x2))), x3, x3) → f2839_0_insert_Load(EOS, java.lang.Object(x2), x3, java.lang.Object(x2), x3, x3) | <=(x3, x0)

Filtered ground terms:

f2839_0_insert_Load(x1, x2, x3, x4, x5, x6) → f2839_0_insert_Load(x2, x3, x4, x5, x6)
Cond_f2839_0_insert_Load(x1, x2, x3, x4, x5, x6, x7) → Cond_f2839_0_insert_Load(x1, x3, x4, x5, x6, x7)
f2991_1_insert_Load(x1, x2, x3, x4, x5, x6, x7) → f2991_1_insert_Load(x2, x3, x4, x5, x6, x7)
Cond_f2839_0_insert_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f2839_0_insert_Load1(x1, x3, x4, x5, x6, x7)
Cond_f2839_0_insert_Load2(x1, x2, x3, x4, x5, x6, x7) → Cond_f2839_0_insert_Load2(x1, x3, x4, x5, x6, x7)
f2999_1_insert_Load(x1, x2, x3, x4, x5, x6, x7) → f2999_1_insert_Load(x2, x3, x4, x5, x6, x7)
Cond_f2839_0_insert_Load3(x1, x2, x3, x4, x5, x6, x7) → Cond_f2839_0_insert_Load3(x1, x3, x4, x5, x6, x7)
SearchTreeR.Tree(x1, x2, x3, x4) → SearchTreeR.Tree(x2, x3, x4)

Filtered duplicate terms:

f2839_0_insert_Load(x1, x2, x3, x4, x5) → f2839_0_insert_Load(x3, x5)
Cond_f2839_0_insert_Load(x1, x2, x3, x4, x5, x6) → Cond_f2839_0_insert_Load(x1, x4, x6)
f2991_1_insert_Load(x1, x2, x3, x4, x5, x6) → f2991_1_insert_Load(x1, x6)
Cond_f2839_0_insert_Load1(x1, x2, x3, x4, x5, x6) → Cond_f2839_0_insert_Load1(x1, x4, x6)
Cond_f2839_0_insert_Load2(x1, x2, x3, x4, x5, x6) → Cond_f2839_0_insert_Load2(x1, x4, x6)
f2999_1_insert_Load(x1, x2, x3, x4, x5, x6) → f2999_1_insert_Load(x1, x6)
Cond_f2839_0_insert_Load3(x1, x2, x3, x4, x5, x6) → Cond_f2839_0_insert_Load3(x1, x4, x6)

Filtered unneeded terms:

Cond_f2839_0_insert_Load(x1, x2, x3) → Cond_f2839_0_insert_Load(x1)
Cond_f2839_0_insert_Load2(x1, x2, x3) → Cond_f2839_0_insert_Load2(x1)

Prepared 4 rules for path length conversion:

P rules:
f2839_0_insert_Load(java.lang.Object(SearchTreeR.Tree(x0, java.lang.Object(x1), x2)), x3) → f2991_1_insert_Load(java.lang.Object(SearchTreeR.Tree(x0, java.lang.Object(x1), x2)), x3) | >(x3, x0)
f2839_0_insert_Load(java.lang.Object(SearchTreeR.Tree(x0, java.lang.Object(x1), x2)), x3) → f2839_0_insert_Load(java.lang.Object(x1), x3) | >(x3, x0)
f2839_0_insert_Load(java.lang.Object(SearchTreeR.Tree(x0, x1, java.lang.Object(x2))), x3) → f2999_1_insert_Load(java.lang.Object(SearchTreeR.Tree(x0, x1, java.lang.Object(x2))), x3) | <=(x3, x0)
f2839_0_insert_Load(java.lang.Object(SearchTreeR.Tree(x0, x1, java.lang.Object(x2))), x3) → f2839_0_insert_Load(java.lang.Object(x2), x3) | <=(x3, x0)

Finished conversion. Obtained 2 rules.

P rules:
f2839_0_insert_Load(v18, x7) → f2839_0_insert_Load(v19, x7) | &&(&&(&&(>(x7, x4), >(+(v19, 1), 1)), <=(+(v19, 2), v18)), >(+(v18, 1), 3))
f2839_0_insert_Load(v20, x15) → f2839_0_insert_Load(v21, x15) | &&(&&(&&(<=(x15, x12), >(+(v21, 1), 1)), <=(+(v21, 2), v20)), >(+(v20, 1), 3))

(7) Obligation:

Rules:
f2839_0_insert_Load(v18, x7) → f2839_0_insert_Load(v19, x7) | &&(&&(&&(>(x7, x4), >(+(v19, 1), 1)), <=(+(v19, 2), v18)), >(+(v18, 1), 3))
f2839_0_insert_Load(v20, x15) → f2839_0_insert_Load(v21, x15) | &&(&&(&&(<=(x15, x12), >(+(v21, 1), 1)), <=(+(v21, 2), v20)), >(+(v20, 1), 3))

(8) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2839_0_insert_Load(x9, x11)] = x9

Therefore the following rule(s) have been dropped:

f2839_0_insert_Load(x0, x1) → f2839_0_insert_Load(x2, x1) | &&(&&(&&(>(x1, x3), >(+(x2, 1), 1)), <=(+(x2, 2), x0)), >(+(x0, 1), 3))
f2839_0_insert_Load(x4, x5) → f2839_0_insert_Load(x6, x5) | &&(&&(&&(<=(x5, x7), >(+(x6, 1), 1)), <=(+(x6, 2), x4)), >(+(x4, 1), 3))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: SearchTreeR.SearchTreeR.main([Ljava/lang/String;)V
SCC calls the following helper methods: SearchTreeR.Tree.insert(I)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
- java.lang.String: [count]
Marker field analysis yielded the following relations that could be markers:

(11) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 39 IRules

P rules:
f2617_0_main_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, i837) → f2620_0_main_GE(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, i837, i118)
f2620_0_main_GE(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, i837, i118) → f2622_0_main_GE(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, i837, i118)
f2622_0_main_GE(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, i837, i118) → f2626_0_main_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837) | <(i837, i118)
f2626_0_main_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837) → f2629_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)))
f2629_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC))) → f2631_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)))
f2631_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC))) → f2634_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)))
f2634_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834))) → f2640_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)), i835)
f2640_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)), i848) → f2643_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)), i848)
f2643_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)), i848) → f2647_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)), i848)
f2647_0_random_ArrayAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(ARRAY(i834)), i848) → f2651_0_random_Store(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386) | <(i848, i834)
f2651_0_random_Store(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386) → f2660_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386)
f2660_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386) → f2664_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386, i848)
f2664_0_random_ConstantStackPush(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386, i848) → f2671_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386, i848, 1)
f2671_0_random_IntArithmetic(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386, i848, matching1) → f2678_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386, +(i848, 1)) | &&(>=(i848, 0), =(matching1, 1))
f2678_0_random_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386, i857) → f2683_0_random_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386)
f2683_0_random_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386) → f2696_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), o1386)
f2696_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(o1431sub)) → f2704_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(o1431sub))
f2704_0_random_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(o1431sub)) → f2709_0_length_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(o1431sub), java.lang.Object(o1431sub))
f2709_0_length_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(o1431sub), java.lang.Object(o1431sub)) → f2729_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(o1431sub), java.lang.Object(o1431sub))
f2729_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(java.lang.String(o1449sub, i889)), java.lang.Object(java.lang.String(o1449sub, i889))) → f2733_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(java.lang.String(o1449sub, i889)), java.lang.Object(java.lang.String(o1449sub, i889))) | >=(i889, 0)
f2733_0_length_FieldAccess(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(java.lang.String(o1449sub, i889)), java.lang.Object(java.lang.String(o1449sub, i889))) → f2745_0_length_Return(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(java.lang.String(o1449sub, i889)), i889)
f2745_0_length_Return(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), java.lang.Object(java.lang.String(o1449sub, i889)), i889) → f2757_0_random_Return(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i889)
f2757_0_random_Return(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i889) → f2764_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i889)
f2764_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i889) → f2783_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC)), i889, java.lang.Object(SearchTreeR.Tree(EOC)), i889)
f2764_0_main_InvokeMethod(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i889) → f2783_1_insert_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i889, java.lang.Object(SearchTreeR.Tree(EOC)), i889)
f2783_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC)), i889, java.lang.Object(SearchTreeR.Tree(EOC)), i889) → f2795_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC)), i889, java.lang.Object(SearchTreeR.Tree(EOC)), i889)
f3086_0_insert_Return(EOS, java.lang.Object(ARRAY(i1005)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1009) → f3148_0_insert_Return(EOS, java.lang.Object(ARRAY(i1005)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1009)
f3148_0_insert_Return(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1086) → f3168_0_main_Inc(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837)
f3168_0_main_Inc(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837) → f3171_0_main_JMP(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, +(i837, 1)) | >=(i837, 0)
f3171_0_main_JMP(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i1099) → f3192_0_main_Load(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i1099)
f3192_0_main_Load(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i1099) → f2612_0_main_Load(EOS, java.lang.Object(ARRAY(i1083)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i1099)
f2612_0_main_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837) → f2617_0_main_Load(EOS, java.lang.Object(ARRAY(i834)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, i837)
f3147_0_insert_Return(EOS, java.lang.Object(ARRAY(i1067)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1071) → f3148_0_insert_Return(EOS, java.lang.Object(ARRAY(i1067)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1071)
f3294_0_insert_Return(EOS, java.lang.Object(ARRAY(i1158)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1162) → f3148_0_insert_Return(EOS, java.lang.Object(ARRAY(i1158)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1162)
f3827_0_insert_Return(EOS, java.lang.Object(ARRAY(i1259)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1263) → f3148_0_insert_Return(EOS, java.lang.Object(ARRAY(i1259)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1263)
f2783_1_insert_Load(EOS, java.lang.Object(ARRAY(i1005)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1009, java.lang.Object(SearchTreeR.Tree(EOC)), i1009) → f3086_0_insert_Return(EOS, java.lang.Object(ARRAY(i1005)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1009)
f2783_1_insert_Load(EOS, java.lang.Object(ARRAY(i1067)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1071, java.lang.Object(SearchTreeR.Tree(EOC)), i1071) → f3147_0_insert_Return(EOS, java.lang.Object(ARRAY(i1067)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1071)
f2783_1_insert_Load(EOS, java.lang.Object(ARRAY(i1158)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1162, java.lang.Object(SearchTreeR.Tree(EOC)), i1162) → f3294_0_insert_Return(EOS, java.lang.Object(ARRAY(i1158)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1162)
f2783_1_insert_Load(EOS, java.lang.Object(ARRAY(i1259)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1263, java.lang.Object(SearchTreeR.Tree(EOC)), i1263) → f3827_0_insert_Return(EOS, java.lang.Object(ARRAY(i1259)), java.lang.Object(SearchTreeR.Tree(EOC)), i118, i837, java.lang.Object(SearchTreeR.Tree(EOC)), i1263)

Combined rules. Obtained 2 IRules

P rules:
f2617_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(SearchTreeR.Tree(EOC)), x1, x2, x2) → f2795_0_insert_Load(EOS, java.lang.Object(SearchTreeR.Tree(EOC)), x3, java.lang.Object(SearchTreeR.Tree(EOC)), x3) | &&(<(x2, x1), >(+(x3, 1), 0))
f2617_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(SearchTreeR.Tree(EOC)), x1, x2, x2) → f2617_0_main_Load(EOS, java.lang.Object(ARRAY(x0)), java.lang.Object(SearchTreeR.Tree(EOC)), x1, +(x2, 1), +(x2, 1)) | &&(<(x2, x1), >(+(x2, 1), 0))

Filtered ground terms:

f2617_0_main_Load(x1, x2, x3, x4, x5, x6) → f2617_0_main_Load(x2, x4, x5, x6)
Cond_f2617_0_main_Load(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f2617_0_main_Load(x1, x3, x5, x6, x7, x8)
f2795_0_insert_Load(x1, x2, x3, x4, x5) → f2795_0_insert_Load(x3, x5)
Cond_f2617_0_main_Load1(x1, x2, x3, x4, x5, x6, x7) → Cond_f2617_0_main_Load1(x1, x3, x5, x6, x7)
SearchTreeR.Tree(x1) → SearchTreeR.Tree

Filtered duplicate terms:

f2617_0_main_Load(x1, x2, x3, x4) → f2617_0_main_Load(x1, x2, x4)
Cond_f2617_0_main_Load(x1, x2, x3, x4, x5, x6) → Cond_f2617_0_main_Load(x1, x2, x3, x5, x6)
f2795_0_insert_Load(x1, x2) → f2795_0_insert_Load(x2)
Cond_f2617_0_main_Load1(x1, x2, x3, x4, x5) → Cond_f2617_0_main_Load1(x1, x2, x3, x5)

Filtered unneeded terms:

Cond_f2617_0_main_Load(x1, x2, x3, x4, x5) → Cond_f2617_0_main_Load(x1)
Cond_f2617_0_main_Load1(x1, x2, x3, x4) → Cond_f2617_0_main_Load1(x1, x3, x4)
f2617_0_main_Load(x1, x2, x3) → f2617_0_main_Load(x2, x3)

Prepared 2 rules for path length conversion:

P rules:
f2617_0_main_Load(x1, x2) → f2795_0_insert_Load(x3) | &&(<(x2, x1), >(+(x3, 1), 0))
f2617_0_main_Load(x1, x2) → f2617_0_main_Load(x1, +(x2, 1)) | &&(<(x2, x1), >(+(x2, 1), 0))

Finished conversion. Obtained 1 rules.

P rules:
f2617_0_main_Load(x3, x4) → f2617_0_main_Load(x3, +(x4, 1)) | &&(<(x4, x3), >(x4, -1))

(12) Obligation:

Rules:
f2617_0_main_Load(x3, x4) → f2617_0_main_Load(x3, +(x4, 1)) | &&(<(x4, x3), >(x4, -1))

(13) PolynomialOrderProcessor (EQUIVALENT transformation)