Nice alignment across nodes in logic proof trees typeset with forest

In this answer, user cfr offers the following code which gives output as in the following image:

documentclass[border=11pt]{standalone}
usepackage[linguistics]{forest}
usepackage{amsmath,amssymb}
forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    for tree={math content},
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.quad ##1quad ##3} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=baselineskip}}{},
    close/.style={label=below:textsf{x}},
  },
}
begin{document}
begin{forest}
  ll proof,
  claim=vdash ((plor (qland r))to((plor q)land (plor r)))
  [ lnot ((plor (qland r))to((plor q)land (plor r)))    
    [ (plor (qland r)) , from=1
      [ lnot ((plor q)land (plor r)) , from=1
        [ p , from=2
          [ lnot (plor q) , from=3
            [ lnot p , from=6
              [ lnot q , from=6, close
          ]]]
          [ lnot (plor r) , from=3
            [1 lnot p , from=7
            [1 lnot r , from=7, close
        ]]]]
        [ (qland r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 lnot (plor q) , from=3
                [1 lnot p , from=14
                  [1 lnot q , from=14, close
              ]]]
              [1 lnot (plor r) , from=3
                [1 lnot p , from=15
                  [1 lnot r , from=15, close
  ]]]]]]]]]
end{forest}
end{document}

I am wondering if anyone knows how to modify the code to produce output as in the following image:

One approach I can think of is storing the widths of each of the widest line number, formula, and justification along each branch, and then wrapping the content of each node on the branch in a three-column tabular where the column widths are fixed to these maximum widths. Then the position of the anchors of the nodes would be set to the north of the formula column so that the lines between branches are drawn to the centres of the formulas.

A significantly less elegant but much easier approach would be to have multiline tabulars containing all of the formulas on a branch (i.e. one for the formulas numbered 1, 2, 3; another for 4; another for 5, 8, 11; and so on). But I would like to avoid an approach like this which would require significant changes to the tree itself rather than its style.

Unfortunately I don’t really have the technical expertise at present to even know where to start on actually implementing a more elegant solution, so I’d appreciate whatever help is on offer.

UPDATE

Here’s a partial answer which involves processing the content into a one-line tabular with three columns, one for the line number, one for the wff and another for the justification:

documentclass[border=11pt]{standalone}
usepackage[linguistics]{forest}
usepackage{amsmath,amssymb}
usepackage{array}
forestset{
  declare toks={from}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{begin{tabular}{>{raggedleft}p{1em}cp{1em}}##2. & ensuremath{##1} & ensuremath{##3}end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=baselineskip}}{},
    close/.style={label=below:textsf{x}},
  },
}
begin{document}
begin{forest}
  ll proof,
  claim=vdash ((plor (qland r))to((plor q)land (plor r)))
  [ lnot ((plor (qland r))to((plor q)land (plor r)))    
    [ (plor (qland r)) , from=1
      [ lnot ((plor q)land (plor r)) , from=1
        [ p , from=2
          [ lnot (plor q) , from=3
            [ lnot p , from=6
              [ lnot q , from=6, close
          ]]]
          [ lnot (plor r) , from=3
            [1 lnot p , from=7
            [1 lnot r , from=7, close
        ]]]]
        [ (qland r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 lnot (plor q) , from=3
                [1 lnot p , from=14
                  [1 lnot q , from=14, close
              ]]]
              [1 lnot (plor r) , from=3
                [1 lnot p , from=15
                  [1 lnot r , from=1500, close
  ]]]]]]]]]
end{forest}
end{document}

The above makes it so that the centres of the formulas are horizontally aligned. Thus we obtain

instead of

as in the original code. This already improves legibility and aesthetics.

The missing piece of the puzzle is to organise things such that the widths of the formula columns at 17. and 19. are set to the width of the formula column at 15. so that the line numbers and justifications are horizontally aligned as well. (And similarly throughout the tree.)

I think that this answer by cfr hints towards a way of calculating the width of each formula. But I don’t know how to store the widths and then select the widest appropriate one for each set of formulas.

Another update

I created a fwidth tok that gets passed to the width of the formula column. Now everything is nicely aligned, but the trade-off is that the user needs to set this key for every node on the tree. The best way to find out what it should be set to is to plug the widest formula of a branch into the code

newlength{myl}
settowidth{myl}{formula goes here}
themyl

and then set fwidth to that length for every formula in the branch. See the example code below:

documentclass[border=11pt]{standalone}
usepackage[linguistics]{forest}
usepackage{amsmath,amssymb}
usepackage{array}
forestset{
  declare toks={from}{},
  declare toks={fwidth}{},
  declare toks register={claim},
  claim=,
  ll proof/.style={
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2baselineskip},
      },
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        content/.process={ OR OSl+tt= ? w  Ow4 {content}{tempcounta}{from}{}{}{(##1)}{fwidth}{begin{tabular}{p{1em}>{centeringarraybackslash}p{##4}p{1em}}##2. & ensuremath{##1} & ensuremath{##3}end{tabular}} }
      }
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=baselineskip}}{},
    close/.style={label=below:textsf{x}},
  },
}
begin{document}
begin{forest}
  ll proof,
  claim=vdash ((plor (qland r))to((plor q)land (plor r)))
  [ lnot ((plor (qland r))to((plor q)land (plor r))), fwidth=158.8pt    
    [ (plor (qland r)) , from=1, fwidth=158.8pt
      [ lnot ((plor q)land (plor r)) , from=1, fwidth=158.8pt
        [ p , from=2, fwidth=5.1pt
          [ lnot (plor q) , from=3, fwidth=35.5pt
            [ lnot p , from=6, fwidth=35.5pt
              [ lnot q , from=6, close, fwidth=35.5pt
          ]]]
          [ lnot (plor r) , from=3, fwidth=35.5pt
            [1 lnot p , from=7, fwidth=35.5pt
            [1 lnot r , from=7, close, fwidth=35.5pt
        ]]]]
        [ (qland r) , from=2, fwidth=28.6pt
          [1 q , from=5, fwidth=28.6pt
            [1 r , from=5, fwidth=28.6pt
              [1 lnot (plor q) , from=3, fwidth=40.5pt
                [1 lnot p , from=14, fwidth=40.5pt
                  [1 lnot q , from=14, close, fwidth=40.5pt
              ]]]
              [1 lnot (plor r) , from=3, fwidth=40.5pt
                [1 lnot p , from=15, fwidth=40.5pt
                  [1 lnot r , from=1500, close, fwidth=40.5pt
  ]]]]]]]]]
end{forest}
end{document}

Things look really nice now, but it would be considerably more convenient if fwidth could be calculated and set automatically. (It would also be nice to hide the overfull warnings that come from setting the line number and justification columns to a small fixed width.) I await someone with a deeper knowledge of TikZ and forest to show the way.

% ref.: https://tex.stackexchange.com/q/570449/

documentclass[border=11pt]{standalone}
usepackage[linguistics]{forest}
usepackage{amsmath,amssymb,array}
newcolumntype{C}[1]{>{centering $}p{#1}<{$}}
forestset{
  declare toks={from}{},
  declare toks register={claim},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen register={rmeas},
  rmeas/.pgfmath=width("(99)"),
  claim=,
  ll proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2baselineskip},
      },
    },
    where n children=1{!1.no edge, before computing xy={!1.l'=baselineskip},}{},
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      tempcountb'=0,
      where align me={%
        tempcountb'+=1,
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first,typeset node}}%
        },
        for nodewalk={load=temptoksa}{my width/.register=tempdima, typeset node}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        tempcounta'+=1,
        align=p{foresteregister{lmeas}}C{foresteoption{my width}}p{foresteregister{rmeas}},
        content/.process={ OR OSl+tt= ? w  w3 {content}{tempcounta}{from}{}{}{(##1)}{##2.quad & ##1quad & ##3} },
        typeset node,
      }
    },
    close/.style={label=below:textsf{x}},
  },
}
begin{document}
begin{forest}
  ll proof,
  claim=vdash ((plor (qland r))to((plor q)land (plor r)))
  [ lnot ((plor (qland r))to((plor q)land (plor r)))    
    [ (plor (qland r)) , from=1
      [ lnot ((plor q)land (plor r)) , from=1
        [ p , from=2
          [ lnot (plor q) , from=3
            [ lnot p , from=6
              [ lnot q , from=6, close
          ]]]
          [ lnot (plor r) , from=3
            [1 lnot p , from=7
            [1 lnot r , from=7, close
        ]]]]
        [ (qland r) , from=2
          [1 q , from=5
            [1 r , from=5
              [1 lnot (plor q) , from=3
                [1 lnot p , from=14
                  [1 lnot q , from=14, close
              ]]]
              [1 lnot (plor r) , from=3
                [1 lnot p , from=15
                  [1 lnot r , from=15, close
  ]]]]]]]]]
end{forest}
end{document}