mmtheorems12 - Quantum Logic Explorer

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-1181

Statement List for Quantum Logic Explorer - 1101-1181 - Page 12 of 12

Type	Label	Description
Statement
Theorem	lem4.6.7 1101	Equation 4.15 of [MegPav2000] p. 23. (Contributed by Roy F. Longton, 3-Jul-05.)
a' =< b   =>   b =< (a ->1 b)
Weakly distributive ortholattices (WDOL)
WDOL law
Axiom	ax-wdol 1102	The WDOL (weakly distributive ortholattice) axiom.
((a == b) v (a == b')) = 1
Theorem	wdcom 1103	Any two variables (weakly) commute in a WDOL.
C (a, b) = 1
Theorem	wdwom 1104	Prove 2-variable WOML rule in WDOL. This will make all WOML theorems available to us. The proof does not use ax-r3 439 or ax-wom 361. Since this is the same as ax-wom 361, from here on we will freely use those theorems invoking ax-wom 361.
(a' v (a ^ b)) = 1   =>   (b v (a' ^ b')) = 1
Theorem	wddi1 1105	Prove the weak distributive law in WDOL. This is our first WDOL theorem making use of ax-wom 361, which is justified by wdwom 1104.
((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
Theorem	wddi2 1106	The weak distributive law in WDOL.
(((a v b) ^ c) == ((a ^ c) v (b ^ c))) = 1
Theorem	wddi3 1107	The weak distributive law in WDOL.
((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
Theorem	wddi4 1108	The weak distributive law in WDOL.
(((a ^ b) v c) == ((a v c) ^ (b v c))) = 1
Theorem	wdid0id5 1109	Show that quantum identity follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a == b) = 1
Theorem	wdid0id1 1110	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==1 b) = 1
Theorem	wdid0id2 1111	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==2 b) = 1
Theorem	wdid0id3 1112	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==3 b) = 1
Theorem	wdid0id4 1113	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==4 b) = 1
Theorem	wdka4o 1114	Show WDOL analog of WOM law.
(a ==0 b) = 1   =>   ((a v c) ==0 (b v c)) = 1
Theorem	wddi-0 1115	The weak distributive law in WDOL.
((a ^ (b v c)) ==0 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-1 1116	The weak distributive law in WDOL.
((a ^ (b v c)) ==1 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-2 1117	The weak distributive law in WDOL.
((a ^ (b v c)) ==2 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-3 1118	The weak distributive law in WDOL.
((a ^ (b v c)) ==3 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-4 1119	The weak distributive law in WDOL.
((a ^ (b v c)) ==4 ((a ^ b) v (a ^ c))) = 1
Modular ortholattices (MOL)
Modular law
Axiom	ax-ml 1120	The modular law axiom.
((a v b) ^ (a v c)) =< (a v (b ^ (a v c)))
Theorem	ml 1121	Modular law in equational form.
(a v (b ^ (a v c))) = ((a v b) ^ (a v c))
Theorem	mldual 1122	Dual of modular law.
(a ^ (b v (a ^ c))) = ((a ^ b) v (a ^ c))
Theorem	ml2i 1123	Inference version of modular law.
c =< a   =>   (c v (b ^ a)) = ((c v b) ^ a)
Theorem	mli 1124	Inference version of modular law.
c =< a   =>   ((a ^ b) v c) = (a ^ (b v c))
Theorem	mldual2i 1125	Inference version of dual of modular law.
a =< c   =>   (c ^ (b v a)) = ((c ^ b) v a)
Theorem	mlduali 1126	Inference version of dual of modular law.
a =< c   =>   ((a v b) ^ c) = (a v (b ^ c))
Theorem	ml3le 1127	Form of modular law that swaps two terms.
(a v (b ^ (c v a))) =< (a v (c ^ (b v a)))
Theorem	ml3 1128	Form of modular law that swaps two terms.
(a v (b ^ (c v a))) = (a v (c ^ (b v a)))
Theorem	vneulem1 1129	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((x v y) v u) ^ w) = (((x v y) v u) ^ ((u v w) ^ w))
Theorem	vneulem2 1130	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((x v y) v u) ^ ((u v w) ^ w)) = ((((x v y) ^ (u v w)) v u) ^ w)
Theorem	vneulem3 1131	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((x v y) ^ (u v w)) = 0   =>   ((((x v y) ^ (u v w)) v u) ^ w) = (u ^ w)
Theorem	vneulem4 1132	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((x v y) ^ (u v w)) = 0   =>   (((x v y) v u) ^ w) = (u ^ w)
Theorem	vneulem5 1133	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((x v y) v u) ^ ((x v y) v w)) = ((x v y) v (((x v y) v u) ^ w))
Theorem	vneulem6 1134	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   (((a v b) v d) ^ ((b v c) v d)) = ((c ^ a) v (b v d))
Theorem	vneulem7 1135	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   ((c ^ a) v (b v d)) = (b v d)
Theorem	vneulem8 1136	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   (((a v b) v d) ^ ((b v c) v d)) = (b v d)
Theorem	vneulem9 1137	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   (((a v b) v d) ^ ((a v b) v c)) = ((c ^ d) v (a v b))
Theorem	vneulem10 1138	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   (((a v b) v c) ^ ((a v c) v d)) = (a v c)
Theorem	vneulem11 1139	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   (((b v c) v d) ^ ((a v c) v d)) = ((c v d) v (a ^ b))
Theorem	vneulem12 1140	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
(((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b))) = ((c ^ d) v ((a v b) ^ ((c v d) v (a ^ b))))
Theorem	vneulem13 1141	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   ((c ^ d) v ((a v b) ^ ((c v d) v (a ^ b)))) = ((c ^ d) v (a ^ b))
Theorem	vneulem14 1142	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   (((c ^ d) v (a v b)) ^ ((c v d) v (a ^ b))) = ((c ^ d) v (a ^ b))
Theorem	vneulem15 1143	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   ((a v c) ^ (b v d)) = ((((a v b) v c) ^ ((a v c) v d)) ^ (((a v b) v d) ^ ((b v c) v d)))
Theorem	vneulem16 1144	Part of von Neumann's lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   ((((a v b) v c) ^ ((a v c) v d)) ^ (((a v b) v d) ^ ((b v c) v d))) = ((a ^ b) v (c ^ d))
Theorem	vneulem 1145	von Neumann's modular law lemma. Lemma 9, Kalmbach p. 96
((a v b) ^ (c v d)) = 0   =>   ((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))
Theorem	vneulemexp 1146	Expanded version of vneulem 1145.
((a v b) ^ (c v d)) = 0   =>   ((a v c) ^ (b v d)) = ((a ^ b) v (c ^ d))
Arguesian law
Axiom	ax-arg 1147	The Arguesian law as an axiom.
((a0 v b0) ^ (a1 v b1)) =< (a2 v b2)   =>   ((a0 v a1) ^ (b0 v b1)) =< (((a0 v a2) ^ (b0 v b2)) v ((a1 v a2) ^ (b1 v b2)))
Theorem	dplem15a 1148	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   =>   ((a0 v e) ^ (a1 v b1)) =< (d v b2)
Theorem	dplem15b 1149	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   =>   ((a0 v a1) ^ (e v b1)) =< (((a0 v d) ^ (e v b2)) v ((a1 v d) ^ (b1 v b2)))
Theorem	dplem15c 1150	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   =>   ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< (((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2)) v ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2)))
Theorem	dplem15d 1151	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   =>   (((a0 v (a2 v (a0 ^ (a1 v b1)))) ^ ((b0 ^ (a0 v p0)) v b2)) v ((a1 v (a2 v (a0 ^ (a1 v b1)))) ^ (b1 v b2))) = (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2)))
Theorem	dplem15e 1152	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   =>   (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (a0 ^ (a1 v b1))) ^ (b1 v b2))) =< (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2)))
Theorem	dplem15f 1153	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   =>   (((a0 v a2) ^ ((b0 ^ (a0 v p0)) v b2)) v (((a1 v a2) v (b1 ^ (a0 v a1))) ^ (b1 v b2))) =< (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1))))
Theorem	dplem15g 1154	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   &   c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   =>   (((a1 v a2) ^ (b1 v b2)) v (((a0 v a2) ^ (b0 v b2)) v (b1 ^ (a0 v a1)))) = ((c0 v c1) v (b1 ^ (a0 v a1)))
Theorem	dplem15h 1155	Part of proof (1)=>(5) in Day/Pickering 1982.
d = (a2 v (a0 ^ (a1 v b1)))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   e = (b0 ^ (a0 v p0))   &   c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   =>   ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< ((c0 v c1) v (b1 ^ (a0 v a1)))
Theorem	dp15 1156	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (1)=>(5)
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   p0 = ((a1 v b1) ^ (a2 v b2))   =>   ((a0 v a1) ^ ((b0 ^ (a0 v p0)) v b1)) =< ((c0 v c1) v (b1 ^ (a0 v a1)))
Theorem	dp53lema 1157	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   (b1 v (b0 ^ (a0 v p0))) =< (b1 v ((a0 v a1) ^ (c0 v c1)))
Theorem	dp53lemb 1158	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   (b0 ^ (b1 v (c2 ^ (c0 v c1)))) = (b0 ^ (b1 v ((a0 v a1) ^ (c0 v c1))))
Theorem	dp53lemc 1159	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1)))) = (b0 ^ (b1 v (c2 ^ (c0 v c1))))
Theorem	dp53lemd 1160	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   (b0 ^ (a0 v p0)) =< (b0 ^ (((a0 ^ b0) v b1) v (c2 ^ (c0 v c1))))
Theorem	dp53leme 1161	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   (b0 ^ (a0 v p0)) =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
Theorem	dp53lemf 1162	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   (a0 v p) =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
Theorem	dp53lemg 1163	Part of proof (5)=>(3) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p0 = ((a1 v b1) ^ (a2 v b2))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   p =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
Theorem	dp53 1164	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (5)=>(3)
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   p =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
Theorem	dp34 1165	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(4)
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   p =< ((a0 v b1) v (c2 ^ (c0 v c1)))
Theorem	dp41lema 1166	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   ((a0 v b0) ^ (a1 v b1)) =< ((a0 v b1) v (c2 ^ (c0 v c1)))
Theorem	dp41lemb 1167	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   c2 = ((c2 ^ ((a0 v b0) v b1)) ^ ((a0 v a1) v b1))
Theorem	dp41lemc0 1168	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (((a0 v b0) v b1) ^ ((a0 v a1) v b1)) = ((a0 v b1) v ((a0 v b0) ^ (a1 v b1)))
Theorem	dp41lemc 1169	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   ((c2 ^ ((a0 v b0) v b1)) ^ ((a0 v a1) v b1)) =< (c2 ^ ((a0 v b1) v (c2 ^ (c0 v c1))))
Theorem	dp41lemd 1170	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (c2 ^ ((a0 v b1) v (c2 ^ (c0 v c1)))) = (c2 ^ ((c0 v c1) v (c2 ^ (a0 v b1))))
Theorem	dp41leme 1171	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (c2 ^ ((c0 v c1) v (c2 ^ (a0 v b1)))) =< ((c0 v c1) v ((a0 ^ (b0 v b1)) v (b1 ^ (a0 v a1))))
Theorem	dp41lemf 1172	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   ((c0 v c1) v ((a0 ^ (b0 v b1)) v (b1 ^ (a0 v a1)))) = (((b1 v b2) ^ ((a1 v a2) v (b1 ^ (a0 v a1)))) v ((a0 v a2) ^ ((b0 v b2) v (a0 ^ (b0 v b1)))))
Theorem	dp41lemg 1173	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (((b1 v b2) ^ ((a1 v a2) v (b1 ^ (a0 v a1)))) v ((a0 v a2) ^ ((b0 v b2) v (a0 ^ (b0 v b1))))) = (((b1 v b2) ^ ((a1 v a2) v (a0 ^ (a1 v b1)))) v ((a0 v a2) ^ ((b0 v b2) v (b1 ^ (a0 v b0)))))
Theorem	dp41lemh 1174	Part of proof (4)=>(1) in Day/Pickering 1982. "By CP(a,b)".
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (((b1 v b2) ^ ((a1 v a2) v (a0 ^ (a1 v b1)))) v ((a0 v a2) ^ ((b0 v b2) v (b1 ^ (a0 v b0))))) =< (((b1 v b2) ^ ((a1 v a2) v (a0 ^ (a2 v b2)))) v ((a0 v a2) ^ ((b0 v b2) v (b1 ^ (a2 v b2)))))
Theorem	dp41lemj 1175	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (((b1 v b2) ^ ((a1 v a2) v (a0 ^ (a2 v b2)))) v ((a0 v a2) ^ ((b0 v b2) v (b1 ^ (a2 v b2))))) = (((b1 v b2) ^ ((a1 v a2) v (b2 ^ (a0 v a2)))) v ((a0 v a2) ^ ((b0 v b2) v (a2 ^ (b1 v b2)))))
Theorem	dp41lemk 1176	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   (((b1 v b2) ^ ((a1 v a2) v (b2 ^ (a0 v a2)))) v ((a0 v a2) ^ ((b0 v b2) v (a2 ^ (b1 v b2))))) = ((c0 v (b2 ^ (a0 v a2))) v (c1 v (a2 ^ (b1 v b2))))
Theorem	dp41leml 1177	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   ((c0 v (b2 ^ (a0 v a2))) v (c1 v (a2 ^ (b1 v b2)))) = (c0 v c1)
Theorem	dp41lemm 1178	Part of proof (4)=>(1) in Day/Pickering 1982.
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   c2 =< (c0 v c1)
Theorem	dp41 1179	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (4)=>(1)
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p2 = ((a0 v b0) ^ (a1 v b1))   &   p2 =< (a2 v b2)   =>   c2 =< (c0 v c1)
Theorem	dp32 1180	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (3)=>(2)
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   p =< ((a0 ^ (a1 v (c2 ^ (c0 v c1)))) v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))
Theorem	dp23 1181	Part of theorem from Alan Day and Doug Pickering, "A note on the Arguesian lattice identity," Studia Sci. Math. Hungar. 19:303-305 (1982). (2)=>(3)
c0 = ((a1 v a2) ^ (b1 v b2))   &   c1 = ((a0 v a2) ^ (b0 v b2))   &   c2 = ((a0 v a1) ^ (b0 v b1))   &   p = (((a0 v b0) ^ (a1 v b1)) ^ (a2 v b2))   =>   p =< (a0 v (b0 ^ (b1 v (c2 ^ (c0 v c1)))))