\documentclass[a4paper]{article}

\usepackage[bottom=2cm]{geometry}
\usepackage[english]{babel}

\usepackage{enumitem}
\setenumerate[1]{label=(\alph*)}

\usepackage{fancyhdr}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\fancyhead{}
\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
\pagestyle{fancy}

\usepackage{sv}

\title{Software Verification - assignment 4}
\author{Camil Staps}

\usepackage{rotating}
\usepackage{amsmath}
\usepackage{mathpartir}

\def\List#1{\mathbf{List}(#1)}
\def\Nil{\mathbf{Nil}}
\def\Cons#1#2{\mathbf{Cons}\;#1\;#2}
\def\empt#1{\text{empty}(#1)}
\def\hd#1{\text{hd}(#1)}
\def\tl#1{\text{tl}(#1)}
\def\xs{\mathit{xs}}
\def\ys{\mathit{ys}}
\def\true{\mathbf{true}}
\def\false{\mathbf{false}}
\def\tapp{\tau_{\mathit{app}}}

\begin{document}

\maketitle
\thispagestyle{fancy}

\setcounter{section}{1}
\section{Lists for ML}
\begin{enumerate}
  \item \begin{align*}
      %\tau &::=\enspace \dots\\
      %  &\enspace\enspace|\quad\, \List{\tau}\\
      l &::=\enspace \Nil\\
        &\enspace\enspace|\quad\, \Cons{e}{l}\\
      e &::=\enspace \dots\\
        &\enspace\enspace|\quad\, l\\
        &\enspace\enspace|\quad\, \empt{e}\\
        &\enspace\enspace|\quad\, \hd{e}\\
        &\enspace\enspace|\quad\, \tl{e}\\
    \end{align*}

  \item \begin{mathpar}
      \inferrule*[right=list]
        {\xs \in l} {\xs \eval \xs} \qquad
      \inferrule*[right=hd]
        {\xs \eval \Cons{e}{l}} {\hd\xs \eval e} \qquad
      \inferrule*[right=tl]
        {\xs \eval \Cons{e}{l}} {\tl\xs \eval l} \\
      \inferrule*[right=empty\_true]
        {\xs \eval \Nil} {\empt\xs \eval \true} \qquad
      \inferrule*[right=empty\_false]
        {\xs \eval \Cons e l} {\empt\xs \eval \false}
    \end{mathpar}

  \item $$\mathit{append}=\lambda \xs \ys.\mlif{(\xs=\Nil)}{\ys}{(\Cons{\hd\xs}{\mathit{append}(\tl\xs)(\ys)})}.$$

  \item \begin{mathpar}
      \inferrule*[right=nil]
        {l=\Nil}{\Gamma\vdash l:\List{\sigma}} \qquad
      \inferrule*[right=cons]
        {\Gamma\vdash e:\sigma \quad \Gamma\vdash l:\List{\sigma}}{\Gamma\vdash\Cons{e}{l}:\List{\sigma}} \\
      \inferrule*[right=hd]
        {\Gamma\vdash l:\List\sigma}{\hd{l}:\sigma} \qquad
      \inferrule*[right=tl]
        {\Gamma\vdash l:\List\sigma}{\tl{l}:\List\sigma} \qquad
      \inferrule*[right=empty]
        {\Gamma\vdash l:\List\sigma}{\empt{l}:\Bool} \qquad
    \end{mathpar}

  \item 
    \begin{sidewaysfigure}\begin{mathpar}\scriptsize
      \inferrule*[right=Lambda]
        {
          \inferrule*[right=If]
            {
              \inferrule*[right=Bin Op]
                {
                  = : (\List\sigma, \List\sigma)\to\Bool \\\\
                  \Gamma \vdash \xs:\List\sigma \and
                  \inferrule*[right=nil]{}{\Gamma \vdash \Nil:\List\sigma}
                }
                {\Gamma \vdash (\xs=\Nil):\Bool}
              \and
              \Gamma \vdash \ys:\List\sigma
              \and
              \inferrule*[right=cons]
                {
                  \inferrule*[right=hd]{\Gamma\vdash\xs:\List\sigma}{\Gamma \vdash \hd\xs:\sigma}
                  \and
                  \inferrule*[right=App]
                    {
                      \inferrule*[right=App]
                        {
                          \Gamma \vdash \mathit{a}:\tapp \and
                          \inferrule*[right=tl]
                            {\Gamma \vdash \xs:\List\sigma}
                            {\Gamma \vdash \tl\xs:\List\sigma}
                        }
                        {\Gamma \vdash \mathit{a}(\tl\xs):\List\sigma\to\List\sigma}
                      \and
                      \Gamma \vdash \ys:\List\sigma
                    } %todo
                    {\Gamma \vdash \mathit{a}(\tl\xs)(\ys):\List\sigma}
                }
                {\Gamma \vdash \Cons{\hd\xs}{\mathit{a}(\tl\xs)(\ys)}:\List\sigma}
            } %todo
            {\Gamma \vdash \mlif{(\xs=\Nil)}{\ys}{(\Cons{\hd\xs}{\mathit{a}(\tl\xs)(\ys)})} : \List\sigma}
        }
        {\mathit{a}:\tapp \vdash \lambda \xs \ys.\mlif{(\xs=\Nil)}{\ys}{(\Cons{\hd\xs}{\mathit{a}(\tl\xs)(\ys)})} : \tapp} \\

        \setlength\arraycolsep{1pt}
        \begin{array}{rl}
          \text{where}\qquad a & \stackrel{\text{def}}{=} \mathit{append}, \\
                    \tapp & \stackrel{\text{def}}{=} \List\sigma\;\List\sigma\to\List\sigma, \\
                        \Gamma & \stackrel{\text{def}}{=} \xs:\List\sigma, \ys:\List\sigma, \mathit{a}:\tapp.
        \end{array}
      \end{mathpar}\end{sidewaysfigure}
\end{enumerate}

\end{document}