Line 2,610: |
Line 2,610: |
| | | |
| ===Rule 7=== | | ===Rule 7=== |
− |
| |
− | <pre>
| |
− | Rule 7
| |
− |
| |
− | If P, Q : U -> B,
| |
− |
| |
− | then the following are equivalent:
| |
− |
| |
− | R7a. P = Q. :R6a
| |
− | ::
| |
− | R7b. P(u) = Q(u), for all u C U. :R6b
| |
− | ::
| |
− | R7c. ConjUu (P(u) = Q(u)). :R6c
| |
− | :P1a
| |
− | ::
| |
− | R7d. ConjUu (P(u) <=> Q(u)). :P1b
| |
− | ::
| |
− | R7e. ConjUu (( P(u) , Q(u) )). :P1c
| |
− | :$1a
| |
− | ::
| |
− | R7f. ConjUu (( P , Q ))$(u). :$1b
| |
− | </pre>
| |
| | | |
| <br> | | <br> |
Line 2,686: |
Line 2,664: |
| <p><math>\operatorname{R7c~:~R6c}</math></p> | | <p><math>\operatorname{R7c~:~R6c}</math></p> |
| <p><math>\operatorname{R7c~:~P1a}</math></p> | | <p><math>\operatorname{R7c~:~P1a}</math></p> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:40px" |
| + | | |
| + | | <math>\operatorname{R7d.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))</math> |
| + | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7d~:~P1b}</math> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:60px" |
| + | | |
| + | | <math>\operatorname{R7e.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}</math> |
| + | | style="border-left:1px solid black; text-align:center" | |
| + | <p><math>\operatorname{R7e~:~P1c}</math></p> |
| + | <p><math>\operatorname{R7e~:~$1a}</math></p> |
| + | |- style="height:20px" |
| + | | |
| + | | |
| + | | |
| + | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| + | |- style="height:40px" |
| + | | |
| + | | <math>\operatorname{R7f.}</math> |
| + | | <math>\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\$ (x)</math> |
| + | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7f~:~$1b}</math> |
| |} | | |} |
| |} | | |} |