(VAR x y z u v) (RULES if(true,x,y) -> x if(false,x,y) -> y if(x,y,y) -> y if(if(x,y,z),u,v) -> if(x,if(y,u,v),if(z,u,v)) if(x,if(x,y,z),z) -> if(x,y,z) if(x,y,if(x,y,z)) -> if(x,y,z) ) (COMMENT Example 4.23 (If-Then-Else) in \cite{SK90})