Does anyone know how to do these dots (gaps) in bussproofs?

Question

I'm trying to do something similar to the proof in picture where there is a gap in the steps of the proof. I tried bussproofs-extra package, but it doesn't let me make the dots from two inferences to converge towards one inference (i.e., similar to BinaryInf but dots leading to it from two UnaryInfs).
Any help would be highly appreciated!
For example, a sample without the dots would look like this:
documentclass{article}
usepackage{bussproofs}
usepackage{tikz}
usepackage{bussproofs-extra}
usepackage{amssymb,amsmath}

begin{document} 
begin{prooftree}
deffCenter{mbox{ $vdash$ }}
AxiomC{} 
UnaryInf$Gamma, varphi fCenter Delta$
AxiomC{}
UnaryInf$GammafCenter varphi, Delta$RightLabel{scriptsize Cut}
BinaryInf$ Gamma fCenter Delta$ 
end{prooftree}

end{document}

Rashed Ahmad · Accepted Answer

I have received an answer via twitter–thanks to Shawn Standefer! Here is how it's done:
    documentclass{article}
    usepackage{bussproofs}
    usepackage{tikz}
    usepackage{bussproofs-extra}
    usepackage{amssymb,amsmath}

begin{document}

begin{prooftree}
        deffCenter{mbox{ $vdash$ }}
        AxiomC{}LeftLabel{scriptsize $square$}RightLabel{scriptsize $n$}
        UnaryInfC{$Gamma fCenter varphi$}
        AxiomC{}LeftLabel{scriptsize $square$}RightLabel{scriptsize $n$}
        UnaryInfC{$Delta, varphi fCenter psi$}
        noLine
        BinaryInfC{$ddots   reflectbox{$ddots$}$}
        noLine
        UnaryInfC{$vdots$}
        noLine
        UnaryInfC{$Gamma, Delta fCenter psi$}RightLabel{scriptsize Cut-Un-I, $n$}
        UnaryInfC{$Gamma, Delta fCenter Un(ulcorner varphi urcorner)$}
end{prooftree}

end{document}

It requires reflectbox and use that as a binary inference. The noLine just removes the horizontal line of an inference.

Does anyone know how to do these dots (gaps) in bussproofs?

One Answer

Add your own answers!

Ask a Question