Line 10,882: |
Line 10,882: |
| & + & \texttt{(} u \texttt{)} v \cdot 0 | | & + & \texttt{(} u \texttt{)} v \cdot 0 |
| & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot 0 | | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot 0 |
| + | \end{array}</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | ====Operator Maps for the Logical Implication ''f''<sub>11</sub>(u, v)==== |
| + | |
| + | =====Computation of ε''f''<sub>11</sub>===== |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="10" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.1} ~~ \text{Computation of}~ \boldsymbol\varepsilon f_{11}\!</math> |
| + | | |
| + | <math>\begin{array}{*{10}{l}} |
| + | \boldsymbol\varepsilon f_{11} |
| + | & = && f_{11}(u, v) |
| + | \\[4pt] |
| + | & = && \texttt{(} u \texttt{((} v \texttt{))} |
| + | \\[4pt] |
| + | & = && \texttt{ } u \texttt{ } v \texttt{ } \cdot f_{11}(1, 1) |
| + | & + & \texttt{ } u \texttt{ (} v \texttt{)} \cdot f_{11}(1, 0) |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \cdot f_{11}(0, 1) |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot f_{11}(0, 0) |
| + | \\[4pt] |
| + | & = && \texttt{ } u \texttt{ } v \texttt{ } |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} |
| + | \\[20pt] |
| + | \boldsymbol\varepsilon f_{11} |
| + | & = && \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{(} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \cdot \texttt{(} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{)} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{)} |
| + | \\[4pt] |
| + | && + & \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \cdot \texttt{(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~} |
| + | \\[4pt] |
| + | && + & \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \cdot \texttt{~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)} |
| + | \\[4pt] |
| + | && + & \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \cdot \texttt{~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~} |
| + | \end{array}\!</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | =====Computation of E''f''<sub>11</sub>===== |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="10" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.2} ~~ \text{Computation of}~ \mathrm{E}f_{11}\!</math> |
| + | | |
| + | <math>\begin{array}{*{10}{l}} |
| + | \mathrm{E}f_{11} |
| + | & = && f_{11}(u + \mathrm{d}u, v + \mathrm{d}v) |
| + | \\[4pt] |
| + | & = && |
| + | \texttt{(} |
| + | \\ |
| + | &&& \qquad \texttt{(} u \texttt{,} \mathrm{d}u \texttt{)} |
| + | \\ |
| + | &&& \texttt{(} |
| + | \\ |
| + | &&& \qquad \texttt{(} v \texttt{,} \mathrm{d}v \texttt{)} |
| + | \\ |
| + | &&& \texttt{))} |
| + | \\[4pt] |
| + | & = && |
| + | u v |
| + | \!\cdot\! |
| + | \texttt{((} \mathrm{d}u \texttt{)((} \mathrm{d}v \texttt{)))} |
| + | & + & |
| + | u \texttt{(} v \texttt{)} |
| + | \!\cdot\! |
| + | \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & |
| + | \texttt{(} u \texttt{)} v |
| + | \!\cdot\! |
| + | \texttt{(} \mathrm{d}u \texttt{((} \mathrm{d}v \texttt{)))} |
| + | & + & |
| + | \texttt{(} u \texttt{)(} v \texttt{)} |
| + | \!\cdot\! |
| + | \texttt{(} \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{))} |
| + | \\[4pt] |
| + | & = && |
| + | u v |
| + | \!\cdot\! |
| + | \texttt{((} \mathrm{d}u \texttt{)} \mathrm{d}v \texttt{)} |
| + | & + & |
| + | u \texttt{(} v \texttt{)} |
| + | \!\cdot\! |
| + | \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & |
| + | \texttt{(} u \texttt{)} v |
| + | \!\cdot\! |
| + | \texttt{(} \mathrm{d}u ~ \mathrm{d}v \texttt{)} |
| + | & + & |
| + | \texttt{(} u \texttt{)(} v \texttt{)} |
| + | \!\cdot\! |
| + | \texttt{(} \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{))} |
| + | \\[20pt] |
| + | \mathrm{E}f_{11} |
| + | & = && \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{(} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \!\cdot\! \texttt{(} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{)} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \!\cdot\! \texttt{(} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{)} |
| + | \\[4pt] |
| + | && + & 0 |
| + | & + & \texttt{ } u \texttt{ (} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~} |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \!\cdot\! \texttt{(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \!\cdot\! \texttt{(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~} |
| + | \\[4pt] |
| + | && + & \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)} |
| + | & + & \texttt{ } u \texttt{ (} v \texttt{)} \cdot \texttt{~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)} |
| + | & + & \texttt{(} u \texttt{) } v \texttt{ } \!\cdot\! \texttt{~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | \\[4pt] |
| + | && + & \texttt{ } u \texttt{ } v \texttt{ } \cdot \texttt{~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~} |
| + | & + & \texttt{ } u \texttt{ (} v \texttt{)} \cdot \texttt{~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \!\cdot\! \texttt{~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~} |
| + | \end{array}</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | =====Computation of D''f''<sub>11</sub>===== |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="10" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.3-i} ~~ \text{Computation of}~ \mathrm{D}f_{11} ~\text{(Method 1)}\!</math> |
| + | | |
| + | <math>\begin{array}{*{10}{l}} |
| + | \mathrm{D}f_{11} |
| + | & = && \mathrm{E}f_{11} |
| + | & + & \boldsymbol\varepsilon f_{11} |
| + | \\[4pt] |
| + | & = && f_{11}(u + \mathrm{d}u, v + \mathrm{d}v) |
| + | & + & f_{11}(u, v) |
| + | \\[4pt] |
| + | & = && |
| + | \texttt{(} \texttt{(} u \texttt{,} \mathrm{d}u \texttt{)} |
| + | \texttt{(} \texttt{(} v \texttt{,} \mathrm{d}v \texttt{)} |
| + | \texttt{))} |
| + | & + & |
| + | \texttt{(} u \texttt{(} v \texttt{))} |
| + | \\[20pt] |
| + | \mathrm{D}f_{11} |
| + | & = && 0 |
| + | & + & 0 |
| + | & + & 0 |
| + | & + & 0 |
| + | \\[4pt] |
| + | && + & u v \!\cdot\! \texttt{(} \mathrm{d}u \texttt{)} \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \!\cdot\! \texttt{~(} \mathrm{d}u \texttt{)~} \mathrm{d}v \texttt{~~} |
| + | & + & 0 |
| + | & + & 0 |
| + | \\[4pt] |
| + | && + & 0 |
| + | & + & u \texttt{(} v \texttt{)} \!\cdot\! \texttt{~~} \mathrm{d}u \texttt{~(} \mathrm{d}v \texttt{)~} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \!\cdot\! \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)} |
| + | \\[4pt] |
| + | && + & 0 |
| + | & + & u \texttt{(} v \texttt{)} \!\cdot\! \texttt{~~} \mathrm{d}u \texttt{~~} \mathrm{d}v \texttt{~~} |
| + | & + & \texttt{(} u \texttt{)} v \!\cdot\! \mathrm{d}u ~ \mathrm{d}v |
| + | & + & 0 |
| + | \\[20pt] |
| + | \mathrm{D}f_{11} |
| + | & = && u v \!\cdot\! \texttt{(} \mathrm{d}u \texttt{)} \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \!\cdot\! \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & \texttt{(} u \texttt{)} v \!\cdot\! \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \!\cdot\! \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)} |
| + | \end{array}</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="10" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.3-ii} ~~ \text{Computation of}~ \mathrm{D}f_{11} ~\text{(Method 2)}\!</math> |
| + | | |
| + | <math>\begin{array}{c*{9}{l}} |
| + | \mathrm{D}f_{11} |
| + | & = & \boldsymbol\varepsilon f_{11} ~+~ \mathrm{E}f_{11} |
| + | \\[20pt] |
| + | \boldsymbol\varepsilon f_{11} |
| + | & = & u v \cdot 1 |
| + | & + & u \texttt{(} v \texttt{)} \cdot 0 |
| + | & + & \texttt{(} u \texttt{)} v \cdot 1 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot 1 |
| + | \\[6pt] |
| + | \mathrm{E}f_{11} |
| + | & = & |
| + | u v |
| + | \cdot |
| + | \texttt{((} \mathrm{d}u \texttt{)} \mathrm{d}v \texttt{)} |
| + | & + & |
| + | u \texttt{(} v \texttt{)} |
| + | \cdot |
| + | \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & |
| + | \texttt{(} u \texttt{)} v |
| + | \cdot |
| + | \texttt{(} \mathrm{d}u ~ \mathrm{d}v \texttt{)} |
| + | & + & |
| + | \texttt{(} u \texttt{)(} v \texttt{)} |
| + | \cdot |
| + | \texttt{(} \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{))} |
| + | \\[20pt] |
| + | \mathrm{D}f_{11} |
| + | & = & |
| + | u v |
| + | \cdot |
| + | \texttt{~(} \mathrm{d}u \texttt{)} \mathrm{d}v \texttt{~} |
| + | & + & |
| + | u \texttt{(} v \texttt{)} |
| + | \cdot |
| + | \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & |
| + | \texttt{(} u \texttt{)} v |
| + | \cdot |
| + | \texttt{~} \mathrm{d}u ~ \mathrm{d}v \texttt{~} |
| + | & + & |
| + | \texttt{(} u \texttt{)(} v \texttt{)} |
| + | \cdot |
| + | \texttt{~} \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)~} |
| + | \end{array}</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | =====Computation of d''f''<sub>11</sub>===== |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="20" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.4} ~~ \text{Computation of}~ \mathrm{d}f_{11}\!</math> |
| + | | |
| + | <math>\begin{array}{c*{8}{l}} |
| + | \mathrm{D}f_{11} |
| + | & = & u v \cdot \texttt{(} \mathrm{d}u \texttt{)} \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)} |
| + | \\[6pt] |
| + | \Downarrow |
| + | \\[6pt] |
| + | \mathrm{d}f_{11} |
| + | & = & u v \cdot \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u |
| + | \end{array}</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | =====Computation of r''f''<sub>11</sub>===== |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="20" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.5} ~~ \text{Computation of}~ \mathrm{r}f_{11}\!</math> |
| + | | |
| + | <math>\begin{array}{c*{8}{l}} |
| + | \mathrm{r}f_{11} & = & \mathrm{D}f_{11} ~+~ \mathrm{d}f_{11} |
| + | \\[20pt] |
| + | \mathrm{D}f_{11} |
| + | & = & u v \cdot \texttt{(} \mathrm{d}u \texttt{)} \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)} |
| + | \\[6pt] |
| + | \mathrm{d}f_{11} |
| + | & = & u v \cdot \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u |
| + | \\[20pt] |
| + | \mathrm{r}f_{11} |
| + | & = & u v \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | \end{array}</math> |
| + | |} |
| + | |
| + | <br> |
| + | |
| + | =====Computation Summary for Implication===== |
| + | |
| + | <br> |
| + | |
| + | {| align="center" border="1" cellpadding="20" cellspacing="0" style="text-align:left; width:90%" |
| + | |+ style="height:30px" | <math>\text{Table F11.6} ~~ \text{Computation Summary for}~ f_{11}(u, v) = \texttt{(} u \texttt{(} v \texttt{))}\!</math> |
| + | | |
| + | <math>\begin{array}{c*{8}{l}} |
| + | \boldsymbol\varepsilon f_{11} |
| + | & = & u v \cdot 1 |
| + | & + & u \texttt{(} v \texttt{)} \cdot 0 |
| + | & + & \texttt{(} u \texttt{)} v \cdot 1 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot 1 |
| + | \\[6pt] |
| + | \mathrm{E}f_{11} |
| + | & = & u v \cdot \texttt{((} \mathrm{d}u \texttt{)} \mathrm{d}v \texttt{)} |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & \texttt{(} u \texttt{)} v \cdot \texttt{(} \mathrm{d}u ~ \mathrm{d}v \texttt{)} |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{))} |
| + | \\[6pt] |
| + | \mathrm{D}f_{11} |
| + | & = & u v \cdot \texttt{(} \mathrm{d}u \texttt{)} \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{((} \mathrm{d}u \texttt{)(} \mathrm{d}v \texttt{))} |
| + | & + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u \texttt{(} \mathrm{d}v \texttt{)} |
| + | \\[6pt] |
| + | \mathrm{d}f_{11} |
| + | & = & u v \cdot \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \texttt{(} \mathrm{d}u \texttt{,} \mathrm{d}v \texttt{)} |
| + | & + & 0 |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u |
| + | \\[6pt] |
| + | \mathrm{r}f_{11} |
| + | & = & uv \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & u \texttt{(} v \texttt{)} \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)} v \cdot \mathrm{d}u ~ \mathrm{d}v |
| + | & + & \texttt{(} u \texttt{)(} v \texttt{)} \cdot \mathrm{d}u ~ \mathrm{d}v |
| \end{array}</math> | | \end{array}</math> |
| |} | | |} |
Line 10,948: |
Line 11,285: |
| & = && f_{14}(u + \mathrm{d}u, v + \mathrm{d}v) | | & = && f_{14}(u + \mathrm{d}u, v + \mathrm{d}v) |
| \\[4pt] | | \\[4pt] |
− | & = && \texttt{(((} u \texttt{,} \mathrm{d}u \texttt{))((} v \texttt{,} \mathrm{d}v \texttt{)))} | + | & = && |
| + | \texttt{((} |
| + | \\ |
| + | &&& \qquad \texttt{(} u \texttt{,} \mathrm{d}u \texttt{)} |
| + | \\ |
| + | &&& \texttt{)(} |
| + | \\ |
| + | &&& \qquad \texttt{(} v \texttt{,} \mathrm{d}v \texttt{)} |
| + | \\ |
| + | &&& \texttt{))} |
| \\[4pt] | | \\[4pt] |
| & = && \texttt{ } u \texttt{ } v \texttt{ } \!\cdot\! f_{14}(\texttt{(} \mathrm{d}u \texttt{)}, \texttt{(} \mathrm{d}v \texttt{)}) | | & = && \texttt{ } u \texttt{ } v \texttt{ } \!\cdot\! f_{14}(\texttt{(} \mathrm{d}u \texttt{)}, \texttt{(} \mathrm{d}v \texttt{)}) |