MyWikiBiz, Author Your Legacy — Wednesday December 25, 2024
Jump to navigationJump to searchDifferential Logic
o-------------------------------------------------o
| |
| |
| o-------------o o-------------o |
| / \ / \ |
| / o \ |
| / /%\ \ |
| / /%%%\ \ |
| o o%%%%%o o |
| | |%%%%%| | |
| | P |%%%%%| Q | |
| | |%%%%%| | |
| o o%%%%%o o |
| \ \%%%/ / |
| \ \%/ / |
| \ o / |
| \ / \ / |
| o-------------o o-------------o |
| |
| |
o-------------------------------------------------o
| f = p q |
o-------------------------------------------------o
Figure 22-a. Conjunction pq : X -> B
|
|
\(\text{Figure 22-a. Conjunction}~ pq : X \to \mathbb{B}\)
|
o-------------------------------------------------o
| |
| |
| o-------------o o-------------o |
| / \ / \ |
| / P o Q \ |
| / /%\ \ |
| / /%%%\ \ |
| o o.->-.o o |
| | p(q)(dp)dq |%\%/%| (p)q dp(dq) | |
| | o---------------|->o<-|---------------o | |
| | |%%^%%| | |
| o o%%|%%o o |
| \ \%|%/ / |
| \ \|/ / |
| \ o / |
| \ /|\ / |
| o-------------o | o-------------o |
| | |
| | |
| | |
| o |
| (p)(q) dp dq |
| |
o-------------------------------------------------o
| f = p q |
o-------------------------------------------------o
| |
| Ef = p q (dp)(dq) |
| |
| + p (q) (dp) dq |
| |
| + (p) q dp (dq) |
| |
| + (p)(q) dp dq |
| |
o-------------------------------------------------o
Figure 22-b. Enlargement E[pq] : EX -> B
|
o-------------------------------------------------o
| |
| |
| o-------------o o-------------o |
| / \ / \ |
| / P o Q \ |
| / /%\ \ |
| / /%%%\ \ |
| o o%%%%%o o |
| | (dp)dq |%%%%%| dp(dq) | |
| | o<--------------|->o<-|-------------->o | |
| | |%%^%%| | |
| o o%%|%%o o |
| \ \%|%/ / |
| \ \|/ / |
| \ o / |
| \ /|\ / |
| o-------------o | o-------------o |
| | |
| | |
| v |
| o |
| dp dq |
| |
o-------------------------------------------------o
| f = p q |
o-------------------------------------------------o
| |
| Df = p q ((dp)(dq)) |
| |
| + p (q) (dp) dq |
| |
| + (p) q dp (dq) |
| |
| + (p)(q) dp dq |
| |
o-------------------------------------------------o
Figure 22-c. Difference D[pq] : EX -> B
|