Term Rewriting System R:

   [X, Y, X1, X2, X3]
   a__f(X) -> a__if(mark(X), c, f(true))
   a__f(X) -> f(X)
   a__if(true, X, Y) -> mark(X)
   a__if(false, X, Y) -> mark(Y)
   a__if(X1, X2, X3) -> if(X1, X2, X3)
   mark(f(X)) -> a__f(mark(X))
   mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3)
   mark(c) -> c
   mark(true) -> true
   mark(false) -> false

Termination of R to be shown.


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

   a__f(X) -> f(X)

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



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


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

   a__if(false, X, Y) -> mark(Y)

where the Polynomial interpretation:
POL(a__f(x_1)) = x_1
POL(true) = 0
POL(a__if(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(mark(x_1)) = x_1
POL(c) = 0
POL(f(x_1)) = x_1
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.


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

   a__f(X) -> a__if(mark(X), c, f(true))

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



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


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

   a__if(true, X, Y) -> mark(X)

where the Polynomial interpretation:
POL(a__f(x_1)) = x_1
POL(true) = 1
POL(a__if(x_1, x_2, x_3)) = x_1 + x_2 + x_3
POL(mark(x_1)) = x_1
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) = 0
was used. 



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


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

   a__if(X1, X2, X3) -> if(X1, X2, X3)

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



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


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

   mark(f(X)) -> a__f(mark(X))

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



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


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

   mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3)

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



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


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

   mark(c) -> c

where the Polynomial interpretation:
POL(true) = 0
POL(mark(x_1)) = 2*x_1
POL(c) = 1
POL(false) = 0
was used. 



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


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

   mark(true) -> true
   mark(false) -> false

where the Polynomial interpretation:
POL(true) = 0
POL(mark(x_1)) = 1 + x_1
POL(false) = 0
was used. 



All Rules of R can be deleted.



Termination of R successfully shown.


Duration: 0.558 seconds.