我目前正在為方案中的正規表示式製作證明樹。在我正在學習的課程中，建議的編寫這些內容的方法如下，我已手動將其輸入到 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}