YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 5 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 TransformationProof (⇔, 0 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 QDP
↳23 TransformationProof (⇔, 0 ms)
↳24 QDP
↳25 TransformationProof (⇔, 0 ms)
↳26 QDP
↳27 TransformationProof (⇔, 0 ms)
↳28 QDP
↳29 TransformationProof (⇔, 0 ms)
↳30 QDP
↳31 TransformationProof (⇔, 0 ms)
↳32 QDP
↳33 TransformationProof (⇔, 0 ms)
↳34 QDP
↳35 UsableRulesProof (⇔, 0 ms)
↳36 QDP
↳37 QReductionProof (⇔, 0 ms)
↳38 QDP
↳39 TransformationProof (⇔, 0 ms)
↳40 QDP
↳41 UsableRulesProof (⇔, 0 ms)
↳42 QDP
↳43 TransformationProof (⇔, 0 ms)
↳44 QDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 QDP
↳47 QReductionProof (⇔, 0 ms)
↳48 QDP
↳49 TransformationProof (⇔, 0 ms)
↳50 QDP
↳51 UsableRulesProof (⇔, 0 ms)
↳52 QDP
↳53 TransformationProof (⇔, 0 ms)
↳54 QDP
↳55 UsableRulesProof (⇔, 0 ms)
↳56 QDP
↳57 QReductionProof (⇔, 0 ms)
↳58 QDP
↳59 TransformationProof (⇔, 0 ms)
↳60 QDP
↳61 QDPQMonotonicMRRProof (⇔, 0 ms)
↳62 QDP
↳63 DependencyGraphProof (⇔, 0 ms)
↳64 QDP
↳65 QDPOrderProof (⇔, 0 ms)
↳66 QDP
↳67 DependencyGraphProof (⇔, 0 ms)
↳68 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))
COUNT(empty, y1) → IF(true, isEmpty(left(empty)), right(empty), node(left(left(empty)), node(right(left(empty)), right(empty))), y1, inc(y1)) → 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)) → 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)) → 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)) → 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)) → 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)) → 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)) → 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(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)) → 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)) → 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)) → 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)) → 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)) → 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, 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))
IF(false, true, z0, node(empty, node(empty, z0)), z1, y_0) → COUNT(z0, y_0)
POL(0) = 0
POL(COUNT(x1, x2)) = 2 + 2·x1
POL(IF(x1, x2, x3, x4, x5, x6)) = x2 + 2·x4
POL(empty) = 1
POL(false) = 2
POL(inc(x1)) = 1 + x1
POL(node(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
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))
trivial
dummyConstant=1
node_1=1
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))