Termination proof of /tmp/tmpaxUkB8/DuplicateNodes.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇒)

↳2 JBCTerminationGraph

↳3 FIGtoITRSProof (⇒)

↳4 AND

    ↳5 IDP

        ↳6 IDPtoQDPProof (⇒)

        ↳7 QDP

        ↳8 QDPSizeChangeProof (⇔)

        ↳9 YES

    ↳10 IDP

        ↳11 IDPNonInfProof (⇒)

        ↳12 AND

            ↳13 IDP

                ↳14 IDependencyGraphProof (⇔)

                ↳15 TRUE

            ↳16 IDP

                ↳17 IDependencyGraphProof (⇔)

                ↳18 TRUE

(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.

(4) Complex Obligation (AND)

(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

(9) YES

(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_InvokeMethod → 11290_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod → 11307_0_createNode_InvokeMethod
10624_0_createTree_LE(0) → 10721_0_createTree_Return
11187_0_createNode_InvokeMethod → 2546_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)=TRUE∧x2[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])∧(U^Increasing(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)=TRUE ⇒ 10624_0_CREATETREE_LE(x2[0])≥NonInfC∧10624_0_CREATETREE_LE(x2[0])≥COND_10624_0_CREATETREE_LE(>(x2[0], 0), x2[0])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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])∧(U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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])∧(U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)=TRUE∧x1[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])∧(U^Increasing(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)=TRUE ⇒ 10624_0_CREATETREE_LE(x1[3])≥NonInfC∧10624_0_CREATETREE_LE(x1[3])≥COND_10624_0_CREATETREE_LE1(>(x1[3], 0), x1[3])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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))∧(U^Increasing(10624_0_CREATETREE_LE(+(x1[4], -1))), ≥))

We simplified constraint (23) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(24)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)=TRUE∧x0[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])∧(U^Increasing(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)=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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))∧(U^Increasing(10624_0_CREATETREE_LE(+(x1[6], -1))), ≥))

We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(35)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)=TRUE∧x0[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])∧(U^Increasing(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)=TRUE ⇒ 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])∧(U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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 ⇒ (U^Increasing(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))∧(U^Increasing(10624_0_CREATETREE_LE(+(x1[8], -1))), ≥))

We simplified constraint (45) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(46)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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])∧(U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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)    ((U^Increasing(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 ⇒ (U^Increasing(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)
- ((U^Increasing(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)
- ((U^Increasing(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 ⇒ (U^Increasing(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))
- ((U^Increasing(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 ⇒ (U^Increasing(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))
- ((U^Increasing(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 ⇒ (U^Increasing(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))
- ((U^Increasing(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)
- ((U^Increasing(11286_1_CREATETREE_INVOKEMETHOD(11187_0_createNode_InvokeMethod, x0[9], x1[9])), ≥)∧0 = 0∧[(-1)bso_56] ≥ 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(11187_0_createNode_InvokeMethod) = [-1]
POL(11290_0_createNode_InvokeMethod) = [-1]
POL(11307_0_createNode_InvokeMethod) = [-1]
POL(10624_0_createTree_LE(x₁)) = [-1]
POL(0) = 0
POL(10721_0_createTree_Return) = [-1]
POL(2546_1_createNode_InvokeMethod(x₁)) = [-1]
POL(2546_0_random_ArrayAccess(x₁)) = [-1]
POL(java.lang.Object(x₁)) = [-1]
POL(ARRAY(x₁)) = [-1]
POL(11187_1_createTree_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(3291_0_createNode_InvokeMethod) = [-1]
POL(11259_0_createTree_InvokeMethod(x₁, x₂)) = [-1]
POL(3338_0_createNode_InvokeMethod) = [-1]
POL(3660_0_createNode_InvokeMethod) = [-1]
POL(11286_1_createTree_InvokeMethod(x₁, x₂, x₃)) = [-1]
POL(11338_0_createTree_InvokeMethod(x₁, x₂)) = [-1]
POL(11356_0_createTree_InvokeMethod(x₁, x₂)) = [-1]
POL(3032_0_createNode_Return) = [-1]
POL(3384_0_createNode_Return) = [-1]
POL(10624_0_CREATETREE_LE(x₁)) = [2] + [2]x₁
POL(COND_10624_0_CREATETREE_LE(x₁, x₂)) = [1] + [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(11187_1_CREATETREE_INVOKEMETHOD(x₁, x₂, x₃)) = [1] + [2]x₃
POL(11286_1_CREATETREE_INVOKEMETHOD(x₁, x₂, x₃)) = [1] + [2]x₃
POL(COND_10624_0_CREATETREE_LE1(x₁, x₂)) = [2]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(COND_11286_1_CREATETREE_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [1] + [2]x₄
POL(COND_11286_1_CREATETREE_INVOKEMETHOD1(x₁, x₂, x₃, x₄)) = [2]x₄

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 P_bound:

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.

(12) Complex Obligation (AND)

(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_InvokeMethod → 11290_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod → 11307_0_createNode_InvokeMethod
10624_0_createTree_LE(0) → 10721_0_createTree_Return
11187_0_createNode_InvokeMethod → 2546_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]))

(14) IDependencyGraphProof (EQUIVALENT transformation)

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

(15) TRUE

(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_InvokeMethod → 11290_0_createNode_InvokeMethod
11187_0_createNode_InvokeMethod → 11307_0_createNode_InvokeMethod
10624_0_createTree_LE(0) → 10721_0_createTree_Return
11187_0_createNode_InvokeMethod → 2546_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]))

(17) IDependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) JBC2FIG (SOUND transformation)

(2) Obligation:

(3) FIGtoITRSProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) IDPtoQDPProof (SOUND transformation)

(7) Obligation:

(8) QDPSizeChangeProof (EQUIVALENT transformation)

(9) YES

(10) Obligation:

(11) IDPNonInfProof (SOUND transformation)

(12) Complex Obligation (AND)

(13) Obligation:

(14) IDependencyGraphProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) IDependencyGraphProof (EQUIVALENT transformation)

(18) TRUE