Quantification in the infer command of the proof package
I propose a \qinfer
command:
\documentclass{article}
\usepackage{proof,amsmath}
\newcommand{\func}[1]{\mathrm{#1}}
\newcommand{\qinfer}[3]{%
\sbox0{\infer{#2}{#3}}%
\raisebox{\dimexpr(\ht0-1ex)/2}{$#1\;$}%
\box0
}
\begin{document}
\[
\infer{s = s'}{%
R \subseteq A^{\omega} \times A^{\omega}
& R \; s \; s'
&
\qinfer{\forall s_1,s_2}
{\func{head}(s_1) = \func{head}(s_2) \land R(\func{tail}(s_1), \func{tail}(s_2))}
{R \; s_1 \; s_2}
}
\]
\end{document}
I also fixed \text
into \mathrm
, which is the correct command to use here (if not \operatorname
).
The name of the inference rule can be added as an optional argument to \infer
:
\infer[label]{conclusion}{premises}
However, the label is added to the right.
\documentclass{article}
\usepackage{proof}
\usepackage{amsmath}
\begin{document}
$\infer{s = s'}{%
R \subseteq A^{\omega} \times A^{\omega}
& R \; s \; s'
& \infer[\forall s_1, s_2]{%
\text{head}(s_1) = \text{head}(s_2)
\land R(\text{tail}(s_1), \text{tail}(s_2))%
}{%
R \; s_1 \; s_2
}
}$
\end{document}
You can raise this into position using \raisebox{<len>}{<stuff>}
:
\documentclass{article}
\usepackage{proof,amsmath}
\begin{document}
\[
\infer{s = s'}{%
R \subseteq A^{\omega} \times A^{\omega}
& R \; s \; s'
& \raisebox{.6\baselineskip}{$\forall s_1, s_2$~}
\infer{\text{head}(s_1) = \text{head}(s_2) \land R(\text{tail}(s_1), \text{tail}(s_2))}{%
R \; s_1 \; s_2
}
}
\]
\end{document}