Term Rewriting System R:

   [x, y, z]
   del(.(x, .(y, z))) -> f(=(x, y), x, y, z)
   f(true, x, y, z) -> del(.(y, z))
   f(false, x, y, z) -> .(x, del(.(y, z)))
   =(nil, nil) -> true
   =(.(x, y), nil) -> false
   =(nil, .(y, z)) -> false
   =(.(x, y), .(u, v)) -> and(=(x, u), =(y, v))

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: 


   ='(.(x, y), .(u, v)) -> ='(x, u)
   ='(.(x, y), .(u, v)) -> ='(y, v)
   DEL(.(x, .(y, z))) -> F(=(x, y), x, y, z)
   DEL(.(x, .(y, z))) -> ='(x, y)
   F(true, x, y, z) -> DEL(.(y, z))
   F(false, x, y, z) -> DEL(.(y, z))

Furthermore, R contains one SCC.


SCC1:

F(false, x, y, z) -> DEL(.(y, z))
F(true, x, y, z) -> DEL(.(y, z))
DEL(.(x, .(y, z))) -> F(=(x, y), x, y, z)

By using a polynomial ordering, at least one Dependency Pair of this SCC can be strictly oriented.

Additionally, the following rules can be oriented: 

   =(.(x, y), nil) -> false
   =(nil, nil) -> true
   =(nil, .(y, z)) -> false
   =(.(x, y), .(u, v)) -> and(=(x, u), =(y, v))


Used ordering: Polynomial ordering with Polynomial interpretation:
POL(nil) = 1
POL(v) = 0
POL(DEL(x_1)) = x_1
POL(true) = 1
POL(and(x_1, x_2)) = 0
POL(F(x_1, x_2, x_3, x_4)) = 1 + x_1 + x_3 + x_4
POL(u) = 0
POL(=(x_1, x_2)) = x_1
POL(.(x_1, x_2)) = 1 + x_1 + x_2
POL(false) = 1

 resulting in no subcycles.




Termination of R successfully shown.


Duration: 0.759 seconds.