R
↳Dependency Pair Analysis
HALF(s(s(x))) -> S(half(x))
HALF(s(s(x))) -> HALF(x)
S(log(0)) -> S(0)
LOG(s(x)) -> S(log(half(s(x))))
LOG(s(x)) -> LOG(half(s(x)))
LOG(s(x)) -> HALF(s(x))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Remaining
HALF(s(s(x))) -> HALF(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
s(log(0)) -> s(0)
log(s(x)) -> s(log(half(s(x))))
HALF(s(s(x))) -> HALF(x)
trivial
HALF(x1) -> HALF(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Remaining
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
s(log(0)) -> s(0)
log(s(x)) -> s(log(half(s(x))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
LOG(s(x)) -> LOG(half(s(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
s(log(0)) -> s(0)
log(s(x)) -> s(log(half(s(x))))