| Line 3,093: |
Line 3,093: |
| | | | |
| | ===Rule 11=== | | ===Rule 11=== |
| − |
| |
| − | ====Variant 1====
| |
| | | | |
| | <br> | | <br> |
| Line 3,167: |
Line 3,165: |
| | | <math>\operatorname{R11d.}</math> | | | <math>\operatorname{R11d.}</math> |
| | | | | | |
| − | <math>\begin{array}{lcl} | + | <math>\begin{array}{ccccl} |
| − | \upharpoonleft Q \upharpoonright | + | \upharpoonleft Q \upharpoonright & : & X & \to & \underline\mathbb{B} |
| − | & : & | |
| − | X \to \underline\mathbb{B} | |
| | \\ | | \\ |
| − | \upharpoonleft Q \upharpoonright (x) | + | \upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x) |
| − | & = & | |
| − | \downharpoonleft s \downharpoonright (x) \quad (\forall x \in X) | |
| | \end{array}</math> | | \end{array}</math> |
| | | style="border-left:1px solid black; text-align:center" | | | | style="border-left:1px solid black; text-align:center" | |
| Line 3,184: |
Line 3,178: |
| | | | | | |
| | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> | | | style="border-left:1px solid black; text-align:center" | <math>::\!</math> |
| − | |- style="height:40px" | + | |- style="height:60px" |
| | | | | | |
| | | <math>\operatorname{R11e.}</math> | | | <math>\operatorname{R11e.}</math> |
| − | | <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math> | + | | <math>\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)</math> |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11e~:~\_\_?\_\_}</math>
| |
| − | |}
| |
| − | |}
| |
| − | | |
| − | <br>
| |
| − | | |
| − | ====Variant 2====
| |
| − | | |
| − | <br>
| |
| − | | |
| − | {| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px; text-align:center"
| |
| − | | width="80%" |
| |
| − | | width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~11}</math>
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| |
| − | | width="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black" |
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\text{then}\!</math>
| |
| − | | <math>\text{the following are equivalent:}\!</math>
| |
| − | | style="border-left:1px solid black" |
| |
| − | |}
| |
| − | |-
| |
| − | |
| |
| − | {| align="center" cellpadding="0" cellspacing="0" width="100%"
| |
| − | |- style="height:40px"
| |
| − | | width="2%" style="border-top:1px solid black" |
| |
| − | | width="18%" style="border-top:1px solid black" | <math>\operatorname{R11a.}</math>
| |
| − | | width="60%" style="border-top:1px solid black" | <math>Q ~=~ \{ x \in X ~:~ s \}</math>
| |
| − | | width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R11a~:~R5a}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:40px"
| |
| − | |
| |
| − | | <math>\operatorname{R11b.}</math>
| |
| − | | <math>\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright</math>
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11b~:~R5e}</math>
| |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R11c.}</math>
| |
| − | |
| |
| − | <math>\begin{array}{lcl}
| |
| − | \upharpoonleft Q \upharpoonright | |
| − | & \subseteq &
| |
| − | X \times \underline\mathbb{B}
| |
| − | \\
| |
| − | \upharpoonleft Q \upharpoonright
| |
| − | & = &
| |
| − | \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y = \, \downharpoonleft s \downharpoonright (x) \}
| |
| − | \end{array}</math>
| |
| | | style="border-left:1px solid black; text-align:center" | | | | style="border-left:1px solid black; text-align:center" | |
| − | <p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p> | + | <p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p> |
| − | <p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p> | + | <p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p> |
| − | |- style="height:20px"
| |
| − | |
| |
| − | |
| |
| − | |
| |
| − | | style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| |
| − | |- style="height:60px"
| |
| − | |
| |
| − | | <math>\operatorname{R11d.}</math>
| |
| − | |
| |
| − | <math>\begin{array}{ccccl}
| |
| − | \upharpoonleft Q \upharpoonright & : & X & \to & \underline\mathbb{B}
| |
| − | \\
| |
| − | \upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x)
| |
| − | \end{array}</math>
| |
| − | | style="border-left:1px solid black; text-align:center" |
| |
| − | <p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
| |
| − | <p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
| |
| | |- style="height:20px" | | |- style="height:20px" |
| | | | | | |
| Line 3,282: |
Line 3,192: |
| | |- style="height:40px" | | |- style="height:40px" |
| | | | | | |
| − | | <math>\operatorname{R11e.}</math> | + | | <math>\operatorname{R11f.}</math> |
| | | <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math> | | | <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math> |
| − | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11e~:~\_\_?\_\_}</math> | + | | style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11f~:~\_\_?\_\_}</math> |
| | |} | | |} |
| | |} | | |} |