Theorem List for Quantum Logic Explorer - 1201-1217   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremxxdp41 1201 Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       c2 ≤ (c0c1)

Theoremxxdp15 1202 Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremxxdp53 1203 Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremxdp45lem 1204 Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremxdp43lem 1205 Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2b2)    &   c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremxdp45 1206 Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremxdp43 1207 Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a2 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))    &   p0 = ((a1b1) ∩ (a2b2))    &   p2 = ((a0b0) ∩ (a1b1))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theorem3dp43 1208 "3OA" version of xdp43 1207. Changed a2 to a1 and b2 to b1. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1a1) ∩ (b1b1))    &   c1 = ((a0a1) ∩ (b0b1))    &   c2 = ((a0a1) ∩ (b0b1))    &   d = (a1 ∪ (a0 ∩ (a1b1)))    &   e = (b0 ∩ (a0p0))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a1b1))    &   p0 = ((a1b1) ∩ (a1b1))    &   p2 = ((a0b0) ∩ (a1b1))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremoadp35lemg 1209 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremoadp35lemf 1210 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremoadp35lemc 1211 Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (b0 ∩ (((a0b0) ∪ b1) ∪ (c2 ∩ (c0c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0c1))))

Theoremoadp35 1212 Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(5) (Contributed by NM, 12-Apr-2012.)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   p0 = ((a1b1) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremtestmod 1213 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = ((b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) ∪ a)

Theoremtestmod1 1214 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Theoremtestmod2 1215 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
((ab) ∩ (a ∪ (cd))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Theoremtestmod2expanded 1216 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
((ab) ∩ (a ∪ (cd))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Theoremtestmod3 1217 A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (((ca) ∪ ((bc) ∩ (da))) ∩ (b ∩ (d ∪ ((ac) ∩ (bd))))))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1217
 Copyright terms: Public domain < Previous  Wrap >