MyWikiBiz, Author Your Legacy — Thursday November 06, 2025
Jump to navigationJump to search
859 bytes added
, 16:33, 1 February 2009
| 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> |
| | |} | | |} |
| | |} | | |} |