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 UsableRulesProof (⇔)
        ↳9 QDP
        ↳10 QReductionProof (⇔)
        ↳11 QDP
        ↳12 MRRProof (⇔)
        ↳13 QDP
        ↳14 DependencyGraphProof (⇔)
        ↳15 QDP
        ↳16 QDPSizeChangeProof (⇔)
        ↳17 YES
    ↳18 IDP
        ↳19 IDPtoQDPProof (⇒)
        ↳20 QDP
        ↳21 UsableRulesProof (⇔)
        ↳22 QDP
        ↳23 QReductionProof (⇔)
        ↳24 QDP
        ↳25 QDPQMonotonicMRRProof (⇔)
        ↳26 QDP
        ↳27 DependencyGraphProof (⇔)
        ↳28 QDP
        ↳29 QDPOrderProof (⇔)
        ↳30 QDP
        ↳31 DependencyGraphProof (⇔)
        ↳32 TRUE
    ↳33 IDP
        ↳34 IDPNonInfProof (⇒)
        ↳35 IDP
        ↳36 IDependencyGraphProof (⇔)
        ↳37 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Count 
public class Count {
  public static void main(String[] args) {
    Random.args = args;
    Tree tree = Tree.createTree();

    int c = count(tree);
  }

  public static Tree flatten(Tree start) {
    Tree result = null;
    Tree s,t,u;

    while (start != null) {

      if (start.left == null) {

        result = new Tree(null,result);
        start = start.right;
      }
      else {
        s = start.left.left;
        t = start.left.right;
        u = start.right;
        start = new Tree(s, new Tree(t,u));



      }
    }

    return result;
  }


  public static int count(Tree start) {

    int res = 0;

    while (start != null) {

      if (start.left == null) {

        res++;
        start = start.right;
      }
      else {
        start = flatten(start);    

      }
    }

    return res;
  }
}


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() {
    Tree result = new Tree();
    result.value = new Object();
    return result;
  }

  public static Tree createTree() {
    int counter = Random.random();
    if (counter == 0) {
      return null;
    }
    Tree result = createNode();
    Tree t = result;

    while (counter > 0) {
      int branch = Random.random();
      if (branch > 0) {
        if (t.left == null) {
          t.left = createNode();
          t = result;
        } else {
          t = t.left;
        }
      } else {
        if (t.right == null) {
          t.right = createNode();
          t = result;
        } else {
          t = t.right;
        }
      }
      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:
Count.main([Ljava/lang/String;)V: Graph of 55 nodes with 0 SCCs.

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

Count.count(LTree;)I: Graph of 50 nodes with 1 SCC.

Count.flatten(LTree;)LTree;: Graph of 195 nodes with 1 SCC.


(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 196 rules for P and 3 rules for R.


Combined rules. Obtained 16 rules for P and 1 rules for R.


Filtered ground terms:


24307_0_flatten_Store(x1, x2, x3) → 24307_0_flatten_Store(x2, x3)
Tree(x1, x2, x3) → Tree(x2, x3)
14185_0_flatten_NULL(x1, x2, x3, x4) → 14185_0_flatten_NULL(x2, x3, x4)
22994_0_flatten_Store(x1, x2, x3, x4, x5) → 22994_0_flatten_Store(x2, x3, x4, x5)
22978_0_flatten_Store(x1, x2, x3, x4, x5) → 22978_0_flatten_Store(x2, x3, x4, x5)
24360_0_flatten_Store(x1, x2, x3) → 24360_0_flatten_Store(x2, x3)
23618_0_flatten_Store(x1, x2, x3, x4, x5) → 23618_0_flatten_Store(x2, x3, x4, x5)
23578_0_flatten_Store(x1, x2, x3, x4, x5) → 23578_0_flatten_Store(x2, x3, x4, x5)
23897_0_flatten_Store(x1, x2, x3, x4, x5) → 23897_0_flatten_Store(x2, x3, x4, x5)
14759_0_flatten_Return(x1, x2) → 14759_0_flatten_Return(x2)

Filtered duplicate args:


14185_0_flatten_NULL(x1, x2, x3) → 14185_0_flatten_NULL(x2, x3)

Finished conversion. Obtained 16 rules for P and 1 rules for R. System has no predefined symbols.



Log for SCC 1:

Generated 42 rules for P and 211 rules for R.


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


Filtered ground terms:


7947_0_count_Store(x1, x2) → 7947_0_count_Store(x2)
6201_0_count_NULL(x1, x2, x3) → 6201_0_count_NULL(x2, x3)
Tree(x1, x2, x3) → Tree(x2, x3)
14759_0_flatten_Return(x1, x2) → 14759_0_flatten_Return(x2)
7665_0_flatten_ConstantStackPush(x1, x2) → 7665_0_flatten_ConstantStackPush(x2)
7650_0_flatten_ConstantStackPush(x1, x2) → 7650_0_flatten_ConstantStackPush(x2)
14185_0_flatten_NULL(x1, x2, x3, x4) → 14185_0_flatten_NULL(x2, x3, x4)
22780_0_flatten_FieldAccess(x1, x2, x3, x4, x5) → 22780_0_flatten_FieldAccess(x2, x3, x4, x5)
23249_0_flatten_FieldAccess(x1, x2, x3, x4, x5) → 23249_0_flatten_FieldAccess(x2, x3, x4, x5)
23897_0_flatten_Store(x1, x2, x3, x4, x5) → 23897_0_flatten_Store(x2, x3, x4, x5)
23578_0_flatten_Store(x1, x2, x3, x4, x5) → 23578_0_flatten_Store(x2, x3, x4, x5)
22978_0_flatten_Store(x1, x2, x3, x4, x5) → 22978_0_flatten_Store(x2, x3, x4, x5)
24267_0_flatten_FieldAccess(x1, x2, x3) → 24267_0_flatten_FieldAccess(x2, x3)
24360_0_flatten_Store(x1, x2, x3) → 24360_0_flatten_Store(x2, x3)
6394_0_count_Return(x1) → 6394_0_count_Return

Filtered duplicate args:


6201_0_count_NULL(x1, x2) → 6201_0_count_NULL(x2)
14185_0_flatten_NULL(x1, x2, x3) → 14185_0_flatten_NULL(x2, x3)

Finished conversion. Obtained 7 rules for P and 20 rules for R. System has no predefined symbols.



Log for SCC 2:

Generated 257 rules for P and 74 rules for R.


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


Filtered ground terms:


Tree(x1, x2, x3) → Tree(x2, x3)
29267_0_random_ArrayAccess(x1, x2, x3) → 29267_0_random_ArrayAccess(x2, x3)
29429_0_random_IntArithmetic(x1, x2, x3, x4) → 29429_0_random_IntArithmetic(x2, x3)
Cond_29429_1_createTree_InvokeMethod9(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod9(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod2(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod2(x1, x2, x3)

Filtered all non-integer terms:


29267_1_createTree_InvokeMethod(x1, x2, x3, x4) → 29267_1_createTree_InvokeMethod(x1, x2)
Cond_29267_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_29267_1_createTree_InvokeMethod(x1, x2, x3)
29429_1_createTree_InvokeMethod(x1, x2, x3, x4) → 29429_1_createTree_InvokeMethod(x1, x2)
29429_0_random_IntArithmetic(x1, x2) → 29429_0_random_IntArithmetic(x2)
Tree(x1, x2) → Tree
Cond_29429_1_createTree_InvokeMethod(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod1(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod1(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod3(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod3(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod4(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod4(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod5(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod5(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod6(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod6(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod7(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod7(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod8(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod8(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod10(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod10(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod11(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod11(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod12(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod12(x1, x2, x3)
Cond_29429_1_createTree_InvokeMethod13(x1, x2, x3, x4, x5) → Cond_29429_1_createTree_InvokeMethod13(x1, x2, x3)

Filtered all free variables:


29429_1_createTree_InvokeMethod(x1, x2) → 29429_1_createTree_InvokeMethod(x2)
Cond_29429_1_createTree_InvokeMethod(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod(x1, x3)
29267_1_createTree_InvokeMethod(x1, x2) → 29267_1_createTree_InvokeMethod(x2)
Cond_29429_1_createTree_InvokeMethod1(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod1(x1, x3)
Cond_29429_1_createTree_InvokeMethod2(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod2(x1, x3)
Cond_29429_1_createTree_InvokeMethod3(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod3(x1, x3)
Cond_29429_1_createTree_InvokeMethod4(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod4(x1, x3)
Cond_29429_1_createTree_InvokeMethod5(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod5(x1, x3)
Cond_29429_1_createTree_InvokeMethod6(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod6(x1, x3)
Cond_29429_1_createTree_InvokeMethod7(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod7(x1, x3)
Cond_29429_1_createTree_InvokeMethod8(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod8(x1, x3)
Cond_29429_1_createTree_InvokeMethod9(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod9(x1, x3)
Cond_29429_1_createTree_InvokeMethod10(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod10(x1, x3)
Cond_29429_1_createTree_InvokeMethod11(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod11(x1, x3)
Cond_29429_1_createTree_InvokeMethod12(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod12(x1, x3)
Cond_29429_1_createTree_InvokeMethod13(x1, x2, x3) → Cond_29429_1_createTree_InvokeMethod13(x1, x3)
Cond_29267_1_createTree_InvokeMethod(x1, x2, x3) → Cond_29267_1_createTree_InvokeMethod(x1, x3)

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


Finished conversion. Obtained 1 rules for P and 0 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


The ITRS R consists of the following rules:
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The integer pair graph contains the following rules and edges:
(0): 23897_0_FLATTEN_STORE(x0[0], x1[0], x2[0], x3[0]) → 14185_0_FLATTEN_NULL(x0[0], java.lang.Object(Tree(x1[0], java.lang.Object(Tree(x2[0], x3[0])))))
(1): 14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(java.lang.Object(Tree(x0[1], x1[1])), x2[1]))) → 14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(x0[1], java.lang.Object(Tree(x1[1], x2[1])))))
(2): 14185_0_FLATTEN_NULL(x3[2], java.lang.Object(Tree(java.lang.Object(Tree(x0[2], x1[2])), x2[2]))) → 23897_0_FLATTEN_STORE(x3[2], x0[2], x1[2], x2[2])
(3): 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])
(4): 14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
(5): 14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])

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


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


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


(0) -> (5), if ((x0[0] →* x1[5])∧(java.lang.Object(Tree(x1[0], java.lang.Object(Tree(x2[0], x3[0])))) →* java.lang.Object(Tree(NULL, x0[5]))))


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


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


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


(1) -> (5), if ((x3[1] →* x1[5])∧(java.lang.Object(Tree(x0[1], java.lang.Object(Tree(x1[1], x2[1])))) →* java.lang.Object(Tree(NULL, x0[5]))))


(2) -> (0), if ((x3[2] →* x0[0])∧(x0[2] →* x1[0])∧(x1[2] →* x2[0])∧(x2[2] →* x3[0]))


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


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


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


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


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


(4) -> (2), if ((java.lang.Object(Tree(NULL, x1[4])) →* x3[2])∧(x0[4] →* java.lang.Object(Tree(java.lang.Object(Tree(x0[2], x1[2])), x2[2]))))


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


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


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



The set Q consists of the following terms:
14185_0_flatten_NULL(x0, NULL)

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

23897_0_FLATTEN_STORE(x0[0], x1[0], x2[0], x3[0]) → 14185_0_FLATTEN_NULL(x0[0], java.lang.Object(Tree(x1[0], java.lang.Object(Tree(x2[0], x3[0])))))
14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(java.lang.Object(Tree(x0[1], x1[1])), x2[1]))) → 14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(x0[1], java.lang.Object(Tree(x1[1], x2[1])))))
14185_0_FLATTEN_NULL(x3[2], java.lang.Object(Tree(java.lang.Object(Tree(x0[2], x1[2])), x2[2]))) → 23897_0_FLATTEN_STORE(x3[2], x0[2], x1[2], x2[2])
24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])
14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])

The TRS R consists of the following rules:

14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The set Q consists of the following terms:

14185_0_flatten_NULL(x0, NULL)

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

23897_0_FLATTEN_STORE(x0[0], x1[0], x2[0], x3[0]) → 14185_0_FLATTEN_NULL(x0[0], java.lang.Object(Tree(x1[0], java.lang.Object(Tree(x2[0], x3[0])))))
14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(java.lang.Object(Tree(x0[1], x1[1])), x2[1]))) → 14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(x0[1], java.lang.Object(Tree(x1[1], x2[1])))))
14185_0_FLATTEN_NULL(x3[2], java.lang.Object(Tree(java.lang.Object(Tree(x0[2], x1[2])), x2[2]))) → 23897_0_FLATTEN_STORE(x3[2], x0[2], x1[2], x2[2])
24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])
14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])

R is empty.
The set Q consists of the following terms:

14185_0_flatten_NULL(x0, NULL)

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

14185_0_flatten_NULL(x0, NULL)

(11) Obligation:

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

23897_0_FLATTEN_STORE(x0[0], x1[0], x2[0], x3[0]) → 14185_0_FLATTEN_NULL(x0[0], java.lang.Object(Tree(x1[0], java.lang.Object(Tree(x2[0], x3[0])))))
14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(java.lang.Object(Tree(x0[1], x1[1])), x2[1]))) → 14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(x0[1], java.lang.Object(Tree(x1[1], x2[1])))))
14185_0_FLATTEN_NULL(x3[2], java.lang.Object(Tree(java.lang.Object(Tree(x0[2], x1[2])), x2[2]))) → 23897_0_FLATTEN_STORE(x3[2], x0[2], x1[2], x2[2])
24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])
14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])

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

(12) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(java.lang.Object(Tree(x0[1], x1[1])), x2[1]))) → 14185_0_FLATTEN_NULL(x3[1], java.lang.Object(Tree(x0[1], java.lang.Object(Tree(x1[1], x2[1])))))
14185_0_FLATTEN_NULL(x3[2], java.lang.Object(Tree(java.lang.Object(Tree(x0[2], x1[2])), x2[2]))) → 23897_0_FLATTEN_STORE(x3[2], x0[2], x1[2], x2[2])


Used ordering: Polynomial interpretation [POLO]:

POL(14185_0_FLATTEN_NULL(x1, x2)) = x1 + x2   
POL(23897_0_FLATTEN_STORE(x1, x2, x3, x4)) = 2 + x1 + 2·x2 + 2·x3 + x4   
POL(24360_0_FLATTEN_STORE(x1, x2)) = x1 + x2   
POL(NULL) = 0   
POL(Tree(x1, x2)) = 1 + 2·x1 + x2   
POL(java.lang.Object(x1)) = x1   

(13) Obligation:

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

23897_0_FLATTEN_STORE(x0[0], x1[0], x2[0], x3[0]) → 14185_0_FLATTEN_NULL(x0[0], java.lang.Object(Tree(x1[0], java.lang.Object(Tree(x2[0], x3[0])))))
24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])
14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])

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

(14) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(15) Obligation:

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

14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])
24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])

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

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

  • 14185_0_FLATTEN_NULL(x1[4], java.lang.Object(Tree(NULL, x0[4]))) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x1[4])), x0[4])
    The graph contains the following edges 2 > 2

  • 14185_0_FLATTEN_NULL(x1[5], java.lang.Object(Tree(NULL, x0[5]))) → 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x1[5])), x0[5])
    The graph contains the following edges 2 > 2

  • 24360_0_FLATTEN_STORE(java.lang.Object(Tree(NULL, x0[3])), x1[3]) → 14185_0_FLATTEN_NULL(java.lang.Object(Tree(NULL, x0[3])), x1[3])
    The graph contains the following edges 1 >= 1, 2 >= 2

(17) YES

(18) 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


The ITRS R consists of the following rules:
6201_0_count_NULL(NULL) → 6394_0_count_Return
7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))

The integer pair graph contains the following rules and edges:
(0): 6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
(1): 7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
(2): 7947_0_COUNT_STORE(x0[2]) → 6201_0_COUNT_NULL(x0[2])
(3): 6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[3]))) → 6201_0_COUNT_NULL(x0[3])
(4): 6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[4]))) → 7947_0_COUNT_STORE(x0[4])

(0) -> (1), if ((7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) →* 14759_0_flatten_Return(x0[1]))∧(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])) →* java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))))


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


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


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


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


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


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


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


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


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


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



The set Q consists of the following terms:
6201_0_count_NULL(NULL)
7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

(19) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(20) Obligation:

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

6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
7947_0_COUNT_STORE(x0[2]) → 6201_0_COUNT_NULL(x0[2])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[3]))) → 6201_0_COUNT_NULL(x0[3])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[4]))) → 7947_0_COUNT_STORE(x0[4])

The TRS R consists of the following rules:

6201_0_count_NULL(NULL) → 6394_0_count_Return
7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))

The set Q consists of the following terms:

6201_0_count_NULL(NULL)
7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

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

(21) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

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

6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
7947_0_COUNT_STORE(x0[2]) → 6201_0_COUNT_NULL(x0[2])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[3]))) → 6201_0_COUNT_NULL(x0[3])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[4]))) → 7947_0_COUNT_STORE(x0[4])

The TRS R consists of the following rules:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The set Q consists of the following terms:

6201_0_count_NULL(NULL)
7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

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

(23) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

6201_0_count_NULL(NULL)

(24) Obligation:

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

6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
7947_0_COUNT_STORE(x0[2]) → 6201_0_COUNT_NULL(x0[2])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[3]))) → 6201_0_COUNT_NULL(x0[3])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[4]))) → 7947_0_COUNT_STORE(x0[4])

The TRS R consists of the following rules:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The set Q consists of the following terms:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

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

(25) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented dependency pairs:

6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[3]))) → 6201_0_COUNT_NULL(x0[3])
6201_0_COUNT_NULL(java.lang.Object(Tree(NULL, x0[4]))) → 7947_0_COUNT_STORE(x0[4])


Used ordering: Polynomial interpretation [POLO]:

POL(14185_0_flatten_NULL(x1, x2)) = 1 + x1 + x2   
POL(14759_0_flatten_Return(x1)) = 2 + x1   
POL(22978_0_flatten_Store(x1, x2, x3, x4)) = 1 + x1 + x2 + x3 + x4   
POL(23249_0_flatten_FieldAccess(x1, x2, x3, x4)) = 1 + x1 + x4   
POL(24267_0_flatten_FieldAccess(x1, x2)) = x1 + x2   
POL(24360_0_flatten_Store(x1, x2)) = 1 + x1 + x2   
POL(6201_0_COUNT_NULL(x1)) = 2 + x1   
POL(7650_0_flatten_ConstantStackPush(x1)) = 2 + x1   
POL(7650_1_COUNT_INVOKEMETHOD(x1, x2)) = x1   
POL(7947_0_COUNT_STORE(x1)) = 2 + x1   
POL(NULL) = 1   
POL(Tree(x1, x2)) = x1 + x2   
POL(java.lang.Object(x1)) = x1   

(26) Obligation:

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

6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))
7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
7947_0_COUNT_STORE(x0[2]) → 6201_0_COUNT_NULL(x0[2])

The TRS R consists of the following rules:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The set Q consists of the following terms:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

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

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(28) Obligation:

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

7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

The TRS R consists of the following rules:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The set Q consists of the following terms:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

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

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


7650_1_COUNT_INVOKEMETHOD(14759_0_flatten_Return(x0[1]), java.lang.Object(Tree(java.lang.Object(x1[1]), x2[1]))) → 6201_0_COUNT_NULL(x0[1])
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(7650_1_COUNT_INVOKEMETHOD(x1, x2)) = 0A + 1A·x1 + -I·x2

POL(14759_0_flatten_Return(x1)) = -I + 0A·x1

POL(java.lang.Object(x1)) = 1A + 0A·x1

POL(Tree(x1, x2)) = 0A + 1A·x1 + 0A·x2

POL(6201_0_COUNT_NULL(x1)) = -I + 0A·x1

POL(7650_0_flatten_ConstantStackPush(x1)) = 1A + -I·x1

POL(14185_0_flatten_NULL(x1, x2)) = 1A + 0A·x1 + -I·x2

POL(NULL) = 0A

POL(22978_0_flatten_Store(x1, x2, x3, x4)) = 1A + 0A·x1 + -I·x2 + -I·x3 + -I·x4

POL(24360_0_flatten_Store(x1, x2)) = -I + 0A·x1 + -I·x2

POL(24267_0_flatten_FieldAccess(x1, x2)) = -I + 0A·x1 + -I·x2

POL(23249_0_flatten_FieldAccess(x1, x2, x3, x4)) = 1A + 0A·x1 + -I·x2 + -I·x3 + -I·x4

The following usable rules [FROCOS05] were oriented:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

(30) Obligation:

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

6201_0_COUNT_NULL(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))) → 7650_1_COUNT_INVOKEMETHOD(7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0]))), java.lang.Object(Tree(java.lang.Object(x0[0]), x1[0])))

The TRS R consists of the following rules:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1))) → 14185_0_flatten_NULL(NULL, java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 14185_0_flatten_NULL(x3, java.lang.Object(Tree(x0, java.lang.Object(Tree(x1, x2)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x1)), x0)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 22978_0_flatten_Store(x3, x0, x1, x2)
22978_0_flatten_Store(x0, x1, x2, x3) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24360_0_flatten_Store(java.lang.Object(Tree(NULL, x1)), x0)
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x1, java.lang.Object(Tree(NULL, x0))) → 24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x1)), java.lang.Object(Tree(NULL, x0)))
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1))) → 14185_0_flatten_NULL(java.lang.Object(Tree(NULL, x0)), x1)
14185_0_flatten_NULL(x3, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2))) → 23249_0_flatten_FieldAccess(x3, x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1)), x2)))
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3))) → 14185_0_flatten_NULL(x0, java.lang.Object(Tree(x1, java.lang.Object(Tree(x2, x3)))))
14185_0_flatten_NULL(x0, NULL) → 14759_0_flatten_Return(x0)

The set Q consists of the following terms:

7650_0_flatten_ConstantStackPush(java.lang.Object(Tree(java.lang.Object(x0), x1)))
14185_0_flatten_NULL(x0, NULL)
14185_0_flatten_NULL(x0, java.lang.Object(Tree(NULL, x1)))
14185_0_flatten_NULL(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))
24360_0_flatten_Store(java.lang.Object(Tree(NULL, x0)), x1)
24267_0_flatten_FieldAccess(java.lang.Object(Tree(NULL, x0)), java.lang.Object(Tree(NULL, x1)))
22978_0_flatten_Store(x0, x1, x2, x3)
23249_0_flatten_FieldAccess(x0, x1, x2, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2)), x3)))

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

(31) DependencyGraphProof (EQUIVALENT transformation)

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

(32) TRUE

(33) 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:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): 29267_1_CREATETREE_INVOKEMETHOD(x0[0]) → COND_29267_1_CREATETREE_INVOKEMETHOD(x0[0] > 0 && 0 < x0[0] + -1, x0[0])
(1): COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1]) → 29267_1_CREATETREE_INVOKEMETHOD(x0[1] + -1)

(0) -> (1), if ((x0[0] > 0 && 0 < x0[0] + -1 →* TRUE)∧(x0[0] →* x0[1]))


(1) -> (0), if ((x0[1] + -1 →* x0[0]))



The set Q is empty.

(34) 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 29267_1_CREATETREE_INVOKEMETHOD(x0) → COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0, 0), <(0, +(x0, -1))), x0) the following chains were created:
  • We consider the chain 29267_1_CREATETREE_INVOKEMETHOD(x0[0]) → COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0]), COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1]) → 29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1)) which results in the following constraint:

    (1)    (&&(>(x0[0], 0), <(0, +(x0[0], -1)))=TRUE∧x0[0]=x0[1] ⇒ 29267_1_CREATETREE_INVOKEMETHOD(x0[0])≥NonInfC∧29267_1_CREATETREE_INVOKEMETHOD(x0[0])≥COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])∧(UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥))



    We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (2)    (>(x0[0], 0)=TRUE∧<(0, +(x0[0], -1))=TRUE ⇒ 29267_1_CREATETREE_INVOKEMETHOD(x0[0])≥NonInfC∧29267_1_CREATETREE_INVOKEMETHOD(x0[0])≥COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])∧(UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥))



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

    (3)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[1 + (-1)bso_11] ≥ 0)



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

    (4)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[1 + (-1)bso_11] ≥ 0)



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

    (5)    (x0[0] + [-1] ≥ 0∧x0[0] + [-2] ≥ 0 ⇒ (UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥)∧[(-1)Bound*bni_10] + [(2)bni_10]x0[0] ≥ 0∧[1 + (-1)bso_11] ≥ 0)



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

    (6)    (x0[0] ≥ 0∧[-1] + x0[0] ≥ 0 ⇒ (UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥)∧[(-1)Bound*bni_10 + (2)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[1 + (-1)bso_11] ≥ 0)



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

    (7)    ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥)∧[(-1)Bound*bni_10 + (4)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[1 + (-1)bso_11] ≥ 0)







For Pair COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0) → 29267_1_CREATETREE_INVOKEMETHOD(+(x0, -1)) the following chains were created:
  • We consider the chain COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1]) → 29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1)) which results in the following constraint:

    (8)    (COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1])≥NonInfC∧COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1])≥29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))∧(UIncreasing(29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))), ≥))



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

    (9)    ((UIncreasing(29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))), ≥)∧[1 + (-1)bso_13] ≥ 0)



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

    (10)    ((UIncreasing(29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))), ≥)∧[1 + (-1)bso_13] ≥ 0)



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

    (11)    ((UIncreasing(29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))), ≥)∧[1 + (-1)bso_13] ≥ 0)



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

    (12)    ((UIncreasing(29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))), ≥)∧0 = 0∧[1 + (-1)bso_13] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • 29267_1_CREATETREE_INVOKEMETHOD(x0) → COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0, 0), <(0, +(x0, -1))), x0)
    • ([1] + x0[0] ≥ 0∧x0[0] ≥ 0 ⇒ (UIncreasing(COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])), ≥)∧[(-1)Bound*bni_10 + (4)bni_10] + [(2)bni_10]x0[0] ≥ 0∧[1 + (-1)bso_11] ≥ 0)

  • COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0) → 29267_1_CREATETREE_INVOKEMETHOD(+(x0, -1))
    • ((UIncreasing(29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))), ≥)∧0 = 0∧[1 + (-1)bso_13] ≥ 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(29267_1_CREATETREE_INVOKEMETHOD(x1)) = [2]x1   
POL(COND_29267_1_CREATETREE_INVOKEMETHOD(x1, x2)) = [-1] + [2]x2   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(-1) = [-1]   

The following pairs are in P>:

29267_1_CREATETREE_INVOKEMETHOD(x0[0]) → COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])
COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1]) → 29267_1_CREATETREE_INVOKEMETHOD(+(x0[1], -1))

The following pairs are in Pbound:

29267_1_CREATETREE_INVOKEMETHOD(x0[0]) → COND_29267_1_CREATETREE_INVOKEMETHOD(&&(>(x0[0], 0), <(0, +(x0[0], -1))), x0[0])

The following pairs are in P≥:
none

There are no usable rules.

(35) 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


R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_29267_1_CREATETREE_INVOKEMETHOD(TRUE, x0[1]) → 29267_1_CREATETREE_INVOKEMETHOD(x0[1] + -1)


The set Q is empty.

(36) IDependencyGraphProof (EQUIVALENT transformation)

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

(37) TRUE