# How to format semantic rules (picture attached)?

I am wondering how to type semantic rules shown in the following picture:

Thanks!

• – cfr
Mar 31 '14 at 3:09
• Please show you have made some effort by posting the code you have so far!
– cfr
Apr 1 '14 at 0:51

\documentclass[a4paper]{article}
\usepackage{geometry}
\usepackage{amsmath,mathtools,bussproofs,turnstile}

\begin{document}

\noindent
\begin{prooftree}
\def\ScoreOverhang{1pt}
\AxiomC{}
\UnaryInfC{$so, E, S \sststile{}{} 2: Int(2), S$}
\AxiomC{$\cdots$}\RightLabel{(2)}
\UnaryInfC{$so, E[l_{new}/x], S[Int(2)/l_{new}] \sststile{}{} \text{while } 1 < x \text{ loop } x \leftarrow x - 1 \text{ pool } : void, S_{final}$}\RightLabel{(3)}
\BinaryInfC{$so, E, S \sststile{}{} \text{ let } x : Int \leftarrow 2 \text{ in while } 1 < \text{ loop } x \leftarrow x - 1 \text{ pool } : void, S_{final}$}
\end{prooftree}

\end{document}