Compute proper left and right adjustments for bussproof tables. (mathjax/MathJax#3251)

[dpvc]

This PR fixes problems with the computation of the left- and right-hand width adjustments that are used to get the correct bounding box for the final proof table. Currently, the left-hand adjustment can be too big, while the right-hand can be too small or too big. This is true, for example, with this proof:

$$\bbox[orange]{
\begin{prooftree}\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{¬p, p ⊢ ¬ ¬q}
\RightLabel{DNE}\UnaryInfC{¬p, p ⊢ q}
\RightLabel{I→}\UnaryInfC{¬p ⊢ p → q}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{(p → q) → p ⊢ (p → q) → p}
\RightLabel{E→}\BinaryInfC{(p → q) → p, ¬p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{p ⊢ p}
\AxiomC{}
\RightLabel{Ax}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{¬p ⊢ ¬p}
\RightLabel{E→}\BinaryInfC{¬p, (p → q) → p ⊢ ⊥}
\RightLabel{I→}\UnaryInfC{(p → q) → p ⊢ ¬ ¬p}
\RightLabel{DNE}\UnaryInfC{(p → q) → p ⊢ p}
\RightLabel{I→}\UnaryInfC{ ⊢ ((p → q) → p) → p}
\end{prooftree}
}$$

On the right, the maxAdjust computations are not correct, leading to the wrong size. Some things that can show this are labels that exceed past the width of the material above it, and conclusions that are shorter than the lines below it.

On the left, too much space will be added if a conclusion above a rule is shorter than the rule itself.

This PR introduces a new means of computing the maxAdjust value (that doesn't rely on saving it in a property), and takes care of the short-conclusion-over-longer-rule discrepancy as well. I don't have any knowledge of the buss proofs package myself, so relied on this example and a few others to test this, so I may have missed something, but I think it is correct.

I also fixed the label placement and bounding boxes, which were not quite right.

I didn't adjust the comments above balanceRules() as I didn't really understand them, but they no longer completely apply.

Resolves issues mathjax/MathJax#3251 and mathjax/MathJax#3240.

[zorkow]

lgtm.