Termination proof of /tmp/tmp2m07hA/GrowTreeR.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1424 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIntTRSProof (⇒, 126 ms)

        ↳7 intTRS

        ↳8 LinearRankingProcessor (⇔, 52 ms)

        ↳9 YES

    ↳10 JBCTerminationSCC

        ↳11 SCCToIDPv1Proof (⇒, 786 ms)

        ↳12 IDP

        ↳13 IDPNonInfProof (⇒, 670 ms)

        ↳14 AND

            ↳15 IDP

                ↳16 IDependencyGraphProof (⇔, 0 ms)

                ↳17 IDP

                ↳18 UsableRulesProof (⇔, 0 ms)

                ↳19 IDP

                ↳20 IDPNonInfProof (⇒, 211 ms)

                ↳21 AND

                    ↳22 IDP

                        ↳23 IDependencyGraphProof (⇔, 0 ms)

                        ↳24 TRUE

                    ↳25 IDP

                        ↳26 IDependencyGraphProof (⇔, 0 ms)

                        ↳27 TRUE

            ↳28 IDP

                ↳29 IDependencyGraphProof (⇔, 0 ms)

                ↳30 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

package GrowTreeR;

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

    final Tree t = Tree.createTree(Random.random());
    growList(t.children);
  }

  public static void growTree(final Tree t) {
      if (t == null) {
          return;
      } else if (t.children == null) {
          t.children = new TreeList(new Tree(), null);
      } else {
          growList(t.children);
      }
  }

  public static void growList(final TreeList l) {
      if (l == null) {
          return;
      } else {
          growTree(l.value);
          growList(l.next);
      }
  }
}


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

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


package GrowTreeR;
public class Tree {
    TreeList children;

    public Tree() {
        this.children = null;
    }

    public void addChild(final Tree t) {
        this.children = new TreeList(t, this.children);
    }

    public static Tree createNode() {
        final Tree result = new Tree();
        return result;
    }

    public static Tree createTree(int depth) {
        if (depth <= 0) {
            return null;
        }
        depth = depth - 1;

        final Tree result = new Tree();
        final int numberOfChildren = Random.random();

        for (int i = 0; i < numberOfChildren; i++) {
            result.addChild(createTree(depth - 1));
        }

        return result;
    }
}


package GrowTreeR;
public class TreeList {
  Tree value;
  TreeList next;

  public TreeList(final Tree value, final TreeList next) {
    this.value = value;
    this.next = next;
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

GrowTreeR.Tree.createTree(I)LGrowTreeR/Tree;: Graph of 163 nodes with 1 SCC.

GrowTreeR.GrowTreeR.growList(LGrowTreeR/TreeList;)V: Graph of 49 nodes with 0 SCCs.

GrowTreeR.GrowTreeR.growTree(LGrowTreeR/Tree;)V: Graph of 52 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: GrowTreeR.GrowTreeR.growList(LGrowTreeR/TreeList;)V, GrowTreeR.GrowTreeR.growTree(LGrowTreeR/Tree;)V
SCC calls the following helper methods: GrowTreeR.GrowTreeR.growList(LGrowTreeR/TreeList;)V, GrowTreeR.GrowTreeR.growTree(LGrowTreeR/Tree;)V
Performed SCC analyses:

Used field analysis yielded the following read fields:
- GrowTreeR.TreeList: [value, next]
- GrowTreeR.Tree: [children]
Marker field analysis yielded the following relations that could be markers:

(6) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 43 IRules

P rules:
f2381_0_growList_NONNULL(EOS, java.lang.Object(o594sub), java.lang.Object(o594sub), java.lang.Object(o594sub)) → f2385_0_growList_NONNULL(EOS, java.lang.Object(o594sub), java.lang.Object(o594sub), java.lang.Object(o594sub))
f2385_0_growList_NONNULL(EOS, java.lang.Object(o594sub), java.lang.Object(o594sub), java.lang.Object(o594sub)) → f2388_0_growList_Load(EOS, java.lang.Object(o594sub), java.lang.Object(o594sub))
f2388_0_growList_Load(EOS, java.lang.Object(o594sub), java.lang.Object(o594sub)) → f2396_0_growList_FieldAccess(EOS, java.lang.Object(o594sub), java.lang.Object(o594sub), java.lang.Object(o594sub))
f2396_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606))) → f2404_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)))
f2404_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606))) → f2416_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), o605)
f2416_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), o605) → f2437_0_growTree_Load(EOS, o605, o605)
f2416_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), o605) → f2437_1_growTree_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), o605, o605)
f2437_0_growTree_Load(EOS, o605, o605) → f2458_0_growTree_Load(EOS, o605, o605)
f2458_0_growTree_Load(EOS, o605, o605) → f2488_0_growTree_Load(EOS, o605, o605)
f2488_0_growTree_Load(EOS, o605, o605) → f2495_0_growTree_NONNULL(EOS, o605, o605, o605)
f2495_0_growTree_NONNULL(EOS, java.lang.Object(o644sub), java.lang.Object(o644sub), java.lang.Object(o644sub)) → f2501_0_growTree_NONNULL(EOS, java.lang.Object(o644sub), java.lang.Object(o644sub), java.lang.Object(o644sub))
f2501_0_growTree_NONNULL(EOS, java.lang.Object(o644sub), java.lang.Object(o644sub), java.lang.Object(o644sub)) → f2506_0_growTree_Load(EOS, java.lang.Object(o644sub), java.lang.Object(o644sub))
f2506_0_growTree_Load(EOS, java.lang.Object(o644sub), java.lang.Object(o644sub)) → f2524_0_growTree_FieldAccess(EOS, java.lang.Object(o644sub), java.lang.Object(o644sub), java.lang.Object(o644sub))
f2524_0_growTree_FieldAccess(EOS, java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661))) → f2532_0_growTree_FieldAccess(EOS, java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661)))
f2532_0_growTree_FieldAccess(EOS, java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661))) → f2555_0_growTree_NONNULL(EOS, java.lang.Object(GrowTreeR.Tree(EOC, o661)), java.lang.Object(GrowTreeR.Tree(EOC, o661)), o661)
f2555_0_growTree_NONNULL(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub)) → f2579_0_growTree_NONNULL(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub))
f2579_0_growTree_NONNULL(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub)) → f2620_0_growTree_Load(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))))
f2620_0_growTree_Load(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub)))) → f2632_0_growTree_FieldAccess(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))))
f2632_0_growTree_FieldAccess(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub)))) → f2656_0_growTree_InvokeMethod(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub))
f2656_0_growTree_InvokeMethod(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub)) → f2681_0_growList_Load(EOS, java.lang.Object(o678sub), java.lang.Object(o678sub))
f2656_0_growTree_InvokeMethod(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub)) → f2681_1_growList_Load(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(o678sub))), java.lang.Object(o678sub), java.lang.Object(o678sub))
f2681_0_growList_Load(EOS, java.lang.Object(o678sub), java.lang.Object(o678sub)) → f2691_0_growList_Load(EOS, java.lang.Object(o678sub), java.lang.Object(o678sub))
f2691_0_growList_Load(EOS, java.lang.Object(o678sub), java.lang.Object(o678sub)) → f2378_0_growList_Load(EOS, java.lang.Object(o678sub), java.lang.Object(o678sub))
f2378_0_growList_Load(EOS, o592, o592) → f2381_0_growList_NONNULL(EOS, o592, o592, o592)
f2556_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), NULL, NULL) → f2582_0_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)))
f2582_0_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606))) → f2622_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)))
f2622_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606))) → f2629_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), o606)
f2629_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), o606) → f2634_0_growList_Load(EOS, o606, o606)
f2629_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), o606) → f2634_1_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), o606, o606)
f2634_0_growList_Load(EOS, o606, o606) → f2651_0_growList_Load(EOS, o606, o606)
f2651_0_growList_Load(EOS, o606, o606) → f2378_0_growList_Load(EOS, o606, o606)
f3459_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), o606)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), o606)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL))))) → f3460_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), o606)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), o606)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))))
f3460_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189))))) → f3516_0_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)))
f3516_0_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186))) → f3527_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)))
f3527_0_growList_FieldAccess(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186))) → f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), o1186)
f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), o1186) → f3645_0_growList_Load(EOS, o1186, o1186)
f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), o1186) → f3645_1_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), o1186, o1186)
f3645_0_growList_Load(EOS, o1186, o1186) → f3667_0_growList_Load(EOS, o1186, o1186)
f3667_0_growList_Load(EOS, o1186, o1186) → f2378_0_growList_Load(EOS, o1186, o1186)
f4116_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))), o606)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))), o606)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547))))) → f3460_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))), o606)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))), o606)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))))
f2437_1_growTree_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), NULL, NULL) → f2556_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, o606)), NULL, NULL)
f2437_1_growTree_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), o605, o605) → f3459_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), o606)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), o606)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))))
f2437_1_growTree_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), java.lang.Object(GrowTreeR.TreeList(EOC, o605, o606)), o605, o605) → f4116_0_growTree_Return(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))), o606)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))), o606)), java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1548, o1547)))))

Combined rules. Obtained 8 IRules

P rules:
f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), o1186) → f3645_1_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, o1190, o1189)))), o1186)), o1186, o1186)
f2381_0_growList_NONNULL(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), x1)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), x1)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), x1))) → f2681_1_growList_Load(EOS, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), java.lang.Object(x0), java.lang.Object(x0))
f2381_0_growList_NONNULL(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), x1)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), x1)), java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(x0))), x1))) → f2381_0_growList_NONNULL(EOS, java.lang.Object(x0), java.lang.Object(x0), java.lang.Object(x0))
f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1)))), x2)), x2) → f2381_0_growList_NONNULL(EOS, x2, x2, x2)
f2381_0_growList_NONNULL(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0))) → f2634_1_growList_Load(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0)), x0, x0)
f2381_0_growList_NONNULL(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0)), java.lang.Object(GrowTreeR.TreeList(EOC, NULL, x0))) → f2381_0_growList_NONNULL(EOS, x0, x0, x0)
f2381_0_growList_NONNULL(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1)), java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1)), java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1))) → f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, NULL)), NULL)))), x1)), x1)
f2381_0_growList_NONNULL(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1)), java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1)), java.lang.Object(GrowTreeR.TreeList(EOC, x0, x1))) → f3535_0_growList_InvokeMethod(EOS, java.lang.Object(GrowTreeR.TreeList(EOC, java.lang.Object(GrowTreeR.Tree(EOC, java.lang.Object(GrowTreeR.TreeList(EOC, x2, x3)))), x1)), x1)

Filtered ground terms:

f3535_0_growList_InvokeMethod(x1, x2, x3) → f3535_0_growList_InvokeMethod(x2, x3)
f3645_1_growList_Load(x1, x2, x3, x4) → f3645_1_growList_Load(x2, x3, x4)
f2381_0_growList_NONNULL(x1, x2, x3, x4) → f2381_0_growList_NONNULL(x2, x3, x4)
f2681_1_growList_Load(x1, x2, x3, x4) → f2681_1_growList_Load(x2, x3, x4)
f2634_1_growList_Load(x1, x2, x3, x4) → f2634_1_growList_Load(x2, x3, x4)
GrowTreeR.TreeList(x1, x2, x3) → GrowTreeR.TreeList(x2, x3)
GrowTreeR.Tree(x1, x2) → GrowTreeR.Tree(x2)

Filtered duplicate terms:

f3535_0_growList_InvokeMethod(x1, x2) → f3535_0_growList_InvokeMethod(x1)
f3645_1_growList_Load(x1, x2, x3) → f3645_1_growList_Load(x1)
f2381_0_growList_NONNULL(x1, x2, x3) → f2381_0_growList_NONNULL(x3)
f2681_1_growList_Load(x1, x2, x3) → f2681_1_growList_Load(x1)
f2634_1_growList_Load(x1, x2, x3) → f2634_1_growList_Load(x1)

Prepared 8 rules for path length conversion:

P rules:
f3535_0_growList_InvokeMethod(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(GrowTreeR.TreeList(o1190, o1189)))), o1186)), o1186) → f3645_1_growList_Load(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(GrowTreeR.TreeList(o1190, o1189)))), o1186)))
f2381_0_growList_NONNULL(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(x0))), x1))) → f2681_1_growList_Load(java.lang.Object(GrowTreeR.Tree(java.lang.Object(x0))))
f2381_0_growList_NONNULL(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(x0))), x1))) → f2381_0_growList_NONNULL(java.lang.Object(x0))
f3535_0_growList_InvokeMethod(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(GrowTreeR.TreeList(x0, x1)))), x2)), x2) → f2381_0_growList_NONNULL(x2)
f2381_0_growList_NONNULL(java.lang.Object(GrowTreeR.TreeList(NULL, x0))) → f2634_1_growList_Load(java.lang.Object(GrowTreeR.TreeList(NULL, x0)))
f2381_0_growList_NONNULL(java.lang.Object(GrowTreeR.TreeList(NULL, x0))) → f2381_0_growList_NONNULL(x0)
f2381_0_growList_NONNULL(java.lang.Object(GrowTreeR.TreeList(x0, x1))) → f3535_0_growList_InvokeMethod(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(NULL)), NULL)))), x1)), x1)
f2381_0_growList_NONNULL(java.lang.Object(GrowTreeR.TreeList(x0, x1))) → f3535_0_growList_InvokeMethod(java.lang.Object(GrowTreeR.TreeList(java.lang.Object(GrowTreeR.Tree(java.lang.Object(GrowTreeR.TreeList(x2, x3)))), x1)), x1)

Finished conversion. Obtained 5 rules.

P rules:
f2381_0_growList_NONNULL(v21) → f2381_0_growList_NONNULL(v22) | &&(&&(>(+(v22, 1), 1), <=(+(v22, 4), v21)), >(+(v21, 1), 5))
f3535_0_growList_InvokeMethod(v23, v24) → f2381_0_growList_NONNULL(v25) | &&(&&(&&(&&(>(+(v25, 1), 0), <=(v25, v24)), <=(+(v25, 2), v23)), >(+(v24, 1), 0)), >(+(v23, 1), 5))
f2381_0_growList_NONNULL(v26) → f2381_0_growList_NONNULL(v27) | &&(&&(>(+(v27, 1), 0), <=(+(v27, 2), v26)), >(+(v26, 1), 2))
f2381_0_growList_NONNULL(v28) → f3535_0_growList_InvokeMethod(v29, v30) | &&(&&(&&(&&(>(+(v30, 1), 0), <=(+(v30, 1), v28)), >(+(v29, 1), 8)), <=(-(v29, 7), v28)), >(+(v28, 1), 1))
f2381_0_growList_NONNULL(v31) → f3535_0_growList_InvokeMethod(v32, v33) | &&(&&(&&(>(+(v33, 1), 0), <=(+(v33, 1), v31)), >(+(v32, 1), 5)), >(+(v31, 1), 1))

(7) Obligation:

Rules:
f2381_0_growList_NONNULL(v21) → f2381_0_growList_NONNULL(v22) | &&(&&(>(+(v22, 1), 1), <=(+(v22, 4), v21)), >(+(v21, 1), 5))
f3535_0_growList_InvokeMethod(v23, v24) → f2381_0_growList_NONNULL(v25) | &&(&&(&&(&&(>(+(v25, 1), 0), <=(v25, v24)), <=(+(v25, 2), v23)), >(+(v24, 1), 0)), >(+(v23, 1), 5))
f2381_0_growList_NONNULL(v26) → f2381_0_growList_NONNULL(v27) | &&(&&(>(+(v27, 1), 0), <=(+(v27, 2), v26)), >(+(v26, 1), 2))
f2381_0_growList_NONNULL(v28) → f3535_0_growList_InvokeMethod(v29, v30) | &&(&&(&&(&&(>(+(v30, 1), 0), <=(+(v30, 1), v28)), >(+(v29, 1), 8)), <=(-(v29, 7), v28)), >(+(v28, 1), 1))
f2381_0_growList_NONNULL(v31) → f3535_0_growList_InvokeMethod(v32, v33) | &&(&&(&&(>(+(v33, 1), 0), <=(+(v33, 1), v31)), >(+(v32, 1), 5)), >(+(v31, 1), 1))

(8) LinearRankingProcessor (EQUIVALENT transformation)

Linear ranking:

[f2381_0_growList_NONNULL(x)] = 2·x₁
[f3535_0_growList_InvokeMethod(x)] = 1 + 2·x₂

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

Therefore the following rule(s) have been dropped:

f2381_0_growList_NONNULL(x0) → f2381_0_growList_NONNULL(x1) | &&(&&(>(+(x1, 1), 1), <=(+(x1, 4), x0)), >(+(x0, 1), 5))
f3535_0_growList_InvokeMethod(x2, x3) → f2381_0_growList_NONNULL(x4) | &&(&&(&&(&&(>(+(x4, 1), 0), <=(x4, x3)), <=(+(x4, 2), x2)), >(+(x3, 1), 0)), >(+(x2, 1), 5))
f2381_0_growList_NONNULL(x5) → f2381_0_growList_NONNULL(x6) | &&(&&(>(+(x6, 1), 0), <=(+(x6, 2), x5)), >(+(x5, 1), 2))
f2381_0_growList_NONNULL(x7) → f3535_0_growList_InvokeMethod(x8, x9) | &&(&&(&&(&&(>(+(x9, 1), 0), <=(+(x9, 1), x7)), >(+(x8, 1), 8)), <=(-(x8, 7), x7)), >(+(x7, 1), 1))
f2381_0_growList_NONNULL(x10) → f3535_0_growList_InvokeMethod(x11, x12) | &&(&&(&&(>(+(x12, 1), 0), <=(+(x12, 1), x10)), >(+(x11, 1), 5)), >(+(x10, 1), 1))

(9) YES

(10) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: GrowTreeR.Tree.createTree(I)LGrowTreeR/Tree;
SCC calls the following helper methods: GrowTreeR.Tree.createTree(I)LGrowTreeR/Tree;
Performed SCC analyses:

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

(11) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 101 rules for P and 163 rules for R.

P rules:
f1478_0_createTree_GT(EOS(STATIC_1478), i296, i296, i296) → f1481_0_createTree_GT(EOS(STATIC_1481), i296, i296, i296)
f1481_0_createTree_GT(EOS(STATIC_1481), i296, i296, i296) → f1484_0_createTree_Load(EOS(STATIC_1484), i296, i296) | >(i296, 0)
f1484_0_createTree_Load(EOS(STATIC_1484), i296, i296) → f1486_0_createTree_ConstantStackPush(EOS(STATIC_1486), i296, i296)
f1486_0_createTree_ConstantStackPush(EOS(STATIC_1486), i296, i296) → f1489_0_createTree_IntArithmetic(EOS(STATIC_1489), i296, i296, 1)
f1489_0_createTree_IntArithmetic(EOS(STATIC_1489), i296, i296, matching1) → f1497_0_createTree_Store(EOS(STATIC_1497), i296, -(i296, 1)) | &&(>(i296, 0), =(matching1, 1))
f1497_0_createTree_Store(EOS(STATIC_1497), i296, i304) → f1506_0_createTree_New(EOS(STATIC_1506), i296, i304)
f1506_0_createTree_New(EOS(STATIC_1506), i296, i304) → f1507_0_createTree_Duplicate(EOS(STATIC_1507), i296, i304)
f1507_0_createTree_Duplicate(EOS(STATIC_1507), i296, i304) → f1509_0_createTree_InvokeMethod(EOS(STATIC_1509), i296, i304)
f1509_0_createTree_InvokeMethod(EOS(STATIC_1509), i296, i304) → f1511_0__init__Load(EOS(STATIC_1511), i296, i304)
f1511_0__init__Load(EOS(STATIC_1511), i296, i304) → f1513_0__init__InvokeMethod(EOS(STATIC_1513), i296, i304)
f1513_0__init__InvokeMethod(EOS(STATIC_1513), i296, i304) → f1515_0__init__Load(EOS(STATIC_1515), i296, i304)
f1515_0__init__Load(EOS(STATIC_1515), i296, i304) → f1517_0__init__ConstantStackPush(EOS(STATIC_1517), i296, i304)
f1517_0__init__ConstantStackPush(EOS(STATIC_1517), i296, i304) → f1519_0__init__FieldAccess(EOS(STATIC_1519), i296, i304, NULL)
f1519_0__init__FieldAccess(EOS(STATIC_1519), i296, i304, NULL) → f1521_0__init__Return(EOS(STATIC_1521), i296, i304)
f1521_0__init__Return(EOS(STATIC_1521), i296, i304) → f1522_0_createTree_Store(EOS(STATIC_1522), i296, i304)
f1522_0_createTree_Store(EOS(STATIC_1522), i296, i304) → f1524_0_createTree_InvokeMethod(EOS(STATIC_1524), i296, i304)
f1524_0_createTree_InvokeMethod(EOS(STATIC_1524), i296, i304) → f1525_0_random_FieldAccess(EOS(STATIC_1525), i296, i304)
f1525_0_random_FieldAccess(EOS(STATIC_1525), i296, i304) → f1527_0_random_FieldAccess(EOS(STATIC_1527), i296, i304, java.lang.Object(ARRAY(i91)))
f1527_0_random_FieldAccess(EOS(STATIC_1527), i296, i304, java.lang.Object(ARRAY(i91))) → f1530_0_random_ArrayAccess(EOS(STATIC_1530), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1530_0_random_ArrayAccess(EOS(STATIC_1530), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1532_0_random_ArrayAccess(EOS(STATIC_1532), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1532_0_random_ArrayAccess(EOS(STATIC_1532), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1535_0_random_Store(EOS(STATIC_1535), i296, i304, o269) | <(i291, i91)
f1535_0_random_Store(EOS(STATIC_1535), i296, i304, o269) → f1538_0_random_FieldAccess(EOS(STATIC_1538), i296, i304, o269)
f1538_0_random_FieldAccess(EOS(STATIC_1538), i296, i304, o269) → f1540_0_random_ConstantStackPush(EOS(STATIC_1540), i296, i304, o269, i291)
f1540_0_random_ConstantStackPush(EOS(STATIC_1540), i296, i304, o269, i291) → f1544_0_random_IntArithmetic(EOS(STATIC_1544), i296, i304, o269, i291, 1)
f1544_0_random_IntArithmetic(EOS(STATIC_1544), i296, i304, o269, i291, matching1) → f1547_0_random_FieldAccess(EOS(STATIC_1547), i296, i304, o269, +(i291, 1)) | &&(>(i291, 0), =(matching1, 1))
f1547_0_random_FieldAccess(EOS(STATIC_1547), i296, i304, o269, i306) → f1549_0_random_Load(EOS(STATIC_1549), i296, i304, o269)
f1549_0_random_Load(EOS(STATIC_1549), i296, i304, o269) → f1553_0_random_InvokeMethod(EOS(STATIC_1553), i296, i304, o269)
f1553_0_random_InvokeMethod(EOS(STATIC_1553), i296, i304, java.lang.Object(o273sub)) → f1555_0_random_InvokeMethod(EOS(STATIC_1555), i296, i304, java.lang.Object(o273sub))
f1555_0_random_InvokeMethod(EOS(STATIC_1555), i296, i304, java.lang.Object(o273sub)) → f1557_0_length_Load(EOS(STATIC_1557), i296, i304, java.lang.Object(o273sub), java.lang.Object(o273sub))
f1557_0_length_Load(EOS(STATIC_1557), i296, i304, java.lang.Object(o273sub), java.lang.Object(o273sub)) → f1566_0_length_FieldAccess(EOS(STATIC_1566), i296, i304, java.lang.Object(o273sub), java.lang.Object(o273sub))
f1566_0_length_FieldAccess(EOS(STATIC_1566), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), java.lang.Object(java.lang.String(o277sub, i315))) → f1567_0_length_FieldAccess(EOS(STATIC_1567), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), java.lang.Object(java.lang.String(o277sub, i315))) | >=(i315, 0)
f1567_0_length_FieldAccess(EOS(STATIC_1567), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), java.lang.Object(java.lang.String(o277sub, i315))) → f1573_0_length_Return(EOS(STATIC_1573), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), i315)
f1573_0_length_Return(EOS(STATIC_1573), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), i315) → f1578_0_random_Return(EOS(STATIC_1578), i296, i304, i315)
f1578_0_random_Return(EOS(STATIC_1578), i296, i304, i315) → f1580_0_createTree_Store(EOS(STATIC_1580), i296, i304, i315)
f1580_0_createTree_Store(EOS(STATIC_1580), i296, i304, i315) → f1587_0_createTree_ConstantStackPush(EOS(STATIC_1587), i296, i304, i315)
f1587_0_createTree_ConstantStackPush(EOS(STATIC_1587), i296, i304, i315) → f1594_0_createTree_Store(EOS(STATIC_1594), i296, i304, i315, 0)
f1594_0_createTree_Store(EOS(STATIC_1594), i296, i304, i315, matching1) → f1598_0_createTree_Load(EOS(STATIC_1598), i296, i304, i315, 0) | =(matching1, 0)
f1598_0_createTree_Load(EOS(STATIC_1598), i296, i304, i315, matching1) → f2229_0_createTree_Load(EOS(STATIC_2229), i296, i304, i315, 0) | =(matching1, 0)
f2229_0_createTree_Load(EOS(STATIC_2229), i296, i304, i654, i655) → f3015_0_createTree_Load(EOS(STATIC_3015), i296, i304, i654, i655)
f3015_0_createTree_Load(EOS(STATIC_3015), i296, i304, i654, i1010) → f4421_0_createTree_Load(EOS(STATIC_4421), i296, i304, i654, i1010)
f4421_0_createTree_Load(EOS(STATIC_4421), i296, i304, i654, i1731) → f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i1731)
f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i1944) → f4747_0_createTree_Load(EOS(STATIC_4747), i296, i304, i654, i1944, i1944)
f4747_0_createTree_Load(EOS(STATIC_4747), i296, i304, i654, i1944, i1944) → f4749_0_createTree_GE(EOS(STATIC_4749), i296, i304, i654, i1944, i1944, i654)
f4749_0_createTree_GE(EOS(STATIC_4749), i296, i304, i654, i1944, i1944, i654) → f4752_0_createTree_GE(EOS(STATIC_4752), i296, i304, i654, i1944, i1944, i654)
f4752_0_createTree_GE(EOS(STATIC_4752), i296, i304, i654, i1944, i1944, i654) → f4755_0_createTree_Load(EOS(STATIC_4755), i296, i304, i654, i1944) | <(i1944, i654)
f4755_0_createTree_Load(EOS(STATIC_4755), i296, i304, i654, i1944) → f4757_0_createTree_Load(EOS(STATIC_4757), i296, i304, i654, i1944)
f4757_0_createTree_Load(EOS(STATIC_4757), i296, i304, i654, i1944) → f4760_0_createTree_ConstantStackPush(EOS(STATIC_4760), i296, i304, i654, i1944, i304)
f4760_0_createTree_ConstantStackPush(EOS(STATIC_4760), i296, i304, i654, i1944, i304) → f4770_0_createTree_IntArithmetic(EOS(STATIC_4770), i296, i304, i654, i1944, i304, 1)
f4770_0_createTree_IntArithmetic(EOS(STATIC_4770), i296, i304, i654, i1944, i304, matching1) → f4777_0_createTree_InvokeMethod(EOS(STATIC_4777), i296, i304, i654, i1944, -(i304, 1)) | &&(>=(i304, 0), =(matching1, 1))
f4777_0_createTree_InvokeMethod(EOS(STATIC_4777), i296, i304, i654, i1944, i1960) → f4778_1_createTree_InvokeMethod(f4778_0_createTree_Load(EOS(STATIC_4778), i1960, i1960), i296, i304, i654, i1944, i1960)
f4778_0_createTree_Load(EOS(STATIC_4778), i1960, i1960) → f4780_0_createTree_Load(EOS(STATIC_4780), i1960, i1960)
f4780_0_createTree_Load(EOS(STATIC_4780), i1960, i1960) → f1475_0_createTree_Load(EOS(STATIC_1475), i1960, i1960)
f1475_0_createTree_Load(EOS(STATIC_1475), i292, i292) → f1478_0_createTree_GT(EOS(STATIC_1478), i292, i292, i292)
f4827_0_createTree_Return(EOS(STATIC_4827), i296, i304, i654, i1944, i1972, i1972) → f4844_0_createTree_InvokeMethod(EOS(STATIC_4844), i296, i304, i654, i1944)
f4844_0_createTree_InvokeMethod(EOS(STATIC_4844), i296, i304, i654, i1944) → f4850_0_addChild_Load(EOS(STATIC_4850), i296, i304, i654, i1944)
f4850_0_addChild_Load(EOS(STATIC_4850), i296, i304, i654, i1944) → f4887_0_addChild_New(EOS(STATIC_4887), i296, i304, i654, i1944)
f4887_0_addChild_New(EOS(STATIC_4887), i296, i304, i654, i1944) → f4892_0_addChild_Duplicate(EOS(STATIC_4892), i296, i304, i654, i1944)
f4892_0_addChild_Duplicate(EOS(STATIC_4892), i296, i304, i654, i1944) → f4901_0_addChild_Load(EOS(STATIC_4901), i296, i304, i654, i1944)
f4901_0_addChild_Load(EOS(STATIC_4901), i296, i304, i654, i1944) → f4906_0_addChild_Load(EOS(STATIC_4906), i296, i304, i654, i1944)
f4906_0_addChild_Load(EOS(STATIC_4906), i296, i304, i654, i1944) → f4943_0_addChild_FieldAccess(EOS(STATIC_4943), i296, i304, i654, i1944)
f4943_0_addChild_FieldAccess(EOS(STATIC_4943), i296, i304, i654, i1944) → f4963_0_addChild_InvokeMethod(EOS(STATIC_4963), i296, i304, i654, i1944)
f4963_0_addChild_InvokeMethod(EOS(STATIC_4963), i296, i304, i654, i1944) → f4968_0__init__Load(EOS(STATIC_4968), i296, i304, i654, i1944)
f4968_0__init__Load(EOS(STATIC_4968), i296, i304, i654, i1944) → f4973_0__init__InvokeMethod(EOS(STATIC_4973), i296, i304, i654, i1944)
f4973_0__init__InvokeMethod(EOS(STATIC_4973), i296, i304, i654, i1944) → f4979_0__init__Load(EOS(STATIC_4979), i296, i304, i654, i1944)
f4979_0__init__Load(EOS(STATIC_4979), i296, i304, i654, i1944) → f4985_0__init__Load(EOS(STATIC_4985), i296, i304, i654, i1944)
f4985_0__init__Load(EOS(STATIC_4985), i296, i304, i654, i1944) → f4991_0__init__FieldAccess(EOS(STATIC_4991), i296, i304, i654, i1944)
f4991_0__init__FieldAccess(EOS(STATIC_4991), i296, i304, i654, i1944) → f4997_0__init__Load(EOS(STATIC_4997), i296, i304, i654, i1944)
f4997_0__init__Load(EOS(STATIC_4997), i296, i304, i654, i1944) → f5006_0__init__Load(EOS(STATIC_5006), i296, i304, i654, i1944)
f5006_0__init__Load(EOS(STATIC_5006), i296, i304, i654, i1944) → f5012_0__init__FieldAccess(EOS(STATIC_5012), i296, i304, i654, i1944)
f5012_0__init__FieldAccess(EOS(STATIC_5012), i296, i304, i654, i1944) → f5021_0__init__Return(EOS(STATIC_5021), i296, i304, i654, i1944)
f5021_0__init__Return(EOS(STATIC_5021), i296, i304, i654, i1944) → f5030_0_addChild_FieldAccess(EOS(STATIC_5030), i296, i304, i654, i1944)
f5030_0_addChild_FieldAccess(EOS(STATIC_5030), i296, i304, i654, i1944) → f5038_0_addChild_Return(EOS(STATIC_5038), i296, i304, i654, i1944)
f5038_0_addChild_Return(EOS(STATIC_5038), i296, i304, i654, i1944) → f5046_0_createTree_Inc(EOS(STATIC_5046), i296, i304, i654, i1944)
f5046_0_createTree_Inc(EOS(STATIC_5046), i296, i304, i654, i1944) → f5052_0_createTree_JMP(EOS(STATIC_5052), i296, i304, i654, +(i1944, 1)) | >=(i1944, 0)
f5052_0_createTree_JMP(EOS(STATIC_5052), i296, i304, i654, i2114) → f5065_0_createTree_Load(EOS(STATIC_5065), i296, i304, i654, i2114)
f5065_0_createTree_Load(EOS(STATIC_5065), i296, i304, i654, i2114) → f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i2114)
f4842_0_createTree_Return(EOS(STATIC_4842), i296, i304, i654, i1944, i1997) → f4849_0_createTree_InvokeMethod(EOS(STATIC_4849), i296, i304, i654, i1944)
f4849_0_createTree_InvokeMethod(EOS(STATIC_4849), i296, i304, i654, i1944) → f4853_0_addChild_Load(EOS(STATIC_4853), i296, i304, i654, i1944)
f4853_0_addChild_Load(EOS(STATIC_4853), i296, i304, i654, i1944) → f4890_0_addChild_New(EOS(STATIC_4890), i296, i304, i654, i1944)
f4890_0_addChild_New(EOS(STATIC_4890), i296, i304, i654, i1944) → f4899_0_addChild_Duplicate(EOS(STATIC_4899), i296, i304, i654, i1944)
f4899_0_addChild_Duplicate(EOS(STATIC_4899), i296, i304, i654, i1944) → f4905_0_addChild_Load(EOS(STATIC_4905), i296, i304, i654, i1944)
f4905_0_addChild_Load(EOS(STATIC_4905), i296, i304, i654, i1944) → f4941_0_addChild_Load(EOS(STATIC_4941), i296, i304, i654, i1944)
f4941_0_addChild_Load(EOS(STATIC_4941), i296, i304, i654, i1944) → f4961_0_addChild_FieldAccess(EOS(STATIC_4961), i296, i304, i654, i1944)
f4961_0_addChild_FieldAccess(EOS(STATIC_4961), i296, i304, i654, i1944) → f4966_0_addChild_InvokeMethod(EOS(STATIC_4966), i296, i304, i654, i1944)
f4966_0_addChild_InvokeMethod(EOS(STATIC_4966), i296, i304, i654, i1944) → f4970_0__init__Load(EOS(STATIC_4970), i296, i304, i654, i1944)
f4970_0__init__Load(EOS(STATIC_4970), i296, i304, i654, i1944) → f4977_0__init__InvokeMethod(EOS(STATIC_4977), i296, i304, i654, i1944)
f4977_0__init__InvokeMethod(EOS(STATIC_4977), i296, i304, i654, i1944) → f4983_0__init__Load(EOS(STATIC_4983), i296, i304, i654, i1944)
f4983_0__init__Load(EOS(STATIC_4983), i296, i304, i654, i1944) → f4988_0__init__Load(EOS(STATIC_4988), i296, i304, i654, i1944)
f4988_0__init__Load(EOS(STATIC_4988), i296, i304, i654, i1944) → f4995_0__init__FieldAccess(EOS(STATIC_4995), i296, i304, i654, i1944)
f4995_0__init__FieldAccess(EOS(STATIC_4995), i296, i304, i654, i1944) → f5004_0__init__Load(EOS(STATIC_5004), i296, i304, i654, i1944)
f5004_0__init__Load(EOS(STATIC_5004), i296, i304, i654, i1944) → f5010_0__init__Load(EOS(STATIC_5010), i296, i304, i654, i1944)
f5010_0__init__Load(EOS(STATIC_5010), i296, i304, i654, i1944) → f5016_0__init__FieldAccess(EOS(STATIC_5016), i296, i304, i654, i1944)
f5016_0__init__FieldAccess(EOS(STATIC_5016), i296, i304, i654, i1944) → f5028_0__init__Return(EOS(STATIC_5028), i296, i304, i654, i1944)
f5028_0__init__Return(EOS(STATIC_5028), i296, i304, i654, i1944) → f5034_0_addChild_FieldAccess(EOS(STATIC_5034), i296, i304, i654, i1944)
f5034_0_addChild_FieldAccess(EOS(STATIC_5034), i296, i304, i654, i1944) → f5044_0_addChild_Return(EOS(STATIC_5044), i296, i304, i654, i1944)
f5044_0_addChild_Return(EOS(STATIC_5044), i296, i304, i654, i1944) → f5050_0_createTree_Inc(EOS(STATIC_5050), i296, i304, i654, i1944)
f5050_0_createTree_Inc(EOS(STATIC_5050), i296, i304, i654, i1944) → f5057_0_createTree_JMP(EOS(STATIC_5057), i296, i304, i654, +(i1944, 1)) | >=(i1944, 0)
f5057_0_createTree_JMP(EOS(STATIC_5057), i296, i304, i654, i2115) → f5074_0_createTree_Load(EOS(STATIC_5074), i296, i304, i654, i2115)
f5074_0_createTree_Load(EOS(STATIC_5074), i296, i304, i654, i2115) → f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i2115)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(EOS(STATIC_1485), i1972, i1972), i296, i304, i654, i1944, i1972) → f4827_0_createTree_Return(EOS(STATIC_4827), i296, i304, i654, i1944, i1972, i1972)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(EOS(STATIC_4756), i1997), i296, i304, i654, i1944, i1997) → f4842_0_createTree_Return(EOS(STATIC_4842), i296, i304, i654, i1944, i1997)
R rules:
f1475_0_createTree_Load(EOS(STATIC_1475), i292, i292) → f1478_0_createTree_GT(EOS(STATIC_1478), i292, i292, i292)
f1478_0_createTree_GT(EOS(STATIC_1478), i295, i295, i295) → f1480_0_createTree_GT(EOS(STATIC_1480), i295, i295, i295)
f1478_0_createTree_GT(EOS(STATIC_1478), i296, i296, i296) → f1481_0_createTree_GT(EOS(STATIC_1481), i296, i296, i296)
f1480_0_createTree_GT(EOS(STATIC_1480), i295, i295, i295) → f1483_0_createTree_ConstantStackPush(EOS(STATIC_1483), i295, i295) | <=(i295, 0)
f1481_0_createTree_GT(EOS(STATIC_1481), i296, i296, i296) → f1484_0_createTree_Load(EOS(STATIC_1484), i296, i296) | >(i296, 0)
f1483_0_createTree_ConstantStackPush(EOS(STATIC_1483), i295, i295) → f1485_0_createTree_Return(EOS(STATIC_1485), i295, i295)
f1484_0_createTree_Load(EOS(STATIC_1484), i296, i296) → f1486_0_createTree_ConstantStackPush(EOS(STATIC_1486), i296, i296)
f1486_0_createTree_ConstantStackPush(EOS(STATIC_1486), i296, i296) → f1489_0_createTree_IntArithmetic(EOS(STATIC_1489), i296, i296, 1)
f1489_0_createTree_IntArithmetic(EOS(STATIC_1489), i296, i296, matching1) → f1497_0_createTree_Store(EOS(STATIC_1497), i296, -(i296, 1)) | &&(>(i296, 0), =(matching1, 1))
f1497_0_createTree_Store(EOS(STATIC_1497), i296, i304) → f1506_0_createTree_New(EOS(STATIC_1506), i296, i304)
f1506_0_createTree_New(EOS(STATIC_1506), i296, i304) → f1507_0_createTree_Duplicate(EOS(STATIC_1507), i296, i304)
f1507_0_createTree_Duplicate(EOS(STATIC_1507), i296, i304) → f1509_0_createTree_InvokeMethod(EOS(STATIC_1509), i296, i304)
f1509_0_createTree_InvokeMethod(EOS(STATIC_1509), i296, i304) → f1511_0__init__Load(EOS(STATIC_1511), i296, i304)
f1511_0__init__Load(EOS(STATIC_1511), i296, i304) → f1513_0__init__InvokeMethod(EOS(STATIC_1513), i296, i304)
f1513_0__init__InvokeMethod(EOS(STATIC_1513), i296, i304) → f1515_0__init__Load(EOS(STATIC_1515), i296, i304)
f1515_0__init__Load(EOS(STATIC_1515), i296, i304) → f1517_0__init__ConstantStackPush(EOS(STATIC_1517), i296, i304)
f1517_0__init__ConstantStackPush(EOS(STATIC_1517), i296, i304) → f1519_0__init__FieldAccess(EOS(STATIC_1519), i296, i304, NULL)
f1519_0__init__FieldAccess(EOS(STATIC_1519), i296, i304, NULL) → f1521_0__init__Return(EOS(STATIC_1521), i296, i304)
f1521_0__init__Return(EOS(STATIC_1521), i296, i304) → f1522_0_createTree_Store(EOS(STATIC_1522), i296, i304)
f1522_0_createTree_Store(EOS(STATIC_1522), i296, i304) → f1524_0_createTree_InvokeMethod(EOS(STATIC_1524), i296, i304)
f1524_0_createTree_InvokeMethod(EOS(STATIC_1524), i296, i304) → f1525_0_random_FieldAccess(EOS(STATIC_1525), i296, i304)
f1525_0_random_FieldAccess(EOS(STATIC_1525), i296, i304) → f1527_0_random_FieldAccess(EOS(STATIC_1527), i296, i304, java.lang.Object(ARRAY(i91)))
f1527_0_random_FieldAccess(EOS(STATIC_1527), i296, i304, java.lang.Object(ARRAY(i91))) → f1530_0_random_ArrayAccess(EOS(STATIC_1530), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1530_0_random_ArrayAccess(EOS(STATIC_1530), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1532_0_random_ArrayAccess(EOS(STATIC_1532), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1530_0_random_ArrayAccess(EOS(STATIC_1530), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1533_0_random_ArrayAccess(EOS(STATIC_1533), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1532_0_random_ArrayAccess(EOS(STATIC_1532), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1535_0_random_Store(EOS(STATIC_1535), i296, i304, o269) | <(i291, i91)
f1533_0_random_ArrayAccess(EOS(STATIC_1533), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1536_0__init__Load(EOS(STATIC_1536), i296, i304, java.lang.Object(ARRAY(i91)), i291) | >=(i291, i91)
f1535_0_random_Store(EOS(STATIC_1535), i296, i304, o269) → f1538_0_random_FieldAccess(EOS(STATIC_1538), i296, i304, o269)
f1536_0__init__Load(EOS(STATIC_1536), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1542_0__init__InvokeMethod(EOS(STATIC_1542), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1538_0_random_FieldAccess(EOS(STATIC_1538), i296, i304, o269) → f1540_0_random_ConstantStackPush(EOS(STATIC_1540), i296, i304, o269, i291)
f1540_0_random_ConstantStackPush(EOS(STATIC_1540), i296, i304, o269, i291) → f1544_0_random_IntArithmetic(EOS(STATIC_1544), i296, i304, o269, i291, 1)
f1542_0__init__InvokeMethod(EOS(STATIC_1542), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1546_0__init__Load(EOS(STATIC_1546), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1544_0_random_IntArithmetic(EOS(STATIC_1544), i296, i304, o269, i291, matching1) → f1547_0_random_FieldAccess(EOS(STATIC_1547), i296, i304, o269, +(i291, 1)) | &&(>(i291, 0), =(matching1, 1))
f1546_0__init__Load(EOS(STATIC_1546), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1551_0__init__InvokeMethod(EOS(STATIC_1551), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1547_0_random_FieldAccess(EOS(STATIC_1547), i296, i304, o269, i306) → f1549_0_random_Load(EOS(STATIC_1549), i296, i304, o269)
f1549_0_random_Load(EOS(STATIC_1549), i296, i304, o269) → f1553_0_random_InvokeMethod(EOS(STATIC_1553), i296, i304, o269)
f1551_0__init__InvokeMethod(EOS(STATIC_1551), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1554_0__init__Load(EOS(STATIC_1554), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1553_0_random_InvokeMethod(EOS(STATIC_1553), i296, i304, java.lang.Object(o273sub)) → f1555_0_random_InvokeMethod(EOS(STATIC_1555), i296, i304, java.lang.Object(o273sub))
f1553_0_random_InvokeMethod(EOS(STATIC_1553), i296, i304, NULL) → f1556_0_random_InvokeMethod(EOS(STATIC_1556), i296, i304, NULL)
f1554_0__init__Load(EOS(STATIC_1554), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1561_0__init__InvokeMethod(EOS(STATIC_1561), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1555_0_random_InvokeMethod(EOS(STATIC_1555), i296, i304, java.lang.Object(o273sub)) → f1557_0_length_Load(EOS(STATIC_1557), i296, i304, java.lang.Object(o273sub), java.lang.Object(o273sub))
f1556_0_random_InvokeMethod(EOS(STATIC_1556), i296, i304, NULL) → f1559_0_random_InvokeMethod(EOS(STATIC_1559), i296, i304, NULL)
f1557_0_length_Load(EOS(STATIC_1557), i296, i304, java.lang.Object(o273sub), java.lang.Object(o273sub)) → f1566_0_length_FieldAccess(EOS(STATIC_1566), i296, i304, java.lang.Object(o273sub), java.lang.Object(o273sub))
f1559_0_random_InvokeMethod(EOS(STATIC_1559), i296, i304, NULL) → f1563_0__init__Load(EOS(STATIC_1563), i296, i304, NULL)
f1561_0__init__InvokeMethod(EOS(STATIC_1561), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1565_0__init__Load(EOS(STATIC_1565), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1563_0__init__Load(EOS(STATIC_1563), i296, i304, NULL) → f1568_0__init__InvokeMethod(EOS(STATIC_1568), i296, i304, NULL)
f1565_0__init__Load(EOS(STATIC_1565), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1570_0__init__InvokeMethod(EOS(STATIC_1570), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1566_0_length_FieldAccess(EOS(STATIC_1566), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), java.lang.Object(java.lang.String(o277sub, i315))) → f1567_0_length_FieldAccess(EOS(STATIC_1567), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), java.lang.Object(java.lang.String(o277sub, i315))) | >=(i315, 0)
f1567_0_length_FieldAccess(EOS(STATIC_1567), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), java.lang.Object(java.lang.String(o277sub, i315))) → f1573_0_length_Return(EOS(STATIC_1573), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), i315)
f1568_0__init__InvokeMethod(EOS(STATIC_1568), i296, i304, NULL) → f1574_0__init__Load(EOS(STATIC_1574), i296, i304, NULL)
f1570_0__init__InvokeMethod(EOS(STATIC_1570), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1576_0__init__Load(EOS(STATIC_1576), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1573_0_length_Return(EOS(STATIC_1573), i296, i304, java.lang.Object(java.lang.String(o277sub, i315)), i315) → f1578_0_random_Return(EOS(STATIC_1578), i296, i304, i315)
f1574_0__init__Load(EOS(STATIC_1574), i296, i304, NULL) → f1583_0__init__InvokeMethod(EOS(STATIC_1583), i296, i304, NULL)
f1576_0__init__Load(EOS(STATIC_1576), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1586_0__init__InvokeMethod(EOS(STATIC_1586), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1578_0_random_Return(EOS(STATIC_1578), i296, i304, i315) → f1580_0_createTree_Store(EOS(STATIC_1580), i296, i304, i315)
f1580_0_createTree_Store(EOS(STATIC_1580), i296, i304, i315) → f1587_0_createTree_ConstantStackPush(EOS(STATIC_1587), i296, i304, i315)
f1583_0__init__InvokeMethod(EOS(STATIC_1583), i296, i304, NULL) → f1590_0__init__Load(EOS(STATIC_1590), i296, i304, NULL)
f1586_0__init__InvokeMethod(EOS(STATIC_1586), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1592_0__init__Load(EOS(STATIC_1592), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1587_0_createTree_ConstantStackPush(EOS(STATIC_1587), i296, i304, i315) → f1594_0_createTree_Store(EOS(STATIC_1594), i296, i304, i315, 0)
f1590_0__init__Load(EOS(STATIC_1590), i296, i304, NULL) → f1601_0__init__InvokeMethod(EOS(STATIC_1601), i296, i304, NULL)
f1592_0__init__Load(EOS(STATIC_1592), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1597_0__init__Load(EOS(STATIC_1597), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1594_0_createTree_Store(EOS(STATIC_1594), i296, i304, i315, matching1) → f1598_0_createTree_Load(EOS(STATIC_1598), i296, i304, i315, 0) | =(matching1, 0)
f1597_0__init__Load(EOS(STATIC_1597), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1603_0__init__FieldAccess(EOS(STATIC_1603), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1598_0_createTree_Load(EOS(STATIC_1598), i296, i304, i315, matching1) → f2229_0_createTree_Load(EOS(STATIC_2229), i296, i304, i315, 0) | =(matching1, 0)
f1601_0__init__InvokeMethod(EOS(STATIC_1601), i296, i304, NULL) → f1607_0__init__Load(EOS(STATIC_1607), i296, i304, NULL)
f1603_0__init__FieldAccess(EOS(STATIC_1603), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1615_0__init__Load(EOS(STATIC_1615), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1607_0__init__Load(EOS(STATIC_1607), i296, i304, NULL) → f1623_0__init__InvokeMethod(EOS(STATIC_1623), i296, i304, NULL)
f1615_0__init__Load(EOS(STATIC_1615), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1620_0__init__InvokeMethod(EOS(STATIC_1620), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1620_0__init__InvokeMethod(EOS(STATIC_1620), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1626_0__init__StackPop(EOS(STATIC_1626), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1623_0__init__InvokeMethod(EOS(STATIC_1623), i296, i304, NULL) → f1631_0__init__Load(EOS(STATIC_1631), i296, i304, NULL)
f1626_0__init__StackPop(EOS(STATIC_1626), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1632_0__init__Return(EOS(STATIC_1632), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1631_0__init__Load(EOS(STATIC_1631), i296, i304, NULL) → f1637_0__init__Load(EOS(STATIC_1637), i296, i304, NULL)
f1632_0__init__Return(EOS(STATIC_1632), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1638_0__init__Return(EOS(STATIC_1638), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1637_0__init__Load(EOS(STATIC_1637), i296, i304, NULL) → f1643_0__init__FieldAccess(EOS(STATIC_1643), i296, i304, NULL)
f1638_0__init__Return(EOS(STATIC_1638), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1645_0__init__Return(EOS(STATIC_1645), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1643_0__init__FieldAccess(EOS(STATIC_1643), i296, i304, NULL) → f1674_0__init__Load(EOS(STATIC_1674), i296, i304, NULL)
f1645_0__init__Return(EOS(STATIC_1645), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1677_0__init__Return(EOS(STATIC_1677), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1674_0__init__Load(EOS(STATIC_1674), i296, i304, NULL) → f1683_0__init__InvokeMethod(EOS(STATIC_1683), i296, i304, NULL)
f1677_0__init__Return(EOS(STATIC_1677), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1685_0__init__Return(EOS(STATIC_1685), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1683_0__init__InvokeMethod(EOS(STATIC_1683), i296, i304, NULL) → f1691_0__init__StackPop(EOS(STATIC_1691), i296, i304, NULL)
f1685_0__init__Return(EOS(STATIC_1685), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1694_0_random_ArrayAccess(EOS(STATIC_1694), i296, i304, java.lang.Object(ARRAY(i91)), i291)
f1691_0__init__StackPop(EOS(STATIC_1691), i296, i304, NULL) → f1699_0__init__Return(EOS(STATIC_1699), i296, i304, NULL)
f1694_0_random_ArrayAccess(EOS(STATIC_1694), i296, i304, java.lang.Object(ARRAY(i91)), i291) → f1702_0_createTree_InvokeMethod(EOS(STATIC_1702), i296, i304)
f1699_0__init__Return(EOS(STATIC_1699), i296, i304, NULL) → f1704_0__init__Return(EOS(STATIC_1704), i296, i304, NULL)
f1704_0__init__Return(EOS(STATIC_1704), i296, i304, NULL) → f1757_0__init__Return(EOS(STATIC_1757), i296, i304, NULL)
f1757_0__init__Return(EOS(STATIC_1757), i296, i304, NULL) → f1793_0__init__Return(EOS(STATIC_1793), i296, i304, NULL)
f1793_0__init__Return(EOS(STATIC_1793), i296, i304, NULL) → f1801_0_random_InvokeMethod(EOS(STATIC_1801), i296, i304, NULL)
f1801_0_random_InvokeMethod(EOS(STATIC_1801), i296, i304, NULL) → f1808_0_createTree_InvokeMethod(EOS(STATIC_1808), i296, i304)
f2229_0_createTree_Load(EOS(STATIC_2229), i296, i304, i654, i655) → f3015_0_createTree_Load(EOS(STATIC_3015), i296, i304, i654, i655)
f3015_0_createTree_Load(EOS(STATIC_3015), i296, i304, i654, i1010) → f4421_0_createTree_Load(EOS(STATIC_4421), i296, i304, i654, i1010)
f4421_0_createTree_Load(EOS(STATIC_4421), i296, i304, i654, i1731) → f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i1731)
f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i1944) → f4747_0_createTree_Load(EOS(STATIC_4747), i296, i304, i654, i1944, i1944)
f4747_0_createTree_Load(EOS(STATIC_4747), i296, i304, i654, i1944, i1944) → f4749_0_createTree_GE(EOS(STATIC_4749), i296, i304, i654, i1944, i1944, i654)
f4749_0_createTree_GE(EOS(STATIC_4749), i296, i304, i654, i1944, i1944, i654) → f4751_0_createTree_GE(EOS(STATIC_4751), i296, i304, i654, i1944, i1944, i654)
f4749_0_createTree_GE(EOS(STATIC_4749), i296, i304, i654, i1944, i1944, i654) → f4752_0_createTree_GE(EOS(STATIC_4752), i296, i304, i654, i1944, i1944, i654)
f4751_0_createTree_GE(EOS(STATIC_4751), i296, i304, i654, i1944, i1944, i654) → f4753_0_createTree_Load(EOS(STATIC_4753), i296) | >=(i1944, i654)
f4752_0_createTree_GE(EOS(STATIC_4752), i296, i304, i654, i1944, i1944, i654) → f4755_0_createTree_Load(EOS(STATIC_4755), i296, i304, i654, i1944) | <(i1944, i654)
f4753_0_createTree_Load(EOS(STATIC_4753), i296) → f4756_0_createTree_Return(EOS(STATIC_4756), i296)
f4755_0_createTree_Load(EOS(STATIC_4755), i296, i304, i654, i1944) → f4757_0_createTree_Load(EOS(STATIC_4757), i296, i304, i654, i1944)
f4757_0_createTree_Load(EOS(STATIC_4757), i296, i304, i654, i1944) → f4760_0_createTree_ConstantStackPush(EOS(STATIC_4760), i296, i304, i654, i1944, i304)
f4760_0_createTree_ConstantStackPush(EOS(STATIC_4760), i296, i304, i654, i1944, i304) → f4770_0_createTree_IntArithmetic(EOS(STATIC_4770), i296, i304, i654, i1944, i304, 1)
f4770_0_createTree_IntArithmetic(EOS(STATIC_4770), i296, i304, i654, i1944, i304, matching1) → f4777_0_createTree_InvokeMethod(EOS(STATIC_4777), i296, i304, i654, i1944, -(i304, 1)) | &&(>=(i304, 0), =(matching1, 1))
f4777_0_createTree_InvokeMethod(EOS(STATIC_4777), i296, i304, i654, i1944, i1960) → f4778_1_createTree_InvokeMethod(f4778_0_createTree_Load(EOS(STATIC_4778), i1960, i1960), i296, i304, i654, i1944, i1960)
f4778_0_createTree_Load(EOS(STATIC_4778), i1960, i1960) → f4780_0_createTree_Load(EOS(STATIC_4780), i1960, i1960)
f4827_0_createTree_Return(EOS(STATIC_4827), i296, i304, i654, i1944, i1972, i1972) → f4844_0_createTree_InvokeMethod(EOS(STATIC_4844), i296, i304, i654, i1944)
f4828_0_createTree_InvokeMethod(EOS(STATIC_4828), i296, i304, i654, i1944, i1974) → f4841_0_createTree_InvokeMethod(EOS(STATIC_4841), i296, i304, i654, i1944, i1974)
f4840_0_createTree_InvokeMethod(EOS(STATIC_4840), i296, i304, i654, i1944, i1984) → f4841_0_createTree_InvokeMethod(EOS(STATIC_4841), i296, i304, i654, i1944, i1984)
f4841_0_createTree_InvokeMethod(EOS(STATIC_4841), i296, i304, i654, i1944, i2000) → f4846_0_createTree_InvokeMethod(EOS(STATIC_4846), i296, i304, i654, i1944)
f4842_0_createTree_Return(EOS(STATIC_4842), i296, i304, i654, i1944, i1997) → f4849_0_createTree_InvokeMethod(EOS(STATIC_4849), i296, i304, i654, i1944)
f4844_0_createTree_InvokeMethod(EOS(STATIC_4844), i296, i304, i654, i1944) → f4850_0_addChild_Load(EOS(STATIC_4850), i296, i304, i654, i1944)
f4846_0_createTree_InvokeMethod(EOS(STATIC_4846), i296, i304, i654, i1944) → f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), i296, i304, i654, i1944)
f4849_0_createTree_InvokeMethod(EOS(STATIC_4849), i296, i304, i654, i1944) → f4853_0_addChild_Load(EOS(STATIC_4853), i296, i304, i654, i1944)
f4850_0_addChild_Load(EOS(STATIC_4850), i296, i304, i654, i1944) → f4887_0_addChild_New(EOS(STATIC_4887), i296, i304, i654, i1944)
f4853_0_addChild_Load(EOS(STATIC_4853), i296, i304, i654, i1944) → f4890_0_addChild_New(EOS(STATIC_4890), i296, i304, i654, i1944)
f4887_0_addChild_New(EOS(STATIC_4887), i296, i304, i654, i1944) → f4892_0_addChild_Duplicate(EOS(STATIC_4892), i296, i304, i654, i1944)
f4888_0_createTree_InvokeMethod(EOS(STATIC_4888), i296, i304, i654, i1944, i2022, i2023, i2024) → f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), i296, i304, i654, i1944)
f4890_0_addChild_New(EOS(STATIC_4890), i296, i304, i654, i1944) → f4899_0_addChild_Duplicate(EOS(STATIC_4899), i296, i304, i654, i1944)
f4892_0_addChild_Duplicate(EOS(STATIC_4892), i296, i304, i654, i1944) → f4901_0_addChild_Load(EOS(STATIC_4901), i296, i304, i654, i1944)
f4899_0_addChild_Duplicate(EOS(STATIC_4899), i296, i304, i654, i1944) → f4905_0_addChild_Load(EOS(STATIC_4905), i296, i304, i654, i1944)
f4901_0_addChild_Load(EOS(STATIC_4901), i296, i304, i654, i1944) → f4906_0_addChild_Load(EOS(STATIC_4906), i296, i304, i654, i1944)
f4905_0_addChild_Load(EOS(STATIC_4905), i296, i304, i654, i1944) → f4941_0_addChild_Load(EOS(STATIC_4941), i296, i304, i654, i1944)
f4906_0_addChild_Load(EOS(STATIC_4906), i296, i304, i654, i1944) → f4943_0_addChild_FieldAccess(EOS(STATIC_4943), i296, i304, i654, i1944)
f4941_0_addChild_Load(EOS(STATIC_4941), i296, i304, i654, i1944) → f4961_0_addChild_FieldAccess(EOS(STATIC_4961), i296, i304, i654, i1944)
f4943_0_addChild_FieldAccess(EOS(STATIC_4943), i296, i304, i654, i1944) → f4963_0_addChild_InvokeMethod(EOS(STATIC_4963), i296, i304, i654, i1944)
f4957_0_createTree_InvokeMethod(EOS(STATIC_4957), i296, i304, i654, i1944, i2060, i2061, i2062) → f4888_0_createTree_InvokeMethod(EOS(STATIC_4888), i296, i304, i654, i1944, i2060, i2061, i2062)
f4961_0_addChild_FieldAccess(EOS(STATIC_4961), i296, i304, i654, i1944) → f4966_0_addChild_InvokeMethod(EOS(STATIC_4966), i296, i304, i654, i1944)
f4963_0_addChild_InvokeMethod(EOS(STATIC_4963), i296, i304, i654, i1944) → f4968_0__init__Load(EOS(STATIC_4968), i296, i304, i654, i1944)
f4966_0_addChild_InvokeMethod(EOS(STATIC_4966), i296, i304, i654, i1944) → f4970_0__init__Load(EOS(STATIC_4970), i296, i304, i654, i1944)
f4968_0__init__Load(EOS(STATIC_4968), i296, i304, i654, i1944) → f4973_0__init__InvokeMethod(EOS(STATIC_4973), i296, i304, i654, i1944)
f4970_0__init__Load(EOS(STATIC_4970), i296, i304, i654, i1944) → f4977_0__init__InvokeMethod(EOS(STATIC_4977), i296, i304, i654, i1944)
f4973_0__init__InvokeMethod(EOS(STATIC_4973), i296, i304, i654, i1944) → f4979_0__init__Load(EOS(STATIC_4979), i296, i304, i654, i1944)
f4977_0__init__InvokeMethod(EOS(STATIC_4977), i296, i304, i654, i1944) → f4983_0__init__Load(EOS(STATIC_4983), i296, i304, i654, i1944)
f4979_0__init__Load(EOS(STATIC_4979), i296, i304, i654, i1944) → f4985_0__init__Load(EOS(STATIC_4985), i296, i304, i654, i1944)
f4983_0__init__Load(EOS(STATIC_4983), i296, i304, i654, i1944) → f4988_0__init__Load(EOS(STATIC_4988), i296, i304, i654, i1944)
f4985_0__init__Load(EOS(STATIC_4985), i296, i304, i654, i1944) → f4991_0__init__FieldAccess(EOS(STATIC_4991), i296, i304, i654, i1944)
f4988_0__init__Load(EOS(STATIC_4988), i296, i304, i654, i1944) → f4995_0__init__FieldAccess(EOS(STATIC_4995), i296, i304, i654, i1944)
f4991_0__init__FieldAccess(EOS(STATIC_4991), i296, i304, i654, i1944) → f4997_0__init__Load(EOS(STATIC_4997), i296, i304, i654, i1944)
f4995_0__init__FieldAccess(EOS(STATIC_4995), i296, i304, i654, i1944) → f5004_0__init__Load(EOS(STATIC_5004), i296, i304, i654, i1944)
f4997_0__init__Load(EOS(STATIC_4997), i296, i304, i654, i1944) → f5006_0__init__Load(EOS(STATIC_5006), i296, i304, i654, i1944)
f5004_0__init__Load(EOS(STATIC_5004), i296, i304, i654, i1944) → f5010_0__init__Load(EOS(STATIC_5010), i296, i304, i654, i1944)
f5006_0__init__Load(EOS(STATIC_5006), i296, i304, i654, i1944) → f5012_0__init__FieldAccess(EOS(STATIC_5012), i296, i304, i654, i1944)
f5010_0__init__Load(EOS(STATIC_5010), i296, i304, i654, i1944) → f5016_0__init__FieldAccess(EOS(STATIC_5016), i296, i304, i654, i1944)
f5012_0__init__FieldAccess(EOS(STATIC_5012), i296, i304, i654, i1944) → f5021_0__init__Return(EOS(STATIC_5021), i296, i304, i654, i1944)
f5016_0__init__FieldAccess(EOS(STATIC_5016), i296, i304, i654, i1944) → f5028_0__init__Return(EOS(STATIC_5028), i296, i304, i654, i1944)
f5021_0__init__Return(EOS(STATIC_5021), i296, i304, i654, i1944) → f5030_0_addChild_FieldAccess(EOS(STATIC_5030), i296, i304, i654, i1944)
f5028_0__init__Return(EOS(STATIC_5028), i296, i304, i654, i1944) → f5034_0_addChild_FieldAccess(EOS(STATIC_5034), i296, i304, i654, i1944)
f5030_0_addChild_FieldAccess(EOS(STATIC_5030), i296, i304, i654, i1944) → f5038_0_addChild_Return(EOS(STATIC_5038), i296, i304, i654, i1944)
f5034_0_addChild_FieldAccess(EOS(STATIC_5034), i296, i304, i654, i1944) → f5044_0_addChild_Return(EOS(STATIC_5044), i296, i304, i654, i1944)
f5038_0_addChild_Return(EOS(STATIC_5038), i296, i304, i654, i1944) → f5046_0_createTree_Inc(EOS(STATIC_5046), i296, i304, i654, i1944)
f5044_0_addChild_Return(EOS(STATIC_5044), i296, i304, i654, i1944) → f5050_0_createTree_Inc(EOS(STATIC_5050), i296, i304, i654, i1944)
f5046_0_createTree_Inc(EOS(STATIC_5046), i296, i304, i654, i1944) → f5052_0_createTree_JMP(EOS(STATIC_5052), i296, i304, i654, +(i1944, 1)) | >=(i1944, 0)
f5050_0_createTree_Inc(EOS(STATIC_5050), i296, i304, i654, i1944) → f5057_0_createTree_JMP(EOS(STATIC_5057), i296, i304, i654, +(i1944, 1)) | >=(i1944, 0)
f5052_0_createTree_JMP(EOS(STATIC_5052), i296, i304, i654, i2114) → f5065_0_createTree_Load(EOS(STATIC_5065), i296, i304, i654, i2114)
f5057_0_createTree_JMP(EOS(STATIC_5057), i296, i304, i654, i2115) → f5074_0_createTree_Load(EOS(STATIC_5074), i296, i304, i654, i2115)
f5065_0_createTree_Load(EOS(STATIC_5065), i296, i304, i654, i2114) → f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i2114)
f5074_0_createTree_Load(EOS(STATIC_5074), i296, i304, i654, i2115) → f4744_0_createTree_Load(EOS(STATIC_4744), i296, i304, i654, i2115)
f4780_0_createTree_Load(EOS(STATIC_4780), i1960, i1960) → f1475_0_createTree_Load(EOS(STATIC_1475), i1960, i1960)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(EOS(STATIC_1485), i1972, i1972), i296, i304, i654, i1944, i1972) → f4827_0_createTree_Return(EOS(STATIC_4827), i296, i304, i654, i1944, i1972, i1972)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(EOS(STATIC_1702), i1982, i1974), i296, i304, i654, i1944, i1982) → f4828_0_createTree_InvokeMethod(EOS(STATIC_4828), i296, i304, i654, i1944, i1974)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(EOS(STATIC_1808), i1990, i1984), i296, i304, i654, i1944, i1990) → f4840_0_createTree_InvokeMethod(EOS(STATIC_4840), i296, i304, i654, i1944, i1984)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(EOS(STATIC_4756), i1997), i296, i304, i654, i1944, i1997) → f4842_0_createTree_Return(EOS(STATIC_4842), i296, i304, i654, i1944, i1997)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(EOS(STATIC_4846), i2030, i2022, i2023, i2024), i296, i304, i654, i1944, i2030) → f4888_0_createTree_InvokeMethod(EOS(STATIC_4888), i296, i304, i654, i1944, i2022, i2023, i2024)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), i2068, i2060, i2061, i2062), i296, i304, i654, i1944, i2068) → f4957_0_createTree_InvokeMethod(EOS(STATIC_4957), i296, i304, i654, i1944, i2060, i2061, i2062)

Combined rules. Obtained 3 conditional rules for P and 12 conditional rules for R.

P rules:
f1478_0_createTree_GT(EOS(STATIC_1478), x0, x0, x0) → f4778_1_createTree_InvokeMethod(f1478_0_createTree_GT(EOS(STATIC_1478), -(x0, 2), -(x0, 2), -(x0, 2)), x0, -(x0, 1), x1, 0, -(x0, 2)) | &&(>(x1, 0), >(+(x0, 1), 1))
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(EOS(STATIC_1485), x0, x0), x1, x2, x3, x4, x0) → f4778_1_createTree_InvokeMethod(f1478_0_createTree_GT(EOS(STATIC_1478), -(x2, 1), -(x2, 1), -(x2, 1)), x1, x2, x3, +(x4, 1), -(x2, 1)) | &&(&&(>(+(x4, 1), 0), >(+(x2, 1), 0)), <(+(x4, 1), x3))
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(EOS(STATIC_4756), x0), x1, x2, x3, x4, x0) → f4778_1_createTree_InvokeMethod(f1478_0_createTree_GT(EOS(STATIC_1478), -(x2, 1), -(x2, 1), -(x2, 1)), x1, x2, x3, +(x4, 1), -(x2, 1)) | &&(&&(>(+(x4, 1), 0), >(+(x2, 1), 0)), <(+(x4, 1), x3))
R rules:
f1478_0_createTree_GT(EOS(STATIC_1478), x0, x0, x0) → f1485_0_createTree_Return(EOS(STATIC_1485), x0, x0) | <=(x0, 0)
f1478_0_createTree_GT(EOS(STATIC_1478), x0, x0, x0) → f1702_0_createTree_InvokeMethod(EOS(STATIC_1702), x0, -(x0, 1)) | >(x0, 0)
f1478_0_createTree_GT(EOS(STATIC_1478), x0, x0, x0) → f1808_0_createTree_InvokeMethod(EOS(STATIC_1808), x0, -(x0, 1)) | >(x0, 0)
f1478_0_createTree_GT(EOS(STATIC_1478), x0, x0, x0) → f4749_0_createTree_GE(EOS(STATIC_4749), x0, -(x0, 1), x1, 0, 0, x1) | &&(>(+(x1, 1), 0), >(x0, 0))
f4749_0_createTree_GE(EOS(STATIC_4749), x0, x1, x2, x3, x3, x2) → f4756_0_createTree_Return(EOS(STATIC_4756), x0) | >=(x3, x2)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(EOS(STATIC_4846), x0, x1, x2, x3), x4, x5, x6, x7, x0) → f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), x4, x5, x6, x7)
f4749_0_createTree_GE(EOS(STATIC_4749), x0, x1, x2, x3, x3, x2) → f4778_1_createTree_InvokeMethod(f1478_0_createTree_GT(EOS(STATIC_1478), -(x1, 1), -(x1, 1), -(x1, 1)), x0, x1, x2, x3, -(x1, 1)) | &&(>(+(x1, 1), 0), <(x3, x2))
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(EOS(STATIC_1485), x0, x0), x1, x2, x3, x4, x0) → f4749_0_createTree_GE(EOS(STATIC_4749), x1, x2, x3, +(x4, 1), +(x4, 1), x3) | >(+(x4, 1), 0)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(EOS(STATIC_1702), x0, x1), x2, x3, x4, x5, x0) → f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(EOS(STATIC_1808), x0, x1), x2, x3, x4, x5, x0) → f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(EOS(STATIC_4756), x0), x1, x2, x3, x4, x0) → f4749_0_createTree_GE(EOS(STATIC_4749), x1, x2, x3, +(x4, 1), +(x4, 1), x3) | >(+(x4, 1), 0)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), x0, x1, x2, x3), x4, x5, x6, x7, x0) → f4896_0_createTree_InvokeMethod(EOS(STATIC_4896), x4, x5, x6, x7)

Filtered ground terms:

f1478_0_createTree_GT(x1, x2, x3, x4) → f1478_0_createTree_GT(x2, x3, x4)
Cond_f1478_0_createTree_GT(x1, x2, x3, x4, x5, x6) → Cond_f1478_0_createTree_GT(x1, x3, x4, x5, x6)
f1485_0_createTree_Return(x1, x2, x3) → f1485_0_createTree_Return(x2, x3)
f4756_0_createTree_Return(x1, x2) → f4756_0_createTree_Return(x2)
Cond_f1478_0_createTree_GT(x1, x2, x3, x4, x5) → Cond_f1478_0_createTree_GT(x1, x3, x4, x5)
Cond_f1478_0_createTree_GT1(x1, x2, x3, x4, x5) → Cond_f1478_0_createTree_GT1(x1, x3, x4, x5)
f1702_0_createTree_InvokeMethod(x1, x2, x3) → f1702_0_createTree_InvokeMethod(x2, x3)
Cond_f1478_0_createTree_GT2(x1, x2, x3, x4, x5) → Cond_f1478_0_createTree_GT2(x1, x3, x4, x5)
f1808_0_createTree_InvokeMethod(x1, x2, x3) → f1808_0_createTree_InvokeMethod(x2, x3)
Cond_f1478_0_createTree_GT3(x1, x2, x3, x4, x5, x6) → Cond_f1478_0_createTree_GT3(x1, x3, x4, x5, x6)
f4749_0_createTree_GE(x1, x2, x3, x4, x5, x6, x7) → f4749_0_createTree_GE(x2, x3, x4, x5, x6, x7)
Cond_f4749_0_createTree_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f4749_0_createTree_GE(x1, x3, x4, x5, x6, x7, x8)
f4896_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
Cond_f4749_0_createTree_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f4749_0_createTree_GE1(x1, x3, x4, x5, x6, x7, x8)
f4846_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → f4846_0_createTree_InvokeMethod(x2, x3, x4, x5)

Filtered unneeded arguments:

f4778_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → f4778_1_createTree_InvokeMethod(x1, x3, x4, x5, x6)
Cond_f4778_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_f4778_1_createTree_InvokeMethod(x1, x2, x4, x5, x6, x7)
Cond_f4778_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5, x6, x7) → Cond_f4778_1_createTree_InvokeMethod1(x1, x4, x5, x6)
f4749_0_createTree_GE(x1, x2, x3, x4, x5, x6) → f4749_0_createTree_GE(x2, x3, x4, x5, x6)
Cond_f4749_0_createTree_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_f4749_0_createTree_GE(x1, x4, x5, x6, x7)
Cond_f4749_0_createTree_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_f4749_0_createTree_GE1(x1, x3, x4, x5, x6, x7)

Filtered duplicate args:

f1478_0_createTree_GT(x1, x2, x3) → f1478_0_createTree_GT(x3)
Cond_f1478_0_createTree_GT(x1, x2, x3, x4, x5) → Cond_f1478_0_createTree_GT(x1, x4, x5)
f4778_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → f4778_1_createTree_InvokeMethod(x1, x2, x3, x4)
f1485_0_createTree_Return(x1, x2) → f1485_0_createTree_Return(x2)
Cond_f4778_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_f4778_1_createTree_InvokeMethod(x1, x2, x3, x4, x5)
Cond_f1478_0_createTree_GT(x1, x2, x3, x4) → Cond_f1478_0_createTree_GT(x1, x4)
Cond_f1478_0_createTree_GT1(x1, x2, x3, x4) → Cond_f1478_0_createTree_GT1(x1, x4)
Cond_f1478_0_createTree_GT2(x1, x2, x3, x4) → Cond_f1478_0_createTree_GT2(x1, x4)
Cond_f1478_0_createTree_GT3(x1, x2, x3, x4, x5) → Cond_f1478_0_createTree_GT3(x1, x4, x5)
f4749_0_createTree_GE(x1, x2, x3, x4, x5) → f4749_0_createTree_GE(x1, x4, x5)
Cond_f4749_0_createTree_GE(x1, x2, x3, x4, x5) → Cond_f4749_0_createTree_GE(x1, x4, x5)
Cond_f4749_0_createTree_GE1(x1, x2, x3, x4, x5, x6) → Cond_f4749_0_createTree_GE1(x1, x2, x5, x6)

Filtered unneeded arguments:

Cond_f4778_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_f4778_1_createTree_InvokeMethod(x1, x3, x4, x5)
Cond_f1478_0_createTree_GT(x1, x2) → Cond_f1478_0_createTree_GT(x1)
Cond_f1478_0_createTree_GT1(x1, x2) → Cond_f1478_0_createTree_GT1(x1)
Cond_f1478_0_createTree_GT2(x1, x2) → Cond_f1478_0_createTree_GT2(x1)
Cond_f4749_0_createTree_GE(x1, x2, x3) → Cond_f4749_0_createTree_GE(x1)

Combined rules. Obtained 6 conditional rules for P and 11 conditional rules for R.

P rules:
F1478_0_CREATETREE_GT(x0) → F4778_1_CREATETREE_INVOKEMETHOD(f1478_0_createTree_GT(-(x0, 2)), -(x0, 1), x1, 0) | &&(>(x0, 0), >(x1, 0))
F1478_0_CREATETREE_GT(x0) → F1478_0_CREATETREE_GT(-(x0, 2)) | &&(>(x0, 0), >(x1, 0))
F4778_1_CREATETREE_INVOKEMETHOD(f1485_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1)) | &&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3))
F4778_1_CREATETREE_INVOKEMETHOD(f1485_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT(-(x2, 1)) | &&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3))
F4778_1_CREATETREE_INVOKEMETHOD(f4756_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1)) | &&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3))
F4778_1_CREATETREE_INVOKEMETHOD(f4756_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT(-(x2, 1)) | &&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3))
R rules:
f4749_0_createTree_GE(x1, x3, x2) → f4756_0_createTree_Return(x0) | >=(x3, x2)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, +(x4, 1), x3) | >(x4, -1)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, +(x4, 1), x3) | >(x4, -1)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4749_0_createTree_GE(x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(-(x0, 1)), x0, x2, x1) | &&(&&(>(x2, x1), <=(x0, 1)), >(x0, -1))
f4749_0_createTree_GE(x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(-(x0, 1), -(x0, 2)), x0, x2, x1) | &&(>(x0, 1), >(x2, x1))
f4749_0_createTree_GE(x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(-(x0, 1), -(x0, 2)), x0, x2, x1) | &&(>(x0, 1), >(x2, x1))
f4749_0_createTree_GE(x0, x1, x2) → f4778_1_createTree_InvokeMethod(f4749_0_createTree_GE(-(x0, 2), 0, x3), x0, x2, x1) | &&(&&(>(x3, -1), >(x0, 1)), >(x2, x1))

Finished conversion. Obtained 12 rules for P and 18 rules for R. System has predefined symbols.

P rules:
F1478_0_CREATETREE_GT'(x0) → COND_F1478_0_CREATETREE_GT(&&(>(x0, 0), >(x1, 0)), x0, x1)
COND_F1478_0_CREATETREE_GT(TRUE, x0, x1) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0, 2)), -(x0, 1), x1, 0)
F1478_0_CREATETREE_GT'(x0) → COND_F1478_0_CREATETREE_GT1(>(x0, 0), x0)
COND_F1478_0_CREATETREE_GT1(TRUE, x0) → F1478_0_CREATETREE_GT'(-(x0, 2))
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f1485_0_createTree_Return(x0), x2, x3, x4)
COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1))
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f1485_0_createTree_Return(x0), x2, x3, x4)
COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT'(-(x2, 1))
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f4756_0_createTree_Return(x0), x2, x3, x4)
COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1))
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f4756_0_createTree_Return(x0), x2, x3, x4)
COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT'(-(x2, 1))
R rules:
f4749_0_createTree_GE(x1, x3, x2) → Cond_f4749_0_createTree_GE(>=(x3, x2), x1, x3, x2, x0)
Cond_f4749_0_createTree_GE(TRUE, x1, x3, x2, x0) → f4756_0_createTree_Return(x0)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0), x2, x3, x4) → Cond_f4778_1_createTree_InvokeMethod(>(x4, -1), f1485_0_createTree_Return(x0), x2, x3, x4)
Cond_f4778_1_createTree_InvokeMethod(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, +(x4, 1), x3)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(x0), x2, x3, x4) → Cond_f4778_1_createTree_InvokeMethod1(>(x4, -1), f4756_0_createTree_Return(x0), x2, x3, x4)
Cond_f4778_1_createTree_InvokeMethod1(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, +(x4, 1), x3)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE1(&&(&&(>(x2, x1), <=(x0, 1)), >(x0, -1)), x0, x1, x2)
Cond_f4749_0_createTree_GE1(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(-(x0, 1)), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE2(&&(>(x0, 1), >(x2, x1)), x0, x1, x2)
Cond_f4749_0_createTree_GE2(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(-(x0, 1), -(x0, 2)), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE3(&&(>(x0, 1), >(x2, x1)), x0, x1, x2)
Cond_f4749_0_createTree_GE3(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(-(x0, 1), -(x0, 2)), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE4(&&(&&(>(x3, -1), >(x0, 1)), >(x2, x1)), x0, x1, x2, x3)
Cond_f4749_0_createTree_GE4(TRUE, x0, x1, x2, x3) → f4778_1_createTree_InvokeMethod(f4749_0_createTree_GE(-(x0, 2), 0, x3), x0, x2, x1)

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
f4749_0_createTree_GE(x1, x3, x2) → Cond_f4749_0_createTree_GE(x3 >= x2, x1, x3, x2, x0)
Cond_f4749_0_createTree_GE(TRUE, x1, x3, x2, x0) → f4756_0_createTree_Return(x0)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0), x2, x3, x4) → Cond_f4778_1_createTree_InvokeMethod(x4 > -1, f1485_0_createTree_Return(x0), x2, x3, x4)
Cond_f4778_1_createTree_InvokeMethod(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, x4 + 1, x3)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(x0), x2, x3, x4) → Cond_f4778_1_createTree_InvokeMethod1(x4 > -1, f4756_0_createTree_Return(x0), x2, x3, x4)
Cond_f4778_1_createTree_InvokeMethod1(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, x4 + 1, x3)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE1(x2 > x1 && x0 <= 1 && x0 > -1, x0, x1, x2)
Cond_f4749_0_createTree_GE1(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0 - 1), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE2(x0 > 1 && x2 > x1, x0, x1, x2)
Cond_f4749_0_createTree_GE2(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0 - 1, x0 - 2), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE3(x0 > 1 && x2 > x1, x0, x1, x2)
Cond_f4749_0_createTree_GE3(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0 - 1, x0 - 2), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE4(x3 > -1 && x0 > 1 && x2 > x1, x0, x1, x2, x3)
Cond_f4749_0_createTree_GE4(TRUE, x0, x1, x2, x3) → f4778_1_createTree_InvokeMethod(f4749_0_createTree_GE(x0 - 2, 0, x3), x0, x2, x1)

The integer pair graph contains the following rules and edges:
(0): F1478_0_CREATETREE_GT'(x0[0]) → COND_F1478_0_CREATETREE_GT(x0[0] > 0 && x1[0] > 0, x0[0], x1[0])
(1): COND_F1478_0_CREATETREE_GT(TRUE, x0[1], x1[1]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(x0[1] - 2), x0[1] - 1, x1[1], 0)
(2): F1478_0_CREATETREE_GT'(x0[2]) → COND_F1478_0_CREATETREE_GT1(x0[2] > 0, x0[2])
(3): COND_F1478_0_CREATETREE_GT1(TRUE, x0[3]) → F1478_0_CREATETREE_GT'(x0[3] - 2)
(4): F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4]) → COND_F4778_1_CREATETREE_INVOKEMETHOD(x4[4] > -1 && x2[4] > -1 && x4[4] + 1 < x3[4], f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])
(5): COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(x2[5] - 1), x2[5], x3[5], x4[5] + 1)
(6): F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6]) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(x4[6] > -1 && x2[6] > -1 && x4[6] + 1 < x3[6], f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])
(7): COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0[7]), x2[7], x3[7], x4[7]) → F1478_0_CREATETREE_GT'(x2[7] - 1)
(8): F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8]) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(x4[8] > -1 && x2[8] > -1 && x4[8] + 1 < x3[8], f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])
(9): COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(x2[9] - 1), x2[9], x3[9], x4[9] + 1)
(10): F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10]) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(x4[10] > -1 && x2[10] > -1 && x4[10] + 1 < x3[10], f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])
(11): COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0[11]), x2[11], x3[11], x4[11]) → F1478_0_CREATETREE_GT'(x2[11] - 1)

(0) -> (1), if (x0[0] > 0 && x1[0] > 0 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1])

(1) -> (4), if (f1478_0_createTree_GT(x0[1] - 2) →^* f1485_0_createTree_Return(x0[4])∧x0[1] - 1 →^* x2[4]∧x1[1] →^* x3[4]∧0 →^* x4[4])

(1) -> (6), if (f1478_0_createTree_GT(x0[1] - 2) →^* f1485_0_createTree_Return(x0[6])∧x0[1] - 1 →^* x2[6]∧x1[1] →^* x3[6]∧0 →^* x4[6])

(1) -> (8), if (f1478_0_createTree_GT(x0[1] - 2) →^* f4756_0_createTree_Return(x0[8])∧x0[1] - 1 →^* x2[8]∧x1[1] →^* x3[8]∧0 →^* x4[8])

(1) -> (10), if (f1478_0_createTree_GT(x0[1] - 2) →^* f4756_0_createTree_Return(x0[10])∧x0[1] - 1 →^* x2[10]∧x1[1] →^* x3[10]∧0 →^* x4[10])

(2) -> (3), if (x0[2] > 0 ∧x0[2] →^* x0[3])

(3) -> (0), if (x0[3] - 2 →^* x0[0])

(3) -> (2), if (x0[3] - 2 →^* x0[2])

(4) -> (5), if (x4[4] > -1 && x2[4] > -1 && x4[4] + 1 < x3[4] ∧f1485_0_createTree_Return(x0[4]) →^* f1485_0_createTree_Return(x0[5])∧x2[4] →^* x2[5]∧x3[4] →^* x3[5]∧x4[4] →^* x4[5])

(5) -> (4), if (f1478_0_createTree_GT(x2[5] - 1) →^* f1485_0_createTree_Return(x0[4])∧x2[5] →^* x2[4]∧x3[5] →^* x3[4]∧x4[5] + 1 →^* x4[4])

(5) -> (6), if (f1478_0_createTree_GT(x2[5] - 1) →^* f1485_0_createTree_Return(x0[6])∧x2[5] →^* x2[6]∧x3[5] →^* x3[6]∧x4[5] + 1 →^* x4[6])

(5) -> (8), if (f1478_0_createTree_GT(x2[5] - 1) →^* f4756_0_createTree_Return(x0[8])∧x2[5] →^* x2[8]∧x3[5] →^* x3[8]∧x4[5] + 1 →^* x4[8])

(5) -> (10), if (f1478_0_createTree_GT(x2[5] - 1) →^* f4756_0_createTree_Return(x0[10])∧x2[5] →^* x2[10]∧x3[5] →^* x3[10]∧x4[5] + 1 →^* x4[10])

(6) -> (7), if (x4[6] > -1 && x2[6] > -1 && x4[6] + 1 < x3[6] ∧f1485_0_createTree_Return(x0[6]) →^* f1485_0_createTree_Return(x0[7])∧x2[6] →^* x2[7]∧x3[6] →^* x3[7]∧x4[6] →^* x4[7])

(7) -> (0), if (x2[7] - 1 →^* x0[0])

(7) -> (2), if (x2[7] - 1 →^* x0[2])

(8) -> (9), if (x4[8] > -1 && x2[8] > -1 && x4[8] + 1 < x3[8] ∧f4756_0_createTree_Return(x0[8]) →^* f4756_0_createTree_Return(x0[9])∧x2[8] →^* x2[9]∧x3[8] →^* x3[9]∧x4[8] →^* x4[9])

(9) -> (4), if (f1478_0_createTree_GT(x2[9] - 1) →^* f1485_0_createTree_Return(x0[4])∧x2[9] →^* x2[4]∧x3[9] →^* x3[4]∧x4[9] + 1 →^* x4[4])

(9) -> (6), if (f1478_0_createTree_GT(x2[9] - 1) →^* f1485_0_createTree_Return(x0[6])∧x2[9] →^* x2[6]∧x3[9] →^* x3[6]∧x4[9] + 1 →^* x4[6])

(9) -> (8), if (f1478_0_createTree_GT(x2[9] - 1) →^* f4756_0_createTree_Return(x0[8])∧x2[9] →^* x2[8]∧x3[9] →^* x3[8]∧x4[9] + 1 →^* x4[8])

(9) -> (10), if (f1478_0_createTree_GT(x2[9] - 1) →^* f4756_0_createTree_Return(x0[10])∧x2[9] →^* x2[10]∧x3[9] →^* x3[10]∧x4[9] + 1 →^* x4[10])

(10) -> (11), if (x4[10] > -1 && x2[10] > -1 && x4[10] + 1 < x3[10] ∧f4756_0_createTree_Return(x0[10]) →^* f4756_0_createTree_Return(x0[11])∧x2[10] →^* x2[11]∧x3[10] →^* x3[11]∧x4[10] →^* x4[11])

(11) -> (0), if (x2[11] - 1 →^* x0[0])

(11) -> (2), if (x2[11] - 1 →^* x0[2])

The set Q consists of the following terms:
f4749_0_createTree_GE(x0, x1, x2)
Cond_f4749_0_createTree_GE(TRUE, x0, x1, x2, x3)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0), x1, x2, x3)
Cond_f4778_1_createTree_InvokeMethod(TRUE, f1485_0_createTree_Return(x0), x1, x2, x3)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0, x1), x2, x3, x4)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0, x1), x2, x3, x4)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(x0), x1, x2, x3)
Cond_f4778_1_createTree_InvokeMethod1(TRUE, f4756_0_createTree_Return(x0), x1, x2, x3)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(x0, x1, x2, x3), x4, x5, x6)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(x0, x1, x2, x3), x4, x5, x6)
Cond_f4749_0_createTree_GE1(TRUE, x0, x1, x2)
Cond_f4749_0_createTree_GE2(TRUE, x0, x1, x2)
Cond_f4749_0_createTree_GE3(TRUE, x0, x1, x2)
Cond_f4749_0_createTree_GE4(TRUE, x0, x1, x2, x3)

(13) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpCand1ShapeHeuristic@41d44ad8 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 0 Max Right Steps: 0

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair F1478_0_CREATETREE_GT'(x0) → COND_F1478_0_CREATETREE_GT(&&(>(x0, 0), >(x1, 0)), x0, x1) the following chains were created:

We consider the chain F1478_0_CREATETREE_GT'(x0[0]) → COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0]) which results in the following constraint:
(1)    (F1478_0_CREATETREE_GT'(x0[0])≥NonInfC∧F1478_0_CREATETREE_GT'(x0[0])≥COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])∧(U^Increasing(COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])), ≥)∧[bni_50] = 0∧[(-1)bso_51] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])), ≥)∧[bni_50] = 0∧[(-1)bso_51] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])), ≥)∧[bni_50] = 0∧[(-1)bso_51] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])), ≥)∧[bni_50] = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)

For Pair COND_F1478_0_CREATETREE_GT(TRUE, x0, x1) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0, 2)), -(x0, 1), x1, 0) the following chains were created:

We consider the chain COND_F1478_0_CREATETREE_GT(TRUE, x0[1], x1[1]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0) which results in the following constraint:
(6)    (COND_F1478_0_CREATETREE_GT(TRUE, x0[1], x1[1])≥NonInfC∧COND_F1478_0_CREATETREE_GT(TRUE, x0[1], x1[1])≥F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)∧(U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)), ≥))

We simplified constraint (6) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(7)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)), ≥)∧[bni_52] = 0∧[1 + (-1)bso_53] ≥ 0)

We simplified constraint (7) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(8)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)), ≥)∧[bni_52] = 0∧[1 + (-1)bso_53] ≥ 0)

We simplified constraint (8) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(9)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)), ≥)∧[bni_52] = 0∧[1 + (-1)bso_53] ≥ 0)

We simplified constraint (9) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(10)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)), ≥)∧[bni_52] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_53] ≥ 0)

For Pair F1478_0_CREATETREE_GT'(x0) → COND_F1478_0_CREATETREE_GT1(>(x0, 0), x0) the following chains were created:

We consider the chain F1478_0_CREATETREE_GT'(x0[2]) → COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2]), COND_F1478_0_CREATETREE_GT1(TRUE, x0[3]) → F1478_0_CREATETREE_GT'(-(x0[3], 2)) which results in the following constraint:
(11)    (>(x0[2], 0)=TRUE∧x0[2]=x0[3] ⇒ F1478_0_CREATETREE_GT'(x0[2])≥NonInfC∧F1478_0_CREATETREE_GT'(x0[2])≥COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])∧(U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥))

We simplified constraint (11) using rule (IV) which results in the following new constraint:
(12)    (>(x0[2], 0)=TRUE ⇒ F1478_0_CREATETREE_GT'(x0[2])≥NonInfC∧F1478_0_CREATETREE_GT'(x0[2])≥COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])∧(U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]x0[2] ≥ 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]x0[2] ≥ 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15)    (x0[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥)∧[(-1)bni_54 + (-1)Bound*bni_54] + [bni_54]x0[2] ≥ 0∧[(-1)bso_55] ≥ 0)

We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(16)    (x0[2] ≥ 0 ⇒ (U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥)∧[(-1)Bound*bni_54] + [bni_54]x0[2] ≥ 0∧[(-1)bso_55] ≥ 0)

For Pair COND_F1478_0_CREATETREE_GT1(TRUE, x0) → F1478_0_CREATETREE_GT'(-(x0, 2)) the following chains were created:

We consider the chain COND_F1478_0_CREATETREE_GT1(TRUE, x0[3]) → F1478_0_CREATETREE_GT'(-(x0[3], 2)) which results in the following constraint:
(17)    (COND_F1478_0_CREATETREE_GT1(TRUE, x0[3])≥NonInfC∧COND_F1478_0_CREATETREE_GT1(TRUE, x0[3])≥F1478_0_CREATETREE_GT'(-(x0[3], 2))∧(U^Increasing(F1478_0_CREATETREE_GT'(-(x0[3], 2))), ≥))

We simplified constraint (17) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(18)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x0[3], 2))), ≥)∧[bni_56] = 0∧[2 + (-1)bso_57] ≥ 0)

We simplified constraint (18) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(19)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x0[3], 2))), ≥)∧[bni_56] = 0∧[2 + (-1)bso_57] ≥ 0)

We simplified constraint (19) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(20)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x0[3], 2))), ≥)∧[bni_56] = 0∧[2 + (-1)bso_57] ≥ 0)

We simplified constraint (20) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(21)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x0[3], 2))), ≥)∧[bni_56] = 0∧0 = 0∧[2 + (-1)bso_57] ≥ 0)

For Pair F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f1485_0_createTree_Return(x0), x2, x3, x4) the following chains were created:

We consider the chain F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4]) → COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4]), COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1)) which results in the following constraint:
(22)    (&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4]))=TRUE∧f1485_0_createTree_Return(x0[4])=f1485_0_createTree_Return(x0[5])∧x2[4]=x2[5]∧x3[4]=x3[5]∧x4[4]=x4[5] ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])≥COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥))

We simplified constraint (22) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(23)    (<(+(x4[4], 1), x3[4])=TRUE∧>(x4[4], -1)=TRUE∧>(x2[4], -1)=TRUE ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])≥COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    (x3[4] + [-2] + [-1]x4[4] ≥ 0∧x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥)∧[(-1)bni_58 + (-1)Bound*bni_58] + [bni_58]x2[4] ≥ 0∧[(-1)bso_59] ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(25)    (x3[4] + [-2] + [-1]x4[4] ≥ 0∧x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥)∧[(-1)bni_58 + (-1)Bound*bni_58] + [bni_58]x2[4] ≥ 0∧[(-1)bso_59] ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(26)    (x3[4] + [-2] + [-1]x4[4] ≥ 0∧x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥)∧[(-1)bni_58 + (-1)Bound*bni_58] + [bni_58]x2[4] ≥ 0∧[(-1)bso_59] ≥ 0)

We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(27)    (x3[4] + [-2] + [-1]x4[4] ≥ 0∧x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥)∧0 = 0∧[(-1)bni_58 + (-1)Bound*bni_58] + [bni_58]x2[4] ≥ 0∧0 = 0∧[(-1)bso_59] ≥ 0)

We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(28)    (x3[4] ≥ 0∧x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥)∧0 = 0∧[(-1)bni_58 + (-1)Bound*bni_58] + [bni_58]x2[4] ≥ 0∧0 = 0∧[(-1)bso_59] ≥ 0)

For Pair COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1)) the following chains were created:

We consider the chain COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1)) which results in the following constraint:
(29)    (COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5])≥NonInfC∧COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5])≥F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))∧(U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))), ≥))

We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(30)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))), ≥)∧[bni_60] = 0∧[(-1)bso_61] ≥ 0)

We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(31)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))), ≥)∧[bni_60] = 0∧[(-1)bso_61] ≥ 0)

We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(32)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))), ≥)∧[bni_60] = 0∧[(-1)bso_61] ≥ 0)

We simplified constraint (32) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(33)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))), ≥)∧[bni_60] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_61] ≥ 0)

For Pair F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f1485_0_createTree_Return(x0), x2, x3, x4) the following chains were created:

We consider the chain F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6]) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6]), COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0[7]), x2[7], x3[7], x4[7]) → F1478_0_CREATETREE_GT'(-(x2[7], 1)) which results in the following constraint:
(34)    (&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6]))=TRUE∧f1485_0_createTree_Return(x0[6])=f1485_0_createTree_Return(x0[7])∧x2[6]=x2[7]∧x3[6]=x3[7]∧x4[6]=x4[7] ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])≥COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥))

We simplified constraint (34) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(35)    (<(+(x4[6], 1), x3[6])=TRUE∧>(x4[6], -1)=TRUE∧>(x2[6], -1)=TRUE ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])≥COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥))

We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(36)    (x3[6] + [-2] + [-1]x4[6] ≥ 0∧x4[6] ≥ 0∧x2[6] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥)∧[(-1)bni_62 + (-1)Bound*bni_62] + [bni_62]x2[6] ≥ 0∧[(-1)bso_63] ≥ 0)

We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(37)    (x3[6] + [-2] + [-1]x4[6] ≥ 0∧x4[6] ≥ 0∧x2[6] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥)∧[(-1)bni_62 + (-1)Bound*bni_62] + [bni_62]x2[6] ≥ 0∧[(-1)bso_63] ≥ 0)

We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(38)    (x3[6] + [-2] + [-1]x4[6] ≥ 0∧x4[6] ≥ 0∧x2[6] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥)∧[(-1)bni_62 + (-1)Bound*bni_62] + [bni_62]x2[6] ≥ 0∧[(-1)bso_63] ≥ 0)

We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(39)    (x3[6] + [-2] + [-1]x4[6] ≥ 0∧x4[6] ≥ 0∧x2[6] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥)∧0 = 0∧[(-1)bni_62 + (-1)Bound*bni_62] + [bni_62]x2[6] ≥ 0∧0 = 0∧[(-1)bso_63] ≥ 0)

We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(40)    (x3[6] ≥ 0∧x4[6] ≥ 0∧x2[6] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥)∧0 = 0∧[(-1)bni_62 + (-1)Bound*bni_62] + [bni_62]x2[6] ≥ 0∧0 = 0∧[(-1)bso_63] ≥ 0)

For Pair COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT'(-(x2, 1)) the following chains were created:

We consider the chain COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0[7]), x2[7], x3[7], x4[7]) → F1478_0_CREATETREE_GT'(-(x2[7], 1)) which results in the following constraint:
(41)    (COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0[7]), x2[7], x3[7], x4[7])≥NonInfC∧COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0[7]), x2[7], x3[7], x4[7])≥F1478_0_CREATETREE_GT'(-(x2[7], 1))∧(U^Increasing(F1478_0_CREATETREE_GT'(-(x2[7], 1))), ≥))

We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(42)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[7], 1))), ≥)∧[bni_64] = 0∧[1 + (-1)bso_65] ≥ 0)

We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(43)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[7], 1))), ≥)∧[bni_64] = 0∧[1 + (-1)bso_65] ≥ 0)

We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(44)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[7], 1))), ≥)∧[bni_64] = 0∧[1 + (-1)bso_65] ≥ 0)

We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(45)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[7], 1))), ≥)∧[bni_64] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_65] ≥ 0)

For Pair F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f4756_0_createTree_Return(x0), x2, x3, x4) the following chains were created:

We consider the chain F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8]) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8]), COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1)) which results in the following constraint:
(46)    (&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8]))=TRUE∧f4756_0_createTree_Return(x0[8])=f4756_0_createTree_Return(x0[9])∧x2[8]=x2[9]∧x3[8]=x3[9]∧x4[8]=x4[9] ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])≥COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥))

We simplified constraint (46) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(47)    (<(+(x4[8], 1), x3[8])=TRUE∧>(x4[8], -1)=TRUE∧>(x2[8], -1)=TRUE ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])≥COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥))

We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(48)    (x3[8] + [-2] + [-1]x4[8] ≥ 0∧x4[8] ≥ 0∧x2[8] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥)∧[(-1)bni_66 + (-1)Bound*bni_66] + [bni_66]x2[8] ≥ 0∧[(-1)bso_67] ≥ 0)

We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(49)    (x3[8] + [-2] + [-1]x4[8] ≥ 0∧x4[8] ≥ 0∧x2[8] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥)∧[(-1)bni_66 + (-1)Bound*bni_66] + [bni_66]x2[8] ≥ 0∧[(-1)bso_67] ≥ 0)

We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(50)    (x3[8] + [-2] + [-1]x4[8] ≥ 0∧x4[8] ≥ 0∧x2[8] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥)∧[(-1)bni_66 + (-1)Bound*bni_66] + [bni_66]x2[8] ≥ 0∧[(-1)bso_67] ≥ 0)

We simplified constraint (50) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(51)    (x3[8] + [-2] + [-1]x4[8] ≥ 0∧x4[8] ≥ 0∧x2[8] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥)∧0 = 0∧[(-1)bni_66 + (-1)Bound*bni_66] + [bni_66]x2[8] ≥ 0∧0 = 0∧[(-1)bso_67] ≥ 0)

We simplified constraint (51) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(52)    (x3[8] ≥ 0∧x4[8] ≥ 0∧x2[8] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥)∧0 = 0∧[(-1)bni_66 + (-1)Bound*bni_66] + [bni_66]x2[8] ≥ 0∧0 = 0∧[(-1)bso_67] ≥ 0)

For Pair COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1)) the following chains were created:

We consider the chain COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1)) which results in the following constraint:
(53)    (COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9])≥NonInfC∧COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9])≥F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))∧(U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))), ≥))

We simplified constraint (53) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(54)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))), ≥)∧[bni_68] = 0∧[(-1)bso_69] ≥ 0)

We simplified constraint (54) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(55)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))), ≥)∧[bni_68] = 0∧[(-1)bso_69] ≥ 0)

We simplified constraint (55) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(56)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))), ≥)∧[bni_68] = 0∧[(-1)bso_69] ≥ 0)

We simplified constraint (56) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(57)    ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))), ≥)∧[bni_68] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_69] ≥ 0)

For Pair F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f4756_0_createTree_Return(x0), x2, x3, x4) the following chains were created:

We consider the chain F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10]) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10]), COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0[11]), x2[11], x3[11], x4[11]) → F1478_0_CREATETREE_GT'(-(x2[11], 1)) which results in the following constraint:
(58)    (&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10]))=TRUE∧f4756_0_createTree_Return(x0[10])=f4756_0_createTree_Return(x0[11])∧x2[10]=x2[11]∧x3[10]=x3[11]∧x4[10]=x4[11] ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])≥COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥))

We simplified constraint (58) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(59)    (<(+(x4[10], 1), x3[10])=TRUE∧>(x4[10], -1)=TRUE∧>(x2[10], -1)=TRUE ⇒ F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])≥NonInfC∧F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])≥COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])∧(U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥))

We simplified constraint (59) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(60)    (x3[10] + [-2] + [-1]x4[10] ≥ 0∧x4[10] ≥ 0∧x2[10] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] + [bni_70]x2[10] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (60) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(61)    (x3[10] + [-2] + [-1]x4[10] ≥ 0∧x4[10] ≥ 0∧x2[10] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] + [bni_70]x2[10] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (61) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(62)    (x3[10] + [-2] + [-1]x4[10] ≥ 0∧x4[10] ≥ 0∧x2[10] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥)∧[(-1)bni_70 + (-1)Bound*bni_70] + [bni_70]x2[10] ≥ 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (62) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(63)    (x3[10] + [-2] + [-1]x4[10] ≥ 0∧x4[10] ≥ 0∧x2[10] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥)∧0 = 0∧[(-1)bni_70 + (-1)Bound*bni_70] + [bni_70]x2[10] ≥ 0∧0 = 0∧[(-1)bso_71] ≥ 0)

We simplified constraint (63) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(64)    (x3[10] ≥ 0∧x4[10] ≥ 0∧x2[10] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥)∧0 = 0∧[(-1)bni_70 + (-1)Bound*bni_70] + [bni_70]x2[10] ≥ 0∧0 = 0∧[(-1)bso_71] ≥ 0)

For Pair COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT'(-(x2, 1)) the following chains were created:

We consider the chain COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0[11]), x2[11], x3[11], x4[11]) → F1478_0_CREATETREE_GT'(-(x2[11], 1)) which results in the following constraint:
(65)    (COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0[11]), x2[11], x3[11], x4[11])≥NonInfC∧COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0[11]), x2[11], x3[11], x4[11])≥F1478_0_CREATETREE_GT'(-(x2[11], 1))∧(U^Increasing(F1478_0_CREATETREE_GT'(-(x2[11], 1))), ≥))

We simplified constraint (65) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(66)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[11], 1))), ≥)∧[bni_72] = 0∧[1 + (-1)bso_73] ≥ 0)

We simplified constraint (66) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(67)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[11], 1))), ≥)∧[bni_72] = 0∧[1 + (-1)bso_73] ≥ 0)

We simplified constraint (67) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(68)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[11], 1))), ≥)∧[bni_72] = 0∧[1 + (-1)bso_73] ≥ 0)

We simplified constraint (68) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(69)    ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[11], 1))), ≥)∧[bni_72] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_73] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

F1478_0_CREATETREE_GT'(x0) → COND_F1478_0_CREATETREE_GT(&&(>(x0, 0), >(x1, 0)), x0, x1)
- ((U^Increasing(COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])), ≥)∧[bni_50] = 0∧0 = 0∧0 = 0∧[(-1)bso_51] ≥ 0)
COND_F1478_0_CREATETREE_GT(TRUE, x0, x1) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0, 2)), -(x0, 1), x1, 0)
- ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)), ≥)∧[bni_52] = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_53] ≥ 0)
F1478_0_CREATETREE_GT'(x0) → COND_F1478_0_CREATETREE_GT1(>(x0, 0), x0)
- (x0[2] ≥ 0 ⇒ (U^Increasing(COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])), ≥)∧[(-1)Bound*bni_54] + [bni_54]x0[2] ≥ 0∧[(-1)bso_55] ≥ 0)
COND_F1478_0_CREATETREE_GT1(TRUE, x0) → F1478_0_CREATETREE_GT'(-(x0, 2))
- ((U^Increasing(F1478_0_CREATETREE_GT'(-(x0[3], 2))), ≥)∧[bni_56] = 0∧0 = 0∧[2 + (-1)bso_57] ≥ 0)
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f1485_0_createTree_Return(x0), x2, x3, x4)
- (x3[4] ≥ 0∧x4[4] ≥ 0∧x2[4] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])), ≥)∧0 = 0∧[(-1)bni_58 + (-1)Bound*bni_58] + [bni_58]x2[4] ≥ 0∧0 = 0∧[(-1)bso_59] ≥ 0)
COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1))
- ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))), ≥)∧[bni_60] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_61] ≥ 0)
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f1485_0_createTree_Return(x0), x2, x3, x4)
- (x3[6] ≥ 0∧x4[6] ≥ 0∧x2[6] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])), ≥)∧0 = 0∧[(-1)bni_62 + (-1)Bound*bni_62] + [bni_62]x2[6] ≥ 0∧0 = 0∧[(-1)bso_63] ≥ 0)
COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT'(-(x2, 1))
- ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[7], 1))), ≥)∧[bni_64] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_65] ≥ 0)
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f4756_0_createTree_Return(x0), x2, x3, x4)
- (x3[8] ≥ 0∧x4[8] ≥ 0∧x2[8] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])), ≥)∧0 = 0∧[(-1)bni_66 + (-1)Bound*bni_66] + [bni_66]x2[8] ≥ 0∧0 = 0∧[(-1)bso_67] ≥ 0)
COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2, 1)), x2, x3, +(x4, 1))
- ((U^Increasing(F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))), ≥)∧[bni_68] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_69] ≥ 0)
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0), x2, x3, x4) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4, -1), >(x2, -1)), <(+(x4, 1), x3)), f4756_0_createTree_Return(x0), x2, x3, x4)
- (x3[10] ≥ 0∧x4[10] ≥ 0∧x2[10] ≥ 0 ⇒ (U^Increasing(COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])), ≥)∧0 = 0∧[(-1)bni_70 + (-1)Bound*bni_70] + [bni_70]x2[10] ≥ 0∧0 = 0∧[(-1)bso_71] ≥ 0)
COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → F1478_0_CREATETREE_GT'(-(x2, 1))
- ((U^Increasing(F1478_0_CREATETREE_GT'(-(x2[11], 1))), ≥)∧[bni_72] = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_73] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(f4749_0_createTree_GE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + [-1]x₃ + [-1]x₁
POL(Cond_f4749_0_createTree_GE(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₃ + [-1]x₄ + [-1]x₂
POL(>=(x₁, x₂)) = [-1]
POL(f4756_0_createTree_Return(x₁)) = x₁
POL(f4778_1_createTree_InvokeMethod(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + [-1]x₂ + [-1]x₁ + [-1]x₄
POL(f1485_0_createTree_Return(x₁)) = x₁
POL(Cond_f4778_1_createTree_InvokeMethod(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄ + [-1]x₃ + [-1]x₂ + [-1]x₅
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(f1702_0_createTree_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(f4896_0_createTree_InvokeMethod(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₁ + [-1]x₃ + [-1]x₂ + [-1]x₄
POL(f1808_0_createTree_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(Cond_f4778_1_createTree_InvokeMethod1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄ + [-1]x₃ + [-1]x₂ + [-1]x₅
POL(f4846_0_createTree_InvokeMethod(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₃ + [-1]x₂ + [-1]x₁
POL(Cond_f4749_0_createTree_GE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₃ + [-1]x₂
POL(&&(x₁, x₂)) = [-1]
POL(<=(x₁, x₂)) = [-1]
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(Cond_f4749_0_createTree_GE2(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₃ + [-1]x₂
POL(2) = [2]
POL(Cond_f4749_0_createTree_GE3(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₄ + [-1]x₃ + [-1]x₂
POL(Cond_f4749_0_createTree_GE4(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [-1]x₄ + [-1]x₃ + [-1]x₂
POL(0) = 0
POL(F1478_0_CREATETREE_GT'(x₁)) = [-1] + x₁
POL(COND_F1478_0_CREATETREE_GT(x₁, x₂, x₃)) = [-1] + x₂
POL(F4778_1_CREATETREE_INVOKEMETHOD'(x₁, x₂, x₃, x₄)) = [-1] + x₂
POL(f1478_0_createTree_GT(x₁)) = x₁
POL(COND_F1478_0_CREATETREE_GT1(x₁, x₂)) = [-1] + x₂
POL(COND_F4778_1_CREATETREE_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅)) = [-1] + x₃
POL(<(x₁, x₂)) = [-1]
POL(COND_F4778_1_CREATETREE_INVOKEMETHOD1(x₁, x₂, x₃, x₄, x₅)) = [-1] + x₃
POL(COND_F4778_1_CREATETREE_INVOKEMETHOD2(x₁, x₂, x₃, x₄, x₅)) = [-1] + x₃
POL(COND_F4778_1_CREATETREE_INVOKEMETHOD3(x₁, x₂, x₃, x₄, x₅)) = [-1] + x₃

The following pairs are in P_>:

COND_F1478_0_CREATETREE_GT(TRUE, x0[1], x1[1]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x0[1], 2)), -(x0[1], 1), x1[1], 0)
COND_F1478_0_CREATETREE_GT1(TRUE, x0[3]) → F1478_0_CREATETREE_GT'(-(x0[3], 2))
COND_F4778_1_CREATETREE_INVOKEMETHOD1(TRUE, f1485_0_createTree_Return(x0[7]), x2[7], x3[7], x4[7]) → F1478_0_CREATETREE_GT'(-(x2[7], 1))
COND_F4778_1_CREATETREE_INVOKEMETHOD3(TRUE, f4756_0_createTree_Return(x0[11]), x2[11], x3[11], x4[11]) → F1478_0_CREATETREE_GT'(-(x2[11], 1))

The following pairs are in P_bound:

F1478_0_CREATETREE_GT'(x0[2]) → COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4]) → COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6]) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8]) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10]) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])

The following pairs are in P_≥:

F1478_0_CREATETREE_GT'(x0[0]) → COND_F1478_0_CREATETREE_GT(&&(>(x0[0], 0), >(x1[0], 0)), x0[0], x1[0])
F1478_0_CREATETREE_GT'(x0[2]) → COND_F1478_0_CREATETREE_GT1(>(x0[2], 0), x0[2])
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4]) → COND_F4778_1_CREATETREE_INVOKEMETHOD(&&(&&(>(x4[4], -1), >(x2[4], -1)), <(+(x4[4], 1), x3[4])), f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])
COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[5], 1)), x2[5], x3[5], +(x4[5], 1))
F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6]) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(&&(&&(>(x4[6], -1), >(x2[6], -1)), <(+(x4[6], 1), x3[6])), f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8]) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(&&(&&(>(x4[8], -1), >(x2[8], -1)), <(+(x4[8], 1), x3[8])), f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])
COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(-(x2[9], 1)), x2[9], x3[9], +(x4[9], 1))
F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10]) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(&&(&&(>(x4[10], -1), >(x2[10], -1)), <(+(x4[10], 1), x3[10])), f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])

There are no usable rules.

(14) Complex Obligation (AND)

(15) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
f4749_0_createTree_GE(x1, x3, x2) → Cond_f4749_0_createTree_GE(x3 >= x2, x1, x3, x2, x0)
Cond_f4749_0_createTree_GE(TRUE, x1, x3, x2, x0) → f4756_0_createTree_Return(x0)
f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0), x2, x3, x4) → Cond_f4778_1_createTree_InvokeMethod(x4 > -1, f1485_0_createTree_Return(x0), x2, x3, x4)
Cond_f4778_1_createTree_InvokeMethod(TRUE, f1485_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, x4 + 1, x3)
f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0, x1), x3, x4, x5) → f4896_0_createTree_InvokeMethod(x2, x3, x4, x5)
f4778_1_createTree_InvokeMethod(f4756_0_createTree_Return(x0), x2, x3, x4) → Cond_f4778_1_createTree_InvokeMethod1(x4 > -1, f4756_0_createTree_Return(x0), x2, x3, x4)
Cond_f4778_1_createTree_InvokeMethod1(TRUE, f4756_0_createTree_Return(x0), x2, x3, x4) → f4749_0_createTree_GE(x2, x4 + 1, x3)
f4778_1_createTree_InvokeMethod(f4896_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4778_1_createTree_InvokeMethod(f4846_0_createTree_InvokeMethod(x0, x1, x2, x3), x5, x6, x7) → f4896_0_createTree_InvokeMethod(x4, x5, x6, x7)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE1(x2 > x1 && x0 <= 1 && x0 > -1, x0, x1, x2)
Cond_f4749_0_createTree_GE1(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1485_0_createTree_Return(x0 - 1), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE2(x0 > 1 && x2 > x1, x0, x1, x2)
Cond_f4749_0_createTree_GE2(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1702_0_createTree_InvokeMethod(x0 - 1, x0 - 2), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE3(x0 > 1 && x2 > x1, x0, x1, x2)
Cond_f4749_0_createTree_GE3(TRUE, x0, x1, x2) → f4778_1_createTree_InvokeMethod(f1808_0_createTree_InvokeMethod(x0 - 1, x0 - 2), x0, x2, x1)
f4749_0_createTree_GE(x0, x1, x2) → Cond_f4749_0_createTree_GE4(x3 > -1 && x0 > 1 && x2 > x1, x0, x1, x2, x3)
Cond_f4749_0_createTree_GE4(TRUE, x0, x1, x2, x3) → f4778_1_createTree_InvokeMethod(f4749_0_createTree_GE(x0 - 2, 0, x3), x0, x2, x1)

The integer pair graph contains the following rules and edges:
(0): F1478_0_CREATETREE_GT'(x0[0]) → COND_F1478_0_CREATETREE_GT(x0[0] > 0 && x1[0] > 0, x0[0], x1[0])
(2): F1478_0_CREATETREE_GT'(x0[2]) → COND_F1478_0_CREATETREE_GT1(x0[2] > 0, x0[2])
(4): F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4]) → COND_F4778_1_CREATETREE_INVOKEMETHOD(x4[4] > -1 && x2[4] > -1 && x4[4] + 1 < x3[4], f1485_0_createTree_Return(x0[4]), x2[4], x3[4], x4[4])
(5): COND_F4778_1_CREATETREE_INVOKEMETHOD(TRUE, f1485_0_createTree_Return(x0[5]), x2[5], x3[5], x4[5]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(x2[5] - 1), x2[5], x3[5], x4[5] + 1)
(6): F4778_1_CREATETREE_INVOKEMETHOD'(f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6]) → COND_F4778_1_CREATETREE_INVOKEMETHOD1(x4[6] > -1 && x2[6] > -1 && x4[6] + 1 < x3[6], f1485_0_createTree_Return(x0[6]), x2[6], x3[6], x4[6])
(8): F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8]) → COND_F4778_1_CREATETREE_INVOKEMETHOD2(x4[8] > -1 && x2[8] > -1 && x4[8] + 1 < x3[8], f4756_0_createTree_Return(x0[8]), x2[8], x3[8], x4[8])
(9): COND_F4778_1_CREATETREE_INVOKEMETHOD2(TRUE, f4756_0_createTree_Return(x0[9]), x2[9], x3[9], x4[9]) → F4778_1_CREATETREE_INVOKEMETHOD'(f1478_0_createTree_GT(x2[9] - 1), x2[9], x3[9], x4[9] + 1)
(10): F4778_1_CREATETREE_INVOKEMETHOD'(f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10]) → COND_F4778_1_CREATETREE_INVOKEMETHOD3(x4[10] > -1 && x2[10] > -1 && x4[10] + 1 < x3[10], f4756_0_createTree_Return(x0[10]), x2[10], x3[10], x4[10])