zeros -> cons(0, zeros)

tail(cons(

R

↳Removing Redundant Rules

Removing the following rules from

tail(cons(X,XS)) ->XS

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(cons(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(tail(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(zeros)= 0 _{ }^{ }

Not all Rules of

R

↳RRRPolo

→TRS2

↳Dependency Pair Analysis

ZEROS -> ZEROS

Furthermore,

R

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳Usable Rules (Innermost)

**ZEROS -> ZEROS**

zeros -> cons(0, zeros)

innermost

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

R

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳UsableRules

...

→DP Problem 2

↳Non Termination

**ZEROS -> ZEROS**

none

innermost

Found an infinite P-chain over R:

P =

ZEROS -> ZEROS

R = none

s = ZEROS

evaluates to t =ZEROS

Thus, s starts an infinite chain.

Duration:

0:03 minutes