In case 5 of definition 5 of figure 3 (safety constraints on flows), you are
say
if b is x = case y of ... | Ci zi ei => ..., then for all i,
but what you meant was
if b is case y of ... | Ci zi => ei | ..., then for all i,
(Note, the ei is to the right of the =>, you have | on both sides, and b is
just the right-hand side of a binding.)
In case 9, some how you say flow(z) instead of F(z).