Term Rewriting System R:

   []
   f(a, b) -> f(a, c)
   f(c, d) -> f(b, d)

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: 


   F(c, d) -> F(b, d)
   F(a, b) -> F(a, c)

R contains no SCCs.




Termination of R successfully shown.


Duration: 0.375 seconds.