R
↳Dependency Pair Analysis
HALF(s(s(x))) -> HALF(x)
LOG(s(s(x))) -> LOG(s(half(x)))
LOG(s(s(x))) -> HALF(x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
HALF(s(s(x))) -> HALF(x)
half(0) -> 0
half(s(s(x))) -> s(half(x))
log(s(0)) -> 0
log(s(s(x))) -> s(log(s(half(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
↳AFS
half(0) -> 0
half(s(s(x))) -> s(half(x))
log(s(0)) -> 0
log(s(s(x))) -> s(log(s(half(x))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
LOG(s(s(x))) -> LOG(s(half(x)))
half(0) -> 0
half(s(s(x))) -> s(half(x))
log(s(0)) -> 0
log(s(s(x))) -> s(log(s(half(x))))
LOG(s(s(x))) -> LOG(s(half(x)))
half(0) -> 0
half(s(s(x))) -> s(half(x))
s > half
LOG(x1) -> LOG(x1)
s(x1) -> s(x1)
half(x1) -> half(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 4
↳Dependency Graph
half(0) -> 0
half(s(s(x))) -> s(half(x))
log(s(0)) -> 0
log(s(s(x))) -> s(log(s(half(x))))