mmtheorems11 - 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 - 1001-1100 - Page 11 of 12

Type	Label	Description
Statement
Theorem	oaliii 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))))
Theorem	oalii 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'
Theorem	oaliv 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)))
Theorem	oath1 1004	OA theorem.
((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (a ->2 c))
Theorem	oalem1 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))
Theorem	oalem2 1006	Lemma
((a ->2 b) v ((a ->2 c) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c))))) = (a ->2 b)
Theorem	oadist2a 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)))))
Theorem	oadist2b 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)))))
Theorem	oadist2 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)))))
Theorem	oadist12 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)))))
Theorem	oacom 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))
Theorem	oacom2 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))
Theorem	oacom3 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))
Theorem	oagen1 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))
Theorem	oagen1b 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))
Theorem	oagen2 1016	"Generalized" OA.
d =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ d) =< (a ->2 c)
Theorem	oagen2b 1017	"Generalized" OA.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   (d ^ e) =< (a ->2 c)
Theorem	mloa 1018	Mladen's OA
((a == b) ^ ((b == c) v ((b v (a == b)) ^ (c v (a == c))))) =< (c v (a == c))
Theorem	oadist 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))))
Theorem	oadistb 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))))
Theorem	oadistc0 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)
Theorem	oadistc 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))
Theorem	oadistd 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))
Theorem	3oa2 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)
Theorem	3oa3 1025	3-variable orthoarguesion law expressed with the 3OA identity abbreviation.
((a ->1 c) ^ (a == c ==OA b)) =< (b ->1 c)
4-variable orthoarguesian law
Axiom	ax-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)))))
Theorem	oa4cl 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'))))))
Theorem	oa43v 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)
6-variable orthoarguesian law
Axiom	ax-oa6 1029	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)))))))
Theorem	oa64v 1030	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)))))
Theorem	oa63v 1031	Derivation of 3-variable OA from 6-variable OA.
((a ->2 b) ^