0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 Instantiation (⇔)
↳20 QDP
↳21 Narrowing (⇔)
↳22 QDP
↳23 DependencyGraphProof (⇔)
↳24 QDP
↳25 Rewriting (⇔)
↳26 QDP
↳27 Rewriting (⇔)
↳28 QDP
↳29 Rewriting (⇔)
↳30 QDP
↳31 Rewriting (⇔)
↳32 QDP
↳33 Rewriting (⇔)
↳34 QDP
↳35 Narrowing (⇔)
↳36 QDP
↳37 UsableRulesProof (⇔)
↳38 QDP
↳39 QReductionProof (⇔)
↳40 QDP
↳41 Rewriting (⇔)
↳42 QDP
↳43 UsableRulesProof (⇔)
↳44 QDP
↳45 Rewriting (⇔)
↳46 QDP
↳47 UsableRulesProof (⇔)
↳48 QDP
↳49 QReductionProof (⇔)
↳50 QDP
↳51 Rewriting (⇔)
↳52 QDP
↳53 UsableRulesProof (⇔)
↳54 QDP
↳55 Rewriting (⇔)
↳56 QDP
↳57 UsableRulesProof (⇔)
↳58 QDP
↳59 QReductionProof (⇔)
↳60 QDP
↳61 Instantiation (⇔)
↳62 QDP
↳63 QDPOrderProof (⇔)
↳64 QDP
↳65 DependencyGraphProof (⇔)
↳66 QDP
↳67 QDPOrderProof (⇔)
↳68 QDP
↳69 DependencyGraphProof (⇔)
↳70 TRUE
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)
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)
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)
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)
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)
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)
INC(s(x)) → INC(x)
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)
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)
INC(s(x)) → INC(x)
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)
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)
INC(s(x)) → INC(x)
From the DPs we obtained the following set of size-change graphs:
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)
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)
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)
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)
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))
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)
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)
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)
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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)
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)
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
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))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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)
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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, 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))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
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))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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)
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))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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, 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))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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)
COUNT(node(x0, x1), y1) → IF(false, isEmpty(x0), x1, node(left(x0), node(right(x0), x1)), y1, inc(y1))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
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))
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))
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
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
isEmpty(empty)
isEmpty(node(x0, x1))
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
isEmpty(empty)
isEmpty(node(x0, x1))
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))
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
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
COUNT(node(empty, y1), y2) → IF(false, true, y1, node(empty, node(right(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(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))
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
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
right(empty) → empty
inc(0) → s(0)
inc(s(x)) → s(inc(x))
left(node(l, r)) → l
right(node(l, r)) → r
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(right(node(x0, x1)), y1)), y2, inc(y2))
right(empty) → empty
inc(0) → s(0)
inc(s(x)) → s(inc(x))
left(node(l, r)) → l
right(node(l, r)) → r
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty
left(empty)
left(node(x0, x1))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
left(empty)
left(node(x0, x1))
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))
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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(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))
right(node(l, r)) → r
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty) → empty
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(node(l, r)) → r
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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)
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))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(node(l, r)) → r
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
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))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
right(empty)
right(node(x0, x1))
inc(0)
inc(s(x0))
right(empty)
right(node(x0, x1))
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))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(0)
inc(s(x0))
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
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)
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(0)
inc(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
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
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))
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(0)
inc(s(x0))
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)
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(0)
inc(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COUNT(node(node(x0, x1), y1), y2) → IF(false, false, y1, node(x0, node(x1, y1)), y2, inc(y2))
POL(0) = 0
POL(COUNT(x1, x2)) = x1
POL(IF(x1, x2, x3, x4, x5, x6)) = x4
POL(false) = 0
POL(inc(x1)) = 0
POL(node(x1, x2)) = 1 + x1
POL(s(x1)) = 0
IF(false, false, n, m, x, y) → COUNT(m, x)
inc(0) → s(0)
inc(s(x)) → s(inc(x))
inc(0)
inc(s(x0))