from(

after(0,

after(s(

R

↳Overlay and local confluence Check

The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost.

R

↳OC

→TRS2

↳Dependency Pair Analysis

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

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

Furthermore,

R

↳OC

→TRS2

↳DPs

→DP Problem 1

↳Usable Rules (Innermost)

**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

As we are in the innermost case, we can delete all 3 non-usable-rules.

R

↳OC

→TRS2

↳DPs

→DP Problem 1

↳UsableRules

...

→DP Problem 3

↳Non Termination

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

none

innermost

Found an infinite P-chain over R:

P =

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

R = none

s = FROM(

evaluates to t =FROM(s(

Thus, s starts an infinite chain as s matches t.

Duration:

0:02 minutes