from(

after(0,

after(s(

R

↳Dependency Pair Analysis

FROM(X) -> FROM(s(X))

AFTER(s(N), cons(X,XS)) -> AFTER(N,XS)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****FROM(***X*) -> FROM(s(*X*))**Rules:**

from(*X*) -> cons(*X*, from(s(*X*)))

after(0,*XS*) ->*XS*

after(s(*N*), cons(*X*,*XS*)) -> after(*N*,*XS*)**Strategy:**innermost

**Dependency Pair:****AFTER(s(***N*), cons(*X*,*XS*)) -> AFTER(*N*,*XS*)**Rules:**

from(*X*) -> cons(*X*, from(s(*X*)))

after(0,*XS*) ->*XS*

after(s(*N*), cons(*X*,*XS*)) -> after(*N*,*XS*)**Strategy:**innermost

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****FROM(***X*) -> FROM(s(*X*))**Rules:**

from(*X*) -> cons(*X*, from(s(*X*)))

after(0,*XS*) ->*XS*

after(s(*N*), cons(*X*,*XS*)) -> after(*N*,*XS*)**Strategy:**innermost

**Dependency Pair:****AFTER(s(***N*), cons(*X*,*XS*)) -> AFTER(*N*,*XS*)**Rules:**

from(*X*) -> cons(*X*, from(s(*X*)))

after(0,*XS*) ->*XS*

after(s(*N*), cons(*X*,*XS*)) -> after(*N*,*XS*)**Strategy:**innermost

Duration:

0:00 minutes