Home Quantum Logic ExplorerTheorem List (p. 13 of 13) < Previous  Wrap > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

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

Theoremxxdp53 1201 Part of proof (5)=>(3) in Day/Pickering 1982.
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 1202 Part of proof (4)=>(5) in Day/Pickering 1982.
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 1203 Part of proof (4)=>(3) in Day/Pickering 1982.
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 1204 Part of proof (4)=>(5) in Day/Pickering 1982.
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 1205 Part of proof (4)=>(3) in Day/Pickering 1982.
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 1206 "3OA" version of xdp43 1205. Changed a2 to a1 and b2 to b1.
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 1207 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremoadp35lemf 1208 Part of proof (3)=>(5) in Day/Pickering 1982.
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   c2 = ((a0a1) ∩ (b0b1))    &   p0 = ((a1b1) ∩ (a2b2))    &   p = (((a0b0) ∩ (a1b1)) ∩ (a2b2))       (a0p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0c1)))))

Theoremoadp35lemc 1209 Part of proof (3)=>(5) in Day/Pickering 1982.
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 1210 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)
c0 = ((a1a2) ∩ (b1b2))    &   c1 = ((a0a2) ∩ (b0b2))    &   p0 = ((a1b1) ∩ (a2b2))       ((a0a1) ∩ ((b0 ∩ (a0p0)) ∪ b1)) ≤ ((c0c1) ∪ (b1 ∩ (a0a1)))

Theoremtestmod 1211 A modular law experiment.
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = ((b ∩ ((((ac) ∪ ((bc) ∩ (da))) ∩ d) ∪ ((ac) ∩ (bd)))) ∪ a)

Theoremtestmod1 1212 A modular law experiment.
(((ca) ∪ ((bc) ∩ (da))) ∩ (a ∪ (b ∩ (d ∪ ((ac) ∩ (bd)))))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Theoremtestmod2 1213 A modular law experiment.
((ab) ∩ (a ∪ (cd))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Theoremtestmod2expanded 1214 A modular law experiment.
((ab) ∩ (a ∪ (cd))) = (a ∪ (b ∩ (((ac) ∩ (bd)) ∪ (d ∩ ((ac) ∪ ((bc) ∩ (da)))))))

Theoremtestmod3 1215 A modular law experiment.
(((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-1215
 Copyright terms: Public domain < Previous  Wrap >