P. 9 of Theorem List - Quantum Logic Explorer

Theorem List for Quantum Logic Explorer - 801-900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	i1abs 801	An absorption law for →1 . (Contributed by NM, 21-Feb-2002.)
((a →1 b)⊥ ∪ (a ∩ b)) = a
Theorem	test 802	Part of an attempt to crack a potential Kalmbach axiom. (Contributed by NM, 29-Dec-1997.)
(((c ∪ (a⊥ ∪ b⊥ )) ∩ (c⊥ ∩ (c ∪ (a ∩ b)))) ∪ ((c⊥ ∩ (a ∩ b)) ∪ (c ∩ (c⊥ ∪ (a ∩ b))))) = ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b)))
Theorem	test2 803	Part of an attempt to crack a potential Kalmbach axiom. (Contributed by NM, 29-Dec-1997.)
(a ∪ b) ≤ ((a ≡ b)⊥ ∪ ((c ∪ (a ∩ b)) ∩ (c⊥ ∪ (a ∩ b))))
0.3.9  Some 3-variable theorems
Theorem	3vth1 804	A 3-variable theorem. Equivalent to OML. (Contributed by NM, 18-Oct-1998.)
((a →2 b) ∩ (b ∪ c)⊥ ) ≤ (a →2 c)
Theorem	3vth2 805	A 3-variable theorem. Equivalent to OML. (Contributed by NM, 18-Oct-1998.)
((a →2 b) ∩ (b ∪ c)⊥ ) = ((a →2 c) ∩ (b ∪ c)⊥ )
Theorem	3vth3 806	A 3-variable theorem. Equivalent to OML. (Contributed by NM, 18-Oct-1998.)
((a →2 c) ∪ ((a →2 b) ∩ (b ∪ c)⊥ )) = (a →2 c)
Theorem	3vth4 807	A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a →2 b)⊥ →2 (b ∪ c)) = ((a →2 c)⊥ →2 (b ∪ c))
Theorem	3vth5 808	A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a →2 b)⊥ →2 (b ∪ c)) = (c ∪ ((a →2 b) ∩ (c →2 b)))
Theorem	3vth6 809	A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a →2 b)⊥ →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
Theorem	3vth7 810	A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
((a →2 b)⊥ →2 (b ∪ c)) = (a →2 (b ∪ c))
Theorem	3vth8 811	A 3-variable theorem. (Contributed by NM, 18-Oct-1998.)
(a →2 (b ∪ c)) = (((a →2 b) ∩ (c →2 b)) ∪ ((a →2 c) ∩ (b →2 c)))
Theorem	3vth9 812	A 3-variable theorem. (Contributed by NM, 16-Nov-1998.)
((a ∪ b) →1 (c →2 b)) = ((b ∪ c) →2 (a →2 b))
Theorem	3vcom 813	3-variable commutation theorem. (Contributed by NM, 19-Mar-1999.)
((a →1 c) ∪ (b →1 c)) C ((a⊥ →1 c) ∩ (b⊥ →1 c))
Theorem	3vded11 814	A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)
b ≤ (c →1 (b →1 a))    ⇒   c ≤ (b →1 a)
Theorem	3vded12 815	A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)
(a ∩ (c →1 a)) ≤ (c →1 (b →1 a))    &   c ≤ a    ⇒   c ≤ (b →1 a)
Theorem	3vded13 816	A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 25-Oct-1998.)
(b ∩ (c →1 a)) ≤ (c →1 (b →1 a))    &   c ≤ a    ⇒   c ≤ (b →1 a)
Theorem	3vded21 817	A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 31-Oct-1998.)
c ≤ ((a →0 b) →0 (c →2 b))    &   c ≤ (a →0 b)    ⇒   c ≤ b
Theorem	3vded22 818	A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 31-Oct-1998.)
c ≤ ( C (a, b) ∪ C (c, b))    &   c ≤ a    &   c ≤ (a →0 b)    ⇒   c ≤ b
Theorem	3vded3 819	A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 24-Jan-1999.)
(c →0 C (a, c)) = 1    &   (c →0 a) = 1    &   (c →0 (a →0 b)) = 1    ⇒   (c →0 b) = 1
Theorem	1oa 820	Orthoarguesian-like law with →1 instead of →0 but true in all OMLs. (Contributed by NM, 1-Nov-1998.)
((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	1oai1 821	Orthoarguesian-like OM law. (Contributed by NM, 30-Dec-1998.)
((a →1 c) ∩ ((a ∩ b)⊥ →1 ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
Theorem	2oai1u 822	Orthoarguesian-like OM law. (Contributed by NM, 28-Feb-1999.)
((a →1 c) ∩ (((a →1 c) ∩ (b →1 c))⊥ →2 ((a⊥ →1 c) ∩ (b⊥ →1 c)))) ≤ (b →1 c)
Theorem	1oaiii 823	OML analog to orthoarguesian law of Godowski/Greechie, Eq. III with →1 instead of →0 . (Contributed by NM, 1-Nov-1998.)
((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) = ((a →2 c) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c))))
Theorem	1oaii 824	OML analog to orthoarguesian law of Godowski/Greechie, Eq. II with →1 instead of →0 . (Contributed by NM, 1-Nov-1998.)
(b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))))) ≤ a⊥
Theorem	2oalem1 825	Lemma for OA-like stuff with →2 instead of →0 . (Contributed by NM, 15-Nov-1998.)
((a →2 b)⊥ ∪ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))) = 1
Theorem	2oath1 826	OA-like theorem with →2 instead of →0 . (Contributed by NM, 15-Nov-1998.)
((a →2 b) ∩ ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))) = ((a →2 b) ∩ (a →2 c))
Theorem	2oath1i1 827	Orthoarguesian-like OM law. (Contributed by NM, 30-Dec-1998.)
((a →1 c) ∩ ((a ∩ b)⊥ →2 ((a →1 c) ∩ (b →1 c)))) = ((a →1 c) ∩ (b →1 c))
Theorem	1oath1i1u 828	Orthoarguesian-like OM law. (Contributed by NM, 28-Feb-1999.)
((a →1 c) ∩ (((a →1 c) ∩ (b →1 c))⊥ →1 ((a⊥ →1 c) ∩ (b⊥ →1 c)))) = ((a →1 c) ∩ (b →1 c))
Theorem	oale 829	Relation for studying OA. (Contributed by NM, 18-Nov-1998.)
((a →2 b) ∩ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))⊥ ) ≤ (a →2 c)
Theorem	oaeqv 830	Weakened OA implies OA). (Contributed by NM, 16-Nov-1998.)
((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))    ⇒   ((a →2 b) ∩ ((b ∪ c)⊥ ∪ ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	3vroa 831	OA-like inference rule (requires OM only). (Contributed by NM, 13-Nov-1998.)
((a →2 b) ∩ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))) = 1    ⇒   (a →2 c) = 1
Theorem	mlalem 832	Lemma for Mladen's OML. (Contributed by NM, 4-Nov-1998.)
((a ≡ b) ∩ (b →1 c)) ≤ (a →1 c)
Theorem	mlaoml 833	Mladen's OML. (Contributed by NM, 4-Nov-1998.)
((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)
Theorem	eqtr4 834	4-variable transitive law for equivalence. (Contributed by NM, 26-Jun-2003.)
(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (a ≡ d)
Theorem	sac 835	Theorem showing "Sasaki complement" is an operation. (Contributed by NM, 3-Jan-1999.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) = (b⊥ →1 c)
Theorem	sa5 836	Possible axiom for a "Sasaki algebra" for orthoarguesian lattices. (Contributed by NM, 3-Jan-1999.)
(a →1 c) ≤ (b →1 c)    ⇒   (b⊥ →1 c) ≤ ((a⊥ →1 c) ∪ c)
Theorem	salem1 837	Lemma for attempt at Sasaki algebra. (Contributed by NM, 4-Jan-1999.)
(((a⊥ →1 b) ∪ b) →1 b) = (a →2 b)
Theorem	sadm3 838	Weak DeMorgan's law for attempt at Sasaki algebra. (Contributed by NM, 4-Jan-1999.)
(((a⊥ →1 c) ∩ (b⊥ →1 c)) →1 c) ≤ ((a →1 c) ∪ (b →1 c))
Theorem	bi3 839	Chained biconditional. (Contributed by NM, 2-Mar-2000.)
((a ≡ b) ∩ (b ≡ c)) = (((a ∩ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
Theorem	bi4 840	Chained biconditional. (Contributed by NM, 25-Jun-2003.)
(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
Theorem	imp3 841	Implicational product with 3 variables. Theorem 3.20 of "Equations, states, and lattices..." paper. (Contributed by NM, 3-Mar-2000.)
((a →2 b) ∩ (b →1 c)) = ((a⊥ ∩ b⊥ ) ∪ (b ∩ c))
Theorem	orbi 842	Disjunction of biconditionals. (Contributed by NM, 5-Jul-2000.)
((a ≡ c) ∪ (b ≡ c)) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))
Theorem	orbile 843	Disjunction of biconditionals. (Contributed by NM, 5-Jul-2000.)
((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b) →2 c) ∩ (c →1 (a ∪ b)))
Theorem	mlaconj4 844	For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper. (Contributed by NM, 8-Jul-2000.)
((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (d ≡ c)    &   d = (a ∪ b)    &   e = (a ∩ b)    ⇒   ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	mlaconj 845	For 5GO proof of Mladen's conjecture. (Contributed by NM, 20-Jan-2002.)
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ ((((a →1 (a ∩ b)) ∩ ((a ∩ b) →1 ((a ∩ b) ∪ c))) ∩ ((((a ∩ b) ∪ c) →1 c) ∩ (c →1 (a ∪ b)))) ∩ ((a ∪ b) →1 a))
Theorem	mlaconj2 846	For 5GO proof of Mladen's conjecture. Hypothesis is 5GO law consequence. (Contributed by NM, 6-Jul-2000.)
((((a →1 (a ∩ b)) ∩ ((a ∩ b) →1 ((a ∩ b) ∪ c))) ∩ ((((a ∩ b) ∪ c) →1 c) ∩ (c →1 (a ∪ b)))) ∩ ((a ∪ b) →1 a)) ≤ (a ≡ c)    ⇒   ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	i1orni1 847	Complemented antecedent lemma. (Contributed by NM, 6-Aug-2001.)
((a →1 b) ∪ (a⊥ →1 b)) = 1
Theorem	negantlem1 848	Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   a C (b →1 c)
Theorem	negantlem2 849	Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   a ≤ (b⊥ →1 c)
Theorem	negantlem3 850	Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∩ c) ≤ (b⊥ →1 c)
Theorem	negantlem4 851	Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) ≤ (b⊥ →1 c)
Theorem	negant 852	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) = (b⊥ →1 c)
Theorem	negantlem5 853	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∩ c⊥ ) = (b⊥ ∩ c⊥ )
Theorem	negantlem6 854	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a ∩ c⊥ ) = (b ∩ c⊥ )
Theorem	negantlem7 855	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a ∪ c) = (b ∪ c)
Theorem	negantlem8 856	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∪ c) = (b⊥ ∪ c)
Theorem	negant0 857	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →0 c) = (b⊥ →0 c)
Theorem	negant2 858	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →2 c) = (b⊥ →2 c)
Theorem	negantlem9 859	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a →3 c) ≤ (b →3 c)
Theorem	negant3 860	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →3 c) = (b⊥ →3 c)
Theorem	negantlem10 861	Lemma for negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a →4 c) ≤ (b →4 c)
Theorem	negant4 862	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →4 c) = (b⊥ →4 c)
Theorem	negant5 863	Negated antecedent identity. (Contributed by NM, 6-Aug-2001.)
(a →1 c) = (b →1 c)    ⇒   (a⊥ →5 c) = (b⊥ →5 c)
Theorem	neg3antlem1 864	Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
(a →3 c) = (b →3 c)    ⇒   (a ∩ c) ≤ (b →1 c)
Theorem	neg3antlem2 865	Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
(a →3 c) = (b →3 c)    ⇒   a⊥ ≤ (b →1 c)
Theorem	neg3ant1 866	Lemma for negated antecedent identity. (Contributed by NM, 7-Aug-2001.)
(a →3 c) = (b →3 c)    ⇒   (a →1 c) = (b →1 c)
Theorem	elimconslem 867	Lemma for consequent elimination law. (Contributed by NM, 3-Mar-2002.)
(a →1 c) = (b →1 c)    &   (a ∩ c) ≤ (b ∪ c⊥ )    ⇒   a ≤ (b ∪ c⊥ )
Theorem	elimcons 868	Consequent elimination law. (Contributed by NM, 3-Mar-2002.)
(a →1 c) = (b →1 c)    &   (a ∩ c) ≤ (b ∪ c⊥ )    ⇒   a ≤ b
Theorem	elimcons2 869	Consequent elimination law. (Contributed by NM, 12-Mar-2002.)
(a →1 c) = (b →1 c)    &   (a ∩ (c ∩ (b →1 c))) ≤ (b ∪ (c⊥ ∪ (a →1 c)⊥ ))    ⇒   a ≤ b
Theorem	comanblem1 870	Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
((a ≡ c) ∩ (b ≡ c)) = (((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →1 c))
Theorem	comanblem2 871	Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
((a ∩ b) ∩ ((a ≡ c) ∩ (b ≡ c))) = ((a ∩ b) ∩ c)
Theorem	comanb 872	Biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
(a ∩ b) C ((a ≡ c) ∩ (b ≡ c))
Theorem	comanbn 873	Biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
(a⊥ ∩ b⊥ ) C ((a ≡ c) ∩ (b ≡ c))
Theorem	mhlemlem1 874	Lemma for Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   (((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) = (a ∪ c)
Theorem	mhlemlem2 875	Lemma for Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d))) = (b ∪ d)
Theorem	mhlem 876	Lemma 7.1 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	mhlem1 877	Lemma for Marsden-Herman distributive law. (Contributed by NM, 10-Mar-2002.)
a C b    &   c C b    ⇒   ((a ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ c))
Theorem	mhlem2 878	Lemma for Marsden-Herman distributive law. (Contributed by NM, 10-Mar-2002.)
a C c    &   a C d    &   b C c    &   b C d    ⇒   (((a ∪ c) ∩ (c⊥ ∪ b⊥ )) ∩ ((b ∪ d) ∩ (a⊥ ∪ d⊥ ))) = (((a ∩ c⊥ ) ∩ (b ∩ d⊥ )) ∪ ((c ∩ b⊥ ) ∩ (d ∩ a⊥ )))
Theorem	mh 879	Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91. (Contributed by NM, 10-Mar-2002.)
a C c    &   a C d    &   b C c    &   b C d    ⇒   ((a ∪ c) ∩ (b ∪ d)) = (((a ∩ b) ∪ (a ∩ d)) ∪ ((c ∩ b) ∪ (c ∩ d)))
Theorem	marsdenlem1 880	Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a    ⇒   ((a ∪ b) ∩ (a⊥ ∪ d⊥ )) = ((a⊥ ∩ (a ∪ b)) ∪ (d⊥ ∩ (a ∪ b)))
Theorem	marsdenlem2 881	Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a    ⇒   ((c ∪ d) ∩ (b⊥ ∪ c⊥ )) = (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∪ (b⊥ ∩ d))
Theorem	marsdenlem3 882	Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a    ⇒   (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∩ (b ∩ d⊥ )) = 0
Theorem	marsdenlem4 883	Lemma for Marsden-Herman distributive law. (Contributed by NM, 26-Feb-2002.)
a C b    &   b C c    &   c C d    &   d C a    ⇒   (((a⊥ ∩ b) ∪ (a ∩ d⊥ )) ∩ (b⊥ ∩ d)) = 0
Theorem	mh2 884	Marsden-Herman distributive law. Corollary 3.3 of Beran, p. 259. (Contributed by NM, 10-Mar-2002.)
a C b    &   b C c    &   c C d    &   d C a    ⇒   ((a ∪ b) ∩ (c ∪ d)) = (((a ∩ c) ∪ (a ∩ d)) ∪ ((b ∩ c) ∪ (b ∩ d)))
Theorem	mlaconjolem 885	Lemma for OML proof of Mladen's conjecture. (Contributed by NM, 10-Mar-2002.)
((a ≡ c) ∪ (b ≡ c)) ≤ ((c ∩ (a ∪ b)) ∪ (c⊥ ∩ (a⊥ ∪ b⊥ )))
Theorem	mlaconjo 886	OML proof of Mladen's conjecture. (Contributed by NM, 10-Mar-2002.)
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	distid 887	Distributive law for identity. (Contributed by NM, 17-Mar-2002.)
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) = (((a ≡ b) ∩ (a ≡ c)) ∪ ((a ≡ b) ∩ (b ≡ c)))
Theorem	mhcor1 888	Corollary of Marsden-Herman Lemma. (Contributed by NM, 26-Jun-2003.)
((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
Theorem	oago3.29 889	Equation (3.29) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO. (Contributed by NM, 22-Jun-2003.)
((a →1 b) ∩ ((b →2 c) ∩ (c →1 a))) ≤ (a ≡ c)
Theorem	oago3.21x 890	4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO. (Contributed by NM, 26-Jun-2003.)
((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
Theorem	cancellem 891	Lemma for cancellation law eliminating →1 consequent. (Contributed by NM, 21-Feb-2002.)
((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)    ⇒   (d ∪ (a →1 c)) ≤ (d ∪ (b →1 c))
Theorem	cancel 892	Cancellation law eliminating →1 consequent. (Contributed by NM, 21-Feb-2002.)
((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)    ⇒   (d ∪ (a →1 c)) = (d ∪ (b →1 c))
Theorem	kb10iii 893	Exercise 10(iii) of Kalmbach p. 30 (in a rewritten form). (Contributed by NM, 9-Jan-2004.)
b⊥ ≤ (a →1 c)    ⇒   c⊥ ≤ (a →1 b)
Theorem	e2ast2 894	Show that the E*2 derivative on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs. (Contributed by NM, 24-Jun-2006.)
a ≤ b⊥    &   c ≤ d⊥    &   a ≤ c⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ ((b ∪ d) ∪ (a ∪ c)⊥ )
Theorem	e2astlem1 895	Lemma towards a possible proof that E*2 on p. 23 of Mayet, "Equations holding in Hilbert lattices" IJTP 2006, holds in all OMLs. (Contributed by NM, 25-Jun-2006.)
a ≤ b⊥    &   c ≤ d⊥    &   r ≤ a⊥    &   a ≤ c⊥    &   c ≤ r⊥    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ ((a ∪ c) ∪ r)) = ((a ∪ (b ∩ (c ∪ r))) ∩ (c ∪ (d ∩ (a ∪ r))))
0.3.10  OML lemmas for studying Godowski equations
Theorem	govar 896	Lemma for converting n-variable Godowski equations to 2n-variable equations. (Contributed by NM, 19-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    ⇒   ((a ∪ b) ∩ (a →2 c)) ≤ (b ∪ c)
Theorem	govar2 897	Lemma for converting n-variable to 2n-variable Godowski equations. (Contributed by NM, 19-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    ⇒   (a ∪ b) ≤ (c →2 a)
Theorem	gon2n 898	Lemma for converting n-variable to 2n-variable Godowski equations. (Contributed by NM, 19-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   ((c →2 a) ∩ d) ≤ (a →2 c)    &   e ≤ d    ⇒   ((a ∪ b) ∩ e) ≤ (b ∪ c)
Theorem	go2n4 899	8-variable Godowski equation derived from 4-variable one. The last hypothesis is the 4-variable Godowski equation. (Contributed by NM, 19-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   d ≤ e⊥    &   e ≤ f⊥    &   f ≤ g⊥    &   g ≤ h⊥    &   h ≤ a⊥    &   (((c →2 a) ∩ (a →2 g)) ∩ ((g →2 e) ∩ (e →2 c))) ≤ (a →2 c)    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ ((e ∪ f) ∩ (g ∪ h))) ≤ (b ∪ c)
Theorem	gomaex4 900	Proof of Mayet Example 4 from 4-variable Godowski equation. R. Mayet, "Equational bases for some varieties of orthomodular lattices related to states", Algebra Universalis 23 (1986), 167-195. (Contributed by NM, 19-Nov-1999.)
a ≤ b⊥    &   b ≤ c⊥    &   c ≤ d⊥    &   d ≤ e⊥    &   e ≤ f⊥    &   f ≤ g⊥    &   g ≤ h⊥    &   h ≤ a⊥    &   (((a →2 g) ∩ (g →2 e)) ∩ ((e →2 c) ∩ (c →2 a))) ≤ (g →2 a)    &   (((e →2 c) ∩ (c →2 a)) ∩ ((a →2 g) ∩ (g →2 e))) ≤ (c →2 e)    ⇒   ((((a ∪ b) ∩ (c ∪ d)) ∩ ((e ∪ f) ∩ (g ∪ h))) ∩ ((a ∪ h) →1 (d ∪ e)⊥ )) = 0