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(X)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
AFTER(s(N), cons(X, XS)) -> AFTER(N, activate(XS))
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(X) -> X
two 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(X''))
AFTER(s(N), cons(X, XS')) -> AFTER(N, XS')
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
AFTER(s(N), cons(X, XS')) -> AFTER(N, XS')
AFTER(s(N), cons(X, nfrom(X''))) -> AFTER(N, from(X''))
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(X) -> X
two new Dependency Pairs are created:
AFTER(s(N), cons(X, nfrom(X''))) -> AFTER(N, from(X''))
AFTER(s(N), cons(X, nfrom(X'''))) -> AFTER(N, cons(X''', nfrom(s(X'''))))
AFTER(s(N), cons(X, nfrom(X'''))) -> AFTER(N, nfrom(X'''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Polynomial Ordering
AFTER(s(N), cons(X, nfrom(X'''))) -> AFTER(N, cons(X''', nfrom(s(X'''))))
AFTER(s(N), cons(X, XS')) -> AFTER(N, XS')
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(X) -> X
AFTER(s(N), cons(X, nfrom(X'''))) -> AFTER(N, cons(X''', nfrom(s(X'''))))
AFTER(s(N), cons(X, XS')) -> AFTER(N, XS')
POL(n__from(x1)) = 0 POL(AFTER(x1, x2)) = x1 POL(cons(x1, x2)) = 0 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Dependency Graph
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
after(0, XS) -> XS
after(s(N), cons(X, XS)) -> after(N, activate(XS))
activate(nfrom(X)) -> from(X)
activate(X) -> X