P. 13 of Theorem List - Quantum Logic Explorer

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

Type	Label	Description
Statement
Theorem	xxdp41 1201	Part of proof (4)=>(1) in Day/Pickering 1982. (Contributed by NM, 3-Apr-2012.)
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   c2 ≤ (c0 ∪ c1)
Theorem	xxdp15 1202	Part of proof (1)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	xxdp53 1203	Part of proof (5)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	xdp45lem 1204	Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	xdp43lem 1205	Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
p2 ≤ (a2 ∪ b2)    &   c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	xdp45 1206	Part of proof (4)=>(5) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	xdp43 1207	Part of proof (4)=>(3) in Day/Pickering 1982. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a2 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	3dp43 1208	"3OA" version of xdp43 1207. Changed a2 to a1 and b2 to b1. (Contributed by NM, 11-Apr-2012.)
c0 = ((a1 ∪ a1) ∩ (b1 ∪ b1))    &   c1 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   d = (a1 ∪ (a0 ∩ (a1 ∪ b1)))    &   e = (b0 ∩ (a0 ∪ p0))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a1 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a1 ∪ b1))    &   p2 = ((a0 ∪ b0) ∩ (a1 ∪ b1))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	oadp35lemg 1209	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   p ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	oadp35lemf 1210	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (a0 ∪ p) ≤ (a0 ∪ (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1)))))
Theorem	oadp35lemc 1211	Part of proof (3)=>(5) in Day/Pickering 1982. (Contributed by NM, 12-Jul-2015.)
c0 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   c2 = ((a0 ∪ a1) ∩ (b0 ∪ b1))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    &   p = (((a0 ∪ b0) ∩ (a1 ∪ b1)) ∩ (a2 ∪ b2))    ⇒   (b0 ∩ (((a0 ∩ b0) ∪ b1) ∪ (c2 ∩ (c0 ∪ c1)))) = (b0 ∩ (b1 ∪ (c2 ∩ (c0 ∪ c1))))
Theorem	oadp35 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 = ((a1 ∪ a2) ∩ (b1 ∪ b2))    &   c1 = ((a0 ∪ a2) ∩ (b0 ∪ b2))    &   p0 = ((a1 ∪ b1) ∩ (a2 ∪ b2))    ⇒   ((a0 ∪ a1) ∩ ((b0 ∩ (a0 ∪ p0)) ∪ b1)) ≤ ((c0 ∪ c1) ∪ (b1 ∩ (a0 ∪ a1)))
Theorem	testmod 1213	A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))) = ((b ∩ ((((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ d) ∪ ((a ∪ c) ∩ (b ∪ d)))) ∪ a)
Theorem	testmod1 1214	A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))
Theorem	testmod2 1215	A modular law experiment. (Contributed by NM, 21-Apr-2012.)
((a ∪ b) ∩ (a ∪ (c ∪ d))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))
Theorem	testmod2expanded 1216	A modular law experiment. (Contributed by NM, 21-Apr-2012.)
((a ∪ b) ∩ (a ∪ (c ∪ d))) = (a ∪ (b ∩ (((a ∪ c) ∩ (b ∪ d)) ∪ (d ∩ ((a ∪ c) ∪ ((b ∪ c) ∩ (d ∪ a)))))))
Theorem	testmod3 1217	A modular law experiment. (Contributed by NM, 21-Apr-2012.)
(((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))) = (a ∪ (((c ∪ a) ∪ ((b ∪ c) ∩ (d ∪ a))) ∩ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d))))))

< Previous  Wrap >