(VAR x y z )
(RULES 
        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))
        
)