asdfasfdfasdfa.tex

$\Gamma_1 \equiv y:\tau_1$

$\Gamma_2 \equiv \Gamma_1, x:\tau_2$

$\Gamma_3 \equiv x:\tau_3'$

$$
\cfrac
{
  \cfrac
  {
    \cfrac
    {
    \cfrac
    {
      \cfrac
      {
        \cfrac{}
        {\Gamma_2\vdash y :: (\tau_4 \rightarrow \tau_3, \tau_5)}Var
      }
      {\Gamma_2\vdash\textbf{fst } y :: \tau_4 \rightarrow \tau_3}fst
      \quad
      \cfrac
      {
      \cfrac{}
      {\Gamma_2\vdash x :: \tau_6\rightarrow \tau_4}Var
      \quad
      \cfrac
      {
      \cfrac{}
      {\Gamma_2\vdash y :: (\tau_7, \tau_6)}Var
      }
      {\Gamma_2\vdash \textbf{snd }y :: \tau_6}snd
      }
      {\Gamma_2\vdash x(\textbf{snd }y) :: \tau_4}App
    }
    {\Gamma_2\vdash(\textbf{fst } y)(x(\textbf{snd }y)) :: \tau_3}App
    }
    {\Gamma_1\vdash\lambda x (\textbf{fst } y)(x(\textbf{snd }y)):: \tau_0}Abs
  }
  {\vdash\lambda y . \lambda x (\textbf{fst } y)(x(\textbf{snd }y))::\tau_1\rightarrow \tau_0} Abs
  \quad
  \cfrac
  {
    \cfrac
    {
      \cfrac{}
      {\Gamma_3 \vdash x :: \tau_{4}'} Var
    }
    {\vdash\lambda x . x::\tau_2'}Abs
    \quad
    \cfrac
    {
      \cfrac
      {}
      {\vdash 42 :: Int}Int
    }
    {\vdash\textbf{iszero } 42 :: Bool} iszero
  }
  {\vdash((\lambda x . x), \textbf{iszero } 42)::\tau_1} Tuple
}
{\vdash(\lambda y . \lambda x (\textbf{fst } y)(x(\textbf{snd }y))((\lambda x . x), \textbf{iszero } 42)::\tau_0}App
$$

Constraints:

Left subtree:

- $\tau_0 \equiv \tau_2 \rightarrow \tau_3$
- $\tau_1\equiv(\tau_4\rightarrow\tau_3, \tau_5)$
- $\tau_2 \equiv\tau_6 \rightarrow \tau_4$
- $\tau_1 \equiv (\tau_7, \tau_6)$

Right subtree:

- $\tau_1 \equiv (\tau_2', Bool)$
- $\tau_2' \equiv \tau_{3}' \rightarrow \tau_{4}'$
- $\tau_3' \equiv \tau_{4}'$

Variables:

- $\tau_2 \equiv \tau_3'$

Apply constraints: $\tau_0 \equiv (Bool \rightarrow t) \rightarrow t$