Math test

This is a test of MathJax. $$\newcommand{\zero}{\mathsf{z}} \newcommand{\succ}[1]{\mathsf{s}({#1})} \newcommand{\iter}[4]{\mathsf{iter}({#1}, \zero \to {#2}, \succ{#3} \to {#4})} \begin{array}{lcl} A & ::= & 1 \bnfalt A \times B \bnfalt A \to B \bnfalt \N \\ e & ::= & () \bnfalt (e, e) \bnfalt \fst{e} \bnfalt \snd{e} \bnfalt \fun{x}{e} \bnfalt e \; e' \\ & | & \zero \bnfalt \succ{e} \bnfalt \iter{e}{e_z}{x}{e_s} \bnfalt x \bnfalt e : A \\ \Gamma & ::= & \cdot \bnfalt \Gamma, x:A \end{array}$$ $$\begin{array}{cc} \frac{ x:A \in \Gamma } { \judge{\Gamma}{x}{A} } & \frac{ } {\judge{\Gamma}{()}{1}} \\[1em] \frac{\judge{\Gamma}{e_1}{A_1} \qquad \judge{\Gamma}{e_2}{A_2}} {\judge{\Gamma}{(e_1, e_2)}{A_1 \times A_2}} & \frac{\judge{\Gamma}{e}{A_1 \times A_2}} {\judge{\Gamma}{\pi_i(e)}{A_i}} \\[1em] \frac{\judge{\Gamma, x:A}{e}{B}} {\judge{\Gamma}{\fun{x}{e}}{A \to B}} & \frac{\judge{\Gamma}{e}{A \to B} \qquad \judge{\Gamma}{e'}{A}} {\judge{\Gamma}{e\;e'}{B}} \\[1em] \frac{ } {\judge{\Gamma}{\zero}{\N}} & \frac{\judge{\Gamma}{e}{\N} } {\judge{\Gamma}{\succ{e}}{\N}} \\[1em] \frac{\begin{array}{l} \judge{\Gamma}{e}{\N} \\ \judge{\Gamma}{e_z}{A} \\ \judge{\Gamma, x:A}{e_s}{A} \end{array}} {\judge{\Gamma}{\iter{e}{e_z}{x}{e_s}}{A}} & \frac{\judge{\Gamma}{e}{A}} {\judge{\Gamma}{(e:A)}{A}} \end{array}$$ ​It seems to work!