0

I came to

enter image description here

the universally quantified assumption overflows the derivation line.

My source is

\documentclass{beamer}
\usepackage{bussproofs}

\newcommand{\mydots}{
\def\extraVskip{-2pt}
\noLine
\UnaryInfC{\vdots}
\def\extraVskip{2pt}
\noLine
}

\begin{document}

\AxiomC{$\exists t. A(t)$}
\AxiomC{[$\forall t. A(t)$]}
\mydots
\UnaryInfC{$C$}
\RightLabel{$\exists$E}
\BinaryInfC{$C$}
\DisplayProof

\end{document}

How can I fix this within using bussproofs.sty ?

1 Answer 1

1

I believe it's a precise choice of bussproofs as the examples on page 4 show: here's one

enter image description here

You can tell it to use the same width as a previous item with a box:

\documentclass{beamer}
\usepackage{calc}
\usepackage{bussproofs}

\newcommand{\mydots}{%
  \noLine
  \UnaryInfC{\vphantom{\ensuremath{X}}\smash{\vdots}}%
  \noLine
}

\begin{document}

\begin{frame}

\AxiomC{$\exists t. A(t)$}
\AxiomC{[$\forall t. A(t)$]}
\mydots
\UnaryInfC{\makebox[\widthof{[$\forall t. A(t)$]}]{$C$}}
\RightLabel{$\exists$E}
\BinaryInfC{$C$}
\DisplayProof

\end{frame}

\end{document}

enter image description here

1
  • Ah yes, bussproofs' aim is to draw proof trees and that is why it typeset that way.
    – Gergely
    Commented Apr 11, 2023 at 15:00

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .