View on GitHub
File Changes
      & \fun{currentIssueNo} \in \OCertEnv \to (\KeyHash_{pool} \to \N)
                                           \to \KeyHash_{pool}
                                           \to \N^? \\
-
      & \fun{currentIssueNo}~(\var{stpools}, \var{genDelegs})~ \var{cs} ~\var{hk} \\
-
      & \begin{array}{ccl}
-
        ~~~~ & | & \var{hk}\mapsto \var{n} \in \var{cs} = n \\
-
        ~~~~ & | & \var{hk} \in \var{stpools} = 0 \\
-
        ~~~~ & | & \var{hk} \in \var{genDelegs} = 0 \\
-
        ~~~~ & | & \text{otherwise} = \Nothing
-
      \end{array}
+
      & \fun{currentIssueNo}~(\var{stpools}, \var{genDelegs})~ \var{cs} ~\var{hk} =
+
      \begin{cases}
+
        \var{hk}\mapsto \var{n} \in \var{cs} & n \\
+
        \var{hk} \in \var{stpools} & 0 \\
+
        \var{hk} \in \var{genDelegs} & 0 \\
+
        \text{otherwise} & \Nothing
+
      \end{cases}
  \end{align*}
  \caption{OCert transition-system types}
  \label{fig:ts-types:ocert}