4 集合・クラスの例②

4.1 和・積

word(c,c) … \(\bigcup\)  \(\bigcap\)
word(s,s)R … \(\bigcup\)  \(\bigcap\)
クラスの和・積は綺麗に定義でき、集合の和・積の定義はそこから誘導されます。
⋃_. … \(\bigcup \mathcal{X} = \{ x \mid \exists X \in \mathcal{X} . x \in X \}\)
⋂_. … \(\bigcap \mathcal{X} = \{ x \mid \forall X \in \mathcal{X} . x \in X \}\)
⋃. … \([\bigcup] \stackrel{\star}{=} [\bigcup]\)
⋂. … \(\mathcal{X} \neq \emptyset \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)
例えば　⋃.|cvt … \(\forall x ( x \in \bigcup \mathcal{X} \Longleftrightarrow \exists X \in \mathcal{X} . x \in X )\)
⋂_∅ … \(\bigcap \emptyset = \mathbb{V}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm ⋂_∅ <- `⋂_ ∅ =_ 𝕍` ◀ W.　prf ⋂_∅ / W. -| O p; ⋂_∅ -| W. h;
W. に入るのは gram に c を含まない語の定義だけ（4.book）なので、⋂_. ・𝕍. ・=_. は W. に入りません。これらの定義は、-| の中の |cvt+（5.book）が開きます。W. から来るのは ∅. などです。

Bookではhidden propを使うこともできます。ソースでは次のように !prop/thm と書くと、表示されずに Thm として示され、後の prf で使えます。
　ソース：!prop/thm ⋂.' ◀ W.　prf ⋂.' /// W. -| O p; ⋂.' -| W. h;
ここでは中身を特別に表示しておきます。
⋂.' … \(\exists X \, X \in \mathcal{X} \Longrightarrow \bigcap \mathcal{X} = \bigcap \mathcal{X}\)

4.2 合併・共通部分

word(cc,c) … \(\cup\)  \(\cap\)
∪_. … \(A \cup B = \{ x \mid x \in A \mathbin{\rm o\!r} x \in B \}\)
∩_. … \(A \cap B = \{ x \mid x \in A , x \in B \}\)
word(ss,s) … \(\cup\)  \(\cap\)
∪. … \([\cup] \stackrel{\star\!\star}{=} [\cup]\)
∩. … \([\cap] \stackrel{\star\!\star}{=} [\cap]\)

4.3 特殊なslash計算

∩=⋂ … \(X \cap Y = \bigcap \{ X , Y \}\) \(\blacktriangleleft\) \(\mathbb{W}.\)
　ソース：prop/thm ∩=⋂ <- `X ∩ Y = ⋂ \{ set X ; Y \}` ◀ W.　prf ∩=⋂ /// W.' -| O p; ∩=⋂ -| W. h;
\({\tt P}\) / W. は「\({\tt P}\) を 〇. で展開したもの」でした。 \({\tt P}\) / W.' は「\({\tt P}\) を 〇.' があれば 〇.'、無ければ 〇. で展開したもの」です。ただし 〇.' の左辺が 〇. の左辺の形を含まないときは、〇. でも展開します（両方が別の場所に当たる）。〇.' の左辺が \(=\) の式（ \(X = \emptyset\) など）のときは、W.' では \(=\) の定義 =. が先に当たるので、〇.' を使うには W.'!=. と書きます。
〇. が \(P \Longrightarrow Q \Leftrightarrow R\) のときは \(Q \Longleftrightarrow \begin{cases} P \Rightarrow R \\ \neg P \Rightarrow Q' \end{cases}\) に変換してから展開します。
ただし \(Q'\) は \(Q\) の 〇 を 〇_alias にしたものです。〇_alias は無駄な展開を防ぐためにあり / の処理終了時に 〇 に戻されます。
上のprfでは
　/ W.' … [∀ w1 [⇔ [∈ w1 [∩ X Y]] [∈ w1 [⋂ [set2 X Y]]]]]
　// W.' … [∀ w1 [⇔ [and [∈ w1 X] [∈ w1 Y]] [and [⇒ [∃ w2 [∈ w2 [set2 X Y]]] [∀ w3 [⇒ [∈ w3 [set2 X Y]] [∈ w1 w3]]]] [⇒ [¬ [∃ w2 [∈ w2 [set2 X Y]]]] [∈ w1 [⋂ [set2 X Y]]]]]]]
　/// W.' … [∀ w1 [⇔ [and [∈ w1 X] [∈ w1 Y]] [and [⇒ [∃ w2 [or [= w2 X] [= w2 Y]]] [∀ w3 [⇒ [or [= w3 X] [= w3 Y]] [∈ w1 w3]]]] [⇒ [¬ [∃ w2 [or [= w2 X] [= w2 Y]]]] [∈ w1 [⋂ [set2 X Y]]]]]]]
（slash_cli の出力そのまま＝前置記法。〇_alias は / の処理の終わりに 〇 へ戻るので、出力には出ません。）