Quantum Logic Explorer - mmtheorems9

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 - 801-900 - Page 9 of 11

Type	Label	Description
Statement
Theorem	3vded3 801	A 3-variable theorem. Experiment with weak deduction theorem.
(c →0 C (a, c)) = 1    &   (c →0 a) = 1    &   (c →0 (a →0 b)) = 1    ⇒   (c →0 b) = 1
Theorem	1oa 802	Orthoarguesian-like law with →1 instead of →0 but true in all OMLs.
((a →2 b) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))) ≤ (a →2 c)
Theorem	1oai1 803	Orthoarguesian-like OM law.
((a →1 c) ∩ ((a ∩ b)⊥ →1 ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
Theorem	2oai1u 804	Orthoarguesian-like OM law.
((a →1 c) ∩ (((a →1 c) ∩ (b →1 c))⊥ →2 ((a⊥ →1 c) ∩ (b⊥ →1 c)))) ≤ (b →1 c)
Theorem	1oaiii 805	OML analog to orthoarguesian law of Godowski/Greechie, Eq. III with →1 instead of →0 .
((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 806	OML analog to orthoarguesian law of Godowski/Greechie, Eq. II with →1 instead of →0 .
(b⊥ ∩ ((a →2 b) ∪ ((a →2 c) ∩ ((b ∪ c) →1 ((a →2 b) ∩ (a →2 c)))))) ≤ a⊥
Theorem	2oalem1 807	Lemma for OA-like stuff with →2 instead of →0 .
((a →2 b)⊥ ∪ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))) = 1
Theorem	2oath1 808	OA-like theorem with →2 instead of →0 .
((a →2 b) ∩ ((b ∪ c) →2 ((a →2 b) ∩ (a →2 c)))) = ((a →2 b) ∩ (a →2 c))
Theorem	2oath1i1 809	Orthoarguesian-like OM law.
((a →1 c) ∩ ((a ∩ b)⊥ →2 ((a →1 c) ∩ (b →1 c)))) = ((a →1 c) ∩ (b →1 c))
Theorem	1oath1i1u 810	Orthoarguesian-like OM law.
((a →1 c) ∩ (((a →1 c) ∩ (b →1 c))⊥ →1 ((a⊥ →1 c) ∩ (b⊥ →1 c)))) = ((a →1 c) ∩ (b →1 c))
Theorem	oale 811	Relation for studying OA.
((a →2 b) ∩ ((b ∪ c) ∪ ((a →2 b) ∩ (a →2 c)))⊥ ) ≤ (a →2 c)
Theorem	oaeqv 812	Weakened OA implies OA).
((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 813	OA-like inference rule (requires OM only).
((a →2 b) ∩ ((b ∪ c) →0 ((a →2 b) ∩ (a →2 c)))) = 1    ⇒   (a →2 c) = 1
Theorem	mlalem 814	Lemma for Mladen's OML.
((a ≡ b) ∩ (b →1 c)) ≤ (a →1 c)
Theorem	mlaoml 815	Mladen's OML.
((a ≡ b) ∩ (b ≡ c)) ≤ (a ≡ c)
Theorem	eqtr4 816	4-variable transitive law for equivalence.
(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) ≤ (a ≡ d)
Theorem	sac 817	Theorem showing "Sasaki complement" is an operation.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) = (b⊥ →1 c)
Theorem	sa5 818	Possible axiom for a "Sasaki algebra" for orthoarguesian lattices.
(a →1 c) ≤ (b →1 c)    ⇒   (b⊥ →1 c) ≤ ((a⊥ →1 c) ∪ c)
Theorem	salem1 819	Lemma for attempt at Sasaki algebra.
(((a⊥ →1 b) ∪ b) →1 b) = (a →2 b)
Theorem	sadm3 820	Weak DeMorgan's law for attempt at Sasaki algebra.
(((a⊥ →1 c) ∩ (b⊥ →1 c)) →1 c) ≤ ((a →1 c) ∪ (b →1 c))
Theorem	bi3 821	Chained biconditional.
((a ≡ b) ∩ (b ≡ c)) = (((a ∩ b) ∩ c) ∪ ((a⊥ ∩ b⊥ ) ∩ c⊥ ))
Theorem	bi4 822	Chained biconditional.
(((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d)) = ((((a ∩ b) ∩ c) ∩ d) ∪ (((a⊥ ∩ b⊥ ) ∩ c⊥ ) ∩ d⊥ ))
Theorem	imp3 823	Implicational product with 3 variables. Theorem 3.20 of "Equations, states, and lattices..." paper.
((a →2 b) ∩ (b →1 c)) = ((a⊥ ∩ b⊥ ) ∪ (b ∩ c))
Theorem	orbi 824	Disjunction of biconditionals.
((a ≡ c) ∪ (b ≡ c)) = (((a →2 c) ∪ (b →2 c)) ∩ ((c →1 a) ∪ (c →1 b)))
Theorem	orbile 825	Disjunction of biconditionals.
((a ≡ c) ∪ (b ≡ c)) ≤ (((a ∩ b) →2 c) ∩ (c →1 (a ∪ b)))
Theorem	mlaconj4 826	For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper.
((d ≡ e) ∩ ((e⊥ ∩ c⊥ ) ∪ (d ∩ c))) ≤ (d ≡ c)    &   d = (a ∪ b)    &   e = (a ∩ b)    ⇒   ((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	mlaconj 827	For 5GO proof of Mladen's conjecture.
((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 828	For 5GO proof of Mladen's conjecture. Hypothesis is 5GO law consequence.
((((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 829	Complemented antecedent lemma.
((a →1 b) ∪ (a⊥ →1 b)) = 1
Theorem	negantlem1 830	Lemma for negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   a C (b →1 c)
Theorem	negantlem2 831	Lemma for negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   a ≤ (b⊥ →1 c)
Theorem	negantlem3 832	Lemma for negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∩ c) ≤ (b⊥ →1 c)
Theorem	negantlem4 833	Lemma for negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) ≤ (b⊥ →1 c)
Theorem	negant 834	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →1 c) = (b⊥ →1 c)
Theorem	negantlem5 835	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∩ c⊥ ) = (b⊥ ∩ c⊥ )
Theorem	negantlem6 836	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a ∩ c⊥ ) = (b ∩ c⊥ )
Theorem	negantlem7 837	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a ∪ c) = (b ∪ c)
Theorem	negantlem8 838	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ ∪ c) = (b⊥ ∪ c)
Theorem	negant0 839	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →0 c) = (b⊥ →0 c)
Theorem	negant2 840	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →2 c) = (b⊥ →2 c)
Theorem	negantlem9 841	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a →3 c) ≤ (b →3 c)
Theorem	negant3 842	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →3 c) = (b⊥ →3 c)
Theorem	negantlem10 843	Lemma for negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a →4 c) ≤ (b →4 c)
Theorem	negant4 844	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →4 c) = (b⊥ →4 c)
Theorem	negant5 845	Negated antecedent identity.
(a →1 c) = (b →1 c)    ⇒   (a⊥ →5 c) = (b⊥ →5 c)
Theorem	neg3antlem1 846	Lemma for negated antecedent identity.
(a →3 c) = (b →3 c)    ⇒   (a ∩ c) ≤ (b →1 c)
Theorem	neg3antlem2 847	Lemma for negated antecedent identity.
(a →3 c) = (b →3 c)    ⇒   a⊥ ≤ (b →1 c)
Theorem	neg3ant1 848	Lemma for negated antecedent identity.
(a →3 c) = (b →3 c)    ⇒   (a →1 c) = (b →1 c)
Theorem	elimconslem 849	Lemma for consequent elimination law.
(a →1 c) = (b →1 c)    &   (a ∩ c) ≤ (b ∪ c⊥ )    ⇒   a ≤ (b ∪ c⊥ )
Theorem	elimcons 850	Consequent elimination law.
(a →1 c) = (b →1 c)    &   (a ∩ c) ≤ (b ∪ c⊥ )    ⇒   a ≤ b
Theorem	elimcons2 851	Consequent elimination law.
(a →1 c) = (b →1 c)    &   (a ∩ (c ∩ (b →1 c))) ≤ (b ∪ (c⊥ ∪ (a →1 c)⊥ ))    ⇒   a ≤ b
Theorem	comanblem1 852	Lemma for biconditional commutation law.
((a ≡ c) ∩ (b ≡ c)) = (((a ∪ c)⊥ ∪ ((a ∩ b) ∩ c)) ∩ (b →1 c))
Theorem	comanblem2 853	Lemma for biconditional commutation law.
((a ∩ b) ∩ ((a ≡ c) ∩ (b ≡ c))) = ((a ∩ b) ∩ c)
Theorem	comanb 854	Biconditional commutation law.
(a ∩ b) C ((a ≡ c) ∩ (b ≡ c))
Theorem	comanbn 855	Biconditional commutation law.
(a⊥ ∩ b⊥ ) C ((a ≡ c) ∩ (b ≡ c))
Theorem	mhlemlem1 856	Lemma for Lemma 7.1 of Kalmbach, p. 91.
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   (((a ∪ b) ∪ c) ∩ (a ∪ (c ∪ d))) = (a ∪ c)
Theorem	mhlemlem2 857	Lemma for Lemma 7.1 of Kalmbach, p. 91.
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   (((a ∪ b) ∪ d) ∩ (b ∪ (c ∪ d))) = (b ∪ d)
Theorem	mhlem 858	Lemma 7.1 of Kalmbach, p. 91.
(a ∪ b) ≤ (c ∪ d)⊥    ⇒   ((a ∪ c) ∩ (b ∪ d)) = ((a ∩ b) ∪ (c ∩ d))
Theorem	mhlem1 859	Lemma for Marsden-Herman distributive law.
a C b    &   c C b    ⇒   ((a ∪ b) ∩ (b⊥ ∪ c)) = ((a ∩ b⊥ ) ∪ (b ∩ c))
Theorem	mhlem2 860	Lemma for Marsden-Herman distributive law.
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 861	Marsden-Herman distributive law. Lemma 7.2 of Kalmbach, p. 91.
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 862	Lemma for Marsden-Herman distributive law.
a C b    &   b C c    &   c C d    &   d C a    ⇒   ((a ∪ b) ∩ (a⊥ ∪ d⊥ )) = ((a⊥ ∩ (a ∪ b)) ∪ (d⊥ ∩ (a ∪ b)))
Theorem	marsdenlem2 863	Lemma for Marsden-Herman distributive law.
a C b    &   b C c    &   c C d    &   d C a    ⇒   ((c ∪ d) ∩ (b⊥ ∪ c⊥ )) = (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∪ (b⊥ ∩ d))
Theorem	marsdenlem3 864	Lemma for Marsden-Herman distributive law.
a C b    &   b C c    &   c C d    &   d C a    ⇒   (((b⊥ ∩ c) ∪ (c⊥ ∩ d)) ∩ (b ∩ d⊥ )) = 0
Theorem	marsdenlem4 865	Lemma for Marsden-Herman distributive law.
a C b    &   b C c    &   c C d    &   d C a    ⇒   (((a⊥ ∩ b) ∪ (a ∩ d⊥ )) ∩ (b⊥ ∩ d)) = 0
Theorem	mh2 866	Marsden-Herman distributive law. Corollary 3.3 of Beran, p. 259.
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 867	Lemma for OML proof of Mladen's conjecture,
((a ≡ c) ∪ (b ≡ c)) ≤ ((c ∩ (a ∪ b)) ∪ (c⊥ ∩ (a⊥ ∪ b⊥ )))
Theorem	mlaconjo 868	OML proof of Mladen's conjecture.
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) ≤ (a ≡ c)
Theorem	distid 869	Distributive law for identity.
((a ≡ b) ∩ ((a ≡ c) ∪ (b ≡ c))) = (((a ≡ b) ∩ (a ≡ c)) ∪ ((a ≡ b) ∩ (b ≡ c)))
Theorem	mhcor1 870	Corollary of Marsden-Herman Lemma.
((((a →1 b) ∩ (b →2 c)) ∩ (c →1 d)) ∩ (d →2 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
Theorem	oago3.29 871	Equation (3.29) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO.
((a →1 b) ∩ ((b →2 c) ∩ (c →1 a))) ≤ (a ≡ c)
Theorem	oago3.21x 872	4-variable extension of Equation (3.21) of "Equations, states, and lattices..." paper. This shows that it holds in all OMLs, not just 4GO.
((((a →5 b) ∩ (b →5 c)) ∩ (c →5 d)) ∩ (d →5 a)) = (((a ≡ b) ∩ (b ≡ c)) ∩ (c ≡ d))
Theorem	cancellem 873	Lemma for cancellation law eliminating →1 consequent.
((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)    ⇒   (d ∪ (a →1 c)) ≤ (d ∪ (b →1 c))
Theorem	cancel 874	Cancellation law eliminating →1 consequent.
((d ∪ (a →1 c)) →1 c) = ((d ∪ (b →1 c)) →1 c)    ⇒   (d ∪ (a →1 c)) = (d ∪ (b →1 c))
Theorem	kb10iii 875	Exercise 10(iii) of Kalmbach p. 30 (in a rewritten form).
b⊥ ≤ (a →1 c)    ⇒   c⊥ ≤ (a →1 b)
Theorem	govar 876	Lemma for converting n-variable Godowski equations to 2n-variable equations
a ≤ b⊥    &   b ≤ c⊥    ⇒   ((a ∪ b) ∩ (a →2 c)) ≤ (b ∪ c)
Theorem	govar2 877	Lemma for converting n-variable to 2n-variable Godowski equations.
a ≤ b⊥    &   b ≤ c⊥    ⇒   (a ∪ b) ≤ (c →2 a)
Theorem	gon2n 878	Lemma for converting n-variable to 2n-variable Godowski equations.
a ≤ b⊥    &   b ≤ c⊥    &   ((c →2 a) ∩ d) ≤ (a →2 c)    &   e ≤ d    ⇒   ((a ∪ b) ∩ e) ≤ (b ∪ c)
Theorem	go2n4 879	8-variable Godowski equation derived from 4-variable one. The last hypothesis is the 4-variable Godowski equation.
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 880	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.
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
Theorem	go2n6 881	12-variable Godowski equation derived from 6-variable one. The last hypothesis is the 6-variable Godowski equation.
g ≤ h⊥    &   h ≤ i⊥    &   i ≤ j⊥    &   j ≤ k⊥    &   k ≤ m⊥    &   m ≤ n⊥    &   n ≤ u⊥    &   u ≤ w⊥    &   w ≤ x⊥    &   x ≤ y⊥    &   y ≤ z⊥    &   z ≤ g⊥    &   (((i →2 g) ∩ (g →2 y)) ∩ (((y →2 w) ∩ (w →2 n)) ∩ ((n →2 k) ∩ (k →2 i)))) ≤ (g →2 i)    ⇒   (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)
Theorem	gomaex3h1 882	Hypothesis for Godowski 6-var -> Mayet Example 3.
a ≤ b⊥    &   g = a    &   h = b    ⇒   g ≤ h⊥
Theorem	gomaex3h2 883	Hypothesis for Godowski 6-var -> Mayet Example 3.
b ≤ c⊥    &   h = b    &   i = c    ⇒   h ≤ i⊥
Theorem	gomaex3h3 884	Hypothesis for Godowski 6-var -> Mayet Example 3.
i = c    &   j = (c ∪ d)⊥    ⇒   i ≤ j⊥
Theorem	gomaex3h4 885	Hypothesis for Godowski 6-var -> Mayet Example 3.
r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   j = (c ∪ d)⊥    &   k = r    ⇒   j ≤ k⊥
Theorem	gomaex3h5 886	Hypothesis for Godowski 6-var -> Mayet Example 3.
r = ((p⊥ →1 q)⊥ ∩ (c ∪ d))    &   k = r    &   m = (p⊥ →1 q)    ⇒   k ≤ m⊥
Theorem	gomaex3h6 887	Hypothesis for Godowski 6-var -> Mayet Example 3.
m = (p⊥ →1 q)    &   n = (p⊥ →1 q)⊥    ⇒   m ≤ n⊥
Theorem	gomaex3h7 888	Hypothesis for Godowski 6-var -> Mayet Example 3.
n = (p⊥ →1 q)⊥    &   u = (p⊥ ∩ q)    ⇒   n ≤ u⊥
Theorem	gomaex3h8 889	Hypothesis for Godowski 6-var -> Mayet Example 3.
u = (p⊥ ∩ q)    &   w = q⊥    ⇒   u ≤ w⊥
Theorem	gomaex3h9 890	Hypothesis for Godowski 6-var -> Mayet Example 3.
w = q⊥    &   x = q    ⇒   w ≤ x⊥
Theorem	gomaex3h10 891	Hypothesis for Godowski 6-var -> Mayet Example 3.
q = ((e ∪ f) →1 (b ∪ c)⊥ )⊥    &   x = q    &   y = (e ∪ f)⊥    ⇒   x ≤ y⊥
Theorem	gomaex3h11 892	Hypothesis for Godowski 6-var -> Mayet Example 3.
y = (e ∪ f)⊥    &   z = f    ⇒   y ≤ z⊥
Theorem	gomaex3h12 893	Hypothesis for Godowski 6-var -> Mayet Example 3.
f ≤ a⊥    &   g = a    &   z = f    ⇒   z ≤ g⊥
Theorem	gomaex3lem1 894	Lemma for Godowski 6-var -> Mayet Example 3.
c ≤ d⊥    ⇒   (c ∪ (c ∪ d)⊥ ) = d⊥
Theorem	gomaex3lem2 895	Lemma for Godowski 6-var -> Mayet Example 3.
e ≤ f⊥    ⇒   ((e ∪ f)⊥ ∪ f) = e⊥
Theorem	gomaex3lem3 896	Lemma for Godowski 6-var -> Mayet Example 3.
((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q)) = p⊥
Theorem	gomaex3lem4 897	Lemma for Godowski 6-var -> Mayet Example 3.
p = ((a ∪ b) →1 (d ∪ e)⊥ )⊥    ⇒   ((a ∪ b) ∩ (d ∪ e)⊥ ) ≤ p⊥
Theorem	gomaex3lem5 898	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    ⇒   (((g ∪ h) ∩ (i ∪ j)) ∩ (((k ∪ m) ∩ (n ∪ u)) ∩ ((w ∪ x) ∩ (y ∪ z)))) ≤ (h ∪ i)
Theorem	gomaex3lem6 899	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) ∩ (c ∪ (c ∪ d)⊥ )) ∩ (((r ∪ (p⊥ →1 q)) ∩ ((p⊥ →1 q)⊥ ∪ (p⊥ ∩ q))) ∩ ((q⊥ ∪ q) ∩ ((e ∪ f)⊥ ∪ f)))) ≤ (b ∪ c)
Theorem	gomaex3lem7 900	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⊥ ) ∩ (((r ∪ (p⊥ →1 q)) ∩ p⊥ ) ∩ e⊥ )) ≤ (b ∪ c)