f(h(

f(i(

i(

TRS

↳Removing Redundant Rules

Removing the following rules from

f(i(x)) -> a

where the Polynomial interpretation:

was used.

_{ }^{ }POL(i(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(h(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a)= 0 _{ }^{ }_{ }^{ }POL(f(x)_{1})= 1 + x _{1}_{ }^{ }

Not all Rules of

TRS

↳RRRPolo

→TRS2

↳Dependency Pair Analysis

F(h(x)) -> F(i(x))

F(h(x)) -> I(x)

Furthermore,

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳Non Termination

**F(h( x)) -> F(i(x))**

i(x) -> h(x)

f(h(x)) -> f(i(x))

Found an infinite P-chain over R:

P =

F(h(x)) -> F(i(x))

R =

i(x) -> h(x)

f(h(x)) -> f(i(x))

s = F(i(

evaluates to t =F(i(

Thus, s starts an infinite chain.

Duration:

0:01 minutes