if
(
e)
S iff V is definitely assigned after S and V is definitely assigned after e when false.
if
(
e)
S. V is definitely assigned before S iff V is definitely assigned after e when true.
if
(
e)
S else
T iff V is definitely assigned after S and V is definitely assigned after T.
if (
e)
S else
T. V is definitely assigned before S iff V is definitely assigned after e when true. V is definitely assigned before T iff V is definitely assigned after e when false.