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
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
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
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
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
→DP Problem 2
↳Remaining Obligation(s)
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
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