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.
((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)