resultの分割
Prop \({\tt P}\) を２つに分割することがあります。
\({\tt P}\) = \({\tt R}_1,{\tt R}_2\) のとき \(\begin{cases} {\tt P}\rfloor \\ {\tt P}\lfloor \end{cases}\) = \(\begin{cases} {\tt R}_1 \\ {\tt R}_2 \end{cases}\)
\({\tt P}\) = \({\tt R}_1 \Leftrightarrow {\tt R}_2\) のとき \(\begin{cases} {\tt P}\rfloor \\ {\tt P}\lfloor \end{cases}\) = \(\begin{cases} {\tt R}_1\Rightarrow{\tt R}_2 \\ {\tt R}_2\Rightarrow{\tt R}_1 \end{cases}\)
\({\tt P}\) = \({\tt Q}\Rightarrow{\tt R}\) のとき \(\begin{cases} {\tt P}\rfloor \\ {\tt P}\lfloor \end{cases}\) = \(\begin{cases} {\tt Q}\Rightarrow({\tt R}\rfloor) \\ {\tt Q}\Rightarrow({\tt R}\lfloor) \end{cases}\)
\({\tt P}\) = \(\forall{\tt xQ}\) のとき \(\begin{cases} {\tt P}\rfloor \\ {\tt P}\lfloor \end{cases}\) = \(\begin{cases} \forall{\tt x}({\tt Q}\rfloor) \\ \forall{\tt x}({\tt Q}\lfloor) \end{cases}\)
Rite
Prop , \(\mathbb{S}.\) , \({\bf /}\) , \(\rfloor\) , \(\lfloor\) 等から作られるものを Rite と呼びます。Riteもp-Formを指し示します。
Riteのinputでは区切りはスペースとしますが、( ) の前後のスペースは略せます。
Thmの分割
次に注意しましょう。\({\tt P}\) ≡ \({\tt P}\rfloor , {\tt P}\lfloor\)
\({\tt P}\blacktriangleleft\mathcal{A}\) を \({\tt P}\rfloor, {\tt P}\lfloor \,\blacktriangleleft\, \mathcal{A}\) と分割して証明させることが行われます。
\({\tt PX}\blacktriangleleft\mathcal{A},{\tt PY}\blacktriangleleft\mathcal{B}\) を \({\tt P}\big\{{\tt X}\blacktriangleleft\mathcal{A} \,\pmb{\big|}\, {\tt Y}\blacktriangleleft\mathcal{B}\big\}\) と表します。分配則みたいに。
３分割したりも？