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

↳Instantiation Transformation

→DP Problem 2

↳Remaining

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

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

after(0,XS) ->XS

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

innermost

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****FROM(s(***X''*)) -> FROM(s(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

↳Inst

→DP Problem 2

↳Remaining Obligation(s)

The following remains to be proven:

**Dependency Pair:****FROM(s(***X''*)) -> FROM(s(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