Thm②

Prop

p-Formを指し示すことに使われるPropというものを導入します。
Propを紹介するときは、それが指し示すp-Formを右側に書きます。
正規wordの定義と思えるPropには . が付きます。\(=\)と\(\emptyset\) の定義を挙げてみます。
\(\)【\(\)】
\({\emptyset.}\)【\(\emptyset = \{ Array x \mid {\perp} \}\)】

\(\downarrow\) は次のように計算されます。
\(=.\) ≃【\(X = Y \forall x \, ( x \in X x \in Y )\)】
\(\emptyset.\) ≃【\(\forall x \, ( x \in \emptyset \, {\perp} )\)】

rule

2つの$Formは、$var同士の変換、$Var同士の変換、等で移り変わるとき同じとみなされます。

Formを$Formに変換する関数 $ を作ります。
varを$Varに置き換えます。例　$【\(X \in Y\)】=【\({\sf X} \in {\sf Y}\)】
ただし、束縛されたvarは$varに替えます。例　$【\(\forall X ( X \in Y )\)】=【\(\forall {\sf x} ( {\sf x} \in {\sf Y} )\)】

\(=\) か \(\) で始まるPropに対して、Prop変換の規則が作られます。
\({\rm rule}({\tt X} = {\tt Y})\) … $\({\tt X}\) ≃ $\({\tt Y}\)
\({\rm rule}({\tt P} \Leftrightarrow {\tt Q})\) … $\({\tt P}\) ≃ $\({\tt Q}\)
さらに \({\rm rule}(\forall{\tt x P})\) = \({\rm rule}({\tt P})\) とします。
例　\({\rm rule}({=.})\) … 【\({\sf X} = {\sf Y}\)】≃【\(\forall {\sf x} \, ( {\sf x} \in {\sf X} {\sf x} \in {\sf Y} )\)】
例　\({\rm rule}({\emptyset.})\) … 【\({\sf X} \in \emptyset\)】≃【\({\perp}\)】

完全には実装できていません。

slash

Prop \({\tt F}\) を \({\rm rule}({\tt P})\) で変形した結果を \({\tt F}{\bf /}{\tt P}\) とします。変形できるsub Formをすべて変形します。
\(\emptyset0{\bf /}{\emptyset.}\) ≃【\(\neg {\perp}\)】

部分Formに対してruleを適用したいことがあります。\(\downarrow\)をしたときの場所を指定できます。
例えば \([n]\) の部分Formに対して \({\bf /}\) を適用することを \({\bf /}^n\) と書き、\(\emptyset0{\bf /}^{1}{\emptyset.}\) = \(\emptyset0{\bf /}{\emptyset.}\) となります。

\([m][n]\) の部分Formに対して \({\bf /}\) を適用することを \({\bf /}^{mn}\) と書きます。

\({\bf /}\) や \({\bf /}^n\) などはL結合とされます。\({\tt P}{\bf /}{\tt Q}{\bf /}{\tt R}\) = \(({\tt P}{\bf /}{\tt Q}){\bf /}{\tt R}\)

定義によるslash

\(\text{rule}({\tt w}.)\)の左辺の\([0]\)が\({\tt w}\) のとき \({\tt w}\) は0-definedと言われます。
例　\(=\) はdefined
\(\text{rule}({\tt w}.)\) の左辺が \({\sf X}\in{\tt w}(\cdots)\) となる \({\tt w}\) は\(\in\)-definedと言われます。
例　\(\emptyset\) は \(\in\)-defined

\(\text{rule}({\tt w}.)\) (\({\tt w}\)は0-definedか\(\in\)-defined) の形のruleを可能な限り全てに継時的に適用した結果を \({\bf /}\mathbb{D}.\) で作ります。
\(\text{rule}({=}{.})\) だけは、部分p-Formで\([0]\)が\(=\)のものに対し\([1],[2]\)のどちらかでも\([0]\)が\(\in\)-definedなら適用、した結果を \({\bf /}{\rm d\!I}.\) で作ります。
例　\(\emptyset0{\bf /}\) = \(\emptyset0{\bf /}\) = \(\emptyset0{\bf /}{\emptyset.}\)

\({\tt f}.\)だけ除外したいときには / D.-\({\tt f}.\) または / d.-\({\tt f}.\) のようにinputします。

PropのThm

Propは紹介時に「どのPropから推論可能か」というThmが付くことがあります。\(\blacktriangleleft\) をクリックすると出てきます。例えば
\(\emptyset0\)【\(x \notin \emptyset\)】

次に注意しましょう。　\({\tt Q}\blacktriangleright{\tt P}\Leftrightarrow{\tt P}{\bf /}{\tt Q}\)
一般にAssumptionsは少ない方が証明が簡単になります。上のProp紹介はより強い次のものにした方が良いです。
\(\emptyset0\)【\(x \notin \emptyset\)】