Theorem List for Quantum Logic Explorer - 1201-1215 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | xxdp53 1201 |
Part of proof (5)=>(3) in Day/Pickering 1982.
|
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 1202 |
Part of proof (4)=>(5) in Day/Pickering 1982.
|
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 1203 |
Part of proof (4)=>(3) in Day/Pickering 1982.
|
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 1204 |
Part of proof (4)=>(5) in Day/Pickering 1982.
|
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 1205 |
Part of proof (4)=>(3) in Day/Pickering 1982.
|
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 1206 |
"3OA" version of xdp43 1205. Changed a2 to a1 and b2 to
b1.
|
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 1207 |
Part of proof (3)=>(5) in Day/Pickering 1982.
|
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 1208 |
Part of proof (3)=>(5) in Day/Pickering 1982.
|
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 1209 |
Part of proof (3)=>(5) in Day/Pickering 1982.
|
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 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 = ((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 1211 |
A modular law experiment.
|
(((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 1212 |
A modular law experiment.
|
(((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 1213 |
A modular law experiment.
|
((a ∪ b)
∩ (a ∪ (c ∪ d))) =
(a ∪ (b ∩ (((a
∪ c) ∩ (b ∪ d))
∪ (d ∩ ((a ∪ c)
∪ ((b ∪ c) ∩ (d
∪ a))))))) |
|
Theorem | testmod2expanded 1214 |
A modular law experiment.
|
((a ∪ b)
∩ (a ∪ (c ∪ d))) =
(a ∪ (b ∩ (((a
∪ c) ∩ (b ∪ d))
∪ (d ∩ ((a ∪ c)
∪ ((b ∪ c) ∩ (d
∪ a))))))) |
|
Theorem | testmod3 1215 |
A modular law experiment.
|
(((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)))))) |