Form→$Form
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} )\)】
完全には実装できていません。
rule
\(=\) か \(\Leftrightarrow\) で始まる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}({=.})\) … 【\({\sf X} = {\sf Y}\)】≃【\( {\sf X} {\sf Y} \)】
さらに \({\rm rule}(\forall{\tt x P})\) = \({\rm rule}({\tt P})\) とします。
例 \({\rm rule}({\emptyset.})\) … 【\({\sf X} \in \emptyset\)】≃【\({\perp}\)】
いくつかのruleを合わせたruleも考えられます。
\(\text{rule}({\tt P})\) (\({\tt P}\)はs.Prop) の形のruleをすべて合わせたruleを \(\text{rule}(\text{s.})\) とします。
\(\text{rule}({\tt P})\) (\({\tt P}\)はp.Prop) の形のruleをすべて合わせたruleを \(\text{rule}(\text{p.})\) とします。
slash
\({\tt P}\) を \({\rm rule}({\tt Q})\) で変形した結果を \({\tt P}{\bf /}{\tt Q}\) とします。変形できるsub Propをすべて変形します。
例 【\(0=1\)】\(\!{\bf /}=.\) =【\(\forall x\,(x\in0 \Leftrightarrow x\in1)\)】
\((\;)\) はメタ数学語の単語としても使用されます。例 \({\tt P}{\bf /}({\tt Q}{\bf /}{\tt R})\)
\({\bf /}\) はL結合とされます。\({\tt P}{\bf /}{\tt Q}{\bf /}{\tt R}\) = \(({\tt P}{\bf /}{\tt Q}){\bf /}{\tt R}\)
一般にAssumptionsは少ない方が証明が簡単になります。前ページのProp紹介はより強い次のものにした方が良いです。
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】\({\bf /}{\subset.}{\bf /}{=.}\) ◀ O
さらに \({{=.}.}{\bf /}\text{p.}\) = \({{=.}.}{\bf /}{=.}{\bf /}{\subset.}\) ですので、実際には次の記述がされます。
\({=}{.}{.}\)【\(X = Y \Longleftrightarrow X \subset Y \subset X\)】\({\bf /}\text{p.}\) ◀ O