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 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 QDPOrderProof (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 TRUE
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)
The value of delta used in the strict ordering is 1/4.
POL(IF(x1, x2, x3)) = 1/2 + x1 + (1/4)x2 + (1/2)x3
POL(false) = 1/4
POL(BITITER(x1, x2)) = 1/2 + (3/4)x1 + (1/2)x2
POL(half(x1)) = (1/4)x1
POL(zero(x1)) = (1/2)x1
POL(inc(x1)) = x1
POL(s(x1)) = 4 + (4)x1
POL(0) = 0
POL(true) = 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
zero(0) → true
zero(s(x)) → false
inc(0) → 0
inc(s(x)) → s(inc(x))
half(0) → 0
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))