\documentclass[12pt]{article}

\usepackage[paper=a4paper, landscape=true,left=2cm,top=2cm,bottom=2cm,right=2cm]{geometry}

\usepackage{mathpazo}

\usepackage{amssymb}
\usepackage{amsmath}

%%\usepackage{lscape}

\usepackage{bussproofs}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}

\newcommand{\ra}[0]{\rightarrow}
\newcommand{\tn}[0]{\textnormal}

\EnableBpAbbreviations

\newcommand{\T}[3]{\begin{tabular}{c}#1 \\ #2 \\ #3\end{tabular}}

\begin{document}
Theorie der Programmiersprachen, Übung 2 -- Johannes Rössel, Klaus Grohnwaldt, Johanna Frank

  \begin{footnotesize}
    \begin{prooftree}

          \AXC{$[ass_1]$}
        \UIC{$\left< z := 0,s\right>\ra s\left[x\ra 17,y\ra 5,z\ra 0\right]$}
        \AXC{(1)}
        \RL{$[comp]$}
      \BIC{$\left< z := 0; \tn{ while } y \le x \tn{ do } z := z + 1; x := x - y \tn{ end},s\right>\ra s\left[x\ra 2,y\ra 5,z\ra 3\right]$}
      
    \end{prooftree}

    \begin{prooftree}

            \AXC{$[ass_1]$}
          \UIC{$\left< z:=z+1,s\left[ x\ra 17, y\ra 5, z\ra 0 \right]\right>\ra s\left[ x\ra 17, y\ra 5, z\ra 1 \right]$}
            \AXC{$[ass_1]$}
          \UIC{$\left< x:=x-y,s\left[ x\ra 17, y\ra 5, z\ra 1 \right] \right>\ra s\left[ x\ra 12, y\ra 5, z\ra 1 \right]$}
          \RL{$[comp]$}
        \BIC{$\left< z := z + 1; x:=x-y,s\left[x\ra 17,y\ra 5,z\ra 0\right]\right>\ra s\left[x\ra 12,y\ra 5,z\ra 1\right]$}
        \AXC{(2)}
        \RL{$[while_1]$}
      \BIC{$\left< \tn{ while } y\le x \tn{ do } z:=z+1;x:=x-y \tn{ end},s\left[x\ra 17,y\ra 5,z\ra 0\right]\right>\ra s\left[x\ra 2,y\ra 5,z\ra 3\right]$}
      \UIC{(1)}

    \end{prooftree}

    \begin{prooftree}
            \AXC{$[ass_1]$}
          \UIC{$\left< z:=z+1,s\left[ x\ra 12, y\ra 5, z\ra 1 \right]\right>\ra s\left[ x\ra 12, y\ra 5, z\ra 2 \right]$}
            \AXC{$[ass_1]$}
          \UIC{$\left< x:=x-y,s\left[ x\ra 12, y\ra 5, z\ra 2 \right] \right>\ra s\left[ x\ra 7, y\ra 5, z\ra 2 \right]$}
          \RL{$[comp]$}
        \BIC{$\left< z := z + 1; x:=x-y,s\left[x\ra 12,y\ra 5,z\ra 1\right]\right>\ra s\left[x\ra 7,y\ra 5,z\ra 2\right]$}
        \AXC{(3)}
        \RL{$[while_1]$}
      \BIC{$\left< \tn{ while } y\le x \tn{ do } z:=z+1;x:=x-y \tn{ end},s\left[x\ra 12,y\ra 5,z\ra 1\right]\right>\ra s\left[x\ra 2,y\ra 5,z\ra 3\right]$}
      \UIC{(2)}

    \end{prooftree}

    \begin{prooftree}
            \AXC{$[ass_1]$}
          \UIC{$\left< z:=z+1,s\left[ x\ra 7, y\ra 5, z\ra 2 \right]\right>\ra s\left[ x\ra 7, y\ra 5, z\ra 3 \right]$}
            \AXC{$[ass_1]$}
          \UIC{$\left< x:=x-y,s\left[ x\ra 7, y\ra 5, z\ra 3 \right] \right>\ra s\left[ x\ra 2, y\ra 5, z\ra 3 \right]$}
          \RL{$[comp]$}
        \BIC{$\left< z := z + 1; x:=x-y,s\left[x\ra 7,y\ra 5,z\ra 2\right]\right>\ra s\left[x\ra 2,y\ra 5,z\ra 3\right]$}
        \AXC{(4)}
        \RL{$[while_1]$}
      \BIC{$\left< \tn{ while } y\le x \tn{ do } z:=z+1;x:=x-y \tn{ end},s\left[x\ra 12,y\ra 5,z\ra 2\right]\right>\ra s\left[x\ra 2,y\ra 5,z\ra 3\right]$}
      \UIC{(3)}

    \end{prooftree}

    \begin{prooftree}
      \AXC{$[while_2]$}
      \UIC{$\left< \tn{ while } y\le x \tn{ do } z:=z+1;x:=x-y \tn{ end},s\left[x\ra 2,y\ra 5,z\ra 3\right]\right>\ra s\left[x\ra 2,y\ra 5,z\ra 3\right]$}
      \UIC{(4)}

    \end{prooftree}
  \end{footnotesize}

\end{document}