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 v b) ->1 (d v e)_|_)_|_   &   q = ((e v f) ->1 (b v c)_|_)_|_   &   r = ((p_|_ ->1 q)_|_ ^ (c v d))   &   g = a   &   h = b   &   i = c   &   j = (c v d)_|_   &   k = r   &   m = (p_|_ ->1 q)   &   n = (p_|_ ->1 q)_|_   &   u = (p_|_ ^ q)   &   w = q_|_   &   x = q   &   y = (e v f)_|_   &   z = f   =>   (((a v b) ^ (d v e)_|_) ^ ((r v (p_|_ ->1 q)) ^ p_|_)) =< (b v 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 v b) ->1 (d v e)_|_)_|_   &   q = ((e v f) ->1 (b v c)_|_)_|_   &   r = ((p_|_ ->1 q)_|_ ^ (c v d))   &   g = a   &   h = b   &   i = c   &   j = (c v d)_|_   &   k = r   &   m = (p_|_ ->1 q)   &   n = (p_|_ ->1 q)_|_   &   u = (p_|_ ^ q)   &   w = q_|_   &   x = q   &   y = (e v f)_|_   &   z = f   =>   (((a v b) ^ (d v e)_|_) ^ (r v (p_|_ ->1 q))) =< (b v 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 v b) ->1 (d v e)_|_)_|_   &   q = ((e v f) ->1 (b v c)_|_)_|_   &   r = ((p_|_ ->1 q)_|_ ^ (c v d))   &   g = a   &   h = b   &   i = c   &   j = (c v d)_|_   &   k = r   &   m = (p_|_ ->1 q)   &   n = (p_|_ ->1 q)_|_   &   u = (p_|_ ^ q)   &   w = q_|_   &   x = q   &   y = (e v f)_|_   &   z = f   =>   (((a v b) ^ (d v e)_|_) ^ (r v (p_|_ ->1 q))) =< ((b v c) v (e v 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 v b) ->1 (d v e)_|_)_|_   &   q = ((e v f) ->1 (b v c)_|_)_|_   &   r = ((p_|_ ->1 q)_|_ ^ (c v d))   &   g = a   &   i = c   &   k = r   &   n = (p_|_ ->1 q)_|_   &   w = q_|_   &   y = (e v f)_|_   =>   (((a v b) ^ (d v e)_|_) ^ ((((a v b) ->1 (d v e)_|_) ->1 ((e v f) ->1 (b v c)_|_)_|_)_|_ ->1 (c v d))) =< ((b v c) v (e v f)_|_)
Theorem	oas 905	"Strengthening" lemma for studying the orthoarguesian law.
(a_|_ ^ (a v b)) =< c   =>   ((a ->1 c) ^ (a v b)) =< c
Theorem	oasr 906	Reverse of oas 905 lemma for studying the orthoarguesian law.
((a ->1 c) ^ (a v b)) =< c   =>   (a_|_ ^ (a v b)) =< c
Theorem	oat 907	Transformation lemma for studying the orthoarguesian law.
(a_|_ ^ (a v b)) =< c   =>   b =< (a_|_ ->1 c)
Theorem	oatr 908	Reverse transformation lemma for studying the orthoarguesian law.
b =< (a_|_ ->1 c)   =>   (a_|_ ^ (a v b)) =< c
Theorem	oau 909	Transformation lemma for studying the orthoarguesian law.
(a ^ ((a ->1 c) v b)) =< c   =>   b =< (a ->1 c)
Theorem	oaur 910	Transformation lemma for studying the orthoarguesian law.
b =< (a ->1 c)   =>   (a ^ ((a ->1 c) v b)) =< c
Theorem	oaidlem2 911	Lemma for identity-like OA law.
((d v ((a ->1 c) ^ (b ->1 c)))_|_ v ((a ->1 c) ->1 (b ->1 c))) = 1   =>   ((a ->1 c) ^ (d v ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
Theorem	oaidlem2g 912	Lemma for identity-like OA law (generalized).
((c v (a ^ b))_|_ v (a ->1 b)) = 1   =>   (a ^ (c v (a ^ b))) =< b
Theorem	oa6v4v 913	6-variable OA to 4-variable OA.
(((a v b) ^ (c v d)) ^ (e v f)) =< (b v (a ^ (c v (((a v c) ^ (b v d)) ^ (((a v e) ^ (b v f)) v ((c v e) ^ (d v f)))))))   &   e = 0   &   f = 1   =>   ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
Theorem	oa4v3v 914	4-variable OA to 3-variable OA (Godowski/Greechie Eq. IV).
d =< b_|_   &   e =< c_|_   &   ((d v b) ^ (e v c)) =< (b v (d ^ (e v ((d v e) ^ (b v c)))))   &   d = (a ->2 b)_|_   &   e = (a ->2 c)_|_   =>   (b_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< ((b_|_ ^ (a ->2 b)) v (c_|_ ^ (a ->2 c)))
Theorem	oal42 915	Derivation of Godowski/Greechie Eq. II from Eq. IV.
(b_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< ((b_|_ ^ (a ->2 b)) v (c_|_ ^ (a ->2 c)))   =>   (b_|_ ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)_|_ v ((a ->2 b) ^ (a ->2 c)))))) =< a_|_
Theorem	oa23 916	Derivation of OA from Godowski/Greechie Eq. II.
(c_|_ ^ ((a ->2 c) v ((a ->2 b) ^ ((c v b)_|_ v ((a ->2 c) ^ (a ->2 b)))))) =< a_|_   =>   ((a ->2 b) ^ ((b v c)_|_ v ((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 v b) =< ((a v c)_|_ ->2 b)
Theorem	oa4lem2 918	Lemma for 3-var to 4-var OA.
a =< b_|_   &   c =< d_|_   =>   (c v d) =< ((a v c)_|_ ->2 d)
Theorem	oa4lem3 919	Lemma for 3-var to 4-var OA.
a =< b_|_   &   c =< d_|_   =>   ((a v b) ^ (c v d)) =< ((b v d)_|_ v (((a v c)_|_ ->2 b) ^ ((a v c)_|_ ->2 d)))
Theorem	distoah1 920	Satisfaction of distributive law hypothesis.
d = (a ->2 b)   &   e = ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))   &   f = ((b v 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 v c) ->1 ((a ->2 b) ^ (a ->2 c)))   &   f = ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))   =>   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))
Theorem	distoah3 922	Satisfaction of distributive law hypothesis.
d = (a ->2 b)   &   e = ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))   &   f = ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))   =>   f =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))
Theorem	distoah4 923	Satisfaction of distributive law hypothesis.
d = (a ->2 b)   &   e <