ThmとそのPrfの例①
「和集合の定義」 は次です。∪. … \(X \cup Y = \{ x \mid x \in X \mathbin{\rm o\!r} x \in Y \}\)
一般には \(\mathbb{W}.\) は無限列になるので次のThm単独でチェックを通すことはできません。
\(X \cup X = X\) ◀ \(\mathbb{W}.\)
しかし、次の3行のPrfはチェックを通せます。
goal := \(X \cup X = X\)
goal P◀ =. , cup.
goal H◀ \(\mathbb{W}.\)
1行目はPrf内変数 goal の宣言です。
2行目に対しては、次が返ってきます。 % Length of proof is 16.\(\dagger\)
3行目に対しては、=. と ∪. が\(\mathbb{W}.\)に入っていることを確かめられれば、2行目の結果と合わせて OK が返ってきます。
ThmとそのPrfの例②
「\({\tt w}\)の定義による展開」を行う / \({\tt w}\). が証明において有用です。\(X \cup X = X\) / =. = \(\forall x \, ( x \in X \cup X \Leftrightarrow x \in X )\)
\(X \cup X = X\) / =. / ∪. = \(\forall x \, ( x \in X \mathbin{\rm o\!r} x \in X \Leftrightarrow x \in X )\)
この計算は、具体的にどのwordの定義を使うかを記述せず // \(\mathbb{W}.\) としても実行されます。
上のThmのPrfは、次の3行にした方が良いです。
goal := \(X \cup X = X\)
goal // \(\mathbb{W}.\) P◀ O
goal H◀ \(\mathbb{W}.\)
2行目に対しては、次が返ってきます。 % Length of proof is 6.
一般にProver9にはsosが少ないThmを投げた方が良いです。
Hyperionは goal ◀ goal // \(\mathbb{W}.\) , \(\mathbb{W}.\) というThmの生成ができ、最初のPrfより速く3行目を処理するでしょう。