(24) Section 5.1.6 (Implicit Switch Branches?) What is the behavior of if (open) I(p,n) <+ 5; Is this equivalent to; if (open) I(p,n) <+ 5; else I(p,n) <+ 0; Recommendation: These should be considered the same, clarify in LRM.