P. 11 of Theorem List - Quantum Logic Explorer

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. (Contributed by NM, 22-Sep-1998.)
((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. (Contributed by NM, 22-Sep-1998.)
(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. (Contributed by NM, 25-Nov-1998.)
(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. (Contributed by NM, 12-Oct-1998.)
((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) = ((a →2 b) ∩ (a →2 c))
Theorem	oalem1 1005	Lemma. (Contributed by NM, 16-Oct-1998.)
((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. (Contributed by NM, 16-Oct-1998.)
((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. (Contributed by NM, 17-Nov-1998.)
(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. (Contributed by NM, 17-Nov-1998.)
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. (Contributed by NM, 17-Nov-1998.)
(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. (Contributed by NM, 17-Nov-1998.)
((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. (Contributed by NM, 19-Nov-1998.)
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. (Contributed by NM, 19-Nov-1998.)
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. (Contributed by NM, 19-Nov-1998.)
(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. (Contributed by NM, 19-Nov-1998.)
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. (Contributed by NM, 21-Nov-1998.)
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. (Contributed by NM, 19-Nov-1998.)
d ≤ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))    ⇒   ((a →2 b) ∩ d) ≤ (a →2 c)
Theorem	oagen2b 1017	"Generalized" OA. (Contributed by NM, 21-Nov-1998.)
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. (Contributed by NM, 20-Nov-1998.)
((a ≡ b) ∩ ((b ≡ c) ∪ ((b ∪ (a ≡ b)) ∩ (c ∪ (a ≡ c))))) ≤ (c ∪ (a ≡ c))
Theorem	oadist 1019	Distributive law derived from OAL. (Contributed by NM, 20-Nov-1998.)
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. (Contributed by NM, 20-Nov-1998.)
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. Note that the inference of the second hypothesis from the first may be an OM theorem. (Contributed by NM, 30-Nov-1998.)
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. (Contributed by NM, 21-Nov-1998.)
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. (Contributed by NM, 21-Nov-1998.)
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. (Contributed by NM, 27-May-2004.)
((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. (Contributed by NM, 27-May-2004.)
((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). (Contributed by NM, 1-Dec-1998.)
a ≤ b⊥    &   c ≤ d⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa4cl 1027	4-variable OA closed equational form. (Contributed by NM, 1-Dec-1998.)
((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. (Contributed by NM, 28-Nov-1998.)
((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. (Contributed by NM, 3-Apr-2009.) (Revised by NM, 31-Mar-2011.)
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). (Contributed by NM, 29-Nov-1998.)
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. (Contributed by NM, 29-Nov-1998.)
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. (Contributed by NM, 28-Nov-1998.)
((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. (Contributed by NM, 20-Jul-1999.)
((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. (Contributed by NM, 20-Jul-1999.)
(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. (Contributed by NM, 22-Dec-1998.)
((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. (Contributed by NM, 18-Dec-1998.)
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. (Contributed by NM, 22-Dec-1998.)
((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. (Contributed by NM, 24-Dec-1998.)
(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. (Contributed by NM, 29-Dec-1998.)
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. (Contributed by NM, 29-Dec-1998.)
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. (Contributed by NM, 29-Dec-1998.)
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. (Contributed by NM, 29-Dec-1998.)
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. (Contributed by NM, 29-Dec-1998.)
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. (Contributed by NM, 29-Dec-1998.)
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	This is the simplest known example of an equation implied by the set of Mayet--Godowski equations that is independent from all Godowski equations. It was discovered by Norman Megill and Mladen Pavicic between 1997 and August 2003. This is Equation (54) in Mladen Pavicic, Norman D. Megill, Quantum Logic and Quantum Computation, in Handbook of Quantum Logic and Quantum Structures, Volume Quantum Structures, Elsevier, Amsterdam, 2007, pp. 751--787. https://arxiv.org/abs/0812.3072 and Equation (15) in Mladen Pavicic, Brendan D. McKay, Norman D. Megill, Kresimir Fresl, Graph Approach to Quantum Systems, Journal of Mathematical Physics, Volume 51, Issue 10, October 2010. https://arxiv.org/abs/1004.0776 (Contributed by NM, 1-Jan-1998.)
(((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a)
0.7  Contributions of Roy F. Longton
0.7.1  Roy F. Longton's first section
Theorem	lem3.3.2 1046	Equation 3.2 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
a = 1    &   (a →0 b) = 1    ⇒   b = 1
Definition	df-id5 1047	Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by Roy F. Longton, 27-Jun-2005.)
(a ≡5 b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
Definition	df-b1 1048	Define biconditional for →1 . (Contributed by Roy F. Longton, 27-Jun-2005.)
(a ↔1 b) = ((a →1 b) ∩ (b →1 a))
Theorem	lem3.3.3lem1 1049	Lemma for lem3.3.3 1052. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a ≡5 b) ≤ (a →1 b)
Theorem	lem3.3.3lem2 1050	Lemma for lem3.3.3 1052. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a ≡5 b) ≤ (b →1 a)
Theorem	lem3.3.3lem3 1051	Lemma for lem3.3.3 1052. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
((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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
1 ≤ a    ⇒   a = 1
Theorem	lem3.3.5 1055	Equation 3.5 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a →5 (a ∩ b)) = (a →1 b)
0.7.2  Roy F. Longton's second section
Theorem	lem3.4.1 1075	Equation 3.9 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-2005.)
((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, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(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, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a ≡5 b) = 1    ⇒   ((a ∪ c) ≡5 (b ∪ c)) = 1
Theorem	thm3.8i1lem 1080	Lemma intended for ~ thm3.8i1 . (Contributed by Roy F. Longton, 30-Jun-2005.) (Revised by Roy F. Longton, 31-Mar-2011.)
(a ≡1 b) = ((b →0 a) ∩ (a →1 b))
Theorem	thm3.8i5 1081	(Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 31-Mar-2011.)
(a ≡5 b) = 1    ⇒   ((a ∪ c) ≡5 (b ∪ c)) = 1
0.7.3  Roy F. Longton's third section
Theorem	lem4.6.2e1 1082	Equation 4.10 of [MegPav2000] p. 23. This is the first part of the equation. Note that Lemma 4.6.1 is u1lemaa 600. (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
((a →1 b) ∩ (a⊥ →1 b)) = ((a →1 b) ∩ b)
Theorem	lem4.6.2e2 1083	Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a →1 b) ∩ b) = ((a ∩ b) ∪ (a⊥ ∩ b))
Theorem	lem4.6.3le1 1084	Equation 4.11 of [MegPav2000] p. 23. This is the first part of the equation. (Contributed by Roy F. Longton, 1-Jul-2005.)
(a⊥ →1 b)⊥ ≤ a⊥
Theorem	lem4.6.3le2 1085	Equation 4.11 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 1-Jul-2005.)
a⊥ ≤ (a →1 b)
Theorem	lem4.6.4 1086	Equation 4.12 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a →1 b) →1 b) = (a⊥ →1 b)
Theorem	lem4.6.5 1087	Equation 4.13 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a →1 b)⊥ →1 b) = (a →1 b)
Theorem	lem4.6.6i0j1 1088	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, 1-Jul-2005.)
((a →0 b) ∪ (a →1 b)) = (a →0 b)
Theorem	lem4.6.6i0j2 1089	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, 1-Jul-2005.)
((a →0 b) ∪ (a →2 b)) = (a →0 b)
Theorem	lem4.6.6i0j3 1090	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, 1-Jul-2005.)
((a →0 b) ∪ (a →3 b)) = (a →0 b)
Theorem	lem4.6.6i0j4 1091	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, 1-Jul-2005.)
((a →0 b) ∪ (a →4 b)) = (a →0 b)
Theorem	lem4.6.6i1j0 1092	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, 1-Jul-2005.)
((a →1 b) ∪ (a →0 b)) = (a →0 b)
Theorem	lem4.6.6i1j2 1093	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, 1-Jul-2005.)
((a →1 b) ∪ (a →2 b)) = (a →0 b)
Theorem	lem4.6.6i1j3 1094	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, 1-Jul-2005.)
((a →1 b) ∪ (a →3 b)) = (a →0 b)
Theorem	lem4.6.6i2j0 1095	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, 1-Jul-2005.)
((a →2 b) ∪ (a →0 b)) = (a →0 b)
Theorem	lem4.6.6i2j1 1096	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, 1-Jul-2005.)
((a →2 b) ∪ (a →1 b)) = (a →0 b)
Theorem	lem4.6.6i2j4 1097	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, 1-Jul-2005.)
((a →2 b) ∪ (a →4 b)) = (a →0 b)
Theorem	lem4.6.6i3j0 1098	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, 1-Jul-2005.)
((a →3 b) ∪ (a →0 b)) = (a →0 b)
Theorem	lem4.6.6i3j1 1099	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, 1-Jul-2005.)
((a →3 b) ∪ (a →1 b)) = (a →0 b)
Theorem	lem4.6.6i4j0 1100	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, 2-Jul-2005.)
((a →4 b) ∪ (a →0 b)) = (a →0 b)