C_0 = if G_1 [] G_2 fi
G_1 = X >= 0 -> Y := 1
G_2 = X = 0 -> Y := 0
C[[C_0]]s = ...
Case: access [[X]] s = zero
...= { (true, s_1) } where
s_1 = update [[Y]] one s
Case: access [[X]] s > zero
...= { (true, s_1), (true, s_2) } where
s_1 = update [[Y]] one s
s_2 = update [[Y]] zero s
Case: access [[X]] s < zero
...= { (false, s) }