Genzen 式证明树

Question

我想生成以下证明树。这是我目前的尝试：

\def\ae\qquad\mathbf{\forall Elim}
\def\ai\qquad\mathbf{\forall Intro}
\def\be\qquad\mathbf{\leftrightarrow Elim}
\def\bi\qquad\mathbf{\leftrightarrow Intro}
\def\oe\qquad\mathbf{\lor Elim}
\def\oi\qquad\mathbf{\lor Intro}
\def\ne\qquad\mathbf{\neg Elim}
\def\ni\qquad\mathbf{\neg Intro}

\begin{equation}
\dfrac{
  \dfrac{
    \dfrac{
      \dfrac{
        \dfrac{\forall x(Pa \lor Rx)}{Pa \lor Rb}\ae
          \dfrac{\dfrac{Pa}{Pa \lor \forall xRx \quad \lnot(Pa \lor \forall xRx)}}{Rb \qquad Rb}\ne
          }{
            Rb
          }\oe
          }{
            \forall xRx
          }\ai
        }{
          Pa \lor \forall xRx  \quad \lnot(Pa \lor \forall xRx)
        }\oi
      }{
    Pa \lor \forall xRx
}\ne
\end{equation}

是否有可能不延长树的这两段中的分数线？

因此，在第一种情况下，该行看起来如下：

也许，有更好的方法来解决这个问题。我将使用 MathJax。