YS
\implies бóльшие промужутки, чем у других операторов (в данном случае он трактуется не как бинарный, и ставятся дополнительные).\let\saveimplies=\implies
\renewcommand*{\implies}{\mathbin{\Rightarrow}}Size: a a a
H
\begin{figure}[H]
\caption{Computational rules}
\begin{align*}
(v): \ & \langle K; A; v(\overline{tok}) \ t \ \overline{t'} \rangle & \to_1 &
\langle K; A, \ \overline{tok}; t \ \overline{t'} \rangle \\
(v\mbox{-}end): \ & \langle K; A; v(\overline{tok}) \rangle & \to_1 &
K(unseq(A, \overline{tok})) \\
(op): \ & \langle K; A; call(\overline{t}, \overline{a}) \ \overline{t'} \rangle & \to_1 &
\langle \langle K; A; call(?, \overline{a}) \ \overline{t'} \rangle; (); \overline{t} \rangle \\
(args): \ & \langle K; A; call(ident, \overline{a}) \ \overline{t} \rangle & \to_1 & \\
\langle \langle K; A; ident(unseq\mbox{-}cs(?)) \ \overline{t} \rangle; (); \overline{a} \rangle \\
(start): \ & MACROLOP\_EVAL(t \ \overline{t'}) & \to_1 &
\langle halt; (); t \ \overline{t'} \rangle
\end{align*}
\end{figure}NK

(args): \ & \langle K; A; call(ident, \overline{a}) \ \overline{t} \rangle & \to_1 & \langle \\
\langle K; A; ident(unseq\mbox{-}cs(?)) \ \overline{t} \rangle; (); \overline{a} \rangle \\(args) в конце & \\ перенос лишний, просто &