This is pedantic, but could you please try to follow the formatting style used in the rest of the semantics? E.g., 5 space indents, "when" on a line by itself, 80 character lines (although I often make exceptions when line breaks are particularly awkward). I have a short list of some of the conventions I've adopted here:

https://github.com/kframework/c-semantics/tree/master/semantics/README.md