ap(ap(g,

ap(f,

R

↳Removing Redundant Rules

Removing the following rules from

ap(ap(g,x),y) ->y

where the Polynomial interpretation:

was used.

_{ }^{ }POL(g)= 0 _{ }^{ }_{ }^{ }POL(ap(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f)= 0 _{ }^{ }_{ }^{ }POL(app(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }

Not all Rules of

R

↳RRRPolo

→TRS2

↳Dependency Pair Analysis

AP(f,x) -> AP(f, app(g,x))

Furthermore,

R

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳Usable Rules (Innermost)

**AP(f, x) -> AP(f, app(g, x))**

ap(f,x) -> ap(f, app(g,x))

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

↳A-Transformation

**AP(f, x) -> AP(f, app(g, x))**

none

innermost

We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.

R

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳UsableRules

...

→DP Problem 3

↳Non Termination

**F( x) -> F(g(x))**

none

innermost

Found an infinite P-chain over R:

P =

F(x) -> F(g(x))

R = none

s = F(

evaluates to t =F(g(

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

Duration:

0:01 minutes