Term Rewriting System R:

   []
   app(f, a) -> app(f, b)
   app(g, b) -> app(g, a)

Termination of R to be shown.


This program has no overlaps, so it is sufficient to show innermost termination. 


R contains the following Dependency Pairs: 


   APP(g, b) -> APP(g, a)
   APP(f, a) -> APP(f, b)

R contains no SCCs.




Termination of R successfully shown.


Duration: 0.374 seconds.