mmtheorems9 - 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 - 801-900 - Page 9 of 12

Type	Label	Description
Statement
Theorem	i1abs 801	An absorption law for ->1.
((a ->1 b)' v (a ^ b)) = a
Theorem	test 802	Part of an attempt to crack a potential Kalmbach axiom.
(((c v (a' v b')) ^ (c' ^ (c v (a ^ b)))) v ((c' ^ (a ^ b)) v (c ^ (c' v (a ^ b))))) = ((c v (a ^ b)) ^ (c' v (a ^ b)))
Theorem	test2 803	Part of an attempt to crack a potential Kalmbach axiom.
(a v b) =< ((a == b)' v ((c v (a ^ b)) ^ (c' v (a ^ b))))
Some 3-variable theorems
Theorem	3vth1 804	A 3-variable theorem. Equivalent to OML.
((a ->2 b) ^ (b v c)') =< (a ->2 c)
Theorem	3vth2 805	A 3-variable theorem. Equivalent to OML.
((a ->2 b) ^ (b v c)') = ((a ->2 c) ^ (b v c)')
Theorem	3vth3 806	A 3-variable theorem. Equivalent to OML.
((a ->2 c) v ((a ->2 b) ^ (b v c)')) = (a ->2 c)
Theorem	3vth4 807	A 3-variable theorem.
((a ->2 b)' ->2 (b v c)) = ((a ->2 c)' ->2 (b v c))
Theorem	3vth5 808	A 3-variable theorem.
((a ->2 b)' ->2 (b v c)) = (c v ((a ->2 b) ^ (c ->2 b)))
Theorem	3vth6 809	A 3-variable theorem.
((a ->2 b)' ->2 (b v c)) = (((a ->2 b) ^ (c ->2 b)) v ((a ->2 c) ^ (b ->2 c)))
Theorem	3vth7 810	A 3-variable theorem.
((a ->2 b)' ->2 (b v c)) = (a ->2 (b v c))
Theorem	3vth8 811	A 3-variable theorem.
(a ->2 (b v c)) = (((a ->2 b) ^ (c ->2 b)) v ((a ->2 c) ^ (b ->2 c)))
Theorem	3vth9 812	A 3-variable theorem.
((a v b) ->1 (c ->2 b)) = ((b v c) ->2 (a ->2 b))
Theorem	3vcom 813	3-variable commutation theorem
((a ->1 c) v (b ->1 c)) C ((a' ->1 c) ^ (b' ->1 c))
Theorem	3vded11 814	A 3-variable theorem. Experiment with weak deduction theorem.
b =< (c ->1 (b ->1 a))   =>   c =< (b ->1 a)
Theorem	3vded12 815	A 3-variable theorem. Experiment with weak deduction theorem.
(a ^ (c ->1 a)) =< (c ->1 (b ->1 a))   &   c =< a   =>   c =< (b ->1 a)
Theorem	3vded13 816	A 3-variable theorem. Experiment with weak deduction theorem.
(b ^ (c ->1 a)) =< (c ->1 (b ->1 a))   &   c =< a   =>   c =< (b ->1 a)
Theorem	3vded21 817	A 3-variable theorem. Experiment with weak deduction theorem.
c =< ((a ->0 b) ->0 (c ->2 b))   &   c =< (a ->0 b)   =>   c =< b
Theorem	3vded22 818	A 3-variable theorem. Experiment with weak deduction theorem.
c =< ( C (a, b) v C (c, b))   &   c =< a   &   c =< (a ->0 b)   =>   c =< b
Theorem	3vded3 819	A 3-variable theorem. Experiment with weak deduction theorem.
(c ->0 C (a, c)) = 1   &   (c ->0 a) = 1   &   (c ->0 (a ->0 b)) = 1   =>   (c ->0 b) = 1
Theorem	1oa 820	Orthoarguesian-like law with ->1 instead of ->0 but true in all OMLs.
((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Theorem	1oai1 821	Orthoarguesian-like OM law.
((a ->1 c) ^ ((a ^ b)' ->1 ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
Theorem	2oai1u 822	Orthoarguesian-like OM law.
((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c))' ->2 ((a' ->1 c) ^ (b' ->1 c)))) =< (b ->1 c)
Theorem	1oaiii 823	OML analog to orthoarguesian law of Godowski/Greechie, Eq. III with ->1 instead of ->0.
((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 c) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c))))
Theorem	1oaii 824	OML analog to orthoarguesian law of Godowski/Greechie, Eq. II with ->1 instead of ->0.
(b' ^ ((a ->2 b) v ((a ->2 c) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))))) =< a'
Theorem	2oalem1 825	Lemma for OA-like stuff with ->2 instead of ->0.
Theorem	2oath1 826	OA-like theorem with ->2 instead of ->0.
((a ->2 b) ^ ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ (a ->2 c))
Theorem	2oath1i1 827	Orthoarguesian-like OM law.
((a ->1 c) ^ ((a ^ b)' ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ->1 c) ^ (b ->1 c))
Theorem	1oath1i1u 828	Orthoarguesian-like OM law.
((a ->1 c) ^ (((a ->1 c) ^ (b ->1 c))' ->1 ((a' ->1 c) ^ (b' ->1 c)))) = ((a ->1 c) ^ (b ->1 c))
Theorem	oale 829	Relation for studying OA.
((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))') =< (a ->2 c)
Theorem	oaeqv 830	Weakened OA implies OA).
((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< ((b v c) ->2 ((a ->2 b) ^ (a ->2 c)))   =>   ((a ->2 b) ^ ((b v c)' v ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Theorem	3vroa 831	OA-like inference rule (requires OM only).
((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))) = 1   =>   (a ->2 c) = 1
Theorem	mlalem 832	Lemma for Mladen's OML.
Theorem	mlaoml 833	Mladen's OML.
((a == b) ^ (b == c)) =< (a == c)
Theorem	eqtr4 834	4-variable transitive law for equivalence.
(((a == b) ^ (b == c)) ^ (c == d)) =< (a == d)
Theorem	sac 835	Theorem showing "Sasaki complement" is an operation.
(a ->1 c) = (b ->1 c)   =>   (a' ->1 c) = (b' ->1 c)
Theorem	sa5 836	Possible axiom for a "Sasaki algebra" for orthoarguesian lattices.
(a ->1 c) =< (b ->1 c)   =>   (b' ->1 c) =< ((a' ->1 c) v c)
Theorem	salem1 837	Lemma for attempt at Sasaki algebra.
Theorem	sadm3 838	Weak DeMorgan's law for attempt at Sasaki algebra.
(((a' ->1 c) ^ (b' ->1 c)) ->1 c) =< ((a ->1 c) v (b ->1 c))
Theorem	bi3 839	Chained biconditional.
((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
Theorem	bi4 840	Chained biconditional.
(((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) ^ d) v (((a' ^ b') ^ c') ^ d'))
Theorem	imp3 841	Implicational product with 3 variables. Theorem 3.20 of "Equations, states, and lattices..." paper.
((a ->2 b) ^ (b ->1 c)) = ((a' ^ b') v (b ^ c))
Theorem	orbi 842	Disjunction of biconditionals.
((a == c) v (b == c)) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
Theorem	orbile 843	Disjunction of biconditionals.
((a == c) v (b == c)) =< (((a ^ b) ->2 c) ^ (c ->1 (a v b)))
Theorem	mlaconj4 844	For 4GO proof of Mladen's conjecture, that it follows from Eq. (3.30) in OA-GO paper.
((d == e) ^ ((e' ^ c') v (d ^ c))) =< (d == c)   &   d = (a v b)   &   e = (a ^ b)   =>   ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
Theorem	mlaconj 845	For 5GO proof of Mladen's conjecture.
((a == b) ^ ((a == c) v (b == c))) =< ((((a ->1 (a ^ b)) ^ ((a ^ b) ->1 ((a ^ b) v c))) ^ ((((a ^ b) v c) ->1 c) ^ (c ->1 (a v b)))) ^ ((a v b) ->1 a))
Theorem	mlaconj2 846	For 5GO proof of Mladen's conjecture. Hypothesis is 5GO law consequence.
((((a ->1 (a ^ b)) ^ ((a ^ b) ->1 ((a ^ b) v c))) ^ ((((a ^ b) v c) ->1 c) ^ (c ->1 (a v b)))) ^ ((a v b) ->1 a)) =< (a == c)   =>   ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
Theorem	i1orni1 847	Complemented antecedent lemma.
((a ->1 b) v (a' ->1 b)) = 1
Theorem	negantlem1 848	Lemma for negated antecedent identity.
Theorem	negantlem2 849	Lemma for negated antecedent identity.
Theorem	negantlem3 850	Lemma for negated antecedent identity.
Theorem	negantlem4 851	Lemma for negated antecedent identity.
Theorem	negant 852	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a' ->1 c) = (b' ->1 c)
Theorem	negantlem5 853	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a' ^ c') = (b' ^ c')
Theorem	negantlem6 854	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a ^ c') = (b ^ c')
Theorem	negantlem7 855	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a v c) = (b v c)
Theorem	negantlem8 856	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a' v c) = (b