[Lattice L46-7]Home PageHome Quantum Logic Explorer
Theorem List (p. 11 of 13) 		< Previous  Next >
Browser slow? Try the
Unicode 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.
((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 c) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c))))
 
Theoremoalii 1002 Orthoarguesian law. Godowski/Greechie, Eq. II. This proof references oaliii 1001 only.
(b' ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))))) =< a'
 
Theoremoaliv 1003 Orthoarguesian law. Godowski/Greechie, 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)))
 
Theoremoath1 1004 OA theorem.
((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (a ->2 c))
 
Theoremoalem1 1005 Lemma.
((b v c) v ((b v c)' ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c))))))) =< (a ->2 (b v c))
 
Theoremoalem2 1006 Lemma.
((a ->2 b) v ((a ->2 c) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c))))) = (a ->2 b)
 
Theoremoadist2a 1007 Distributive inference derived from OA.
(d v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ (d v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ d) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
 
Theoremoadist2b 1008 Distributive inference derived from OA.
d =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ (d v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ d) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
 
Theoremoadist2 1009 Distributive inference derived from OA.
(d v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ (d v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ d) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
 
Theoremoadist12 1010 Distributive law derived from OA.
((a ->2 b) ^ (((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) v ((b v c) ->2 ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) v ((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))))
 
Theoremoacom 1011 Commutation law requiring OA.
d C ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   &   (d ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))) C (a ->2 b)   =>   d C ((a ->2 b) ^ (a ->2 c))
 
Theoremoacom2 1012 Commutation law requiring OA.
d =< ((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c))))   =>   d C ((a ->2 b) ^ (a ->2 c))
 
Theoremoacom3 1013 Commutation law requiring OA.
(d ^ (a ->2 b)) C ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   &   d C (a ->2 b)   =>   d C ((a ->2 b) ^ (a ->2 c))
 
Theoremoagen1 1014 "Generalized" OA.
d =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ (d v ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (a ->2 c))
 
Theoremoagen1b 1015 "Generalized" OA.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   (d ^ (e v ((a ->2 b) ^ (a ->2 c)))) = (d ^ (a ->2 c))
 
Theoremoagen2 1016 "Generalized" OA.
d =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ d) =< (a ->2 c)
 
Theoremoagen2b 1017 "Generalized" OA.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   (d ^ e) =< (a ->2 c)
 
Theoremmloa 1018 Mladen's OA
((a == b) ^ ((b == c) v ((b v (a == b)) ^ (c v (a == c))))) =< (c v (a == c))
 
Theoremoadist 1019 Distributive law derived from OAL.
d =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ (d v ((a ->2 b) ^ (a ->2 c)))) = (((a ->2 b) ^ d) v ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))))
 
Theoremoadistb 1020 Distributive law derived from OAL.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   (d ^ (e v ((a ->2 b) ^ (a ->2 c)))) = ((d ^ e) v (d ^ ((a ->2 b) ^ (a ->2 c))))
 
Theoremoadistc0 1021 Pre-distributive law.
d =< ((a ->2 b) ^ (a ->2 c))   &   ((a ->2 c) ^ ((a ->2 b) ^ ((b v c)' v d))) =< (((a ->2 b) ^ (b v c)') v d)   =>   ((a ->2 b) ^ ((b v c)' v d)) = (((a ->2 b) ^ (b v c)') v d)
 
Theoremoadistc 1022 Distributive law.
d =< ((a ->2 b) ^ (a ->2 c))   &   ((a ->2 b) ^ ((b v c)' v d)) =< (((a ->2 b) ^ (b v c)') v d)   =>   ((a ->2 b) ^ ((b v c)' v d)) = (((a ->2 b) ^ (b v c)') v ((a ->2 b) ^ d))
 
Theoremoadistd 1023 OA distributive law.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   &   f =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   &   (d ^ (a ->2 c)) =< f   =>   (d ^ (e v f)) = ((d ^ e) v (d ^ f))
 
Theorem3oa2 1024 Alternate form for the 3-variable orthoarguesion law.
((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c)) v ((a' ->1 c) ^ (b' ->1 c)))) =< (b ->1 c)
 
Theorem3oa3 1025 3-variable orthoarguesion law expressed with the 3OA identity abbreviation.
((a ->1 c) ^ (a == c ==OA b)) =< (b ->1 c)
 
0.5.2  4-variable orthoarguesian law
 
Axiomax-oal4 1026 Orthoarguesian law (4-variable version).
a =< b'   &   c =< d'   =>   ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
 
Theoremoa4cl 1027 4-variable OA closed equational form)
((a v (b ^ a')) ^ (c v (d ^ c'))) =< ((b ^ a') v (a ^ (c v ((a v c) ^ ((b ^ a') v (d ^ c'))))))
 
Theoremoa43v 1028 Derivation of 3-variable OA from 4-variable OA.
((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
 
Theoremoa3moa3 1029 4-variable 3OA to 5-variable Mayet's 3OA.
a =< b'   &   c =< d'   &   d =< e'   &   e =< c'   =>   ((a v b) ^ ((c v d) v e)) =< (a v (((b ^ (c v ((b v c) ^ ((a v d) v e)))) ^ (d v ((b v d) ^ ((a v c) v e)))) ^ (e v ((b v e) ^ ((a v c) v d)))))
 
0.5.3  6-variable orthoarguesian law
 
Axiomax-oa6 1030 Orthoarguesian law (6-variable version).
a =< b'   &   c =< d'   &   e =< f'   =>   (((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)))))))
 
Theoremoa64v 1031 Derivation of 4-variable OA from 6-variable OA.
a =< b'   &   c =< d'   =>   ((a v b) ^ (c v d)) =< (b v (a ^ (c v ((a v c) ^ (b v d)))))
 
Theoremoa63v 1032 Derivation of 3-variable OA from 6-variable OA.
((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
 
0.5.4  The proper 4-variable orthoarguesian law
 
Axiomax-4oa 1033 The proper 4-variable OA law.
((a ->1 d) ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< (b ->1 d)
 
Theoremaxoa4 1034 The proper 4-variable OA law.
(a' ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d
 
Theoremaxoa4b 1035 Proper 4-variable OA law variant.
((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< d
 
Theoremoa6 1036 Derivation of 6-variable orthoarguesian law from 4-variable version.
a =< b'   &   c =< d'   &   e =< f'   =>   (((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)))))))
 
Theoremaxoa4a 1037 Proper 4-variable OA law variant.
((a ->1 d) ^ (a v (b ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))))) =< (((a ^ d) v (b ^ d)) v (c ^ d))
 
Theoremaxoa4d 1038 Proper 4-variable OA law variant.
(a ^ (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d)))))) =< (b' ->1 d)
 
Theorem4oa 1039 Variant of proper 4-OA.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   =>   ((a ->1 d) ^ f) =< (b ->1 d)
 
Theorem4oaiii 1040 Proper OA analog to Godowski/Greechie, Eq. III.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   =>   ((a ->1 d) ^ f) = ((b ->1 d) ^ f)
 
Theorem4oath1 1041 Proper 4-OA theorem.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   =>   ((a ->1 d) ^ f) = ((a ->1 d) ^ (b ->1 d))
 
Theorem4oagen1 1042 "Generalized" 4-OA.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   g =< f   =>   ((a ->1 d) ^ (g v ((a ->1 d) ^ (b ->1 d)))) = ((a ->1 d) ^ (b ->1 d))
 
Theorem4oagen1b 1043 "Generalized" OA.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   g =< f   &   h =< (a ->1 d)   =>   (h ^ (g v ((a ->1 d) ^ (b ->1 d)))) = (h ^ (b ->1 d))
 
Theorem4oadist 1044 OA Distributive law. This is equivalent to the 6-variable OA law, as shown by theorem d6oa 997.
e = (((a ^ c) v ((a ->1 d) ^ (c ->1 d))) ^ ((b ^ c) v ((b ->1 d) ^ (c ->1 d))))   &   f = (((a ^ b) v ((a ->1 d) ^ (b ->1 d))) v e)   &   h =< (a ->1 d)   &   j =< f   &   k =< f   &   (h ^ (b ->1 d)) =< k   =>   (h ^ (j v k)) = ((h ^ j) v (h ^ k))
 
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).
(((a ->1 b) ->1 (c ->1 b)) ^ ((a ->1 c) ^ (b ->1 a))) =< (c ->1 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   &   (a ->0 b) = 1   =>   b = 1
 
Definitiondf-id5 1047 Define asymmetrical identity (for "Non-Orthomodular Models..." paper).
(a ==5 b) = ((a ^ b) v (a' ^ b'))
 
Definitiondf-b1 1048 Define biconditional for ->1.
(a <->1 b) = ((a ->1 b) ^ (b ->1 a))
 
Theoremlem3.3.3lem1 1049 Lemma for lem3.3.3 1052.
(a ==5 b) =< (a ->1 b)
 
Theoremlem3.3.3lem2 1050 Lemma for lem3.3.3 1052.
(a ==5 b) =< (b ->1 a)
 
Theoremlem3.3.3lem3 1051 Lemma for lem3.3.3 1052.
(a ==5 b) =< ((a ->1 b) ^ (b ->1 a))
 
Theoremlem3.3.3 1052 Equation 3.3 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
((a ==5 b) ->0 (a <->1 b)) = 1
 
Theoremlem3.3.4 1053 Equation 3.4 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(b ->2 a) = 1   =>   (a ->2 (a ==5 b)) = (a ==5 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.)
(a ==5 b) = 1   =>   (a ->1 (b v c)) = 1
 
Theoremlem3.3.6 1056 Equation 3.6 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a ->2 (b v c)) = ((a v c) ->2 (b v c))
 
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.)
(a ->0 (a ^ b)) = (a ==0 (a ^ b))
 
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.)
(a ==0 (a ^ b)) = ((a ^ b) ==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.)
(a ->0 (a ^ b)) = (a ->1 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.)
(a ->1 (a ^ b)) = (a ==1 (a ^ b))
 
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.)
(a ==1 (a ^ b)) = ((a ^ b) ==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.)
(a ->1 (a ^ b)) = (a ->1 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.)
(a ->2 (a ^ b)) = (a ==2 (a ^ b))
 
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.)
(a ==2 (a ^ b)) = ((a ^ b) ==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.)
(a ->2 (a ^ b)) = (a ->1 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.)
(a ->3 (a ^ b)) = (a ==3 (a ^ b))
 
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.)
(a ==3 (a ^ b)) = ((a ^ b) ==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.)
(a ->3 (a ^ b)) = (a ->1 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.)
(a ->4 (a ^ b)) = (a ==4 (a ^ b))
 
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.)
(a ==4 (a ^ b)) = ((a ^ b) ==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.)
(a ->4 (a ^ b)) = (a ->1 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.)
(a ->5 (a ^ b)) = (a ==5 (a ^ b))
 
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.)
(a ==5 (a ^ b)) = ((a ^ b) ==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.)
(a ->5 (a ^ b)) = (a ->1 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.)
((a ->1 b) ->0 (a ->2 b)) = 1
 
Theoremlem3.4.3 1076 Equation 3.11 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a ->2 b) = 1   =>   (a ->2 (a ==5 b)) = 1
 
Theoremlem3.4.4 1077 Equation 3.12 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a ->2 b) = 1   &   (b ->2 a) = 1   =>   (a ==5 b) = 1
 
Theoremlem3.4.5 1078 Equation 3.13 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a ==5 b) = 1   =>   (a ->2 (b v c)) = 1
 
Theoremlem3.4.6 1079 Equation 3.14 of [PavMeg1999] p. 9. (Contributed by Roy F. Longton, 3-Jul-05.)
(a ==5 b) = 1   =>   ((a v c) ==5 (b v c)) = 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.)
((a ->1 b) ^ (a' ->1 b)) = ((a ->1 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.)
((a ->1 b) ^ b) = ((a ^ b) v (a' ^ b))
 
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.)
(a' ->1 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' =< (a ->1 b)
 
Theoremlem4.6.4 1084 Equation 4.12 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
((a ->1 b) ->1 b) = (a' ->1 b)
 
Theoremlem4.6.5 1085 Equation 4.13 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
((a ->1 b)' ->1 b) = (a ->1 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.)
((a ->0 b) v (a ->1 b)) = (a ->0 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.)
((a ->0 b) v (a ->2 b)) = (a ->0 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.)
((a ->0 b) v (a ->3 b)) = (a ->0 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.)
((a ->0 b) v (a ->4 b)) = (a ->0 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.)
((a ->1 b) v (a ->0 b)) = (a ->0 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.)
((a ->1 b) v (a ->2 b)) = (a ->0 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.)
((a ->1 b) v (a ->3 b)) = (a ->0 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.)
((a ->2 b) v (a ->0 b)) = (a ->0 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.)
((a ->2 b) v (a ->1 b)) = (a ->0 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.)
((a ->2 b) v (a ->4 b)) = (a ->0 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.)
((a ->3 b) v (a ->0 b)) = (a ->0 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.)
((a ->3 b) v (a ->1 b)) = (a ->0 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.)
((a ->4 b) v (a ->0 b)) = (a ->0 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.)
((a ->4 b) v (a ->2 b)) = (a ->0 b)
 
Theoremcom3iia 1100 The dual of com3ii 457. (Contributed by Roy F. Longton, 3-Jul-05.)
a C b   =>   (a v (a' ^ b)) = (a v 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-1215
  Copyright terms: Public domain < Previous  Next >