Term Rewriting System R:
[x, y]
ap(ap(g, x), y) -> y
ap(f, x) -> ap(f, app(g, x))

Innermost Termination of R to be shown.



   R
Removing Redundant Rules



Removing the following rules from R which fullfill a polynomial ordering:

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

where the Polynomial interpretation:
  POL(g)=  0  
  POL(ap(x1, x2))=  1 + x1 + x2  
  POL(f)=  0  
  POL(app(x1, x2))=  x1 + x2  
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R.


   R
RRRPolo
       →TRS2
Dependency Pair Analysis



R contains the following Dependency Pairs:

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

Furthermore, R contains one SCC.


   R
RRRPolo
       →TRS2
DPs
           →DP Problem 1
Usable Rules (Innermost)


Dependency Pair:

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


Rule:


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


Strategy:

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


Dependency Pair:

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


Rule:

none


Strategy:

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


Dependency Pair:

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


Rule:

none


Strategy:

innermost




Found an infinite P-chain over R:
P =

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

R = none

s = F(x)
evaluates to t =F(g(x))

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

Innermost Non-Termination of R could be shown.
Duration:
0:01 minutes