16.1.5 The Boolean Operator !

• V is definitely assigned after !a when true iff V is definitely assigned after a when false.
• V is definitely assigned after !a when false iff V is definitely assigned after a when true.
• V is definitely assigned before a iff V is definitely assigned before !a.