f(h(

f(i(

i(

R

↳Removing Redundant Rules for Innermost Termination

Removing the following rules from

f(i(x)) -> a

R

↳RRRI

→TRS2

↳Dependency Pair Analysis

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

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

Furthermore,

R

↳RRRI

→TRS2

↳DPs

→DP Problem 1

↳Non Termination

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

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

i(x) -> h(x)

Found an infinite P-chain over R:

P =

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

R =

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

i(x) -> h(x)

s = F(i(

evaluates to t =F(i(

Thus, s starts an infinite chain.

Duration:

0:07 minutes