paper: make ebproof happy on linux

final/main.tex

@@ -57,67 +57,68 @@
 % gobble page number for title
 \thispagestyle{empty}
 \newpage
+
 \begin{table}
   \renewcommand{\arraystretch}{3.5}
   \[ \begin{array}{r c}
 
     \textbf{TAUT} & {\begin{prooftree}
-        \Infer 0 {A, (x :: \sigma \bs \bar{x}) \proves x :: \sigma \bs \bar{x}}
+        \infer 0 {A, (x :: \sigma \bs \bar{x}) \proves x :: \sigma \bs \bar{x}}
     \end{prooftree}} \\
 
     \textbf{TAUT-INST} & {\begin{prooftree}
-        \Infer 0 {A, (x ::_i \sigma \bs \bar{x}) \proves x :: \sigma \bs \bar{x}}
+        \infer 0 {A, (x ::_i \sigma \bs \bar{x}) \proves x :: \sigma \bs \bar{x}}
     \end{prooftree}} \\
 
     \textbf{GEN} & {\begin{prooftree}
-        \Hypo{\alpha \text{ not free in } A}
-        \Hypo{A \proves e :: \sigma \bs \bar{e}}
-        \Infer 2 {A \proves e :: \forall \alpha . \sigma \bs \bar{e}}
+        \hypo{\alpha \text{ not free in } A}
+        \hypo{A \proves e :: \sigma \bs \bar{e}}
+        \infer 2 {A \proves e :: \forall \alpha . \sigma \bs \bar{e}}
     \end{prooftree}} \\
 
     \textbf{SPEC} & {\begin{prooftree}
-        \Hypo{A \proves e :: \forall \alpha . \sigma \bs \bar{e}}
-        \Infer 1 {A \proves e :: \left[ \alpha \backslash \tau \right] \sigma \bs \bar{e}}
+        \hypo{A \proves e :: \forall \alpha . \sigma \bs \bar{e}}
+        \infer 1 {A \proves e :: \left[ \alpha \backslash \tau \right] \sigma \bs \bar{e}}
     \end{prooftree}} \\
 
     \textbf{ABS} & {\begin{prooftree}
-        \Hypo{A, (x :: \tau' \bs x) \proves e :: \tau \bs \bar{e}}
-        \Infer 1 {A \proves (\lambda x . e) :: (\tau' \arrow \tau) \bs (\lambda x . \bar{e})}
+        \hypo{A, (x :: \tau' \bs x) \proves e :: \tau \bs \bar{e}}
+        \infer 1 {A \proves (\lambda x . e) :: (\tau' \arrow \tau) \bs (\lambda x . \bar{e})}
     \end{prooftree}} \\
 
     \textbf{APP} & {\begin{prooftree}
-        \Hypo{A \proves e :: (\tau' \arrow \tau) \bs \bar{e}}
-        \Hypo{A \proves e' :: \tau' \bs \bar{e}'}
-        \Infer 2 {A \proves (e\; e') :: \tau \bs (\bar{e}\; \bar{e}')}
+        \hypo{A \proves e :: (\tau' \arrow \tau) \bs \bar{e}}
+        \hypo{A \proves e' :: \tau' \bs \bar{e}'}
+        \infer 2 {A \proves (e\; e') :: \tau \bs (\bar{e}\; \bar{e}')}
     \end{prooftree}} \\
 
     \textbf{LETREC} & {\begin{prooftree}
-        \Hypo{A, (x :: \alpha \bs x) \proves e :: \sigma \bs \bar{e}}
-        \Hypo{A, (x :: \sigma \bs x) \proves e' :: \tau \bs \bar{e}'}
-        \Infer 2 {A \proves (\textbf{let } x = e \textbf{ in } e') :: \tau \bs
+        \hypo{A, (x :: \alpha \bs x) \proves e :: \sigma \bs \bar{e}}
+        \hypo{A, (x :: \sigma \bs x) \proves e' :: \tau \bs \bar{e}'}
+        \infer 2 {A \proves (\textbf{let } x = e \textbf{ in } e') :: \tau \bs
           (\textbf{let } x = \bar{e} \textbf{ in } \bar{e}')}
     \end{prooftree}} \\
 
     \textbf{OVER} & {\begin{prooftree}
-        \Hypo {A, (x ::_o \sigma) \proves e' :: \tau \bs \bar{e}'}
-        \Infer 1 {A \proves (\textbf{over } x :: \sigma \textbf{ in } e') :: \tau \bs \bar{e}'}
+        \hypo {A, (x ::_o \sigma) \proves e' :: \tau \bs \bar{e}'}
+        \infer 1 {A \proves (\textbf{over } x :: \sigma \textbf{ in } e') :: \tau \bs \bar{e}'}
     \end{prooftree}} \\
 
     \textbf{INST} & {\begin{prooftree}
-        \Hypo{(x ::_o \sigma) \in A}
-        \Hypo{A, (x ::_i \sigma \bs x_\sigma) \proves e :: \sigma \bs \bar{e}}
-        \Hypo{A, (x ::_i \sigma \bs x_\sigma) \proves e' :: \tau \bs \bar{e}'}
-        \Infer 3 {A \proves (\textbf{inst } x :: \sigma = e \textbf{ in } e') :: \tau \bs
+        \hypo{(x ::_o \sigma) \in A}
+        \hypo{A, (x ::_i \sigma \bs x_\sigma) \proves e :: \sigma \bs \bar{e}}
+        \hypo{A, (x ::_i \sigma \bs x_\sigma) \proves e' :: \tau \bs \bar{e}'}
+        \infer 3 {A \proves (\textbf{inst } x :: \sigma = e \textbf{ in } e') :: \tau \bs
           (\textbf{let } x_\sigma = \bar{e} \textbf{ in } \bar{e}')}
     \end{prooftree}} \\
 
     % TODO: INST-PRED
 
     \textbf{REL} & {\begin{prooftree}
-        \Hypo{(x ::_o \sigma) \in A}
-        \Hypo{A \proves e :: (x :: \tau) . \rho \bs \bar{e}}
-        \Hypo{A \proves x :: \tau \bs \bar{e}'}
-        \Infer 3 {A \proves e :: \rho \bs (\bar{e}\; \bar{e}')}
+        \hypo{(x ::_o \sigma) \in A}
+        \hypo{A \proves e :: (x :: \tau) . \rho \bs \bar{e}}
+        \hypo{A \proves x :: \tau \bs \bar{e}'}
+        \infer 3 {A \proves e :: \rho \bs (\bar{e}\; \bar{e}')}
     \end{prooftree}} \\
 
   \end{array} \]