Quantum Logic Explorer - mmtheorems9

Jump to page: 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-1024

Statement List for Quantum Logic Explorer - 801-900 - Page 9 of 11

Type	Label	Description
Statement
Theorem	3vded3 801	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 802	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 803	Orthoarguesian-like OM law.
((a ->1 c) ^ ((a ^ b)_|_ ->1 ((a ->1 c) ^ (b ->1 c)))) =< (b ->1 c)
Theorem	2oai1u 804	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 805	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 806	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 807	Lemma for OA-like stuff with ->2 instead of ->0.
((a ->2 b)_|_ v ((b v c) v ((a ->2 b) ^ (a ->2 c)))) = 1
Theorem	2oath1 808	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 809	Orthoarguesian-like OM law.
((a ->1 c) ^ ((a ^ b)_|_ ->2 ((a ->1 c) ^ (b ->1 c)))) = ((a ->1 c) ^ (b ->1 c))
Theorem	1oath1i1u 810	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 811	Relation for studying OA.
((a ->2 b) ^ ((b v c) v ((a ->2 b) ^ (a ->2 c)))_|_) =< (a ->2 c)
Theorem	oaeqv 812	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 813	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 814	Lemma for Mladen's OML.
((a == b) ^ (b ->1 c)) =< (a ->1 c)
Theorem	mlaoml 815	Mladen's OML.
((a == b) ^ (b == c)) =< (a == c)
Theorem	eqtr4 816	4-variable transitive law for equivalence.
(((a == b) ^ (b == c)) ^ (c == d)) =< (a == d)
Theorem	sac 817	Theorem showing "Sasaki complement" is an operation.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->1 c) = (b_|_ ->1 c)
Theorem	sa5 818	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 819	Lemma for attempt at Sasaki algebra.
(((a_|_ ->1 b) v b) ->1 b) = (a ->2 b)
Theorem	sadm3 820	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 821	Chained biconditional.
((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a_|_ ^ b_|_) ^ c_|_))
Theorem	bi4 822	Chained biconditional.
(((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) ^ d) v (((a_|_ ^ b_|_) ^ c_|_) ^ d_|_))
Theorem	imp3 823	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 824	Disjunction of biconditionals.
((a == c) v (b == c)) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
Theorem	orbile 825	Disjunction of biconditionals.
((a == c) v (b == c)) =< (((a ^ b) ->2 c) ^ (c ->1 (a v b)))
Theorem	mlaconj4 826	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 827	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 828	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 829	Complemented antecedent lemma.
((a ->1 b) v (a_|_ ->1 b)) = 1
Theorem	negantlem1 830	Lemma for negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   a C (b ->1 c)
Theorem	negantlem2 831	Lemma for negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   a =< (b_|_ ->1 c)
Theorem	negantlem3 832	Lemma for negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ^ c) =< (b_|_ ->1 c)
Theorem	negantlem4 833	Lemma for negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->1 c) =< (b_|_ ->1 c)
Theorem	negant 834	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->1 c) = (b_|_ ->1 c)
Theorem	negantlem5 835	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ^ c_|_) = (b_|_ ^ c_|_)
Theorem	negantlem6 836	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a ^ c_|_) = (b ^ c_|_)
Theorem	negantlem7 837	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a v c) = (b v c)
Theorem	negantlem8 838	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ v c) = (b_|_ v c)
Theorem	negant0 839	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->0 c) = (b_|_ ->0 c)
Theorem	negant2 840	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->2 c) = (b_|_ ->2 c)
Theorem	negantlem9 841	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a ->3 c) =< (b ->3 c)
Theorem	negant3 842	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->3 c) = (b_|_ ->3 c)
Theorem	negantlem10 843	Lemma for negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a ->4 c) =< (b ->4 c)
Theorem	negant4 844	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->4 c) = (b_|_ ->4 c)
Theorem	negant5 845	Negated antecedent identity.
(a ->1 c) = (b ->1 c)   =>   (a_|_ ->5 c) = (b_|_ ->5 c)
Theorem	neg3antlem1 846	Lemma for negated antecedent identity.
(a ->3 c) = (b ->3 c)   =>   (a ^ c) =< (b ->1 c)
Theorem	neg3antlem2 847	Lemma for negated antecedent identity.
(a ->3 c) = (b ->3 c)   =>   a_|_ =< (b ->1 c)
Theorem	neg3ant1 848	Lemma for negated antecedent identity.
(a ->3 c) = (b ->3 c)   =>   (a ->1 c) = (b ->1 c)
Theorem	elimconslem 849	Lemma for consequent elimination law.
(a ->1 c) = (b ->1 c)   &   (a ^ c) =< (b v c_|_)   =>   a =< (b v c_|_)
Theorem	elimcons 850	Consequent elimination law.
(a ->1 c) = (b ->1 c)   &   (a ^ c) =< (b v c_|_)   =>   a =< b
Theorem	elimcons2 851	Consequent elimination law.
(a ->1 c) = (b ->1 c)   &   (a ^ (c ^ (b ->1 c))) =< (b v (c_|_ v (a ->1 c)_|_))   =>   a =< b
Theorem	comanblem1 852	Lemma for biconditional commutation law.
((a == c) ^ (b == c)) = (((a v c)_|_ v ((a ^ b) ^ c)) ^ (b ->1 c))
Theorem	comanblem2 853	Lemma for biconditional commutation law.
((a ^ b) ^ ((a == c) ^ (b == c))) = ((a ^ b) ^ c)
Theorem	comanb 854	Biconditional commutation law.