Statement List for Quantum Logic Explorer - 1001-1100 - Page 11 of 12
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | oaliii 1001 |
Orthoarguesian law. Godowski/Greechie, Eq. III.
|
| ((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) = ((a →2 c) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) |
| |
| Theorem | oalii 1002 |
Orthoarguesian law. Godowski/Greechie, Eq. II. This proof references
oaliii 1001 only.
|
| (b⊥ ∩ ((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))))) ≤ a⊥ |
| |
| Theorem | oaliv 1003 |
Orthoarguesian law. Godowski/Greechie, Eq. IV.
|
| (b⊥ ∩ ((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c))) |
| |
| Theorem | oath1 1004 |
OA theorem.
|
| ((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) = ((a →2 b) ∩ (a
→2 c)) |
| |
| Theorem | oalem1 1005 |
Lemma
|
| ((b ∪ c)
∪ ((b ∪ c)⊥ ∩ ((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))))) ≤ (a →2 (b ∪ c)) |
| |
| Theorem | oalem2 1006 |
Lemma
|
| ((a →2 b) ∪ ((a
→2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a
→2 c))))) = (a →2 b) |
| |
| Theorem | oadist2a 1007 |
Distributive inference derived from OA.
|
| (d
∪ ((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c)))) ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
⇒ ((a →2
b) ∩ (d ∪ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) = (((a →2 b) ∩ d)
∪ ((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) |
| |
| Theorem | oadist2b 1008 |
Distributive inference derived from OA.
|
| d
≤ ((b ∪ c) →0 ((a →2 b) ∩ (a
→2 c)))
⇒ ((a →2
b) ∩ (d ∪ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) = (((a →2 b) ∩ d)
∪ ((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) |
| |
| Theorem | oadist2 1009 |
Distributive inference derived from OA.
|
| (d
∪ ((b ∪ c) →2 ((a →2 b) ∩ (a
→2 c)))) = ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
⇒ ((a →2
b) ∩ (d ∪ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) = (((a →2 b) ∩ d)
∪ ((a →2 b) ∩ ((b
∪ c) →2 ((a →2 b) ∩ (a
→2 c))))) |
| |
| Theorem | oadist12 1010 |
Distributive law derived from OA.
|
| ((a →2 b) ∩ (((b
∪ c) →1 ((a →2 b) ∩ (a
→2 c))) ∪ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c))))) = (((a
→2 b) ∩ ((b ∪ c)
→1 ((a →2
b) ∩ (a →2 c)))) ∪ ((a
→2 b) ∩ ((b ∪ c)
→2 ((a →2
b) ∩ (a →2 c))))) |
| |
| Theorem | oacom 1011 |
Commutation law requiring OA.
|
| d C ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c)))
& (d ∩ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))) C (a →2 b)
⇒ d C
((a →2 b) ∩ (a
→2 c)) |
| |
| Theorem | oacom2 1012 |
Commutation law requiring OA.
|
| d
≤ ((a →2 b) ∩ ((b
∪ c) →0 ((a →2 b) ∩ (a
→2 c))))
⇒ d C
((a →2 b) ∩ (a
→2 c)) |
| |
| Theorem | oacom3 1013 |
Commutation law requiring OA.
|
| (d
∩ (a →2 b)) C ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
& d C
(a →2 b)
⇒ d C
((a →2 b) ∩ (a
→2 c)) |
| |
| Theorem | oagen1 1014 |
"Generalized" OA.
|
| d
≤ ((b ∪ c) →0 ((a →2 b) ∩ (a
→2 c)))
⇒ ((a →2
b) ∩ (d ∪ ((a
→2 b) ∩ (a →2 c)))) = ((a
→2 b) ∩ (a →2 c)) |
| |
| Theorem | oagen1b 1015 |
"Generalized" OA.
|
| d
≤ (a →2 b)
& e ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
⇒ (d ∩
(e ∪ ((a →2 b) ∩ (a
→2 c)))) = (d ∩ (a
→2 c)) |
| |
| Theorem | oagen2 1016 |
"Generalized" OA.
|
| d
≤ ((b ∪ c) →0 ((a →2 b) ∩ (a
→2 c)))
⇒ ((a →2
b) ∩ d) ≤ (a
→2 c) |
| |
| Theorem | oagen2b 1017 |
"Generalized" OA.
|
| d
≤ (a →2 b)
& e ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
⇒ (d ∩ e) ≤ (a
→2 c) |
| |
| Theorem | mloa 1018 |
Mladen's OA
|
| ((a ≡ b)
∩ ((b ≡ c) ∪ ((b
∪ (a ≡ b)) ∩ (c
∪ (a ≡ c))))) ≤ (c
∪ (a ≡ c)) |
| |
| Theorem | oadist 1019 |
Distributive law derived from OAL.
|
| d
≤ ((b ∪ c) →0 ((a →2 b) ∩ (a
→2 c)))
⇒ ((a →2
b) ∩ (d ∪ ((a
→2 b) ∩ (a →2 c)))) = (((a
→2 b) ∩ d) ∪ ((a
→2 b) ∩ ((a →2 b) ∩ (a
→2 c)))) |
| |
| Theorem | oadistb 1020 |
Distributive law derived from OAL.
|
| d
≤ (a →2 b)
& e ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
⇒ (d ∩
(e ∪ ((a →2 b) ∩ (a
→2 c)))) = ((d ∩ e)
∪ (d ∩ ((a →2 b) ∩ (a
→2 c)))) |
| |
| Theorem | oadistc0 1021 |
Pre-distributive law.
|
| d
≤ ((a →2 b) ∩ (a
→2 c))
& ((a →2
c) ∩ ((a →2 b) ∩ ((b
∪ c)⊥ ∪ d))) ≤ (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ d)
⇒ ((a →2
b) ∩ ((b ∪ c)⊥ ∪ d)) = (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ d) |
| |
| Theorem | oadistc 1022 |
Distributive law.
|
| d
≤ ((a →2 b) ∩ (a
→2 c))
& ((a →2
b) ∩ ((b ∪ c)⊥ ∪ d)) ≤ (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ d)
⇒ ((a →2
b) ∩ ((b ∪ c)⊥ ∪ d)) = (((a
→2 b) ∩ (b ∪ c)⊥ ) ∪ ((a →2 b) ∩ d)) |
| |
| Theorem | oadistd 1023 |
OA distributive law.
|
| d
≤ (a →2 b)
& e ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
& f ≤ ((b ∪ c)
→0 ((a →2
b) ∩ (a →2 c)))
& (d ∩ (a →2 c)) ≤ f
⇒ (d ∩
(e ∪ f)) = ((d ∩
e) ∪ (d ∩ f)) |
| |
| Theorem | 3oa2 1024 |
Alternate form for the 3-variable orthoarguesion law.
|
| ((a →1 c) ∩ (((a
→1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))) ≤ (b
→1 c) |
| |
| Theorem | 3oa3 1025 |
3-variable orthoarguesion law expressed with the 3OA identity
abbreviation.
|
| ((a →1 c) ∩ (a
≡ c ≡OA b)) ≤ (b
→1 c) |
| |
| 4-variable orthoarguesian law |
| |
| Axiom | ax-oal4 1026 |
Orthoarguesian law (4-variable version).
|
| a
≤ b⊥
& c ≤ d⊥
⇒ ((a ∪
b) ∩ (c ∪ d))
≤ (b ∪ (a ∩ (c
∪ ((a ∪ c) ∩ (b
∪ d))))) |
| |
| Theorem | oa4cl 1027 |
4-variable OA closed equational form)
|
| ((a ∪ (b
∩ a⊥ )) ∩
(c ∪ (d ∩ c⊥ ))) ≤ ((b ∩ a⊥ ) ∪ (a ∩ (c
∪ ((a ∪ c) ∩ ((b
∩ a⊥ ) ∪
(d ∩ c⊥ )))))) |
| |
| Theorem | oa43v 1028 |
Derivation of 3-variable OA from 4-variable OA.
|
| ((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) ≤ (a →2 c) |
| |
| 6-variable orthoarguesian law |
| |
| Axiom | ax-oa6 1029 |
Orthoarguesian law (6-variable version).
|
| a
≤ b⊥
& c ≤ d⊥
& e ≤ f⊥
⇒ (((a ∪
b) ∩ (c ∪ d))
∩ (e ∪ f)) ≤ (b
∪ (a ∩ (c ∪ (((a
∪ c) ∩ (b ∪ d))
∩ (((a ∪ e) ∩ (b
∪ f)) ∪ ((c ∪ e)
∩ (d ∪ f))))))) |
| |
| Theorem | oa64v 1030 |
Derivation of 4-variable OA from 6-variable OA.
|
| a
≤ b⊥
& c ≤ d⊥
⇒ ((a ∪
b) ∩ (c ∪ d))
≤ (b ∪ (a ∩ (c
∪ ((a ∪ c) ∩ (b
∪ d))))) |
| |
| Theorem | oa63v 1031 |
Derivation of 3-variable OA from 6-variable OA.
|
| ((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) ≤ (a →2 c) |
| |
| The
proper 4-variable orthoarguesian law |
| |
| Axiom | ax-4oa 1032 |
The proper 4-variable OA law.
|
| ((a →1 d) ∩ (((a
∩ b) ∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c)
∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))) ≤ (b →1 d) |
| |
| Theorem | axoa4 1033 |
The proper 4-variable OA law.
|
| (a⊥ ∩ (a ∪ (b
∩ (((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) ∪ (((a
∩ c) ∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))))) ≤ d |
| |
| Theorem | axoa4b 1034 |
Proper 4-variable OA law variant.
|
| ((a →1 d) ∩ (a
∪ (b ∩ (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c)
∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))))) ≤ d |
| |
| Theorem | oa6 1035 |
Derivation of 6-variable orthoarguesian law from 4-variable
version.
|
| a
≤ b⊥
& c ≤ d⊥
& e ≤ f⊥
⇒ (((a ∪
b) ∩ (c ∪ d))
∩ (e ∪ f)) ≤ (b
∪ (a ∩ (c ∪ (((a
∪ c) ∩ (b ∪ d))
∩ (((a ∪ e) ∩ (b
∪ f)) ∪ ((c ∪ e)
∩ (d ∪ f))))))) |
| |
| Theorem | axoa4a 1036 |
Proper 4-variable OA law variant.
|
| ((a →1 d) ∩ (a
∪ (b ∩ (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ (((a ∩ c)
∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))))) ≤
(((a ∩ d) ∪ (b
∩ d)) ∪ (c ∩ d)) |
| |
| Theorem | axoa4d 1037 |
Proper 4-variable OA law variant.
|
| (a
∩ (((a ∩ b) ∪ ((a
→1 d) ∩ (b →1 d))) ∪ (((a
∩ c) ∪ ((a →1 d) ∩ (c
→1 d))) ∩ ((b ∩ c)
∪ ((b →1 d) ∩ (c
→1 d)))))) ≤ (b⊥ →1 d) |
| |
| Theorem | 4oa 1038 |
Variant of proper 4-OA.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
⇒ ((a →1
d) ∩ f) ≤ (b
→1 d) |
| |
| Theorem | 4oaiii 1039 |
Proper OA analog to Godowski/Greechie, Eq. III.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
⇒ ((a →1
d) ∩ f) = ((b
→1 d) ∩ f) |
| |
| Theorem | 4oath1 1040 |
Proper 4-OA theorem.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
⇒ ((a →1
d) ∩ f) = ((a
→1 d) ∩ (b →1 d)) |
| |
| Theorem | 4oagen1 1041 |
"Generalized" 4-OA.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& g ≤ f
⇒ ((a →1
d) ∩ (g ∪ ((a
→1 d) ∩ (b →1 d)))) = ((a
→1 d) ∩ (b →1 d)) |
| |
| Theorem | 4oagen1b 1042 |
"Generalized" OA.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& g ≤ f & h ≤ (a
→1 d)
⇒ (h ∩
(g ∪ ((a →1 d) ∩ (b
→1 d)))) = (h ∩ (b
→1 d)) |
| |
| Theorem | 4oadist 1043 |
OA Distributive law. This is equivalent to the 6-variable OA
law, as shown by theorem d6oa 997.
|
| e
= (((a ∩ c) ∪ ((a
→1 d) ∩ (c →1 d))) ∩ ((b
∩ c) ∪ ((b →1 d) ∩ (c
→1 d))))
& f = (((a ∩ b)
∪ ((a →1 d) ∩ (b
→1 d))) ∪ e)
& h ≤ (a →1 d)
& j ≤ f & k ≤ f
& (h ∩ (b →1 d)) ≤ k
⇒ (h ∩
(j ∪ k)) = ((h ∩
j) ∪ (h ∩ k)) |
| |
| Other stronger-than-OML laws |
| |
| New
state-related equation |
| |
| Axiom | ax-newstateeq 1044 |
New equation that holds in Hilbert space, discovered by Pavicic and Megill
(unpublished).
|
| (((a →1 b) →1 (c →1 b)) ∩ ((a
→1 c) ∩ (b →1 a))) ≤ (c
→1 a) |
| |
| Contributions of Roy Longton |
| |
| Roy's
first section |
| |
| Theorem | lem3.3.2 1045 |
Equation 3.2 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| a
= 1 & (a →0 b) = 1
⇒ b = 1 |
| |
| Definition | df-id5 1046 |
Define asymmetrical identity (for "Non-Orthomodular Models..."
paper).
|
| (a
≡5 b) = ((a ∩ b)
∪ (a⊥ ∩ b⊥ )) |
| |
| Definition | df-b1 1047 |
Define biconditional for →1 .
|
| (a
↔1 b) = ((a →1 b) ∩ (b
→1 a)) |
| |
| Theorem | lem3.3.3lem1 1048 |
Lemma for lem3.3.3 1051.
|
| |
| Theorem | lem3.3.3lem2 1049 |
Lemma for lem3.3.3 1051.
|
| |
| Theorem | lem3.3.3lem3 1050 |
Lemma for lem3.3.3 1051.
|
| |
| Theorem | lem3.3.3 1051 |
Equation 3.3 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| ((a ≡5 b) →0 (a ↔1 b)) = 1 |
| |
| Theorem | lem3.3.4 1052 |
Equation 3.4 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (b
→2 a) =
1 ⇒ (a →2 (a ≡5 b)) = (a
≡5 b) |
| |
| Theorem | lem3.3.5lem 1053 |
A fundamental property in quantum logic. Lemma for lem3.3.5 1054.
|
| 1 ≤ a
⇒ a = 1 |
| |
| Theorem | lem3.3.5 1054 |
Equation 3.5 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡5 b) =
1 ⇒ (a →1 (b ∪ c)) =
1 |
| |
| Theorem | lem3.3.6 1055 |
Equation 3.6 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→2 (b ∪ c)) = ((a ∪
c) →2 (b ∪ c)) |
| |
| Theorem | lem3.3.7i0e1 1056 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
0, and this is the first part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→0 (a ∩ b)) = (a
≡0 (a ∩ b)) |
| |
| Theorem | lem3.3.7i0e2 1057 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
0, and this is the second part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡0 (a ∩ b)) = ((a ∩
b) ≡0 a) |
| |
| Theorem | lem3.3.7i0e3 1058 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
0, and this is the third part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→0 (a ∩ b)) = (a
→1 b) |
| |
| Theorem | lem3.3.7i1e1 1059 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
1, and this is the first part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→1 (a ∩ b)) = (a
≡1 (a ∩ b)) |
| |
| Theorem | lem3.3.7i1e2 1060 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
1, and this is the second part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡1 (a ∩ b)) = ((a ∩
b) ≡1 a) |
| |
| Theorem | lem3.3.7i1e3 1061 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
1, and this is the third part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→1 (a ∩ b)) = (a
→1 b) |
| |
| Theorem | lem3.3.7i2e1 1062 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
2, and this is the first part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→2 (a ∩ b)) = (a
≡2 (a ∩ b)) |
| |
| Theorem | lem3.3.7i2e2 1063 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
2, and this is the second part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡2 (a ∩ b)) = ((a ∩
b) ≡2 a) |
| |
| Theorem | lem3.3.7i2e3 1064 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
2, and this is the third part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→2 (a ∩ b)) = (a
→1 b) |
| |
| Theorem | lem3.3.7i3e1 1065 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
3, and this is the first part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→3 (a ∩ b)) = (a
≡3 (a ∩ b)) |
| |
| Theorem | lem3.3.7i3e2 1066 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
3, and this is the second part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡3 (a ∩ b)) = ((a ∩
b) ≡3 a) |
| |
| Theorem | lem3.3.7i3e3 1067 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
3, and this is the third part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→3 (a ∩ b)) = (a
→1 b) |
| |
| Theorem | lem3.3.7i4e1 1068 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
4, and this is the first part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→4 (a ∩ b)) = (a
≡4 (a ∩ b)) |
| |
| Theorem | lem3.3.7i4e2 1069 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
4, and this is the second part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡4 (a ∩ b)) = ((a ∩
b) ≡4 a) |
| |
| Theorem | lem3.3.7i4e3 1070 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
4, and this is the third part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→4 (a ∩ b)) = (a
→1 b) |
| |
| Theorem | lem3.3.7i5e1 1071 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
5, and this is the first part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→5 (a ∩ b)) = (a
≡5 (a ∩ b)) |
| |
| Theorem | lem3.3.7i5e2 1072 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
5, and this is the second part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡5 (a ∩ b)) = ((a ∩
b) ≡5 a) |
| |
| Theorem | lem3.3.7i5e3 1073 |
Equation 3.7 of [PavMeg1999] p. 9. The
variable i in the paper is set to
5, and this is the third part of the equation. (Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→5 (a ∩ b)) = (a
→1 b) |
| |
| Roy's
second section |
| |
| Theorem | lem3.4.1 1074 |
Equation 3.9 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| ((a →1 b) →0 (a →2 b)) = 1 |
| |
| Theorem | lem3.4.3 1075 |
Equation 3.11 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→2 b) =
1 ⇒ (a →2 (a ≡5 b)) = 1 |
| |
| Theorem | lem3.4.4 1076 |
Equation 3.12 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
→2 b) =
1 & (b →2 a) = 1
⇒ (a ≡5
b) = 1 |
| |
| Theorem | lem3.4.5 1077 |
Equation 3.13 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡5 b) =
1 ⇒ (a →2 (b ∪ c)) =
1 |
| |
| Theorem | lem3.4.6 1078 |
Equation 3.14 of [PavMeg1999] p. 9.
(Contributed by Roy F.
Longton, 3-Jul-05.)
|
| (a
≡5 b) =
1 ⇒ ((a ∪ c)
≡5 (b ∪ c)) = 1 |
| |
| Roy's
third section |
| |
| Theorem | lem4.6.2e1 1079 |
Equation 4.10 of [MegPav2000] p. 23. This
is the first part of the
equation. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →1 b) ∩ (a⊥ →1 b)) = ((a
→1 b) ∩ b) |
| |
| Theorem | lem4.6.2e2 1080 |
Equation 4.10 of [MegPav2000] p. 23. This
is the second part of the
equation. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →1 b) ∩ b) =
((a ∩ b) ∪ (a⊥ ∩ b)) |
| |
| Theorem | lem4.6.3le1 1081 |
Equation 4.11 of [MegPav2000] p. 23. This
is the first part of the
equation. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| (a⊥ →1 b)⊥ ≤ a⊥ |
| |
| Theorem | lem4.6.3le2 1082 |
Equation 4.11 of [MegPav2000] p. 23. This
is the second part of the
equation. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| a⊥ ≤ (a →1 b) |
| |
| Theorem | lem4.6.4 1083 |
Equation 4.12 of [MegPav2000] p. 23.
(Contributed by Roy F. Longton,
3-Jul-05.)
|
| ((a →1 b) →1 b) = (a⊥ →1 b) |
| |
| Theorem | lem4.6.5 1084 |
Equation 4.13 of [MegPav2000] p. 23.
(Contributed by Roy F. Longton,
3-Jul-05.)
|
| ((a →1 b)⊥ →1 b) = (a
→1 b) |
| |
| Theorem | lem4.6.6i0j1 1085 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 0, and j is set to 1. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →0 b) ∪ (a
→1 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i0j2 1086 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 0, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →0 b) ∪ (a
→2 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i0j3 1087 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 0, and j is set to 3. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →0 b) ∪ (a
→3 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i0j4 1088 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 0, and j is set to 4. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →0 b) ∪ (a
→4 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i1j0 1089 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 1, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →1 b) ∪ (a
→0 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i1j2 1090 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 1, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →1 b) ∪ (a
→2 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i1j3 1091 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 1, and j is set to 3. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →1 b) ∪ (a
→3 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i2j0 1092 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 2, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →2 b) ∪ (a
→0 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i2j1 1093 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 2, and j is set to 1. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →2 b) ∪ (a
→1 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i2j4 1094 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 2, and j is set to 4. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →2 b) ∪ (a
→4 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i3j0 1095 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 3, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →3 b) ∪ (a
→0 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i3j1 1096 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 3, and j is set to 1. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →3 b) ∪ (a
→1 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i4j0 1097 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 4, and j is set to 0. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →4 b) ∪ (a
→0 b)) = (a →0 b) |
| |
| Theorem | lem4.6.6i4j2 1098 |
Equation 4.14 of [MegPav2000] p. 23. The
variable i in the paper is set
to 4, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| ((a →4 b) ∪ (a
→2 b)) = (a →0 b) |
| |
| Theorem | com3iia 1099 |
The dual of com3ii 457. (Contributed by Roy F. Longton, 3-Jul-05.)
|
| a C b
⇒ (a ∪
(a⊥ ∩ b)) = (a ∪
b) |
| |
| Theorem | lem4.6.7 1100 |
Equation 4.15 of [MegPav2000] p. 23.
(Contributed by Roy F. Longton,
3-Jul-05.)
|
| a⊥ ≤ b
⇒ b ≤ (a →1 b) |
![[Lattice L46-7]Home Page](l46-7icon.gif){kind=small}
Home