证明中的证明

Question

我想使用 将证明放入证明中bussproofs。以下代码正好产生了我想要的结果。

\documentclass{amsart}
\usepackage{bussproofs}
\newcommand{\VDots}{\vphantom{\int^0}\smash[t]{\vdots}}

\begin{document}

\begin{center}
\hspace{17mm}
$\left(
        \AxiomC{$(A)$}
        \noLine
        \UnaryInfC{$\VDots$}
        \noLine
        \UnaryInfC{$B$}
    \DisplayProof
\right)$
\end{center}
\vspace{-2mm}
\begin{center}
        \AxiomC{$A\to B$}
        \AxiomC{\mbox{}}
        \noLine
        \UnaryInfC{$\VDots$}
        \noLine
        \UnaryInfC{$C$}
        \BinaryInfC{$C$}
    \DisplayProof
\end{center}

\end{document}

但显然这不是理想的情况。我想能够获取这部分代码：

$\left(
        \AxiomC{$(A)$}
        \noLine
        \UnaryInfC{$\VDots$}
        \noLine
        \UnaryInfC{$B$}
    \DisplayProof
\right)$

并将其推入我目前在第二个证明中的位置\mbox{}。但这会给我带来错误。

Answer 1

看起来 busproofs 不支持嵌套校样。不过，你可以将内部校样保存到盒子中，然后在外部校样内使用该盒子。

\documentclass{amsart}
\usepackage{bussproofs}
\newcommand{\VDots}{\vphantom{\int^0}\smash[t]{\vdots}}
\begin{document}

\newsavebox\InnerProof
\sbox\InnerProof{$\left(
        \AxiomC{$(A)$}
        \noLine
        \UnaryInfC{$\VDots$}
        \noLine
        \UnaryInfC{$B$}
    \DisplayProof
\right)$%
}

\begin{center}
        \AxiomC{$A\to B$}
        \AxiomC{\usebox\InnerProof}
        \noLine
        \UnaryInfC{$\VDots$}
        \noLine
        \UnaryInfC{$C$}
        \BinaryInfC{$C$}
    \DisplayProof
\end{center}

\end{document}