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

Statement List for Quantum Logic Explorer - 1001-1100 - Page 11 of 12

Type	Label	Description
Statement
Theorem	oagen1b 1001	"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 1002	"Generalized" OA.
d =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ d) =< (a ->2 c)
Theorem	oagen2b 1003	"Generalized" OA.
d =< (a ->2 b)   &   e =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))   =>   (d ^ e) =< (a ->2 c)
Theorem	mloa 1004	Mladen's OA
((a == b) ^ ((b == c) v ((b v (a == b)) ^ (c v (a == c))))) =< (c v (a == c))
Theorem	oadist 1005	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 1006	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 1007	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 1008	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 1009	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 1010	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 1011	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 1012	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 1013	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 1014	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 1015	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 1016	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 1017	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)
The proper 4-variable orthoarguesian law
Axiom	ax-4oa 1018	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)
Theorem	axoa4 1019	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
Theorem	axoa4b 1020	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
Theorem	oa6 1021	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)))))))
Theorem	axoa4a 1022	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))
Theorem	axoa4d 1023	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)
Theorem	4oa 1024	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)
Theorem	4oaiii 1025	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)
Theorem	4oath1 1026	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))
Theorem	4oagen1 1027	"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))
Theorem	4oagen1b 1028	"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