
答案1
已經可以使用prooftrees 來完成其中的一些操作,但由於存在錯誤,尚無法在已發布的版本中從6 開始行編號。
如果你細心的話,你可以使用split here
包含在我的另一個答案並基於Sašo Živanović 的程式碼分割prooftrees
prooftree
一次,插入一些解釋或分頁符號或中間的任何內容。
注意:這會損壞。我不知道在哪裡,但毫無疑問它會破裂。這個證明幾乎沒有經過測試,更不用說其他證明了。
prooftrees
事實上,我在玩這個遊戲時發現了兩個現有的錯誤,甚至沒有將證明分成幾個部分。 (這些問題將在下一個版本的 Forest 推送到 CTAN 後不久得到修復。)
買者自負...
例如:
\documentclass{article}
\usepackage{prooftrees,amssymb}
% Sašo Živanović: https://tex.stackexchange.com/a/296771/
\def\hiddenparcommand{\par}
\forestset{%
declare count register={split here level},
declare toks register={split here interject},
split here level'=-1,
split here interject={},
to widest/.style={
tikz+={\path (\forestregister{tempdima}, \forestoption{y}) -- (\forestregister{tempdimb}, \forestoption{y});},
},
split here/.style={%
split here level'/.option=level,
split here interject={#1},
split tree
},
split tree/.code={%
\forestset{%
draw tree stage/.style={
for root'={
tempdima/.min={x()+min_x()}{tree},
tempdimb/.max={x()+max_x()}{tree},
for tree={%
to widest,
},
},
for nodewalk/.wrap pgfmath arg={{draw tree processing order/.style={level<=####1}}{}}{split_here_level},
for root'={draw tree},
TeX/.wrap pgfmath arg={\bigskip\hiddenparcommand ####1\hiddenparcommand}{split_here_interject},
for nodewalk/.wrap pgfmath arg={{draw tree processing order/.style={level>=####1}}{}}{(split_here_level)+1},
for root'={draw tree},
},
}
}
}
\begin{document}
\begin{prooftree}
{
line no shift=5,
just refs right,
}
[Fa, name=fa
[{\lnot((Fa \land \forall y (Fy \supset y=a))} \land Ga), checked
[{\lnot(Fa \land \forall y (Fy \supset y=a))}, checked, split here={So far, so automatic. The right hand branch closes, for we have}
[\lnot Fa, just={from:!u}, close={:!uuu,!c}
]
[{\lnot \forall y (Fy \supset y=a)}, checked
[{\exists y \lnot (Fy \supset y=a)}, just={from:!u}, checked=b
[{\lnot (Fb \supset b=a)}, just={from:!u}
]
]
]
]
[\lnot Ga
[Fa \supset Ga, just=from 3
[\lnot Fa, close={:fa,!c}]
[Ga, close={:!uu,!c}]
]
]
]
]
\end{prooftree}
\end{document}