R
↳Dependency Pair Analysis
HALF(s(s(x))) -> HALF(x)
LASTBIT(s(s(x))) -> LASTBIT(x)
CONV(s(x)) -> CONV(half(s(x)))
CONV(s(x)) -> HALF(s(x))
CONV(s(x)) -> LASTBIT(s(x))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
HALF(s(s(x))) -> HALF(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(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 4
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
LASTBIT(s(s(x))) -> LASTBIT(x)
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
LASTBIT(s(s(x))) -> LASTBIT(x)
trivial
LASTBIT(x1) -> LASTBIT(x1)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Nar
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Narrowing Transformation
CONV(s(x)) -> CONV(half(s(x)))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
two new Dependency Pairs are created:
CONV(s(x)) -> CONV(half(s(x)))
CONV(s(0)) -> CONV(0)
CONV(s(s(x''))) -> CONV(s(half(x'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Narrowing Transformation
CONV(s(s(x''))) -> CONV(s(half(x'')))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
three new Dependency Pairs are created:
CONV(s(s(x''))) -> CONV(s(half(x'')))
CONV(s(s(0))) -> CONV(s(0))
CONV(s(s(s(0)))) -> CONV(s(0))
CONV(s(s(s(s(x'))))) -> CONV(s(s(half(x'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 7
↳Argument Filtering and Ordering
CONV(s(s(s(s(x'))))) -> CONV(s(s(half(x'))))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))
CONV(s(s(s(s(x'))))) -> CONV(s(s(half(x'))))
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
s > half
CONV(x1) -> CONV(x1)
s(x1) -> s(x1)
half(x1) -> half(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Nar
→DP Problem 6
↳Nar
...
→DP Problem 8
↳Dependency Graph
half(0) -> 0
half(s(0)) -> 0
half(s(s(x))) -> s(half(x))
lastbit(0) -> 0
lastbit(s(0)) -> s(0)
lastbit(s(s(x))) -> lastbit(x)
conv(0) -> cons(nil, 0)
conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))