Atualmente estou trabalhando na criação de árvores de prova para expressões regulares no esquema. A maneira sugerida de escrevê-los no curso que estou fazendo é a seguinte, que digitei manualmente no TeX.
No entanto, este é um processo tedioso, especialmente para expressões longas. Então, o que estou procurando é uma maneira sorrateira de fazer o tipo de árvore de prova mostrada acima, ou talvez uma alternativa que possa fazer o mesmo.
Editar:
Aqui está o meu código, não me importo de digitar na árvore, mas dessa forma é muito, muito lento. Então, se houver um pacote que possa fazer parte do trabalho de posicionamento para mim, eu ficaria feliz.
\phantom{ATOM}\ \ \ \ \ 1 is a Scheme integer\qquad\qquad\qquad (\%regexp (atom 2))\\
ATOM ---------------------\qquad\qquad SEQ ------------------------------------------------------------\\
\phantom{ATOM} (\%regexp (atom 1)) \qquad\qquad\qquad\ \ (\%regexp (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty)))\\
\phantom{A}SEQ ---------------------------------------------------------------------------------------------\\
\phantom{ATOM} (\%regexp (seq (atom 1) (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty))))))
Editar 2:
Eu não encontrei uma solução com o bussproofspacote, mas ainda não é o ideal, fica um pouco estranho quando as árvores de prova ficam grandes.
Meu código para criar isso é:
\begin{prooftree}
\def\ScoreOverhang{1pt}
\def\extraVskip{6pt}
\def\defaultHypSeparation{\hskip .2in}
\def\ruleScoreFiller{\hbox to1.1mm{\hss\vrule width0.9mm height0.4pt depth0.0pt\hss}}
\AxiomC{1 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 1))}
\AxiomC{2 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 2))}
\AxiomC{3 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 3))}
\AxiomC{4 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 4))}
\AxiomC{}
\LeftLabel{EMPTY}
\UnaryInfC{(\%regexp (empty))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 4) (empty)))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 3) (seq (atom 4) (empty))))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty)))))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 1) (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty))))))}
\end{prooftree}