4 prover+ の断片と p[whole]

prover+ は Thm の goal を、次の規則で断片に割り、断片ごとに Prover9 に投げます。すべての断片が証明できたとき、その Thm を証明したことになります。
　\({\tt P}\) and \({\tt Q}\) → \({\tt P}\) と \({\tt Q}\)
　\({\tt P}\) ⇔ \({\tt Q}\) → \({\tt P}\) ⇒ \({\tt Q}\) と \({\tt Q}\) ⇒ \({\tt P}\)
　(\({\tt P}\) or \({\tt Q}\)) ⇒ \({\tt R}\) → \({\tt P}\) ⇒ \({\tt R}\) と \({\tt Q}\) ⇒ \({\tt R}\)
これらは ⇒ と ∀ の右側にも、割れなくなるまで繰り返し適用されます。例えば次の Thm の査読では、Prover9 に2つの問題（⊤ と ⊤）が投げられます。
\(\top , \top\) \(\blacktriangleleft\) O
割らずに1つの問題として投げるには、段の末尾の投げ先を p[whole]; と書きます。

\n の入った Thm も扱えます（prf は有限個の n に対してのみ）。
⇔\({\tt n}\) … \(( P_{1} \Leftrightarrow P_{2} \Leftrightarrow \cdots \Leftrightarrow P_{\tt n} ) \Longleftrightarrow ( P_{1} \Rightarrow P_{2} \Rightarrow \cdots \Rightarrow P_{\tt n} \Rightarrow P_{1} )\) \(\blacktriangleleft\) O
ソース：prop/thm ⇔\n ◀ O at \n=2..5（n=2..5 の4つの Thm）、prf ⇔\n -| O p[whole];。
割ると Prover9 への問題は n=2..5 で34本、割らなければ4本です（n=2..8 だと91本と7本。Thm 査読の時間は約4.1秒と約3.3秒）。断片が自明なので、本数だけ起動コストが増えます。
ただし一般には割る方が速く、どの断片が落ちたかまで分かるので、p[whole]; は ⇔\n のように断片が自明な行だけに使います。