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)
↳ QTRS
↳ DependencyPairsProof
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)
IF(false, x, y) → HALF(x)
BITITER(x, y) → INC(y)
IF(false, x, y) → BITITER(half(x), y)
IF(true, x, y) → P(y)
HALF(s(s(x))) → HALF(x)
BITITER(x, y) → IF(zero(x), x, inc(y))
INC(s(x)) → INC(x)
BITITER(x, y) → ZERO(x)
BITS(x) → BITITER(x, 0)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF(false, x, y) → HALF(x)
BITITER(x, y) → INC(y)
IF(false, x, y) → BITITER(half(x), y)
IF(true, x, y) → P(y)
HALF(s(s(x))) → HALF(x)
BITITER(x, y) → IF(zero(x), x, inc(y))
INC(s(x)) → INC(x)
BITITER(x, y) → ZERO(x)
BITS(x) → BITITER(x, 0)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
INC(s(x)) → INC(x)
The value of delta used in the strict ordering is 4.
POL(INC(x1)) = (4)x_1
POL(s(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
HALF(s(s(x))) → HALF(x)
The value of delta used in the strict ordering is 4.
POL(HALF(x1)) = (2)x_1
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
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)