YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 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 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 QDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 QDP
↳24 QReductionProof (⇔, 0 ms)
↳25 QDP
↳26 QDPOrderProof (⇔, 37 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(0) → 0
inc(s(x)) → s(inc(x))
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(x)) → x
bits(x) → bitIter(x, 0)
bitIter(x, y) → if(zero(x), x, inc(y))
if(true, x, y) → p(y)
if(false, x, y) → bitIter(half(x), y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(0) → 0
inc(s(x)) → s(inc(x))
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(x)) → x
bits(x) → bitIter(x, 0)
bitIter(x, y) → if(zero(x), x, inc(y))
if(true, x, y) → p(y)
if(false, x, y) → bitIter(half(x), y)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
HALF(s(s(x))) → HALF(x)
INC(s(x)) → INC(x)
BITS(x) → BITITER(x, 0)
BITITER(x, y) → IF(zero(x), x, inc(y))
BITITER(x, y) → ZERO(x)
BITITER(x, y) → INC(y)
IF(true, x, y) → P(y)
IF(false, x, y) → BITITER(half(x), y)
IF(false, x, y) → HALF(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(0) → 0
inc(s(x)) → s(inc(x))
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(x)) → x
bits(x) → bitIter(x, 0)
bitIter(x, y) → if(zero(x), x, inc(y))
if(true, x, y) → p(y)
if(false, x, y) → bitIter(half(x), y)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
INC(s(x)) → INC(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(0) → 0
inc(s(x)) → s(inc(x))
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(x)) → x
bits(x) → bitIter(x, 0)
bitIter(x, y) → if(zero(x), x, inc(y))
if(true, x, y) → p(y)
if(false, x, y) → bitIter(half(x), y)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
INC(s(x)) → INC(x)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
INC(s(x)) → INC(x)
From the DPs we obtained the following set of size-change graphs:
HALF(s(s(x))) → HALF(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(0) → 0
inc(s(x)) → s(inc(x))
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(x)) → x
bits(x) → bitIter(x, 0)
bitIter(x, y) → if(zero(x), x, inc(y))
if(true, x, y) → p(y)
if(false, x, y) → bitIter(half(x), y)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
HALF(s(s(x))) → HALF(x)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
HALF(s(s(x))) → HALF(x)
From the DPs we obtained the following set of size-change graphs:
IF(false, x, y) → BITITER(half(x), y)
BITITER(x, y) → IF(zero(x), x, inc(y))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(0) → 0
inc(s(x)) → s(inc(x))
zero(0) → true
zero(s(x)) → false
p(0) → 0
p(s(x)) → x
bits(x) → bitIter(x, 0)
bitIter(x, y) → if(zero(x), x, inc(y))
if(true, x, y) → p(y)
if(false, x, y) → bitIter(half(x), y)
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
IF(false, x, y) → BITITER(half(x), y)
BITITER(x, y) → IF(zero(x), x, inc(y))
zero(0) → true
zero(s(x)) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
p(0)
p(s(x0))
bits(x0)
bitIter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
IF(false, x, y) → BITITER(half(x), y)
BITITER(x, y) → IF(zero(x), x, inc(y))
zero(0) → true
zero(s(x)) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(false, x, y) → BITITER(half(x), y)
BITITER(x, y) → IF(zero(x), x, inc(y))
The value of delta used in the strict ordering is 1/4.
POL(0) = [1/2]
POL(BITITER(x1, x2)) = [1/2] + x1
POL(IF(x1, x2, x3)) = [1/4]x1 + [1/2]x2
POL(false) = [4]
POL(half(x1)) = [1/4] + [1/2]x1
POL(inc(x1)) = x1
POL(s(x1)) = [2] + x1
POL(true) = [1/2]
POL(zero(x1)) = [1/4] + [2]x1
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
zero(0) → true
zero(s(x)) → false
zero(0) → true
zero(s(x)) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
half(0)
half(s(0))
half(s(s(x0)))
inc(0)
inc(s(x0))
zero(0)
zero(s(x0))