Quantum Logic Explorer - mmtheorems10

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1024

Statement List for Quantum Logic Explorer - 901-1000 - Page 10 of 11

Type	Label	Description
Statement
Theorem	gomaex3lem8 901	Lemma for Godowski 6-var -> Mayet Example 3.
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((r ∪ (p⊥ →1 q)) ∩ p⊥ )) ≤ (b ∪ c)
Theorem	gomaex3lem9 902	Lemma for Godowski 6-var -> Mayet Example 3.
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ (r ∪ (p⊥ →1 q))) ≤ (b ∪ c)
Theorem	gomaex3lem10 903	Lemma for Godowski 6-var -> Mayet Example 3.
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   h = b    &   i = c    &   j = (c ∪ d)⊥    &   k = r    &   m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    &   w = q⊥    &   x = q    &   y = (e ∪ f)⊥    &   z = f    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ (r ∪ (p⊥ →1 q))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )
Theorem	gomaex3 904	Proof of Mayet Example 3 from 6-variable Godowski equation. R. Mayet, "Equational bases for some varieties of orthomodular lattices related to states," Algebra Universalis 23 (1986), 167-195.
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   f ≤ a⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    &   p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    &   q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   g = a    &   i = c    &   k = r    &   n = (p⊥ →1 q)⊥    &   w = q⊥    &   y = (e ∪ f)⊥    ⇒   (((a ∪ b) ∩ (d ∪ e)⊥ ) ∩ ((((a ∪ b) →1 (d ∪ e)⊥ ) →1 ((e ∪ f) →1 (b ∪ c)⊥ )⊥ )⊥ →1 (c ∪ d))) ≤ ((b ∪ c) ∪ (e ∪ f)⊥ )
Theorem	oas 905	"Strengthening" lemma for studying the orthoarguesian law.
(a⊥ ∩ (a ∪ b)) ≤ c    ⇒   ((a →1 c) ∩ (a ∪ b)) ≤ c
Theorem	oasr 906	Reverse of oas 905 lemma for studying the orthoarguesian law.
((a →1 c) ∩ (a ∪ b)) ≤ c    ⇒   (a⊥ ∩ (a ∪ b)) ≤ c
Theorem	oat 907	Transformation lemma for studying the orthoarguesian law.
(a⊥ ∩ (a ∪ b)) ≤ c    ⇒   b ≤ (a⊥ →1 c)
Theorem	oatr 908	Reverse transformation lemma for studying the orthoarguesian law.
b ≤ (a⊥ →1 c)    ⇒   (a⊥ ∩ (a ∪ b)) ≤ c
Theorem	oau 909	Transformation lemma for studying the orthoarguesian law.
(a ∩ ((a →1 c) ∪ b)) ≤ c    ⇒   b ≤ (a →1 c)
Theorem	oaur 910	Transformation lemma for studying the orthoarguesian law.
b ≤ (a →1 c)    ⇒   (a ∩ ((a →1 c) ∪ b)) ≤ c
Theorem	oaidlem2 911	Lemma for identity-like OA law.
((d ∪ ((a →1 c) ∩ (b →1 c)))⊥ ∪ ((a →1 c) →1 (b →1 c))) = 1    ⇒   ((a →1 c) ∩ (d ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
Theorem	oaidlem2g 912	Lemma for identity-like OA law (generalized).
((c ∪ (a ∩ b))⊥ ∪ (a →1 b)) = 1    ⇒   (a ∩ (c ∪ (a ∩ b))) ≤ b
Theorem	oa6v4v 913	6-variable OA to 4-variable OA.
(((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))    &   e = 0    &   f = 1    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa4v3v 914	4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV).
d ≤ b⊥    &   e ≤ c⊥    &   ((d ∪ b) ∩ (e ∪ c)) ≤ (b ∪ (d ∩ (e ∪ ((d ∪ e) ∩ (b ∪ c)))))    &   d = (a →2 b)⊥    &   e = (a →2 c)⊥    ⇒   (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ ((b⊥ ∩ (a →2 b)) ∪ (c⊥ ∩ (a →2 c)))
Theorem	oal42 915	Derivation of Godowski/Greechie Eq. II from 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)))    ⇒   (b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))))) ≤ a⊥
Theorem	oa23 916	Derivation of OA from Godowski/Greechie Eq. II.
(c⊥ ∩ ((a →2 c) ∪ ((a →2 b) ∩ ((c ∪ b)⊥ ∪ ((a →2 c) ∩ (a →2 b)))))) ≤ a⊥    ⇒   ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	oa4lem1 917	Lemma for 3-var to 4-var OA.
a ≤ b⊥    &   c ≤ d⊥    ⇒   (a ∪ b) ≤ ((a ∪ c)⊥ →2 b)
Theorem	oa4lem2 918	Lemma for 3-var to 4-var OA.
a ≤ b⊥    &   c ≤ d⊥    ⇒   (c ∪ d) ≤ ((a ∪ c)⊥ →2 d)
Theorem	oa4lem3 919	Lemma for 3-var to 4-var OA.
a ≤ b⊥    &   c ≤ d⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ ((b ∪ d)⊥ ∪ (((a ∪ c)⊥ →2 b) ∩ ((a ∪ c)⊥ →2 d)))
Theorem	distoah1 920	Satisfaction of distributive law hypothesis.
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   d ≤ (a →2 b)
Theorem	distoah2 921	Satisfaction of distributive law hypothesis.
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   e ≤ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))
Theorem	distoah3 922	Satisfaction of distributive law hypothesis.
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   f ≤ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))
Theorem	distoah4 923	Satisfaction of distributive law hypothesis.
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   (d ∩ (a →2 c)) ≤ f
Theorem	distoa 924	Derivation in OM of OA, assuming OA distributive law oadistd 1003.
d = (a →2 b)    &   e = ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))    &   f = ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    &   (d ∩ (e ∪ f)) = ((d ∩ e) ∪ (d ∩ f))    ⇒   ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	oa3to4lem1 925	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    ⇒   b ≤ (a →1 g)
Theorem	oa3to4lem2 926	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    ⇒   d ≤ (c →1 g)
Theorem	oa3to4lem3 927	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    ⇒   (a ∩ (b ∪ (d ∩ ((a ∩ c) ∪ (b ∩ d))))) ≤ (a ∩ ((a →1 g) ∪ ((c →1 g) ∩ ((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))))))
Theorem	oa3to4lem4 928	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   g = ((a ∩ b) ∪ (c ∩ d))    &   (a ∩ ((a →1 g) ∪ ((c →1 g) ∩ ((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g)))))) ≤ ((a ∩ g) ∪ (c ∩ g))    ⇒   (a ∩ (b ∪ (d ∩ ((a ∩ c) ∪ (b ∩ d))))) ≤ g
Theorem	oa3to4lem5 929	Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
((a ∪ b) ∩ (c ∪ d)) ≤ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))    ⇒   ((b ∪ a) ∩ (d ∪ c)) ≤ (a ∪ (b ∩ (d ∪ ((b ∪ d) ∩ (a ∪ c)))))
Theorem	oa3to4lem6 930	Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only.
a ≤ b⊥    &   c ≤ d⊥    &   g = ((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ ))    &   e = a⊥    &   f = c⊥    &   (e ∩ ((e →1 g) ∪ ((f →1 g) ∩ ((e ∩ f) ∪ ((e →1 g) ∩ (f →1 g)))))) ≤ ((e ∩ g) ∪ (f ∩ g))    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (a ∪ (b ∩ (d ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa3to4 931	Orthoarguesian law (Godowski/Greechie 3-variable to 4-variable). The first 2 hypotheses are those for 4-OA. The next 3 are variable substitutions into 3-OA. The last is the 3-OA. The proof uses OM logic only.
a ≤ b⊥    &   c ≤ d⊥    &   g = ((b⊥ ∩ a⊥ ) ∪ (d⊥ ∩ c⊥ ))    &   e = b⊥    &   f = d⊥    &   (e ∩ ((e →1 g) ∪ ((f →1 g) ∩ ((e ∩ f) ∪ ((e →1 g) ∩ (f →1 g)))))) ≤ ((e ∩ g) ∪ (f ∩ g))    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
Theorem	oa6todual 932	Conventional to dual 6-variable OA law.
(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))    ⇒   (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))
Theorem	oa6fromdual 933	Dual to conventional 6-variable OA law.
(b⊥ ∩ (a⊥ ∪ (c⊥ ∩ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ d⊥ )) ∪ (((a⊥ ∩ e⊥ ) ∪ (b⊥ ∩ f⊥ )) ∩ ((c⊥ ∩ e⊥ ) ∪ (d⊥ ∩ f⊥ ))))))) ≤ (((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	oa6fromdualn 934	Dual to conventional 6-variable OA law.
(b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ (((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	oa6to4h1 935	Satisfaction of 6-variable OA law hypothesis.
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    ⇒   a⊥ ≤ b⊥ ⊥
Theorem	oa6to4h2 936	Satisfaction of 6-variable OA law hypothesis.
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    ⇒   c⊥ ≤ d⊥ ⊥
Theorem	oa6to4h3 937	Satisfaction of 6-variable OA law hypothesis.
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    ⇒   e⊥ ≤ f⊥ ⊥
Theorem	oa6to4 938	Derivation of 4-variable proper OA law, assuming 6-variable OA law.
b⊥ = (a →1 g)⊥    &   d⊥ = (c →1 g)⊥    &   f⊥ = (e →1 g)⊥    &   (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ (e⊥ ∪ f⊥ )) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∪ ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )))))))    ⇒   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))
Theorem	oa4b 939	Derivation of 4-OA law variant.
((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ (((a ∩ g) ∪ (c ∩ g)) ∪ (e ∩ g))    ⇒   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g
Theorem	oa4to6lem1 940	Lemma for orthoarguesian law (4-variable to 6-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   b ≤ (a →1 g)
Theorem	oa4to6lem2 941	Lemma for orthoarguesian law (4-variable to 6-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   d ≤ (c →1 g)
Theorem	oa4to6lem3 942	Lemma for orthoarguesian law (4-variable to 6-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   f ≤ (e →1 g)
Theorem	oa4to6lem4 943	Lemma for orthoarguesian law (4-variable to 6-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    ⇒   (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g))))))))
Theorem	oa4to6dual 944	Lemma for orthoarguesian law (4-variable to 6-variable proof).
a⊥ ≤ b    &   c⊥ ≤ d    &   e⊥ ≤ f    &   g = (((a ∩ b) ∪ (c ∩ d)) ∪ (e ∩ f))    &   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g    ⇒   (b ∩ (a ∪ (c ∩ (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ e) ∪ (b ∩ f)) ∩ ((c ∩ e) ∪ (d ∩ f))))))) ≤ g
Theorem	oa4to6 945	Orthoarguesian law (4-variable to 6-variable proof). The first 3 hypotheses are those for 6-OA. The next 4 are variable substitutions into 4-OA. The last is the 4-OA. The proof uses OM logic only.
a ≤ b⊥    &   c ≤ d⊥    &   e ≤ f⊥    &   g = (((a⊥ ∩ b⊥ ) ∪ (c⊥ ∩ d⊥ )) ∪ (e⊥ ∩ f⊥ ))    &   h = a⊥    &   j = c⊥    &   k = e⊥    &   ((h →1 g) ∩ (h ∪ (j ∩ (((h ∩ j) ∪ ((h →1 g) ∩ (j →1 g))) ∪ (((h ∩ k) ∪ ((h →1 g) ∩ (k →1 g))) ∩ ((j ∩ k) ∪ ((j →1 g) ∩ (k →1 g)))))))) ≤ g    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))
Theorem	oa4btoc 946	Derivation of 4-OA law variant.
((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g    ⇒   (a⊥ ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g
Theorem	oa4ctob 947	Derivation of 4-OA law variant.
(a⊥ ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g    ⇒   ((a →1 g) ∩ (a ∪ (c ∩ (((a ∩ c) ∪ ((a →1 g) ∩ (c →1 g))) ∪ (((a ∩ e) ∪ ((a →1 g) ∩ (e →1 g))) ∩ ((c ∩ e) ∪ ((c →1 g) ∩ (e →1 g)))))))) ≤ g
Theorem	oa4ctod 948	Derivation of 4-OA law variant.
(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    ⇒   (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⊥ →1 d)
Theorem	oa4dtoc 949	Derivation of 4-OA law variant.
(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⊥ →1 d)    ⇒   (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	oa4dcom 950	Lemma commuting terms.
(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)))))) = (b ∩ (((b ∩ a) ∪ ((b →1 d) ∩ (a →1 d))) ∪ (((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))) ∩ ((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))))))
Theorem	oa8todual 951	Conventional to dual 8-variable OA law.
(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))    ⇒   (b ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ ((e ∩ f) ∪ (g ∩ h)))
Theorem	oa8to5 952	Orthoarguesian law 5OA converted from 8 to 5 variables.
(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))    &   b⊥ = (a →1 j)⊥    &   d⊥ = (c →1 j)⊥    &   f⊥ = (e →1 j)⊥    &   h⊥ = (g →1 j)⊥    ⇒   ((a →1 j) ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ ((a →1 j) ∩ (c →1 j))) ∪ (((a ∩ g) ∪ ((a →1 j) ∩ (g →1 j))) ∩ ((c ∩ g) ∪ ((c →1 j) ∩ (g →1 j))))) ∪ ((((a ∩ e) ∪ ((a →1 j) ∩ (e →1 j))) ∪ (((a ∩ g) ∪ ((a →1 j) ∩ (g →1 j))) ∩ ((e ∩ g) ∪ ((e →1 j) ∩ (g →1 j))))) ∩ (((c ∩ e) ∪ ((c →1 j) ∩ (e →1 j))) ∪ (((c ∩ g) ∪ ((c →1 j) ∩ (g →1 j))) ∩ ((e ∩ g) ∪ ((e →1 j) ∩ (g →1 j)))))))))) ≤ (((a ∩ j) ∪ (c ∩ j)) ∪ ((e ∩ j) ∪ (g ∩ j)))
Theorem	oa4to4u 953	A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it.
((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))    &   e = (a⊥ →1 d)    &   f = (b⊥ →1 d)    &   g = (c⊥ →1 d)    ⇒   ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d)))
Theorem	oa4to4u2 954	A weaker-looking "universal" proper 4-OA.
((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))    &   e = (a⊥ →1 d)    &   f = (b⊥ →1 d)    &   g = (c⊥ →1 d)    ⇒   ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ d
Theorem	oa4uto4g 955	Derivation of "Godowski/Greechie" 4-variable proper OA law variant from "universal" variant oa4to4u2 954.
((b⊥ →1 d) ∩ ((b⊥ ⊥ →1