User:Kensteve/Sandbox

${\frac {\Gamma \vdash \alpha \rightarrow \beta \qquad \Gamma \vdash \alpha }{\Gamma \vdash \beta }}{\textit {Modus~Ponens}}$

$\displaystyle {\frac {}{\displaystyle {\frac {A}{\displaystyle {\frac {B}{C}}}}}}$

${\frac {}{\frac {A}{\frac {B}{C}}}}$

$\displaystyle {\frac {}{\displaystyle {\frac {\Gamma x:~\alpha \rightarrow \beta \rightarrow \gamma ~\vdash x:~\alpha \rightarrow \beta \rightarrow \gamma \qquad \Gamma z:~\alpha ~\vdash z:~\alpha }{\displaystyle {\frac {\Gamma x:~\alpha \rightarrow \beta \rightarrow \gamma z:~\alpha ~\vdash xz:\beta \rightarrow \gamma }{C}}}}}}$

$\displaystyle {\frac {}{\displaystyle }}{\frac {\displaystyle {\frac {\Gamma x:~\alpha \rightarrow \beta \rightarrow \gamma ~\vdash x:~\alpha \rightarrow \beta \rightarrow \gamma \qquad \Gamma z:~\alpha ~\vdash z:~\alpha }{\Gamma x:~\alpha \rightarrow \beta \rightarrow \gamma ,z:~\alpha ~\vdash xz:\beta \rightarrow \gamma }}(\rightarrow E)\qquad \displaystyle {\frac {\Gamma y:~\beta \rightarrow \gamma ~\vdash y:~\beta \rightarrow \gamma \qquad \Gamma z:~\alpha ~\vdash z:~\alpha }{\Gamma y:~\alpha \rightarrow \beta ,z:~\alpha ~\vdash yz:\beta }}(\rightarrow E)}{\displaystyle {\frac {{\displaystyle {\frac {\Gamma x:~\alpha \rightarrow \beta \rightarrow \gamma ,~y:~\alpha \rightarrow \beta ,~z:~\alpha \vdash xz(yz):~\alpha }{\displaystyle {\frac {\Gamma x:~\alpha \rightarrow \beta \rightarrow \gamma ,~y:~\alpha \rightarrow \beta \vdash \lambda z.xz(yz):~\alpha }{\Gamma ,x:~\alpha \rightarrow \beta \rightarrow \gamma \vdash \lambda yz.xz(yz):~(\alpha \rightarrow \beta )\rightarrow \alpha }}(\rightarrow I)}}}(\rightarrow I)}{\vdash \lambda xyz.xz(yz):~(\alpha \rightarrow \beta \rightarrow \gamma )\rightarrow (\alpha \rightarrow \beta )\rightarrow \alpha }}(\rightarrow I)}}$

$\displaystyle {\frac {}{\displaystyle {\frac {x:\alpha \vdash x:\alpha }{\vdash \lambda x.x:\alpha \to \alpha }}(2)}}(1)$

Failed to parse (syntax error): {\displaystyle \displaystyle\frac{}{\displaystyle\frac{\displaystyle\frac{x:\alpha \vdash x:\alpha}{\vdash \lambda x.x:\alpha \to \alpha}}}{A}}