The sequence carries the environment from one command to the next. A \mathsf{ret} interrupts the sequence.

\dfrac{}{\Gamma \vdash \varepsilon \dashv \Gamma}\;\textsf{(T-Seq-Empty)}

\dfrac{\Gamma \vdash c \dashv \Gamma_1 \qquad \Gamma_1 \vdash cs \dashv \Gamma_2}{\Gamma \vdash c\ cs \dashv \Gamma_2}\;\textsf{(T-Seq)}

\dfrac{}{\rho, \sigma \vdash \varepsilon \Rightarrow \mathsf{normal}, \rho, \sigma}\;\textsf{(Seq-Empty)}

\dfrac{\rho, \sigma \vdash c \Rightarrow \mathsf{normal}, \rho_1, \sigma_1 \qquad \rho_1, \sigma_1 \vdash cs \Rightarrow r, \rho_2, \sigma_2}{\rho, \sigma \vdash c\ cs \Rightarrow r, \rho_2, \sigma_2}\;\textsf{(Seq)}

\dfrac{\rho, \sigma \vdash c \Rightarrow \mathsf{ret}\,v, \rho_1, \sigma_1}{\rho, \sigma \vdash c\ cs \Rightarrow \mathsf{ret}\,v, \rho_1, \sigma_1}\;\textsf{(Seq-Ret)}

The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.

The block discards the extension of \rho and removes from \sigma the locations it allocated. The function Eval.fresh computes \rho' \setminus \rho restricted to the owned bindings, so the alias a reference declaration made never frees the location it names. Scope is the restoration of \rho, lifetime is the removal from \sigma.

\dfrac{\Gamma \vdash c_1 \ldots c_n \dashv \Gamma'}{\Gamma \vdash \{\, c_1 \ldots c_n \,\} \dashv \Gamma}\;\textsf{(T-Block)}

\dfrac{\rho, \sigma \vdash c_1 \ldots c_n \Rightarrow r, \rho', \sigma'}{\rho, \sigma \vdash \{\, c_1 \ldots c_n \,\} \Rightarrow r, \rho, \sigma' \setminus (\rho' \setminus \rho)}\;\textsf{(Block)}

Some of the implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.