YES Termination w.r.t. Q proof of ../tpdb/TRS/secret06/aprove/nrOfNodes.trs
Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

Q is empty.


↳ QTRS
  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)


Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

COUNT(n, x) → ISEMPTY(left(n))
NROFNODES(n) → COUNT(n, 0)
COUNT(n, x) → LEFT(n)
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(n, x) → INC(x)
COUNT(n, x) → LEFT(left(n))
COUNT(n, x) → ISEMPTY(n)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
COUNT(n, x) → RIGHT(n)
COUNT(n, x) → RIGHT(left(n))
INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

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

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof

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

COUNT(n, x) → ISEMPTY(left(n))
NROFNODES(n) → COUNT(n, 0)
COUNT(n, x) → LEFT(n)
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(n, x) → INC(x)
COUNT(n, x) → LEFT(left(n))
COUNT(n, x) → ISEMPTY(n)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
COUNT(n, x) → RIGHT(n)
COUNT(n, x) → RIGHT(left(n))
INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 8 less nodes.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
              ↳ QDP

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

INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
              ↳ QDP

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

INC(s(x)) → INC(x)

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

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ QDP

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

INC(s(x)) → INC(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] 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: 



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
count(n, x) → if(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
if(true, b, n, m, x, y) → x
if(false, false, n, m, x, y) → count(m, x)
if(false, true, n, m, x, y) → count(n, y)
nrOfNodes(n) → count(n, 0)

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

count(x0, x1)
if(true, x0, x1, x2, x3, x4)
if(false, false, x0, x1, x2, x3)
if(false, true, x0, x1, x2, x3)
nrOfNodes(x0)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing

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

IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x))
IF(false, true, n, m, x, y) → COUNT(n, y)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule COUNT(n, x) → IF(isEmpty(n), isEmpty(left(n)), right(n), node(left(left(n)), node(right(left(n)), right(n))), x, inc(x)) at position [0] we obtained the following new rules:

COUNT(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), node(right(left(empty)), right(empty))), y1, inc(y1))
COUNT(node(x0, x1), y1) → IF(false, isEmpty(left(node(x0, x1))), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), node(right(left(empty)), right(empty))), y1, inc(y1))
COUNT(node(x0, x1), y1) → IF(false, isEmpty(left(node(x0, x1))), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(x0, x1), y1) → IF(false, isEmpty(left(node(x0, x1))), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(x0, x1), y1) → IF(false, isEmpty(left(node(x0, x1))), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1)) at position [1,0] we obtained the following new rules:

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))
IF(false, true, n, m, x, y) → COUNT(n, y)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), right(node(x0, x1)), node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1)) at position [2] we obtained the following new rules:

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(left(node(x0, x1))), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1)) at position [3,0,0] we obtained the following new rules:

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting

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

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(left(node(x0, x1))), right(node(x0, x1)))), y1, inc(y1)) at position [3,1,0,0] we obtained the following new rules:

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), right(node(x0, x1)))), y1, inc(y1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), right(node(x0, x1)))), y1, inc(y1))
IF(false, true, n, m, x, y) → COUNT(n, y)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), right(node(x0, x1)))), y1, inc(y1)) at position [3,1,1] we obtained the following new rules:

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), x1)), y1, inc(y1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing

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

COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), x1)), y1, inc(y1))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), x1)), y1, inc(y1)) at position [1] we obtained the following new rules:

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(left(empty), node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(left(empty), node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))

The TRS R consists of the following rules:

isEmpty(empty) → true
isEmpty(node(l, r)) → false
left(empty) → empty
left(node(l, r)) → l
right(empty) → empty
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(left(empty), node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))

The TRS R consists of the following rules:

left(node(l, r)) → l
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
left(empty) → empty
right(empty) → empty

The set Q consists of the following terms:

isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isEmpty(empty)
isEmpty(node(x0, x1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(left(empty), node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))

The TRS R consists of the following rules:

left(node(l, r)) → l
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
left(empty) → empty
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(empty, y1), y2) → IF(false, true, y1, node(left(empty), node(right(empty), y1)), y2, inc(y2)) at position [3,0] we obtained the following new rules:

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))

The TRS R consists of the following rules:

left(node(l, r)) → l
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
left(empty) → empty
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))

The TRS R consists of the following rules:

left(node(l, r)) → l
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2)) at position [3,0] we obtained the following new rules:

COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof

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

COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))

The TRS R consists of the following rules:

left(node(l, r)) → l
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty

The set Q consists of the following terms:

left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof

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

COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))

The TRS R consists of the following rules:

right(empty) → empty
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(node(l, r)) → r

The set Q consists of the following terms:

left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

left(empty)
left(node(x0, x1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting

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

COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))

The TRS R consists of the following rules:

right(empty) → empty
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(node(l, r)) → r

The set Q consists of the following terms:

right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2)) at position [3,1,0] we obtained the following new rules:

COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))

The TRS R consists of the following rules:

right(empty) → empty
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(node(l, r)) → r

The set Q consists of the following terms:

right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting

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

IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2)) at position [3,1,0] we obtained the following new rules:

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty

The set Q consists of the following terms:

right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

right(empty)
right(node(x0, x1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF(false, false, n, m, x, y) → COUNT(m, x) we obtained the following new rules:

IF(false, false, z2, node(z0, node(z1, z2)), z3, y_0) → COUNT(node(z0, node(z1, z2)), z3)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, true, n, m, x, y) → COUNT(n, y)
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))
IF(false, false, z2, node(z0, node(z1, z2)), z3, y_0) → COUNT(node(z0, node(z1, z2)), z3)

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IF(false, true, n, m, x, y) → COUNT(n, y) we obtained the following new rules:

IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))
IF(false, false, z2, node(z0, node(z1, z2)), z3, y_0) → COUNT(node(z0, node(z1, z2)), z3)

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule IF(false, false, z2, node(z0, node(z1, z2)), z3, y_0) → COUNT(node(z0, node(z1, z2)), z3) we obtained the following new rules:

IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2)) we obtained the following new rules:

COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
COUNT(node(node(empty, x1), x2), x3) → IF(false, false, x2, node(empty, node(x1, x2)), x3, inc(x3))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation
                                                                                                                      ↳ QDP
                                                                                                                        ↳ ForwardInstantiation

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
COUNT(node(node(empty, x1), x2), x3) → IF(false, false, x2, node(empty, node(x1, x2)), x3, inc(x3))
COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0) we obtained the following new rules:

IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, x2) → COUNT(node(empty, y_0), x2)
IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, x2) → COUNT(node(node(node(y_0, y_1), y_2), y_3), x2)
IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, x2) → COUNT(node(node(empty, y_0), y_1), x2)



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation
                                                                                                                      ↳ QDP
                                                                                                                        ↳ ForwardInstantiation
                                                                                                                          ↳ QDP
                                                                                                                            ↳ ForwardInstantiation

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

COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, x2) → COUNT(node(empty, y_0), x2)
IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, x2) → COUNT(node(node(node(y_0, y_1), y_2), y_3), x2)
IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
COUNT(node(node(empty, x1), x2), x3) → IF(false, false, x2, node(empty, node(x1, x2)), x3, inc(x3))
IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, x2) → COUNT(node(node(empty, y_0), y_1), x2)
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2)) we obtained the following new rules:

COUNT(node(empty, node(node(empty, y_0), y_1)), x1) → IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, inc(x1))
COUNT(node(empty, node(node(node(y_0, y_1), y_2), y_3)), x1) → IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, inc(x1))
COUNT(node(empty, node(empty, y_0)), x1) → IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, inc(x1))



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation
                                                                                                                      ↳ QDP
                                                                                                                        ↳ ForwardInstantiation
                                                                                                                          ↳ QDP
                                                                                                                            ↳ ForwardInstantiation
                                                                                                                              ↳ QDP
                                                                                                                                ↳ QDPOrderProof

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

IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, x2) → COUNT(node(empty, y_0), x2)
COUNT(node(empty, node(node(empty, y_0), y_1)), x1) → IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, inc(x1))
COUNT(node(node(empty, x1), x2), x3) → IF(false, false, x2, node(empty, node(x1, x2)), x3, inc(x3))
COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, x2) → COUNT(node(node(node(y_0, y_1), y_2), y_3), x2)
COUNT(node(empty, node(node(node(y_0, y_1), y_2), y_3)), x1) → IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, inc(x1))
IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, x2) → COUNT(node(node(empty, y_0), y_1), x2)
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)
COUNT(node(empty, node(empty, y_0)), x1) → IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, inc(x1))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, x2) → COUNT(node(empty, y_0), x2)
IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, x2) → COUNT(node(node(node(y_0, y_1), y_2), y_3), x2)
IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, x2) → COUNT(node(node(empty, y_0), y_1), x2)
The remaining pairs can at least be oriented weakly.

COUNT(node(empty, node(node(empty, y_0), y_1)), x1) → IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, inc(x1))
COUNT(node(node(empty, x1), x2), x3) → IF(false, false, x2, node(empty, node(x1, x2)), x3, inc(x3))
COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
COUNT(node(empty, node(node(node(y_0, y_1), y_2), y_3)), x1) → IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, inc(x1))
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)
COUNT(node(empty, node(empty, y_0)), x1) → IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, inc(x1))
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(COUNT(x1, x2)) = 1 + x1   
POL(IF(x1, x2, x3, x4, x5, x6)) = x2 + x4   
POL(empty) = 1   
POL(false) = 1   
POL(inc(x1)) = 0   
POL(node(x1, x2)) = x1 + x2   
POL(s(x1)) = 0   
POL(true) = 0   

The following usable rules [17] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation
                                                                                                                      ↳ QDP
                                                                                                                        ↳ ForwardInstantiation
                                                                                                                          ↳ QDP
                                                                                                                            ↳ ForwardInstantiation
                                                                                                                              ↳ QDP
                                                                                                                                ↳ QDPOrderProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ DependencyGraphProof

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

COUNT(node(empty, node(node(empty, y_0), y_1)), x1) → IF(false, true, node(node(empty, y_0), y_1), node(empty, node(empty, node(node(empty, y_0), y_1))), x1, inc(x1))
IF(false, false, x0, node(empty, node(x2, x0)), x3, x4) → COUNT(node(empty, node(x2, x0)), x3)
COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
COUNT(node(node(empty, x1), x2), x3) → IF(false, false, x2, node(empty, node(x1, x2)), x3, inc(x3))
COUNT(node(empty, node(node(node(y_0, y_1), y_2), y_3)), x1) → IF(false, true, node(node(node(y_0, y_1), y_2), y_3), node(empty, node(empty, node(node(node(y_0, y_1), y_2), y_3))), x1, inc(x1))
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)
COUNT(node(empty, node(empty, y_0)), x1) → IF(false, true, node(empty, y_0), node(empty, node(empty, node(empty, y_0))), x1, inc(x1))

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 5 less nodes.

↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation
                                                                                                                      ↳ QDP
                                                                                                                        ↳ ForwardInstantiation
                                                                                                                          ↳ QDP
                                                                                                                            ↳ ForwardInstantiation
                                                                                                                              ↳ QDP
                                                                                                                                ↳ QDPOrderProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ DependencyGraphProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ QDPOrderProof

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

COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


COUNT(node(node(node(y_1, y_2), x1), x2), x3) → IF(false, false, x2, node(node(y_1, y_2), node(x1, x2)), x3, inc(x3))
The remaining pairs can at least be oriented weakly.

IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)
Used ordering: Polynomial interpretation [25]:

POL(0) = 0   
POL(COUNT(x1, x2)) = 1 + x1   
POL(IF(x1, x2, x3, x4, x5, x6)) = 1 + x4   
POL(false) = 0   
POL(inc(x1)) = 0   
POL(node(x1, x2)) = 1 + x1   
POL(s(x1)) = 0   

The following usable rules [17] were oriented: none



↳ QTRS
  ↳ Overlay + Local Confluence
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ UsableRulesProof
                  ↳ QDP
                    ↳ QReductionProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ QDP
                                ↳ Rewriting
                                  ↳ QDP
                                    ↳ Rewriting
                                      ↳ QDP
                                        ↳ Rewriting
                                          ↳ QDP
                                            ↳ Rewriting
                                              ↳ QDP
                                                ↳ Rewriting
                                                  ↳ QDP
                                                    ↳ Narrowing
                                                      ↳ QDP
                                                        ↳ UsableRulesProof
                                                          ↳ QDP
                                                            ↳ QReductionProof
                                                              ↳ QDP
                                                                ↳ Rewriting
                                                                  ↳ QDP
                                                                    ↳ UsableRulesProof
                                                                      ↳ QDP
                                                                        ↳ Rewriting
                                                                          ↳ QDP
                                                                            ↳ UsableRulesProof
                                                                              ↳ QDP
                                                                                ↳ QReductionProof
                                                                                  ↳ QDP
                                                                                    ↳ Rewriting
                                                                                      ↳ QDP
                                                                                        ↳ UsableRulesProof
                                                                                          ↳ QDP
                                                                                            ↳ Rewriting
                                                                                              ↳ QDP
                                                                                                ↳ UsableRulesProof
                                                                                                  ↳ QDP
                                                                                                    ↳ QReductionProof
                                                                                                      ↳ QDP
                                                                                                        ↳ Instantiation
                                                                                                          ↳ QDP
                                                                                                            ↳ Instantiation
                                                                                                              ↳ QDP
                                                                                                                ↳ ForwardInstantiation
                                                                                                                  ↳ QDP
                                                                                                                    ↳ ForwardInstantiation
                                                                                                                      ↳ QDP
                                                                                                                        ↳ ForwardInstantiation
                                                                                                                          ↳ QDP
                                                                                                                            ↳ ForwardInstantiation
                                                                                                                              ↳ QDP
                                                                                                                                ↳ QDPOrderProof
                                                                                                                                  ↳ QDP
                                                                                                                                    ↳ DependencyGraphProof
                                                                                                                                      ↳ QDP
                                                                                                                                        ↳ QDPOrderProof
                                                                                                                                          ↳ QDP
                                                                                                                                            ↳ DependencyGraphProof

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

IF(false, false, x0, node(node(y_0, y_1), node(x2, x0)), x3, x4) → COUNT(node(node(y_0, y_1), node(x2, x0)), x3)

The TRS R consists of the following rules:

inc(0) → s(0)
inc(s(x)) → s(inc(x))

The set Q consists of the following terms:

inc(0)
inc(s(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.