1\THEOREM DELETE_INSERT pred_sets 2|- !x y s. 3 (x INSERT s) DELETE y = 4 ((x = y) => s DELETE y | x INSERT (s DELETE y)) 5\ENDTHEOREM 6