I would change the stack diagram for `of` to `( C: case-sys1 -- case-sys2 of-sys )` — this stack diagram will formally allow the system to throw an exception if _case-sys1_ is absent on the top of the control-flow stack, and it will require a program to restore _case-sys1_ if it is temporary removed (and the data stack is used for the control-flow stack items).