 Home Quantum Logic ExplorerTheorem 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.
((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.
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ a

Theoremoaliv 1003 Orthoarguesian law. Godowski/Greechie, Eq. IV.
(b ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))))) ≤ ((b ∩ (a2 b)) ∪ (c ∩ (a2 c)))

Theoremoath1 1004 OA theorem.
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ (a2 c))

Theoremoalem1 1005 Lemma.
((bc) ∪ ((bc) ∩ ((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))))) ≤ (a2 (bc))

Theoremoalem2 1006 Lemma.
((a2 b) ∪ ((a2 c) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c))))) = (a2 b)

Theoremoadist2a 1007 Distributive inference derived from OA.
(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.
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.
(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.
((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.
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.
d ≤ ((a2 b) ∩ ((bc) →0 ((a2 b) ∩ (a2 c))))       d C ((a2 b) ∩ (a2 c))

Theoremoacom3 1013 Commutation law requiring OA.
(d ∩ (a2 b)) C ((bc) →0 ((a2 b) ∩ (a2 c)))    &   d C (a2 b)       d C ((a2 b) ∩ (a2 c))

Theoremoagen1 1014 "Generalized" OA.
d ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ (d ∪ ((a2 b) ∩ (a2 c)))) = ((a2 b) ∩ (a2 c))

Theoremoagen1b 1015 "Generalized" OA.
d ≤ (a2 b)    &   e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       (d ∩ (e ∪ ((a2 b) ∩ (a2 c)))) = (d ∩ (a2 c))

Theoremoagen2 1016 "Generalized" OA.
d ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       ((a2 b) ∩ d) ≤ (a2 c)

Theoremoagen2b 1017 "Generalized" OA.
d ≤ (a2 b)    &   e ≤ ((bc) →0 ((a2 b) ∩ (a2 c)))       (de) ≤ (a2 c)

Theoremmloa 1018 Mladen's OA
((ab) ∩ ((bc) ∪ ((b ∪ (ab)) ∩ (c ∪ (ac))))) ≤ (c ∪ (ac))

Theoremoadist 1019 Distributive law derived from OAL.
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.
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.
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.
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.
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.
((a1 c) ∩ (((a1 c) ∩ (b1 c)) ∪ ((a1 c) ∩ (b1 c)))) ≤ (b1 c)

Theorem3oa3 1025 3-variable orthoarguesion law expressed with the 3OA identity abbreviation.
((a1 c) ∩ (acOA b)) ≤ (b1 c)

0.5.2  4-variable orthoarguesian law

Axiomax-oal4 1026 Orthoarguesian law (4-variable version).
ab    &   cd       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Theoremoa4cl 1027 4-variable OA closed equational form)
((a ∪ (ba )) ∩ (c ∪ (dc ))) ≤ ((ba ) ∪ (a ∩ (c ∪ ((ac) ∩ ((ba ) ∪ (dc ))))))

Theoremoa43v 1028 Derivation of 3-variable OA from 4-variable OA.
((a2 b) ∩ ((bc) ∪ ((a2 b) ∩ (a2 c)))) ≤ (a2 c)

Theoremoa3moa3 1029 4-variable 3OA to 5-variable Mayet's 3OA.
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).
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.
ab    &   cd       ((ab) ∩ (cd)) ≤ (b ∪ (a ∩ (c ∪ ((ac) ∩ (bd)))))

Theoremoa63v 1032 Derivation of 3-variable OA from 6-variable OA.
((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.
((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.
(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.
((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.
ab    &   cd    &   ef       (((ab) ∩ (cd)) ∩ (ef)) ≤ (b ∪ (a ∩ (c ∪ (((ac) ∩ (bd)) ∩ (((ae) ∩ (bf)) ∪ ((ce) ∩ (df)))))))

Theoremaxoa4a 1037 Proper 4-variable OA law variant.
((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.
(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.
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.
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.
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.
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.
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.
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 New equation that holds in Hilbert space, discovered by Pavicic and Megill (unpublished).
(((a1 b) →1 (c1 b)) ∩ ((a1 c) ∩ (b1 a))) ≤ (c1 a)

0.7  Contributions of Roy Longton

0.7.1  Roy's first section

Theoremlem3.3.2 1046 Equation 3.2 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
a = 1    &   (a0 b) = 1       b = 1

Definitiondf-id5 1047 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a5 b) = ((ab) ∪ (ab ))

Definitiondf-b1 1048 Define biconditional for 1 .
(a1 b) = ((a1 b) ∩ (b1 a))

Theoremlem3.3.3lem1 1049 Lemma for lem3.3.3 1052.
(a5 b) ≤ (a1 b)

Theoremlem3.3.3lem2 1050 Lemma for lem3.3.3 1052.
(a5 b) ≤ (b1 a)

Theoremlem3.3.3lem3 1051 Lemma for lem3.3.3 1052.
(a5 b) ≤ ((a1 b) ∩ (b1 a))

Theoremlem3.3.3 1052 Equation 3.3 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
((a5 b) →0 (a1 b)) = 1

Theoremlem3.3.4 1053 Equation 3.4 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(b2 a) = 1       (a2 (a5 b)) = (a5 b)

Theoremlem3.3.5lem 1054 A fundamental property in quantum logic. Lemma for lem3.3.5 1055.
1 ≤ a       a = 1

Theoremlem3.3.5 1055 Equation 3.5 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a5 b) = 1       (a1 (bc)) = 1

Theoremlem3.3.6 1056 Equation 3.6 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(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, 3-Jul-05.)
(a5 (ab)) = (a1 b)

0.7.2  Roy's second section

Theoremlem3.4.1 1075 Equation 3.9 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
((a1 b) →0 (a2 b)) = 1

Theoremlem3.4.3 1076 Equation 3.11 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a2 b) = 1       (a2 (a5 b)) = 1

Theoremlem3.4.4 1077 Equation 3.12 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(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, 3-Jul-05.)
(a5 b) = 1       (a2 (bc)) = 1

Theoremlem3.4.6 1079 Equation 3.14 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a5 b) = 1       ((ac) ≡5 (bc)) = 1

0.7.3  Roy's third section

Theoremlem4.6.2e1 1080 Equation 4.10 of [MegPav2000] p. 23. This is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)
((a1 b) ∩ (a1 b)) = ((a1 b) ∩ b)

Theoremlem4.6.2e2 1081 Equation 4.10 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)
((a1 b) ∩ b) = ((ab) ∪ (ab))

Theoremlem4.6.3le1 1082 Equation 4.11 of [MegPav2000] p. 23. This is the first part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)
(a1 b)a

Theoremlem4.6.3le2 1083 Equation 4.11 of [MegPav2000] p. 23. This is the second part of the equation. (Contributed by Roy F. Longton, 3-Jul-05.)
a ≤ (a1 b)

Theoremlem4.6.4 1084 Equation 4.12 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
((a1 b) →1 b) = (a1 b)

Theoremlem4.6.5 1085 Equation 4.13 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
((a1 b)1 b) = (a1 b)

Theoremlem4.6.6i0j1 1086 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, 3-Jul-05.)
((a0 b) ∪ (a1 b)) = (a0 b)

Theoremlem4.6.6i0j2 1087 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, 3-Jul-05.)
((a0 b) ∪ (a2 b)) = (a0 b)

Theoremlem4.6.6i0j3 1088 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, 3-Jul-05.)
((a0 b) ∪ (a3 b)) = (a0 b)

Theoremlem4.6.6i0j4 1089 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, 3-Jul-05.)
((a0 b) ∪ (a4 b)) = (a0 b)

Theoremlem4.6.6i1j0 1090 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, 3-Jul-05.)
((a1 b) ∪ (a0 b)) = (a0 b)

Theoremlem4.6.6i1j2 1091 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, 3-Jul-05.)
((a1 b) ∪ (a2 b)) = (a0 b)

Theoremlem4.6.6i1j3 1092 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, 3-Jul-05.)
((a1 b) ∪ (a3 b)) = (a0 b)

Theoremlem4.6.6i2j0 1093 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, 3-Jul-05.)
((a2 b) ∪ (a0 b)) = (a0 b)

Theoremlem4.6.6i2j1 1094 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, 3-Jul-05.)
((a2 b) ∪ (a1 b)) = (a0 b)

Theoremlem4.6.6i2j4 1095 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, 3-Jul-05.)
((a2 b) ∪ (a4 b)) = (a0 b)

Theoremlem4.6.6i3j0 1096 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, 3-Jul-05.)
((a3 b) ∪ (a0 b)) = (a0 b)

Theoremlem4.6.6i3j1 1097 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, 3-Jul-05.)
((a3 b) ∪ (a1 b)) = (a0 b)

Theoremlem4.6.6i4j0 1098 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, 3-Jul-05.)
((a4 b) ∪ (a0 b)) = (a0 b)

Theoremlem4.6.6i4j2 1099 Equation 4.14 of [MegPav2000] p. 23. The variable i in the paper is set to 4, and j is set to 2. (Contributed by Roy F. Longton, 3-Jul-05.)
((a4 b) ∪ (a2 b)) = (a0 b)

Theoremcom3iia 1100 The dual of com3ii 457. (Contributed by Roy F. Longton, 3-Jul-05.)
a C b       (a ∪ (ab)) = (ab)

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-1215
 Copyright terms: Public domain < Previous  Next >