I have the following proof tree, which latex says is badly specified.
Here is the TeX.
\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{prooftree}
\AxiomC{$Sz + t = 0 \dagger$} \AxiomC{$t = 0 \dagger$}
\BinaryInfC{$Sz + 0 = 0$} \AxiomC{$Sz + 0 = Sz$}
\BinaryInfC{$Sz = 0$} \AxiomC{$\neg (Sz = 0)$}
\BinaryInfC{$\bot$}
\UnaryInfC{$\neg(Sz + t) = 0$}
\AxiomC{$\neg(t = 0)$}
\UnaryInfC{$\exists w (t = Sw)$}
\AxiomC{$t = Sy \dagger$} \AxiomC{$Sz + t = 0 \dagger$}
\BinaryInfC{$S(z + y) = 0$} \AxiomC{$\neg(S(z + y) = 0$}
\BinaryInfC{$\bot$}
\UnaryInfC{$\neg(Sz + t = 0)$}
\BinaryInfC{$\neg(Sz + t) = 0$}
\end{prooftree}
\end{document}
There are two proof trees, with conclusions $\neg(Sz + t = 0)$
(both of them), and I want to join those together to conclude $\neg(Sz + t = 0)$
. I tested it a bit, and it seems the mistake is in the second tree (If I remove the second tree and conclusion it works), but I can't find it.
\documentclass{article}\usepackage{bussproofs}\begin{document} ... \end{document}
. This way people can just copy the code to play with it. It also loads the correct package for theprooftree
environment.\DisplayProof
after the first tree then the code works. Is that what you are looking for?