6

I'm trying to write this inference rule using the infer command of the proof package:

enter image description here

For that I'm using the command:

$\infer{s = s'}{%
        R \subseteq A^{\omega} \times A^{\omega}
        & R \; s \; s'
        & \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
        }
    }$

However, the forall quantification appears in the lower level as:

enter image description here

How can I put it in the middle like above?

  • You may use \operatorname{} instead of \text{} – user94293 Nov 14 at 21:28
5

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).

enter image description here

4

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.

enter image description here

\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}
3

You can raise this into position using \raisebox{<len>}{<stuff>}:

enter image description here

\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}

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.