### (0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: DuplicateNodes
`public class DuplicateNodes {    public static void main(String[] args) {		Random.args = args;        Tree tree = Tree.createTree();		randomlyDuplicate(tree);    }	public static void randomlyDuplicate(Tree tree) {		Tree cur = tree;				while (cur != null) {			if (Random.random() > 42) {				cur.right = new Tree(cur.left, cur.right);				cur = cur.left;			} else {				cur.left = new Tree(cur.left, cur.right);				cur = cur.right;			}		}	}}public class List {  Tree value;  List next;  public List(Tree value, List next) {    this.value = value;    this.next = next;  }}public class Random {  static String[] args;  static int index = 0;  public static int random() {    String string = args[index];    index++;    return string.length();  }}public class Tree {  Tree left;  Tree right;  Object value;  public Tree(Tree l, Tree r) {    this.left = l;    this.right = r;  }  public Tree() {  }  public static Tree createNode() {   if (Random.random() == 0) {      return null;    }    Tree result = new Tree();    return result;  }  public static Tree createTree() {    Tree result = createNode();    List list = new List(result, null);        int counter = Random.random();    while (counter > 0 && list != null) {      Tree first = list.value;      list = list.next;      if (first != null) {        Tree left = createNode();        Tree right = createNode();        first.left = left;        first.right = right;        list = new List(left, list);        list = new List(right, list);      }      counter--;    }    return result;  }  public static void main(String[] args) {    Random.args = args;    createTree();  }}`

### (1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

### (2) Obligation:

FIGraph based on JBC Program:
DuplicateNodes.main([Ljava/lang/String;)V: Graph of 56 nodes with 0 SCCs.

Tree.createTree()LTree;: Graph of 404 nodes with 1 SCC.

Tree.createNode()LTree;: Graph of 108 nodes with 0 SCCs.

DuplicateNodes.randomlyDuplicate(LTree;)V: Graph of 191 nodes with 1 SCC.

### (3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 115 rules for P and 73 rules for R.

Combined rules. Obtained 7 rules for P and 0 rules for R.

Filtered ground terms:

11176_0_randomlyDuplicate_Store(x1, x2) → 11176_0_randomlyDuplicate_Store(x2)
Tree(x1, x2, x3) → Tree(x2, x3)
8591_0_random_IntArithmetic(x1, x2, x3, x4) → 8591_0_random_IntArithmetic(x2, x3)
7873_0_random_ArrayAccess(x1, x2, x3) → 7873_0_random_ArrayAccess(x2, x3)
11172_0_randomlyDuplicate_Store(x1, x2) → 11172_0_randomlyDuplicate_Store(x2)

Filtered all free variables:

8591_1_randomlyDuplicate_InvokeMethod(x1, x2) → 8591_1_randomlyDuplicate_InvokeMethod(x2)
7873_1_randomlyDuplicate_InvokeMethod(x1, x2) → 7873_1_randomlyDuplicate_InvokeMethod(x2)
Cond_8591_1_randomlyDuplicate_InvokeMethod(x1, x2, x3) → Cond_8591_1_randomlyDuplicate_InvokeMethod(x1, x3)
Cond_8591_1_randomlyDuplicate_InvokeMethod1(x1, x2, x3) → Cond_8591_1_randomlyDuplicate_InvokeMethod1(x1, x3)
Cond_8591_1_randomlyDuplicate_InvokeMethod2(x1, x2, x3) → Cond_8591_1_randomlyDuplicate_InvokeMethod2(x1, x3)
Cond_8591_1_randomlyDuplicate_InvokeMethod3(x1, x2, x3) → Cond_8591_1_randomlyDuplicate_InvokeMethod3(x1, x3)
Cond_7873_1_randomlyDuplicate_InvokeMethod(x1, x2, x3) → Cond_7873_1_randomlyDuplicate_InvokeMethod(x1, x3)

Combined rules. Obtained 6 rules for P and 0 rules for R.

Finished conversion. Obtained 6 rules for P and 0 rules for R. System has no predefined symbols.

Log for SCC 1:

Generated 194 rules for P and 134 rules for R.

Combined rules. Obtained 8 rules for P and 20 rules for R.

Filtered ground terms:

10624_0_createTree_LE(x1, x2, x3, x4) → 10624_0_createTree_LE(x2, x3, x4)
List(x1, x2, x3) → List(x2, x3)
Tree(x1) → Tree
Cond_11302_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_11302_1_createTree_InvokeMethod1(x1, x3, x4)
3384_0_createNode_Return(x1, x2) → 3384_0_createNode_Return
11302_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11302_1_createTree_InvokeMethod(x1, x2, x3, x4)
Cond_11302_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_11302_1_createTree_InvokeMethod(x1, x3, x4)
3032_0_createNode_Return(x1, x2) → 3032_0_createNode_Return
11302_0_createNode_InvokeMethod(x1) → 11302_0_createNode_InvokeMethod
Cond_11286_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5, x6) → Cond_11286_1_createTree_InvokeMethod1(x1, x3, x4)
11286_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11286_1_createTree_InvokeMethod(x1, x2, x3, x4)
Cond_11286_1_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → Cond_11286_1_createTree_InvokeMethod(x1, x3, x4)
Cond_10624_0_createTree_LE1(x1, x2, x3, x4, x5) → Cond_10624_0_createTree_LE1(x1, x3, x4, x5)
11286_0_createNode_InvokeMethod(x1) → 11286_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod(x1) → 11187_0_createNode_InvokeMethod
Cond_10624_0_createTree_LE(x1, x2, x3, x4, x5) → Cond_10624_0_createTree_LE(x1, x3, x4, x5)
3291_0_createNode_InvokeMethod(x1, x2) → 3291_0_createNode_InvokeMethod
java.lang.ArrayIndexOutOfBoundsException(x1) → java.lang.ArrayIndexOutOfBoundsException
java.lang.IndexOutOfBoundsException(x1) → java.lang.IndexOutOfBoundsException
2546_0_random_ArrayAccess(x1, x2, x3) → 2546_0_random_ArrayAccess(x2, x3)
Cond_2908_0_createNode_NE(x1, x2, x3) → Cond_2908_0_createNode_NE(x1, x3)
2908_0_createNode_NE(x1, x2) → 2908_0_createNode_NE(x2)
2636_0_random_IntArithmetic(x1, x2, x3, x4) → 2636_0_random_IntArithmetic(x2, x3)
3660_0_createNode_InvokeMethod(x1, x2) → 3660_0_createNode_InvokeMethod
java.lang.NullPointerException(x1) → java.lang.NullPointerException
3338_0_createNode_InvokeMethod(x1, x2) → 3338_0_createNode_InvokeMethod
11356_0_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → 11356_0_createTree_InvokeMethod(x2, x3, x4, x5)
11338_0_createTree_InvokeMethod(x1, x2, x3, x4, x5, x6) → 11338_0_createTree_InvokeMethod(x2, x3, x4, x5)
11259_0_createTree_InvokeMethod(x1, x2, x3, x4, x5) → 11259_0_createTree_InvokeMethod(x2, x3, x4, x5)
10721_0_createTree_Return(x1) → 10721_0_createTree_Return
11307_0_createNode_InvokeMethod(x1, x2) → 11307_0_createNode_InvokeMethod
11290_0_createNode_InvokeMethod(x1, x2) → 11290_0_createNode_InvokeMethod

Filtered duplicate args:

10624_0_createTree_LE(x1, x2, x3) → 10624_0_createTree_LE(x1, x3)
Cond_10624_0_createTree_LE1(x1, x2, x3, x4) → Cond_10624_0_createTree_LE1(x1, x2, x4)
Cond_10624_0_createTree_LE(x1, x2, x3, x4) → Cond_10624_0_createTree_LE(x1, x2, x4)

Filtered unneeded arguments:

Cond_2908_0_createNode_NE(x1, x2) → Cond_2908_0_createNode_NE(x1)

Filtered all non-integer terms:

10624_0_createTree_LE(x1, x2) → 10624_0_createTree_LE(x2)
List(x1, x2) → List
Cond_10624_0_createTree_LE(x1, x2, x3) → Cond_10624_0_createTree_LE(x1, x3)
11187_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11187_1_createTree_InvokeMethod(x1, x2, x3)
11286_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11286_1_createTree_InvokeMethod(x1, x2, x3)
Cond_10624_0_createTree_LE1(x1, x2, x3) → Cond_10624_0_createTree_LE1(x1, x3)
11302_1_createTree_InvokeMethod(x1, x2, x3, x4) → 11302_1_createTree_InvokeMethod(x1, x2, x3)
11259_0_createTree_InvokeMethod(x1, x2, x3, x4) → 11259_0_createTree_InvokeMethod(x2, x3)
11338_0_createTree_InvokeMethod(x1, x2, x3, x4) → 11338_0_createTree_InvokeMethod(x2, x3)
11356_0_createTree_InvokeMethod(x1, x2, x3, x4) → 11356_0_createTree_InvokeMethod(x2, x3)
2636_0_random_IntArithmetic(x1, x2) → 2636_0_random_IntArithmetic(x2)

Filtered all free variables:

2546_0_random_ArrayAccess(x1, x2) → 2546_0_random_ArrayAccess(x1)
ARRAY(x1, x2) → ARRAY(x1)
2636_0_random_IntArithmetic(x1) → 2636_0_random_IntArithmetic
2908_0_createNode_NE(x1) → 2908_0_createNode_NE

Filtered ground terms:

Cond_2636_1_createNode_InvokeMethod1(x1, x2) → Cond_2636_1_createNode_InvokeMethod1(x1)
2636_1_createNode_InvokeMethod(x1) → 2636_1_createNode_InvokeMethod
Cond_2636_1_createNode_InvokeMethod(x1, x2) → Cond_2636_1_createNode_InvokeMethod(x1)

Combined rules. Obtained 8 rules for P and 18 rules for R.

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

### (5) 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:
none

R is empty.

The integer pair graph contains the following rules and edges:
(0): 11172_0_RANDOMLYDUPLICATE_STORE(java.lang.Object(x0[0])) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x0[0]))
(1): 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[1], java.lang.Object(x1[1])))) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x1[1]))
(2): 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[2], x1[2]))) → 11172_0_RANDOMLYDUPLICATE_STORE(x1[2])
(3): 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(java.lang.Object(x0[3]), x1[3]))) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x0[3]))
(4): 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[4], x1[4]))) → 11172_0_RANDOMLYDUPLICATE_STORE(x0[4])

(0) -> (1), if ((java.lang.Object(x0[0]) →* java.lang.Object(Tree(x0[1], java.lang.Object(x1[1])))))

(0) -> (2), if ((java.lang.Object(x0[0]) →* java.lang.Object(Tree(x0[2], x1[2]))))

(0) -> (3), if ((java.lang.Object(x0[0]) →* java.lang.Object(Tree(java.lang.Object(x0[3]), x1[3]))))

(0) -> (4), if ((java.lang.Object(x0[0]) →* java.lang.Object(Tree(x0[4], x1[4]))))

(1) -> (1), if ((java.lang.Object(x1[1]) →* java.lang.Object(Tree(x0[1]', java.lang.Object(x1[1]')))))

(1) -> (2), if ((java.lang.Object(x1[1]) →* java.lang.Object(Tree(x0[2], x1[2]))))

(1) -> (3), if ((java.lang.Object(x1[1]) →* java.lang.Object(Tree(java.lang.Object(x0[3]), x1[3]))))

(1) -> (4), if ((java.lang.Object(x1[1]) →* java.lang.Object(Tree(x0[4], x1[4]))))

(2) -> (0), if ((x1[2]* java.lang.Object(x0[0])))

(3) -> (1), if ((java.lang.Object(x0[3]) →* java.lang.Object(Tree(x0[1], java.lang.Object(x1[1])))))

(3) -> (2), if ((java.lang.Object(x0[3]) →* java.lang.Object(Tree(x0[2], x1[2]))))

(3) -> (3), if ((java.lang.Object(x0[3]) →* java.lang.Object(Tree(java.lang.Object(x0[3]'), x1[3]'))))

(3) -> (4), if ((java.lang.Object(x0[3]) →* java.lang.Object(Tree(x0[4], x1[4]))))

(4) -> (0), if ((x0[4]* java.lang.Object(x0[0])))

The set Q is empty.

### (6) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

### (7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

11172_0_RANDOMLYDUPLICATE_STORE(java.lang.Object(x0[0])) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x0[0]))
7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[1], java.lang.Object(x1[1])))) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x1[1]))
7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[2], x1[2]))) → 11172_0_RANDOMLYDUPLICATE_STORE(x1[2])
7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(java.lang.Object(x0[3]), x1[3]))) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x0[3]))
7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[4], x1[4]))) → 11172_0_RANDOMLYDUPLICATE_STORE(x0[4])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

### (8) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• 11172_0_RANDOMLYDUPLICATE_STORE(java.lang.Object(x0[0])) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x0[0]))
The graph contains the following edges 1 >= 1

• 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[2], x1[2]))) → 11172_0_RANDOMLYDUPLICATE_STORE(x1[2])
The graph contains the following edges 1 > 1

• 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[4], x1[4]))) → 11172_0_RANDOMLYDUPLICATE_STORE(x0[4])
The graph contains the following edges 1 > 1

• 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(x0[1], java.lang.Object(x1[1])))) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x1[1]))
The graph contains the following edges 1 > 1

• 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(Tree(java.lang.Object(x0[3]), x1[3]))) → 7873_1_RANDOMLYDUPLICATE_INVOKEMETHOD(java.lang.Object(x0[3]))
The graph contains the following edges 1 > 1

### (10) 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

The ITRS R consists of the following rules:
11187_0_createNode_InvokeMethod11290_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod11307_0_createNode_InvokeMethod
10624_0_createTree_LE(0) → 10721_0_createTree_Return
11187_0_createNode_InvokeMethod2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))
11187_1_createTree_InvokeMethod(3291_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11187_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11187_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11338_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11338_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11356_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11356_0_createTree_InvokeMethod(x0, x1)
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3338_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3291_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3660_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3032_0_createNode_Return
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3384_0_createNode_Return

The integer pair graph contains the following rules and edges:
(0): 10624_0_CREATETREE_LE(x2[0]) → COND_10624_0_CREATETREE_LE(x2[0] > 0, x2[0])
(1): COND_10624_0_CREATETREE_LE(TRUE, x2[1]) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])
(2): 11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])
(3): 10624_0_CREATETREE_LE(x1[3]) → COND_10624_0_CREATETREE_LE1(x1[3] > 0, x1[3])
(4): COND_10624_0_CREATETREE_LE1(TRUE, x1[4]) → 10624_0_CREATETREE_LE(x1[4] + -1)
(5): 11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5]) → COND_11286_1_CREATETREE_INVOKEMETHOD(x1[5] > 0, 3032_0_createNode_Return, x0[5], x1[5])
(6): COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6]) → 10624_0_CREATETREE_LE(x1[6] + -1)
(7): 11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7]) → COND_11286_1_CREATETREE_INVOKEMETHOD1(x1[7] > 0, 3384_0_createNode_Return, x0[7], x1[7])
(8): COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8]) → 10624_0_CREATETREE_LE(x1[8] + -1)
(9): 11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])

(0) -> (1), if ((x2[0] > 0* TRUE)∧(x2[0]* x2[1]))

(1) -> (2), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x1[1]* x0[2])∧(x2[1]* x1[2]))

(1) -> (9), if ((11187_0_createNode_InvokeMethod* 3384_0_createNode_Return)∧(x1[1]* x0[9])∧(x2[1]* x1[9]))

(2) -> (5), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x0[2]* x0[5])∧(x1[2]* x1[5]))

(2) -> (7), if ((11187_0_createNode_InvokeMethod* 3384_0_createNode_Return)∧(x0[2]* x0[7])∧(x1[2]* x1[7]))

(3) -> (4), if ((x1[3] > 0* TRUE)∧(x1[3]* x1[4]))

(4) -> (0), if ((x1[4] + -1* x2[0]))

(4) -> (3), if ((x1[4] + -1* x1[3]))

(5) -> (6), if ((x1[5] > 0* TRUE)∧(x0[5]* x0[6])∧(x1[5]* x1[6]))

(6) -> (0), if ((x1[6] + -1* x2[0]))

(6) -> (3), if ((x1[6] + -1* x1[3]))

(7) -> (8), if ((x1[7] > 0* TRUE)∧(x0[7]* x0[8])∧(x1[7]* x1[8]))

(8) -> (0), if ((x1[8] + -1* x2[0]))

(8) -> (3), if ((x1[8] + -1* x1[3]))

(9) -> (5), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x0[9]* x0[5])∧(x1[9]* x1[5]))

(9) -> (7), if ((11187_0_createNode_InvokeMethod* 3384_0_createNode_Return)∧(x0[9]* x0[7])∧(x1[9]* x1[7]))

The set Q consists of the following terms:
11187_0_createNode_InvokeMethod
10624_0_createTree_LE(0)
11187_1_createTree_InvokeMethod(3291_0_createNode_InvokeMethod, x0, x1)
11187_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1)
11187_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1)
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))

### (11) IDPNonInfProof (SOUND transformation)

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 10624_0_CREATETREE_LE(x2) → COND_10624_0_CREATETREE_LE(>(x2, 0), x2) the following chains were created:
• We consider the chain 10624_0_CREATETREE_LE(x2[0]) → COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0]), COND_10624_0_CREATETREE_LE(TRUE, x2[1]) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1]) which results in the following constraint:

(1)    (>(x2[0], 0)=TRUEx2[0]=x2[1]10624_0_CREATETREE_LE(x2[0])≥NonInfC∧10624_0_CREATETREE_LE(x2[0])≥COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])∧(UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:

(2)    (>(x2[0], 0)=TRUE10624_0_CREATETREE_LE(x2[0])≥NonInfC∧10624_0_CREATETREE_LE(x2[0])≥COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])∧(UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(3)    (x2[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(2)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(4)    (x2[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(2)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(5)    (x2[0] + [-1] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(2)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(6)    (x2[0] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(4)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

For Pair COND_10624_0_CREATETREE_LE(TRUE, x2) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1, x2) the following chains were created:
• We consider the chain COND_10624_0_CREATETREE_LE(TRUE, x2[1]) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1]) which results in the following constraint:

(7)    (COND_10624_0_CREATETREE_LE(TRUE, x2[1])≥NonInfC∧COND_10624_0_CREATETREE_LE(TRUE, x2[1])≥11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])∧(UIncreasing(11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(8)    ((UIncreasing(11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(9)    ((UIncreasing(11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(10)    ((UIncreasing(11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧[(-1)bso_40] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(11)    ((UIncreasing(11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)

For Pair 11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0, x1) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0, x1) the following chains were created:
• We consider the chain 11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2]) which results in the following constraint:

(12)    (11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2])≥NonInfC∧11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2])≥11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])∧(UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(13)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧[(-1)bso_42] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(14)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧[(-1)bso_42] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(15)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧[(-1)bso_42] ≥ 0)

We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(16)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)

For Pair 10624_0_CREATETREE_LE(x1) → COND_10624_0_CREATETREE_LE1(>(x1, 0), x1) the following chains were created:
• We consider the chain 10624_0_CREATETREE_LE(x1[3]) → COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3]), COND_10624_0_CREATETREE_LE1(TRUE, x1[4]) → 10624_0_CREATETREE_LE(+(x1[4], -1)) which results in the following constraint:

(17)    (>(x1[3], 0)=TRUEx1[3]=x1[4]10624_0_CREATETREE_LE(x1[3])≥NonInfC∧10624_0_CREATETREE_LE(x1[3])≥COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])∧(UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥))

We simplified constraint (17) using rule (IV) which results in the following new constraint:

(18)    (>(x1[3], 0)=TRUE10624_0_CREATETREE_LE(x1[3])≥NonInfC∧10624_0_CREATETREE_LE(x1[3])≥COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])∧(UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(19)    (x1[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(2)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(20)    (x1[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(2)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(21)    (x1[3] + [-1] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(2)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)

We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(22)    (x1[3] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(4)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)

For Pair COND_10624_0_CREATETREE_LE1(TRUE, x1) → 10624_0_CREATETREE_LE(+(x1, -1)) the following chains were created:
• We consider the chain COND_10624_0_CREATETREE_LE1(TRUE, x1[4]) → 10624_0_CREATETREE_LE(+(x1[4], -1)) which results in the following constraint:

(23)    (COND_10624_0_CREATETREE_LE1(TRUE, x1[4])≥NonInfC∧COND_10624_0_CREATETREE_LE1(TRUE, x1[4])≥10624_0_CREATETREE_LE(+(x1[4], -1))∧(UIncreasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(24)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧[(-1)bso_46] ≥ 0)

We simplified constraint (24) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(25)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧[(-1)bso_46] ≥ 0)

We simplified constraint (25) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(26)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧[(-1)bso_46] ≥ 0)

We simplified constraint (26) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(27)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)

For Pair 11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0, x1) → COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1, 0), 3032_0_createNode_Return, x0, x1) the following chains were created:
• We consider the chain 11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5]) → COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5]), COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6]) → 10624_0_CREATETREE_LE(+(x1[6], -1)) which results in the following constraint:

(28)    (>(x1[5], 0)=TRUEx0[5]=x0[6]x1[5]=x1[6]11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5])≥NonInfC∧11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5])≥COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])∧(UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥))

We simplified constraint (28) using rule (IV) which results in the following new constraint:

(29)    (>(x1[5], 0)=TRUE11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5])≥NonInfC∧11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5])≥COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])∧(UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥))

We simplified constraint (29) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(30)    (x1[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥)∧[bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (30) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(31)    (x1[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥)∧[bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (31) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(32)    (x1[5] + [-1] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥)∧[bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(33)    (x1[5] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥)∧[(3)bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)

For Pair COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0, x1) → 10624_0_CREATETREE_LE(+(x1, -1)) the following chains were created:
• We consider the chain COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6]) → 10624_0_CREATETREE_LE(+(x1[6], -1)) which results in the following constraint:

(34)    (COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6])≥NonInfC∧COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6])≥10624_0_CREATETREE_LE(+(x1[6], -1))∧(UIncreasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥))

We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(35)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧[1 + (-1)bso_50] ≥ 0)

We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(36)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧[1 + (-1)bso_50] ≥ 0)

We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(37)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧[1 + (-1)bso_50] ≥ 0)

We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(38)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

For Pair 11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0, x1) → COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1, 0), 3384_0_createNode_Return, x0, x1) the following chains were created:
• We consider the chain 11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7]) → COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7]), COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8]) → 10624_0_CREATETREE_LE(+(x1[8], -1)) which results in the following constraint:

(39)    (>(x1[7], 0)=TRUEx0[7]=x0[8]x1[7]=x1[8]11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7])≥NonInfC∧11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7])≥COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])∧(UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥))

We simplified constraint (39) using rule (IV) which results in the following new constraint:

(40)    (>(x1[7], 0)=TRUE11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7])≥NonInfC∧11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7])≥COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])∧(UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥))

We simplified constraint (40) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(41)    (x1[7] + [-1] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)

We simplified constraint (41) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(42)    (x1[7] + [-1] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)

We simplified constraint (42) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(43)    (x1[7] + [-1] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥)∧[bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)

We simplified constraint (43) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

(44)    (x1[7] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥)∧[(3)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)

For Pair COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0, x1) → 10624_0_CREATETREE_LE(+(x1, -1)) the following chains were created:
• We consider the chain COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8]) → 10624_0_CREATETREE_LE(+(x1[8], -1)) which results in the following constraint:

(45)    (COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8])≥NonInfC∧COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8])≥10624_0_CREATETREE_LE(+(x1[8], -1))∧(UIncreasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥))

We simplified constraint (45) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(46)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧[(-1)bso_54] ≥ 0)

We simplified constraint (46) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(47)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧[(-1)bso_54] ≥ 0)

We simplified constraint (47) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(48)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧[(-1)bso_54] ≥ 0)

We simplified constraint (48) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(49)    ((UIncreasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧0 = 0∧[(-1)bso_54] ≥ 0)

For Pair 11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0, x1) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0, x1) the following chains were created:
• We consider the chain 11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9]) which results in the following constraint:

(50)    (11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9])≥NonInfC∧11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9])≥11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])∧(UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

(51)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧[(-1)bso_56] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

(52)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧[(-1)bso_56] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

(53)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧[(-1)bso_56] ≥ 0)

We simplified constraint (53) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

(54)    ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 0)

To summarize, we get the following constraints P for the following pairs.
• 10624_0_CREATETREE_LE(x2) → COND_10624_0_CREATETREE_LE(>(x2, 0), x2)
• (x2[0] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])), ≥)∧[(4)bni_37 + (-1)Bound*bni_37] + [(2)bni_37]x2[0] ≥ 0∧[1 + (-1)bso_38] ≥ 0)

• COND_10624_0_CREATETREE_LE(TRUE, x2) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1, x2)
• ((UIncreasing(11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])), ≥)∧0 = 0∧[(-1)bso_40] ≥ 0)

• 11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0, x1) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0, x1)
• ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])), ≥)∧0 = 0∧[(-1)bso_42] ≥ 0)

• 10624_0_CREATETREE_LE(x1) → COND_10624_0_CREATETREE_LE1(>(x1, 0), x1)
• (x1[3] ≥ 0 ⇒ (UIncreasing(COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])), ≥)∧[(4)bni_43 + (-1)Bound*bni_43] + [(2)bni_43]x1[3] ≥ 0∧[2 + (-1)bso_44] ≥ 0)

• COND_10624_0_CREATETREE_LE1(TRUE, x1) → 10624_0_CREATETREE_LE(+(x1, -1))
• ((UIncreasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥)∧0 = 0∧[(-1)bso_46] ≥ 0)

• 11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0, x1) → COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1, 0), 3032_0_createNode_Return, x0, x1)
• (x1[5] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])), ≥)∧[(3)bni_47 + (-1)Bound*bni_47] + [(2)bni_47]x1[5] ≥ 0∧[(-1)bso_48] ≥ 0)

• COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0, x1) → 10624_0_CREATETREE_LE(+(x1, -1))
• ((UIncreasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥)∧0 = 0∧[1 + (-1)bso_50] ≥ 0)

• 11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0, x1) → COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1, 0), 3384_0_createNode_Return, x0, x1)
• (x1[7] ≥ 0 ⇒ (UIncreasing(COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])), ≥)∧[(3)bni_51 + (-1)Bound*bni_51] + [(2)bni_51]x1[7] ≥ 0∧[1 + (-1)bso_52] ≥ 0)

• COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0, x1) → 10624_0_CREATETREE_LE(+(x1, -1))
• ((UIncreasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥)∧0 = 0∧[(-1)bso_54] ≥ 0)

• 11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0, x1) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0, x1)
• ((UIncreasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 0)

The constraints for P> respective Pbound 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 Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(11187_0_createNode_InvokeMethod) = [-1]
POL(11290_0_createNode_InvokeMethod) = [-1]
POL(11307_0_createNode_InvokeMethod) = [-1]
POL(10624_0_createTree_LE(x1)) = [-1]
POL(0) = 0
POL(10721_0_createTree_Return) = [-1]
POL(2546_1_createNode_InvokeMethod(x1)) = [-1]
POL(2546_0_random_ArrayAccess(x1)) = [-1]
POL(java.lang.Object(x1)) = [-1]
POL(ARRAY(x1)) = [-1]
POL(11187_1_createTree_InvokeMethod(x1, x2, x3)) = [-1]
POL(3291_0_createNode_InvokeMethod) = [-1]
POL(11259_0_createTree_InvokeMethod(x1, x2)) = [-1]
POL(3338_0_createNode_InvokeMethod) = [-1]
POL(3660_0_createNode_InvokeMethod) = [-1]
POL(11286_1_createTree_InvokeMethod(x1, x2, x3)) = [-1]
POL(11338_0_createTree_InvokeMethod(x1, x2)) = [-1]
POL(11356_0_createTree_InvokeMethod(x1, x2)) = [-1]
POL(3032_0_createNode_Return) = [-1]
POL(3384_0_createNode_Return) = [-1]
POL(10624_0_CREATETREE_LE(x1)) = [2] + [2]x1
POL(COND_10624_0_CREATETREE_LE(x1, x2)) = [1] + [2]x2
POL(>(x1, x2)) = [-1]
POL(11187_1_CREATETREE_INVOKEMETHOD(x1, x2, x3)) = [1] + [2]x3
POL(11286_1_CREATETREE_INVOKEMETHOD(x1, x2, x3)) = [1] + [2]x3
POL(COND_10624_0_CREATETREE_LE1(x1, x2)) = [2]x2
POL(+(x1, x2)) = x1 + x2
POL(-1) = [-1]
POL(COND_11286_1_CREATETREE_INVOKEMETHOD(x1, x2, x3, x4)) = [1] + [2]x4
POL(COND_11286_1_CREATETREE_INVOKEMETHOD1(x1, x2, x3, x4)) = [2]x4

The following pairs are in P>:

10624_0_CREATETREE_LE(x2[0]) → COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])
10624_0_CREATETREE_LE(x1[3]) → COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])
COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6]) → 10624_0_CREATETREE_LE(+(x1[6], -1))
11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7]) → COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])

The following pairs are in Pbound:

10624_0_CREATETREE_LE(x2[0]) → COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])
10624_0_CREATETREE_LE(x1[3]) → COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])
11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5]) → COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])
11286_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[7], x1[7]) → COND_11286_1_CREATETREE_INVOKEMETHOD1(>(x1[7], 0), 3384_0_createNode_Return, x0[7], x1[7])

The following pairs are in P:

COND_10624_0_CREATETREE_LE(TRUE, x2[1]) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])
11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])
COND_10624_0_CREATETREE_LE1(TRUE, x1[4]) → 10624_0_CREATETREE_LE(+(x1[4], -1))
11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5]) → COND_11286_1_CREATETREE_INVOKEMETHOD(>(x1[5], 0), 3032_0_createNode_Return, x0[5], x1[5])
COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8]) → 10624_0_CREATETREE_LE(+(x1[8], -1))
11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])

There are no usable rules.

### (13) 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

The ITRS R consists of the following rules:
11187_0_createNode_InvokeMethod11290_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod11307_0_createNode_InvokeMethod
10624_0_createTree_LE(0) → 10721_0_createTree_Return
11187_0_createNode_InvokeMethod2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))
11187_1_createTree_InvokeMethod(3291_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11187_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11187_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11338_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11338_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11356_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11356_0_createTree_InvokeMethod(x0, x1)
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3338_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3291_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3660_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3032_0_createNode_Return
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3384_0_createNode_Return

The integer pair graph contains the following rules and edges:
(1): COND_10624_0_CREATETREE_LE(TRUE, x2[1]) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])
(2): 11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])
(4): COND_10624_0_CREATETREE_LE1(TRUE, x1[4]) → 10624_0_CREATETREE_LE(x1[4] + -1)
(5): 11286_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[5], x1[5]) → COND_11286_1_CREATETREE_INVOKEMETHOD(x1[5] > 0, 3032_0_createNode_Return, x0[5], x1[5])
(8): COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8]) → 10624_0_CREATETREE_LE(x1[8] + -1)
(9): 11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])

(1) -> (2), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x1[1]* x0[2])∧(x2[1]* x1[2]))

(2) -> (5), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x0[2]* x0[5])∧(x1[2]* x1[5]))

(9) -> (5), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x0[9]* x0[5])∧(x1[9]* x1[5]))

(1) -> (9), if ((11187_0_createNode_InvokeMethod* 3384_0_createNode_Return)∧(x1[1]* x0[9])∧(x2[1]* x1[9]))

The set Q consists of the following terms:
11187_0_createNode_InvokeMethod
10624_0_createTree_LE(0)
11187_1_createTree_InvokeMethod(3291_0_createNode_InvokeMethod, x0, x1)
11187_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1)
11187_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1)
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))

### (14) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.

### (16) 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

The ITRS R consists of the following rules:
11187_0_createNode_InvokeMethod11290_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod11307_0_createNode_InvokeMethod
10624_0_createTree_LE(0) → 10721_0_createTree_Return
11187_0_createNode_InvokeMethod2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))
11187_1_createTree_InvokeMethod(3291_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11187_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11187_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11259_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11338_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11338_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1) → 11356_0_createTree_InvokeMethod(x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1) → 11356_0_createTree_InvokeMethod(x0, x1)
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3338_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3291_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3660_0_createNode_InvokeMethod
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3032_0_createNode_Return
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0)))) → 3384_0_createNode_Return

The integer pair graph contains the following rules and edges:
(1): COND_10624_0_CREATETREE_LE(TRUE, x2[1]) → 11187_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x1[1], x2[1])
(2): 11187_1_CREATETREE_INVOKEMETHOD(3032_0_createNode_Return, x0[2], x1[2]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[2], x1[2])
(4): COND_10624_0_CREATETREE_LE1(TRUE, x1[4]) → 10624_0_CREATETREE_LE(x1[4] + -1)
(6): COND_11286_1_CREATETREE_INVOKEMETHOD(TRUE, 3032_0_createNode_Return, x0[6], x1[6]) → 10624_0_CREATETREE_LE(x1[6] + -1)
(8): COND_11286_1_CREATETREE_INVOKEMETHOD1(TRUE, 3384_0_createNode_Return, x0[8], x1[8]) → 10624_0_CREATETREE_LE(x1[8] + -1)
(9): 11187_1_CREATETREE_INVOKEMETHOD(3384_0_createNode_Return, x0[9], x1[9]) → 11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])

(1) -> (2), if ((11187_0_createNode_InvokeMethod* 3032_0_createNode_Return)∧(x1[1]* x0[2])∧(x2[1]* x1[2]))

(1) -> (9), if ((11187_0_createNode_InvokeMethod* 3384_0_createNode_Return)∧(x1[1]* x0[9])∧(x2[1]* x1[9]))

The set Q consists of the following terms:
11187_0_createNode_InvokeMethod
10624_0_createTree_LE(0)
11187_1_createTree_InvokeMethod(3291_0_createNode_InvokeMethod, x0, x1)
11187_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1)
11187_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1)
11286_1_createTree_InvokeMethod(3338_0_createNode_InvokeMethod, x0, x1)
11286_1_createTree_InvokeMethod(3660_0_createNode_InvokeMethod, x0, x1)
2546_1_createNode_InvokeMethod(2546_0_random_ArrayAccess(java.lang.Object(ARRAY(x0))))

### (17) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.