(0) Obligation:
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.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
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)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
INC(s(x)) → 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))
COUNT(n, x) → ISEMPTY(n)
COUNT(n, x) → ISEMPTY(left(n))
COUNT(n, x) → LEFT(n)
COUNT(n, x) → RIGHT(n)
COUNT(n, x) → LEFT(left(n))
COUNT(n, x) → RIGHT(left(n))
COUNT(n, x) → INC(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 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.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
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.
(8) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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.
(10) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
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)
(11) Obligation:
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.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- INC(s(x)) → INC(x)
The graph contains the following edges 1 > 1
(13) TRUE
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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, 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))
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.
(15) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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, 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))
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.
(17) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
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)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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, 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.
(19) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF(
false,
false,
n,
m,
x,
y) →
COUNT(
m,
x) we obtained the following new rules [LPAR04]:
IF(false, false, y_3, node(y_5, node(y_7, y_8)), z1, y_9) → COUNT(node(y_5, node(y_7, y_8)), z1)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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)
IF(false, false, y_3, node(y_5, node(y_7, y_8)), z1, y_9) → COUNT(node(y_5, node(y_7, y_8)), z1)
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.
(21) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] 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 [LPAR04]:
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))
(22) Obligation:
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.
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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))
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.
(25) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
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))
(26) Obligation:
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), 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.
(27) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
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))
(28) Obligation:
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.
(29) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
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))
(30) Obligation:
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(x0), 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.
(31) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), right(node(x0, x1)))), y1, inc(y1))
(32) Obligation:
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(x0), node(right(x0), 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.
(33) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), x1)), y1, inc(y1))
(34) Obligation:
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(x0), node(right(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.
(35) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] 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 [LPAR04]:
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))
(36) Obligation:
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.
(37) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(38) Obligation:
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.
(39) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
isEmpty(empty)
isEmpty(node(x0, x1))
(40) Obligation:
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.
(41) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(empty), y1)), y2, inc(y2))
(42) Obligation:
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(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))
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))
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.
(43) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(44) Obligation:
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(node(x0, x1), y1), y2) → IF(false, false, y1, node(left(node(x0, x1)), node(right(node(x0, x1)), y1)), y2, inc(y2))
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))
left(node(l, r)) → l
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.
(45) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
(46) Obligation:
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(right(node(x0, 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))
left(node(l, r)) → l
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.
(47) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(48) Obligation:
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(right(node(x0, x1)), y1)), y2, inc(y2))
The TRS R consists of the following rules:
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.
(49) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
left(empty)
left(node(x0, x1))
(50) Obligation:
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(right(node(x0, x1)), y1)), y2, inc(y2))
The TRS R consists of the following rules:
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:
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(51) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
(52) Obligation:
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(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
The TRS R consists of the following rules:
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:
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(53) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(54) Obligation:
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(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
The TRS R consists of the following rules:
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.
(55) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] 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 [LPAR04]:
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))
(56) Obligation:
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(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(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.
(57) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(58) Obligation:
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(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))
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.
(59) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
right(empty)
right(node(x0, x1))
(60) Obligation:
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(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))
The set Q consists of the following terms:
inc(0)
inc(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(61) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF(
false,
true,
n,
m,
x,
y) →
COUNT(
n,
y) we obtained the following new rules [LPAR04]:
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(empty, y1)), y2, inc(y2))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
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.
(63) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
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 [FROCOS05] were oriented:
none
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, false, n, m, x, y) → COUNT(m, x)
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(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))
The set Q consists of the following terms:
inc(0)
inc(s(x0))
We have to consider all minimal (P,Q,R)-chains.
(65) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(66) Obligation:
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(x1, y1)), y2, inc(y2))
IF(false, false, n, m, x, y) → COUNT(m, x)
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.
(67) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(COUNT(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(node(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(IF(x1, x2, x3, x4, x5, x6)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 | + | | · | x5 | + | | · | x6 |
The following usable rules [FROCOS05] were oriented:
none
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, false, n, m, x, y) → COUNT(m, x)
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.
(69) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(70) TRUE