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

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

Type	Label	Description
Statement
Weakly distributive ortholattices (WDOL)
WDOL law
Axiom	ax-wdol 1101	The WDOL (weakly distributive ortholattice) axiom.
((a == b) v (a == b')) = 1
Theorem	wdcom 1102	Any two variables (weakly) commute in a WDOL.
C (a, b) = 1
Theorem	wdwom 1103	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 1104	Prove the weak distributive law in WDOL. This is our first WDOL theorem making use of ax-wom 361, which is justified by wdwom 1103.
((a ^ (b v c)) == ((a ^ b) v (a ^ c))) = 1
Theorem	wddi2 1105	The weak distributive law in WDOL.
(((a v b) ^ c) == ((a ^ c) v (b ^ c))) = 1
Theorem	wddi3 1106	The weak distributive law in WDOL.
((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1
Theorem	wddi4 1107	The weak distributive law in WDOL.
(((a ^ b) v c) == ((a v c) ^ (b v c))) = 1
Theorem	wdid0id5 1108	Show that quantum identity follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a == b) = 1
Theorem	wdid0id1 1109	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==1 b) = 1
Theorem	wdid0id2 1110	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==2 b) = 1
Theorem	wdid0id3 1111	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==3 b) = 1
Theorem	wdid0id4 1112	Show a quantum identity that follows from classical identity in a WDOL.
(a ==0 b) = 1   =>   (a ==4 b) = 1
Theorem	wdka4o 1113	Show WDOL analog of WOM law.
(a ==0 b) = 1   =>   ((a v c) ==0 (b v c)) = 1
Theorem	wddi-0 1114	The weak distributive law in WDOL.
((a ^ (b v c)) ==0 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-1 1115	The weak distributive law in WDOL.
((a ^ (b v c)) ==1 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-2 1116	The weak distributive law in WDOL.
((a ^ (b v c)) ==2 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-3 1117	The weak distributive law in WDOL.
((a ^ (b v c)) ==3 ((a ^ b) v (a ^ c))) = 1
Theorem	wddi-4 1118	The weak distributive law in WDOL.
((a ^ (b v c)) ==4 ((a ^ b) v (a ^ c))) = 1