R
↳Dependency Pair Analysis
HALF(s(s(x))) -> HALF(x)
BITS(s(x)) -> BITS(half(s(x)))
BITS(s(x)) -> HALF(s(x))
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
HALF(s(s(x))) -> HALF(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(0) -> 0
bits(s(x)) -> s(bits(half(s(x))))
BITS(s(x)) -> BITS(half(s(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(0) -> 0
bits(s(x)) -> s(bits(half(s(x))))
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
HALF(s(s(x))) -> HALF(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(0) -> 0
bits(s(x)) -> s(bits(half(s(x))))
BITS(s(x)) -> BITS(half(s(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
bits(0) -> 0
bits(s(x)) -> s(bits(half(s(x))))