[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 11 of 13)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Quantum Logic Explorer - 1001-1100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremoaliii 1001 Orthoarguesian law. Godowski/Greechie, Eq. III. (Contributed by NM, 22-Sep-1998.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) = ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))
 
Theoremoalii 1002 Orthoarguesian law. Godowski/Greechie, Eq. II. This proof references oaliii 1001 only. (Contributed by NM, 22-Sep-1998.)
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ a
 
Theoremoaliv 1003 Orthoarguesian law. Godowski/Greechie, Eq. IV. (Contributed by NM, 25-Nov-1998.)
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ ((b ∩ (a2 b)) ∪ (c ∩ (a2 c)))
 
Theoremoath1 1004 OA theorem. (Contributed by NM, 12-Oct-1998.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ (a2 c))
 
Theoremoalem1 1005 Lemma. (Contributed by NM, 16-Oct-1998.)
((bc) ∪ ((bc) ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))))) ≤ (a2 (bc))
 
Theoremoalem2 1006 Lemma. (Contributed by NM, 16-Oct-1998.)
((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))) = (a2 b)
 
Theoremoadist2a 1007 Distributive inference derived from OA. (Contributed by NM, 17-Nov-1998.)
(d ∪ ((bc) →2 ((a2 b) ∩ (a2 c)))) ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ (d ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))) = (((a2 b) ∩ d) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))))
 
Theoremoadist2b 1008 Distributive inference derived from OA. (Contributed by NM, 17-Nov-1998.)
d ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ (d ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))) = (((a2 b) ∩ d) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))))
 
Theoremoadist2 1009 Distributive inference derived from OA. (Contributed by NM, 17-Nov-1998.)
(d ∪ ((bc) →2 ((a2 b) ∩ (a2 c)))) = ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ (d ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))) = (((a2 b) ∩ d) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))))
 
Theoremoadist12 1010 Distributive law derived from OA. (Contributed by NM, 17-Nov-1998.)
((a2 b) ∩ (((bc) →1 ((a2 b) ∩ (a2 c))) ∪ ((bc) →2 ((a2 b) ∩ (a2 c))))) = (((a2 b) ∩ ((bc) →1 ((a2 b) ∩ (a2 c)))) ∪ ((a2 b) ∩ ((bc) →2 ((a2 b) ∩ (a2 c)))))
 
Theoremoacom 1011 Commutation law requiring OA. (Contributed by NM, 19-Nov-1998.)
d C ((bc) →0 ((a2 b) ∩ (a2 c)))    &   (d ∩ ((bc) →0 ((a2 b) ∩ (a2 c)))) C (a2 b)       d C ((a2 b) ∩ (a2 c))
 
Theoremoacom2 1012 Commutation law requiring OA. (Contributed by NM, 19-Nov-1998.)
d ≤ ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c))))       d C ((a2 b) ∩ (a2 c))
 
Theoremoacom3 1013 Commutation law requiring OA. (Contributed by NM, 19-Nov-1998.)
(d ∩ (a2 b)) C ((bc) →0 ((a2 b) ∩ (a2 c)))    &   d C (a2 b)       d C ((a2 b) ∩ (a2 c))
 
Theoremoagen1 1014 "Generalized" OA. (Contributed by NM, 19-Nov-1998.)
d ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ (d ∪ ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ (a2 c))
 
Theoremoagen1b 1015 "Generalized" OA. (Contributed by NM, 21-Nov-1998.)
d ≤ (a2 b)    &   e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       (d ∩ (e ∪ ((a2 b) ∩ (a2 c)))) = (d ∩ (a2 c))
 
Theoremoagen2 1016 "Generalized" OA. (Contributed by NM, 19-Nov-1998.)
d ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ d) ≤ (a2 c)
 
Theoremoagen2b 1017 "Generalized" OA. (Contributed by NM, 21-Nov-1998.)
d ≤ (a2 b)    &   e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       (de) ≤ (a2 c)
 
Theoremmloa 1018 Mladen's OA (Contributed by NM, 20-Nov-1998.)
((ab) ∩ ((bc) ∪ ((b ∪ (ab)) ∩ (c ∪ (ac))))) ≤ (c ∪ (ac))
 
Theoremoadist 1019 Distributive law derived from OAL. (Contributed by NM, 20-Nov-1998.)
d ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ (d ∪ ((a2 b) ∩ (a2 c)))) = (((a2 b) ∩ d) ∪ ((a2 b) ∩ ((a2 b) ∩ (a2 c))))
 
Theoremoadistb 1020 Distributive law derived from OAL. (Contributed by NM, 20-Nov-1998.)
d ≤ (a2 b)    &   e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       (d ∩ (e ∪ ((a2 b) ∩ (a2 c)))) = ((de) ∪ (d ∩ ((a2 b) ∩ (a2 c))))
 
Theoremoadistc0 1021 Pre-distributive law. Note that the inference of the second hypothesis from the first may be an OM theorem. (Contributed by NM, 30-Nov-1998.)
d ≤ ((a2 b) ∩ (a2 c))    &   ((a2 c) ∩ ((a2 b) ∩ ((bc)d))) ≤ (((a2 b) ∩ (bc) ) ∪ d)       ((a2 b) ∩ ((bc)d)) = (((a2 b) ∩ (bc) ) ∪ d)
 
Theoremoadistc 1022 Distributive law. (Contributed by NM, 21-Nov-1998.)
d ≤ ((a2 b) ∩ (a2 c))    &   ((a2 b) ∩ ((bc)d)) ≤ (((a2 b) ∩ (bc) ) ∪ d)       ((a2 b) ∩ ((bc)d)) = (((a2 b) ∩ (bc) ) ∪ ((a2 b) ∩ d))
 
Theoremoadistd 1023 OA distributive law. (Contributed by NM, 21-Nov-1998.)
d ≤ (a2 b)    &   e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))    &   f ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))    &   (d ∩ (a2 c)) ≤ f       (d ∩ (ef)) = ((de) ∪ (df))
 
Theorem3oa2 1024 Alternate form for the 3-variable orthoarguesion law. (Contributed by NM, 27-May-2004.)
((a1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)
 
Theorem3oa3 1025 3-variable orthoarguesion law expressed with the 3OA identity abbreviation. (Contributed by NM, 27-May-2004.)
((a1 c) ∩ (acOA b)) ≤ (b1 c)
 
0.5.2  4-variable orthoarguesian law
 
Axiomax-oal4 1026 Orthoarguesian law (4-variable version). (Contributed by NM, 1-Dec-1998.)
ab    &   cd       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
 
Theoremoa4cl 1027 4-variable OA closed equational form. (Contributed by NM, 1-Dec-1998.)
((a ∪ (ba )) ∩ (c ∪ (dc ))) ≤ ((ba ) ∪ (a ∩ (c ∪ ((ac) ∩ ((ba ) ∪ (dc ))))))
 
Theoremoa43v 1028 Derivation of 3-variable OA from 4-variable OA. (Contributed by NM, 28-Nov-1998.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
 
Theoremoa3moa3 1029 4-variable 3OA to 5-variable Mayet's 3OA. (Contributed by NM, 3-Apr-2009.) (Revised by NM, 31-Mar-2011.)
ab    &   cd    &   de    &   ec       ((ab) ∩ ((cd) ∪ e)) ≤ (a ∪ (((b ∩ (c ∪ ((bc) ∩ ((ad) ∪ e)))) ∩ (d ∪ ((bd) ∩ ((ac) ∪ e)))) ∩ (e ∪ ((be) ∩ ((ac) ∪ d)))))
 
0.5.3  6-variable orthoarguesian law
 
Axiomax-oa6 1030 Orthoarguesian law (6-variable version). (Contributed by NM, 29-Nov-1998.)
ab    &   cd    &   ef       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
 
Theoremoa64v 1031 Derivation of 4-variable OA from 6-variable OA. (Contributed by NM, 29-Nov-1998.)
ab    &   cd       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))
 
Theoremoa63v 1032 Derivation of 3-variable OA from 6-variable OA. (Contributed by NM, 28-Nov-1998.)
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)
 
0.5.4  The proper 4-variable orthoarguesian law
 
Axiomax-4oa 1033 The proper 4-variable OA law. (Contributed by NM, 20-Jul-1999.)
((a1 d) ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (b1 d)
 
Theoremaxoa4 1034 The proper 4-variable OA law. (Contributed by NM, 20-Jul-1999.)
(a ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d
 
Theoremaxoa4b 1035 Proper 4-variable OA law variant. (Contributed by NM, 22-Dec-1998.)
((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ d
 
Theoremoa6 1036 Derivation of 6-variable orthoarguesian law from 4-variable version. (Contributed by NM, 18-Dec-1998.)
ab    &   cd    &   ef       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))
 
Theoremaxoa4a 1037 Proper 4-variable OA law variant. (Contributed by NM, 22-Dec-1998.)
((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ (((ad) ∪ (bd)) ∪ (cd))
 
Theoremaxoa4d 1038 Proper 4-variable OA law variant. (Contributed by NM, 24-Dec-1998.)
(a ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))) ≤ (b1 d)
 
Theorem4oa 1039 Variant of proper 4-OA. (Contributed by NM, 29-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)       ((a1 d) ∩ f) ≤ (b1 d)
 
Theorem4oaiii 1040 Proper OA analog to Godowski/Greechie, Eq. III. (Contributed by NM, 29-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)       ((a1 d) ∩ f) = ((b1 d) ∩ f)
 
Theorem4oath1 1041 Proper 4-OA theorem. (Contributed by NM, 29-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)       ((a1 d) ∩ f) = ((a1 d) ∩ (b1 d))
 
Theorem4oagen1 1042 "Generalized" 4-OA. (Contributed by NM, 29-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)    &   gf       ((a1 d) ∩ (g ∪ ((a1 d) ∩ (b1 d)))) = ((a1 d) ∩ (b1 d))
 
Theorem4oagen1b 1043 "Generalized" OA. (Contributed by NM, 29-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)    &   gf    &   h ≤ (a1 d)       (h ∩ (g ∪ ((a1 d) ∩ (b1 d)))) = (h ∩ (b1 d))
 
Theorem4oadist 1044 OA Distributive law. This is equivalent to the 6-variable OA law, as shown by theorem d6oa 997. (Contributed by NM, 29-Dec-1998.)
e = (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d))))    &   f = (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ e)    &   h ≤ (a1 d)    &   jf    &   kf    &   (h ∩ (b1 d)) ≤ k       (h ∩ (jk)) = ((hj) ∪ (hk))
 
0.6  Other stronger-than-OML laws
 
0.6.1  New state-related equation
 
Axiomax-newstateeq 1045 This is the simplest known example of an equation implied by the set of Mayet--Godowski equations that is independent from all Godowski equations. It was discovered by Norman Megill and Mladen Pavicic between 1997 and August 2003. This is Equation (54) in

Mladen Pavicic, Norman D. Megill, Quantum Logic and Quantum Computation, in Handbook of Quantum Logic and Quantum Structures, Volume Quantum Structures, Elsevier, Amsterdam, 2007, pp. 751--787. https://arxiv.org/abs/0812.3072

and Equation (15) in

Mladen Pavicic, Brendan D. McKay, Norman D. Megill, Kresimir Fresl, Graph Approach to Quantum Systems, Journal of Mathematical Physics, Volume 51, Issue 10, October 2010. https://arxiv.org/abs/1004.0776

(Contributed by NM, 1-Jan-1998.)

(((a1 b) →1 (c1 b)) ∩ ((a1 c) ∩ (b1 a))) ≤ (c1 a)
 
0.7  Contributions of Roy F. Longton
 
0.7.1  Roy F. Longton's first section
 
Theoremlem3.3.2 1046 Equation 3.2 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
a = 1    &   (a0 b) = 1       b = 1
 
Definitiondf-id5 1047 Define asymmetrical identity (for "Non-Orthomodular Models..." paper). (Contributed by Roy F. Longton, 27-Jun-2005.)
(a5 b) = ((ab) ∪ (ab ))
 
Definitiondf-b1 1048 Define biconditional for 1 . (Contributed by Roy F. Longton, 27-Jun-2005.)
(a1 b) = ((a1 b) ∩ (b1 a))
 
Theoremlem3.3.3lem1 1049 Lemma for lem3.3.3 1052. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 b) ≤ (a1 b)
 
Theoremlem3.3.3lem2 1050 Lemma for lem3.3.3 1052. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 b) ≤ (b1 a)
 
Theoremlem3.3.3lem3 1051 Lemma for lem3.3.3 1052. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 b) ≤ ((a1 b) ∩ (b1 a))
 
Theoremlem3.3.3 1052 Equation 3.3 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 27-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
((a5 b) →0 (a1 b)) = 1
 
Theoremlem3.3.4 1053 Equation 3.4 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(b2 a) = 1       (a2 (a5 b)) = (a5 b)
 
Theoremlem3.3.5lem 1054 A fundamental property in quantum logic. Lemma for lem3.3.5 1055. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
1 ≤ a       a = 1
 
Theoremlem3.3.5 1055 Equation 3.5 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 b) = 1       (a1 (bc)) = 1
 
Theoremlem3.3.6 1056 Equation 3.6 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a2 (bc)) = ((ac) →2 (bc))
 
Theoremlem3.3.7i0e1 1057 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the first part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a0 (ab)) = (a0 (ab))
 
Theoremlem3.3.7i0e2 1058 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the second part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a0 (ab)) = ((ab) ≡0 a)
 
Theoremlem3.3.7i0e3 1059 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 0, and this is the third part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a0 (ab)) = (a1 b)
 
Theoremlem3.3.7i1e1 1060 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-2005.)
(a1 (ab)) = (a1 (ab))
 
Theoremlem3.3.7i1e2 1061 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the second part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a1 (ab)) = ((ab) ≡1 a)
 
Theoremlem3.3.7i1e3 1062 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 1, and this is the third part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a1 (ab)) = (a1 b)
 
Theoremlem3.3.7i2e1 1063 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the first part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a2 (ab)) = (a2 (ab))
 
Theoremlem3.3.7i2e2 1064 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-2005.)
(a2 (ab)) = ((ab) ≡2 a)
 
Theoremlem3.3.7i2e3 1065 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 2, and this is the third part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a2 (ab)) = (a1 b)
 
Theoremlem3.3.7i3e1 1066 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 3, and this is the first part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a3 (ab)) = (a3 (ab))
 
Theoremlem3.3.7i3e2 1067 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 3, and this is the second part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a3 (ab)) = ((ab) ≡3 a)
 
Theoremlem3.3.7i3e3 1068 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 3, and this is the third part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a3 (ab)) = (a1 b)
 
Theoremlem3.3.7i4e1 1069 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, and this is the first part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a4 (ab)) = (a4 (ab))
 
Theoremlem3.3.7i4e2 1070 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, and this is the second part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a4 (ab)) = ((ab) ≡4 a)
 
Theoremlem3.3.7i4e3 1071 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 4, and this is the third part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a4 (ab)) = (a1 b)
 
Theoremlem3.3.7i5e1 1072 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 5, and this is the first part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 (ab)) = (a5 (ab))
 
Theoremlem3.3.7i5e2 1073 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 5, and this is the second part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 (ab)) = ((ab) ≡5 a)
 
Theoremlem3.3.7i5e3 1074 Equation 3.7 of [PavMeg1999] p. 9. The variable i in the paper is set to 5, and this is the third part of the equation. (Contributed by Roy F. Longton, 28-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 (ab)) = (a1 b)
 
0.7.2  Roy F. Longton's second section
 
Theoremlem3.4.1 1075 Equation 3.9 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-2005.)
((a1 b) →0 (a2 b)) = 1
 
Theoremlem3.4.3 1076 Equation 3.11 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a2 b) = 1       (a2 (a5 b)) = 1
 
Theoremlem3.4.4 1077 Equation 3.12 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a2 b) = 1    &   (b2 a) = 1       (a5 b) = 1
 
Theoremlem3.4.5 1078 Equation 3.13 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 b) = 1       (a2 (bc)) = 1
 
Theoremlem3.4.6 1079 Equation 3.14 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
(a5 b) = 1       ((ac) ≡5 (bc)) = 1
 
Theoremthm3.8i1lem 1080 Lemma intended for ~ thm3.8i1 . (Contributed by Roy F. Longton, 30-Jun-2005.) (Revised by Roy F. Longton, 31-Mar-2011.)
(a1 b) = ((b0 a) ∩ (a1 b))
 
Theoremthm3.8i5 1081 (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 31-Mar-2011.)
(a5 b) = 1       ((ac) ≡5 (bc)) = 1
 
0.7.3  Roy F. Longton's third section
 
Theoremlem4.6.2e1 1082 Equation 4.10 of [MegPav2000] p. 23. This is the first part of the equation. Note that Lemma 4.6.1 is u1lemaa 600. (Contributed by Roy F. Longton, 29-Jun-2005.) (Revised by Roy F. Longton, 3-Jul-2005.)
((a1 b) ∩ (a1 b)) = ((a1 b) ∩ b)
 
Theoremlem4.6.2e2 1083 Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a1 b) ∩ b) = ((ab) ∪ (ab))
 
Theoremlem4.6.3le1 1084 Equation 4.11 of [MegPav2000] p. 23. This is the first part of the equation. (Contributed by Roy F. Longton, 1-Jul-2005.)
(a1 b)a
 
Theoremlem4.6.3le2 1085 Equation 4.11 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 1-Jul-2005.)
a ≤ (a1 b)
 
Theoremlem4.6.4 1086 Equation 4.12 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a1 b) →1 b) = (a1 b)
 
Theoremlem4.6.5 1087 Equation 4.13 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a1 b)1 b) = (a1 b)
 
Theoremlem4.6.6i0j1 1088 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 1. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a0 b) ∪ (a1 b)) = (a0 b)
 
Theoremlem4.6.6i0j2 1089 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 2. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a0 b) ∪ (a2 b)) = (a0 b)
 
Theoremlem4.6.6i0j3 1090 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 3. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a0 b) ∪ (a3 b)) = (a0 b)
 
Theoremlem4.6.6i0j4 1091 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 0, and j is set to 4. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a0 b) ∪ (a4 b)) = (a0 b)
 
Theoremlem4.6.6i1j0 1092 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 0. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a1 b) ∪ (a0 b)) = (a0 b)
 
Theoremlem4.6.6i1j2 1093 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 2. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a1 b) ∪ (a2 b)) = (a0 b)
 
Theoremlem4.6.6i1j3 1094 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 1, and j is set to 3. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a1 b) ∪ (a3 b)) = (a0 b)
 
Theoremlem4.6.6i2j0 1095 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 2, and j is set to 0. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a2 b) ∪ (a0 b)) = (a0 b)
 
Theoremlem4.6.6i2j1 1096 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 2, and j is set to 1. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a2 b) ∪ (a1 b)) = (a0 b)
 
Theoremlem4.6.6i2j4 1097 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 2, and j is set to 4. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a2 b) ∪ (a4 b)) = (a0 b)
 
Theoremlem4.6.6i3j0 1098 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 3, and j is set to 0. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a3 b) ∪ (a0 b)) = (a0 b)
 
Theoremlem4.6.6i3j1 1099 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 3, and j is set to 1. (Contributed by Roy F. Longton, 1-Jul-2005.)
((a3 b) ∪ (a1 b)) = (a0 b)
 
Theoremlem4.6.6i4j0 1100 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 4, and j is set to 0. (Contributed by Roy F. Longton, 2-Jul-2005.)
((a4 b) ∪ (a0 b)) = (a0 b)
    < Previous  Next >

Page List
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-1200 13 1201-1217
  Copyright terms: Public domain < Previous  Next >