R
↳Dependency Pair Analysis
FROM(X) -> CONS(X, nfrom(s(X)))
LENGTH(ncons(X, Y)) -> LENGTH1(activate(Y))
LENGTH(ncons(X, Y)) -> ACTIVATE(Y)
LENGTH1(X) -> LENGTH(activate(X))
LENGTH1(X) -> ACTIVATE(X)
ACTIVATE(nfrom(X)) -> FROM(X)
ACTIVATE(nnil) -> NIL
ACTIVATE(ncons(X1, X2)) -> CONS(X1, X2)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
LENGTH1(X) -> LENGTH(activate(X))
LENGTH(ncons(X, Y)) -> LENGTH1(activate(Y))
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
length(nnil) -> 0
length(ncons(X, Y)) -> s(length1(activate(Y)))
length1(X) -> length(activate(X))
nil -> nnil
cons(X1, X2) -> ncons(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(ncons(X1, X2)) -> cons(X1, X2)
activate(X) -> X
four new Dependency Pairs are created:
LENGTH1(X) -> LENGTH(activate(X))
LENGTH1(nfrom(X'')) -> LENGTH(from(X''))
LENGTH1(nnil) -> LENGTH(nil)
LENGTH1(ncons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH1(X'') -> LENGTH(X'')
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
LENGTH1(X'') -> LENGTH(X'')
LENGTH1(ncons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH1(nnil) -> LENGTH(nil)
LENGTH1(nfrom(X'')) -> LENGTH(from(X''))
LENGTH(ncons(X, Y)) -> LENGTH1(activate(Y))
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
length(nnil) -> 0
length(ncons(X, Y)) -> s(length1(activate(Y)))
length1(X) -> length(activate(X))
nil -> nnil
cons(X1, X2) -> ncons(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(ncons(X1, X2)) -> cons(X1, X2)
activate(X) -> X
two new Dependency Pairs are created:
LENGTH1(nfrom(X'')) -> LENGTH(from(X''))
LENGTH1(nfrom(X''')) -> LENGTH(cons(X''', nfrom(s(X'''))))
LENGTH1(nfrom(X''')) -> LENGTH(nfrom(X'''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
LENGTH1(nfrom(X''')) -> LENGTH(cons(X''', nfrom(s(X'''))))
LENGTH1(ncons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH1(nnil) -> LENGTH(nil)
LENGTH(ncons(X, Y)) -> LENGTH1(activate(Y))
LENGTH1(X'') -> LENGTH(X'')
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
length(nnil) -> 0
length(ncons(X, Y)) -> s(length1(activate(Y)))
length1(X) -> length(activate(X))
nil -> nnil
cons(X1, X2) -> ncons(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(ncons(X1, X2)) -> cons(X1, X2)
activate(X) -> X
one new Dependency Pair is created:
LENGTH1(nnil) -> LENGTH(nil)
LENGTH1(nnil) -> LENGTH(nnil)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
LENGTH1(X'') -> LENGTH(X'')
LENGTH1(ncons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH(ncons(X, Y)) -> LENGTH1(activate(Y))
LENGTH1(nfrom(X''')) -> LENGTH(cons(X''', nfrom(s(X'''))))
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
length(nnil) -> 0
length(ncons(X, Y)) -> s(length1(activate(Y)))
length1(X) -> length(activate(X))
nil -> nnil
cons(X1, X2) -> ncons(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(ncons(X1, X2)) -> cons(X1, X2)
activate(X) -> X
one new Dependency Pair is created:
LENGTH1(ncons(X1', X2')) -> LENGTH(cons(X1', X2'))
LENGTH1(ncons(X1'', X2'')) -> LENGTH(ncons(X1'', X2''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Remaining Obligation(s)
LENGTH1(ncons(X1'', X2'')) -> LENGTH(ncons(X1'', X2''))
LENGTH1(nfrom(X''')) -> LENGTH(cons(X''', nfrom(s(X'''))))
LENGTH(ncons(X, Y)) -> LENGTH1(activate(Y))
LENGTH1(X'') -> LENGTH(X'')
from(X) -> cons(X, nfrom(s(X)))
from(X) -> nfrom(X)
length(nnil) -> 0
length(ncons(X, Y)) -> s(length1(activate(Y)))
length1(X) -> length(activate(X))
nil -> nnil
cons(X1, X2) -> ncons(X1, X2)
activate(nfrom(X)) -> from(X)
activate(nnil) -> nil
activate(ncons(X1, X2)) -> cons(X1, X2)
activate(X) -> X