Схема доказательства дерева

Question

В настоящее время я работаю над созданием деревьев доказательств для регулярных выражений в схеме. Предлагаемый способ их записи в курсе, который я прохожу, следующий, который я вручную ввел в TeX.

Однако это утомительный процесс, особенно для длинных выражений. Поэтому я ищу хитрый способ сделать тип дерева доказательств, показанный выше, или, может быть, альтернативу, которая может сделать то же самое.

Редактировать:

Вот мой код, я не против печатать в дереве, но этот способ очень, очень медленный. Так что если есть пакет, который может сделать часть работы по позиционированию за меня, я был бы счастливым кемпером.

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

Редактировать 2: Я пока не нашел решения с bussproofsпакетом, но оно все равно не оптимальное, выглядит немного странно, когда деревья проверки становятся большими.

Мой код для создания этого:

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