Term Rewriting System R:

   [X, Y]
   f(X) -> if(X, c, f(true))
   if(true, X, Y) -> X
   if(false, X, Y) -> Y

Termination of R to be shown.


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

   if(false, X, Y) -> Y

where the Polynomial interpretation:
POL(true) = 0
POL(f(x_1)) = x_1
POL(c) = 0
POL(if(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(false) = 1
was used. 



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


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


R contains the following Dependency Pairs: 


   F(X) -> IF(X, c, f(true))
   F(X) -> F(true)

Furthermore, R contains one SCC.


SCC1:

F(X) -> F(true)

Found an infinite P-chain over R:
P = F(X) -> F(true)
R = []
s = F(true) evaluates to t = F(true)
Thus, s starts an infinite reduction.


Non-Termination of R could be shown.

Duration: 0.467 seconds.