Theorem List for Quantum Logic Explorer - 1001-1100 *Has distinct variable
group(s)
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) |
|
0.5.2 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) |
|
Theorem | oa3moa3 1029 |
4-variable 3OA to 5-variable Mayet's 3OA.
|
a ≤ b⊥
& c
≤ d⊥ & d ≤ e⊥
& e
≤ c⊥ ⇒ ((a ∪ b)
∩ ((c ∪ d) ∪ e))
≤ (a ∪ (((b ∩ (c
∪ ((b ∪ c) ∩ ((a
∪ d) ∪ e)))) ∩ (d
∪ ((b ∪ d) ∩ ((a
∪ c) ∪ e)))) ∩ (e
∪ ((b ∪ e) ∩ ((a
∪ c) ∪ d))))) |
|
0.5.3 6-variable orthoarguesian law
|
|
Axiom | ax-oa6 1030 |
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 1031 |
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 1032 |
Derivation of 3-variable OA from 6-variable OA.
|
((a →2 b) ∩ ((b
∪ c)⊥ ∪
((a →2 b) ∩ (a
→2 c)))) ≤ (a →2 c) |
|
0.5.4 The proper 4-variable orthoarguesian
law
|
|
Axiom | ax-4oa 1033 |
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 1034 |
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 1035 |
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 1036 |
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 1037 |
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 1038 |
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 1039 |
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 1040 |
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 1041 |
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 1042 |
"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 1043 |
"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 1044 |
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)) |
|
0.6 Other stronger-than-OML
laws
|
|
0.6.1 New state-related equation
|
|
Axiom | ax-newstateeq 1045 |
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) |
|
0.7 Contributions of Roy
Longton
|
|
0.7.1 Roy's first section
|
|
Theorem | lem3.3.2 1046 |
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 1047 |
Define asymmetrical identity (for "Non-Orthomodular Models..."
paper).
|
(a ≡5 b) = ((a ∩
b) ∪ (a⊥ ∩ b⊥ )) |
|
Definition | df-b1 1048 |
Define biconditional for →1 .
|
(a ↔1 b) = ((a
→1 b) ∩ (b →1 a)) |
|
Theorem | lem3.3.3lem1 1049 |
Lemma for lem3.3.3 1052.
|
(a ≡5 b) ≤ (a
→1 b) |
|
Theorem | lem3.3.3lem2 1050 |
Lemma for lem3.3.3 1052.
|
(a ≡5 b) ≤ (b
→1 a) |
|
Theorem | lem3.3.3lem3 1051 |
Lemma for lem3.3.3 1052.
|
(a ≡5 b) ≤ ((a
→1 b) ∩ (b →1 a)) |
|
Theorem | lem3.3.3 1052 |
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 1053 |
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 1054 |
A fundamental property in quantum logic. Lemma for lem3.3.5 1055.
|
1 ≤ a ⇒ a = 1 |
|
Theorem | lem3.3.5 1055 |
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 1056 |
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 1057 |
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 1058 |
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 1059 |
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 1060 |
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 1061 |
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 1062 |
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 1063 |
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 1064 |
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 1065 |
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 1066 |
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 1067 |
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 1068 |
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 1069 |
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 1070 |
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 1071 |
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 1072 |
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 1073 |
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 1074 |
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) |
|
0.7.2 Roy's second section
|
|
Theorem | lem3.4.1 1075 |
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 1076 |
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 1077 |
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 1078 |
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 1079 |
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 |
|
0.7.3 Roy's third section
|
|
Theorem | lem4.6.2e1 1080 |
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 1081 |
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 1082 |
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 1083 |
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 1084 |
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 1085 |
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 1086 |
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 1087 |
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 1088 |
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 1089 |
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 1090 |
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 1091 |
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 1092 |
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 1093 |
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 1094 |
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 1095 |
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 1096 |
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 1097 |
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 1098 |
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 1099 |
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 1100 |
The dual of com3ii 457. (Contributed by Roy F. Longton, 3-Jul-05.)
|
a C b ⇒ (a ∪ (a⊥ ∩ b)) = (a ∪
b) |