[Lattice L46-7]Home PageHome Quantum Logic Explorer < Previous   Next >
Browser slow? Try the
Unicode version.

Jump to page: Contents + 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-1100 12 1101-1118

Statement List for Quantum Logic Explorer - 901-1000 - Page 10 of 12
TypeLabelDescription
Statement
 
Theoremgo2n6 901 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 v h) ^ (i v j)) ^ (((k v m) ^ (n v u)) ^ ((w v x) ^ (y v z)))) =< (h v i)
 
Theoremgomaex3h1 902 Hypothesis for Godowski 6-var -> Mayet Example 3.
a =< b'   &   g = a   &   h = b   =>   g =< h'
 
Theoremgomaex3h2 903 Hypothesis for Godowski 6-var -> Mayet Example 3.
b =< c'   &   h = b   &   i = c   =>   h =< i'
 
Theoremgomaex3h3 904 Hypothesis for Godowski 6-var -> Mayet Example 3.
i = c   &   j = (c v d)'   =>   i =< j'
 
Theoremgomaex3h4 905 Hypothesis for Godowski 6-var -> Mayet Example 3.
r = ((p' ->1 q)' ^ (c v d))   &   j = (c v d)'   &   k = r   =>   j =< k'
 
Theoremgomaex3h5 906 Hypothesis for Godowski 6-var -> Mayet Example 3.
r = ((p' ->1 q)' ^ (c v d))   &   k = r   &   m = (p' ->1 q)   =>   k =< m'
 
Theoremgomaex3h6 907 Hypothesis for Godowski 6-var -> Mayet Example 3.
m = (p' ->1 q)   &   n = (p' ->1 q)'   =>   m =< n'
 
Theoremgomaex3h7 908 Hypothesis for Godowski 6-var -> Mayet Example 3.
n = (p' ->1 q)'   &   u = (p' ^ q)   =>   n =< u'
 
Theoremgomaex3h8 909 Hypothesis for Godowski 6-var -> Mayet Example 3.
u = (p' ^ q)   &   w = q'   =>   u =< w'
 
Theoremgomaex3h9 910 Hypothesis for Godowski 6-var -> Mayet Example 3.
w = q'   &   x = q   =>   w =< x'
 
Theoremgomaex3h10 911 Hypothesis for Godowski 6-var -> Mayet Example 3.
q = ((e v f) ->1 (b v c)')'   &   x = q   &   y = (e v f)'   =>   x =< y'
 
Theoremgomaex3h11 912 Hypothesis for Godowski 6-var -> Mayet Example 3.
y = (e v f)'   &   z = f   =>   y =< z'
 
Theoremgomaex3h12 913 Hypothesis for Godowski 6-var -> Mayet Example 3.
f =< a'   &   g = a   &   z = f   =>   z =< g'
 
Theoremgomaex3lem1 914 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem2 915 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem3 916 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem4 917 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem5 918 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem6 919 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem7 920 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem8 921 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem9 922 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3lem10 923 Lemma for Godowski 6-var -> Mayet Example 3.
 
Theoremgomaex3 924 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)')
 
OML Lemmas for studying orthoarguesian laws
 
Theoremoas 925 "Strengthening" lemma for studying the orthoarguesian law.
(a' ^ (a v b)) =< c   =>   ((a ->1 c) ^ (a v b)) =< c
 
Theoremoasr 926 Reverse of oas 925 lemma for studying the orthoarguesian law.
((a ->1 c) ^ (a v b)) =< c   =>   (a' ^ (a v b)) =< c
 
Theoremoat 927 Transformation lemma for studying the orthoarguesian law.
(a' ^ (a v b)) =< c   =>   b =< (a' ->1 c)
 
Theoremoatr 928 Reverse transformation lemma for studying the orthoarguesian law.
b =< (a' ->1 c)   =>   (a' ^ (a v b)) =< c
 
Theoremoau 929 Transformation lemma for studying the orthoarguesian law.
(a ^ ((a ->1 c) v b)) =< c   =>   b =< (a ->1 c)
 
Theoremoaur 930 Transformation lemma for studying the orthoarguesian law.
b =< (a ->1 c)   =>   (a ^ ((a ->1 c) v b)) =< c
 
Theoremoaidlem2 931 Lemma for identity-like OA law.
 
Theoremoaidlem2g 932 Lemma for identity-like OA law (generalized).
 
Theoremoa6v4v 933 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)))))
 
Theoremoa4v3v 934 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)))
 
Theoremoal42 935 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'
 
Theoremoa23 936 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)
 
Theoremoa4lem1 937 Lemma for 3-var to 4-var OA.
 
Theoremoa4lem2 938 Lemma for 3-var to 4-var OA.
 
Theoremoa4lem3 939 Lemma for 3-var to 4-var OA.
 
Theoremdistoah1 940 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)
 
Theoremdistoah2 941 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)))
 
Theoremdistoah3 942 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)))
 
Theoremdistoah4 943 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 c)) =< f
 
Theoremdistoa 944 Derivation in OM of OA, assuming OA distributive law oadistd 1023.
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 ^ (e v f)) = ((d ^ e) v (d ^ f))   =>   ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
 
Theoremoa3to4lem1 945 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
 
Theoremoa3to4lem2 946 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
 
Theoremoa3to4lem3 947 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
 
Theoremoa3to4lem4 948 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
 
Theoremoa3to4lem5 949 Lemma for orthoarguesian law (Godowski/Greechie 3-variable to 4-variable proof).
 
Theoremoa3to4lem6 950 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') v (c' ^ d'))   &   e = a'   &   f = c'   &   (e ^ ((e ->1 g) v ((f ->1 g) ^ ((e ^ f) v ((e ->1 g) ^ (f ->1 g)))))) =< ((e ^ g) v (f ^ g))   =>   ((a v b) ^ (c v d)) =< (a v (b ^ (d v ((a v c) ^ (b v d)))))
 
Theoremoa3to4 951 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') v (d' ^ c'))   &   e = b'   &   f