R
↳Dependency Pair Analysis
AFTER(s(N), cons(X, XS)) -> AFTER(N, activate(XS))
AFTER(s(N), cons(X, XS)) -> ACTIVATE(XS)
ACTIVATE(nfrom(X)) -> FROM(activate(X))
ACTIVATE(nfrom(X)) -> ACTIVATE(X)
ACTIVATE(ns(X)) -> S(activate(X))
ACTIVATE(ns(X)) -> ACTIVATE(X)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
ACTIVATE(ns(X)) -> ACTIVATE(X)
ACTIVATE(nfrom(X)) -> ACTIVATE(X)
from(X) -> cons(X, nfrom(ns(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
s(X) -> ns(X)
activate(nfrom(X)) -> from(activate(X))
activate(ns(X)) -> s(activate(X))
activate(X) -> X
ACTIVATE(ns(X)) -> ACTIVATE(X)
ACTIVATE(nfrom(X)) -> ACTIVATE(X)
ACTIVATE(x1) -> ACTIVATE(x1)
ns(x1) -> ns(x1)
nfrom(x1) -> nfrom(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Nar
from(X) -> cons(X, nfrom(ns(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
s(X) -> ns(X)
activate(nfrom(X)) -> from(activate(X))
activate(ns(X)) -> s(activate(X))
activate(X) -> X
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Narrowing Transformation
AFTER(s(N), cons(X, XS)) -> AFTER(N, activate(XS))
from(X) -> cons(X, nfrom(ns(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
s(X) -> ns(X)
activate(nfrom(X)) -> from(activate(X))
activate(ns(X)) -> s(activate(X))
activate(X) -> X
three new Dependency Pairs are created:
AFTER(s(N), cons(X, XS)) -> AFTER(N, activate(XS))
AFTER(s(N), cons(X, nfrom(X''))) -> AFTER(N, from(activate(X'')))
AFTER(s(N), cons(X, ns(X''))) -> AFTER(N, s(activate(X'')))
AFTER(s(N), cons(X, XS')) -> AFTER(N, XS')
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Remaining Obligation(s)
AFTER(s(N), cons(X, XS')) -> AFTER(N, XS')
AFTER(s(N), cons(X, ns(X''))) -> AFTER(N, s(activate(X'')))
AFTER(s(N), cons(X, nfrom(X''))) -> AFTER(N, from(activate(X'')))
from(X) -> cons(X, nfrom(ns(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
s(X) -> ns(X)
activate(nfrom(X)) -> from(activate(X))
activate(ns(X)) -> s(activate(X))
activate(X) -> X