| Line 309: |
Line 309: |
| | </ol> | | </ol> |
| | | | |
| − | ==Equation Sequences : Old Versions== | + | ==Equation Sequences== |
| − | | |
| − | {| align="center" cellpadding="4" style="text-align:left" width="90%"
| |
| − | |
| |
| − | |-
| |
| − | | <math>[| \downharpoonleft s \downharpoonright |]</math>
| |
| − | | <math>=\!</math>
| |
| − | | <math>[| F |]\!</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>F^{-1} (\underline{1})</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ s ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) = \underline{1} ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} = \underline{1} ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{exclusive~or}~ y ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \operatorname{just~one~true~of}~ x, y ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{not~equal~to}~ y ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \nLeftrightarrow y ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \neq y ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x + y ~\}.</math>
| |
| − | |-
| |
| − | |
| |
| − | |}
| |
| − | | |
| − | {| align="center" cellpadding="4" style="text-align:left" width="90%"
| |
| − | |
| |
| − | |-
| |
| − | | <math>[| F^\$ (p, q) |]</math>
| |
| − | | <math>=\!</math>
| |
| − | | <math>[| \underline{(}~p~,~q~\underline{)}^\$ |]</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>(F^\$ (p, q))^{-1} (\underline{1})</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ F^\$ (p, q)(x) ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ \underline{(}~p~,~q~\underline{)}^\$ (x) ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ \underline{(}~p(x)~,~q(x)~\underline{)} ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ p(x) + q(x) ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ p(x) \neq q(x) ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ \upharpoonleft P \upharpoonright (x) ~\neq~ \upharpoonleft Q \upharpoonright (x) ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ x \in P ~\nLeftrightarrow~ x \in Q ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ x \in P\!-\!Q ~\operatorname{or}~ x \in Q\!-\!P ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ x \in P\!-\!Q ~\cup~ Q\!-\!P ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>\{~ x \in X ~:~ x \in P + Q ~\}</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>P + Q ~\subseteq~ X</math>
| |
| − | |-
| |
| − | |
| |
| − | | <math>=\!</math>
| |
| − | | <math>[|p|] + [|q|] ~\subseteq~ X</math>
| |
| − | |-
| |
| − | |
| |
| − | |}
| |
| − | | |
| − | ==Equation Sequences : New Versions==
| |
| | | | |
| | {| align="center" cellpadding="8" width="90%" | | {| align="center" cellpadding="8" width="90%" |
| Line 868: |
Line 746: |
| | <br> | | <br> |
| | | | |
| − | ===Proof Schemata : Old Versions=== | + | ===Proof Schemata=== |
| − | | |
| − | <br>
| |
| − | | |
| − | {| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black; border-bottom:1px solid black" width="90%"
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" width="20%" |
| |
| − | | align="left" width="60%" |
| |
| − | | align="right" style="border-right:1px solid black" width="20%" | <math>\text{Definition 1}\!</math>
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | style="border-top:1px solid black" | <math>Q \subseteq X</math>
| |
| − | | style="border-right:1px solid black; border-top:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{then}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{such that:}\!</math>
| |
| − | |
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{D1a.}\!</math>
| |
| − | | style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q</math>
| |
| − | | align="right" style="border-right:1px solid black; border-top:1px solid black" | <math>\forall x \in X</math>
| |
| − | |}
| |
| − | | |
| − | <br>
| |
| − | | |
| − | {| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black; border-bottom:1px solid black" width="90%"
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" width="20%" |
| |
| − | | align="left" width="60%" |
| |
| − | | align="right" style="border-right:1px solid black" width="20%" | <math>\text{Rule 1}\!</math>
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | style="border-top:1px solid black" | <math>Q \subseteq X</math>
| |
| − | | style="border-right:1px solid black; border-top:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{then}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{and if}\!</math>
| |
| − | | <math>x \in X</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{R1a.}\!</math>
| |
| − | | style="border-top:1px solid black" | <math>x \in Q</math>
| |
| − | | style="border-right:1px solid black; border-top:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{R1b.}\!</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright (x)</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |}
| |
| − | | |
| − | <br>
| |
| − | | |
| − | {| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black; border-bottom:1px solid black" width="90%"
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" width="20%" |
| |
| − | | align="left" width="60%" |
| |
| − | | align="right" style="border-right:1px solid black" width="20%" | <math>\text{Rule 2}\!</math>
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | style="border-top:1px solid black" | <math>f : X \to \underline\mathbb{B}</math>
| |
| − | | style="border-right:1px solid black; border-top:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{and}\!</math>
| |
| − | | <math>x \in X</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{R2a.}\!</math>
| |
| − | | style="border-top:1px solid black" | <math>f(x)\!</math>
| |
| − | | style="border-right:1px solid black; border-top:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{R2b.}\!</math>
| |
| − | | <math>f(x) = \underline{1}</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |}
| |
| − | | |
| − | <br>
| |
| − | | |
| − | {| align="center" cellpadding="8" cellspacing="0" style="border-top:1px solid black; border-bottom:1px solid black" width="90%"
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" width="20%" |
| |
| − | | align="left" style="border-right:1px solid black" width="60%" |
| |
| − | | align="center" style="border-right:1px solid black" width="20%" | <math>\text{Rule 3}\!</math>
| |
| − | |-
| |
| − | | style="border-left:1px solid black; border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | style="border-top:1px solid black; border-right:1px solid black" | <math>Q \subseteq X</math>
| |
| − | | style="border-top:1px solid black; border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{and}\!</math>
| |
| − | | style="border-right:1px solid black" | <math>x \in X</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | style="border-left:1px solid black" | <math>\text{then}\!</math>
| |
| − | | style="border-right:1px solid black" | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-right:1px solid black" |
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black; border-top:1px solid black" |
| |
| − | <math>\text{R3a.}\!</math>
| |
| − | | align="left" style="border-top:1px solid black; border-right:1px solid black" |
| |
| − | <math>x \in Q</math>
| |
| − | | align="center" style="border-top:1px solid black; border-right:1px solid black" |
| |
| − | <math>\text{R3a : R1a}\!</math>
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" |
| |
| − | | align="left" style="border-right:1px solid black" |
| |
| − | | align="center" style="border-right:1px solid black" | <math>::\!</math>
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" |
| |
| − | <math>\text{R3b.}\!</math>
| |
| − | | align="left" style="border-right:1px solid black" |
| |
| − | <math>\upharpoonleft Q \upharpoonright (x)</math>
| |
| − | | align="center" style="border-right:1px solid black" |
| |
| − | <p><math>\text{R3b : R1b}\!</math></p>
| |
| − | <p><math>\text{R3b : R2a}\!</math></p>
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" |
| |
| − | | align="left" style="border-right:1px solid black" |
| |
| − | | align="center" style="border-right:1px solid black" | <math>::\!</math>
| |
| − | |-
| |
| − | | align="left" style="border-left:1px solid black" |
| |
| − | <math>\text{R3c.}\!</math>
| |
| − | | align="left" style="border-right:1px solid black" |
| |
| − | <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
| |
| − | | align="center" style="border-right:1px solid black" |
| |
| − | <math>\text{R3c : R2b}\!</math>
| |
| − | |}
| |
| − | | |
| − | <br>
| |
| − | | |
| − | ===Proof Schemata : New Versions===
| |
| | | | |
| | <br> | | <br> |