前提中的公式使用总线证明溢出推导线

Question

我来到

普遍量化的假设溢出了推导线。

我的消息来源是

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

我如何在使用过程中修复此问题bussproofs.sty？

Answer 1

我相信这是一个精确的选择，bussproofs如第 4 页的示例所示：这是一个

您可以告诉它使用与前一个带有框的项目相同的宽度：

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