Quantum Logic Explorer - mmtheorems4

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 - 301-400 - Page 4 of 11

Type	Label	Description
Statement
Theorem	nom12 301	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a →2 (a ∩ b)) = (a →1 b)
Theorem	nom13 302	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a →3 (a ∩ b)) = (a →1 b)
Theorem	nom14 303	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a →4 (a ∩ b)) = (a →1 b)
Theorem	nom15 304	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a →5 (a ∩ b)) = (a →1 b)
Theorem	nom20 305	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡0 (a ∩ b)) = (a →1 b)
Theorem	nom21 306	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡1 (a ∩ b)) = (a →1 b)
Theorem	nom22 307	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡2 (a ∩ b)) = (a →1 b)
Theorem	nom23 308	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡3 (a ∩ b)) = (a →1 b)
Theorem	nom24 309	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡4 (a ∩ b)) = (a →1 b)
Theorem	nom25 310	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
(a ≡ (a ∩ b)) = (a →1 b)
Theorem	nom30 311	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((a ∩ b) ≡0 a) = (a →1 b)
Theorem	nom31 312	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((a ∩ b) ≡1 a) = (a →1 b)
Theorem	nom32 313	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((a ∩ b) ≡2 a) = (a →1 b)
Theorem	nom33 314	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((a ∩ b) ≡3 a) = (a →1 b)
Theorem	nom34 315	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((a ∩ b) ≡4 a) = (a →1 b)
Theorem	nom35 316	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
((a ∩ b) ≡ a) = (a →1 b)
Theorem	nom40 317	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) →0 b) = (a →2 b)
Theorem	nom41 318	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) →1 b) = (a →2 b)
Theorem	nom42 319	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) →2 b) = (a →2 b)
Theorem	nom43 320	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) →3 b) = (a →2 b)
Theorem	nom44 321	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) →4 b) = (a →2 b)
Theorem	nom45 322	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) →5 b) = (a →2 b)
Theorem	nom50 323	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) ≡0 b) = (a →2 b)
Theorem	nom51 324	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) ≡1 b) = (a →2 b)
Theorem	nom52 325	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) ≡2 b) = (a →2 b)
Theorem	nom53 326	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) ≡3 b) = (a →2 b)
Theorem	nom54 327	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) ≡4 b) = (a →2 b)
Theorem	nom55 328	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a ∪ b) ≡ b) = (a →2 b)
Theorem	nom60 329	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡0 (a ∪ b)) = (a →2 b)
Theorem	nom61 330	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡1 (a ∪ b)) = (a →2 b)
Theorem	nom62 331	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡2 (a ∪ b)) = (a →2 b)
Theorem	nom63 332	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡3 (a ∪ b)) = (a →2 b)
Theorem	nom64 333	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡4 (a ∪ b)) = (a →2 b)
Theorem	nom65 334	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ≡ (a ∪ b)) = (a →2 b)
Theorem	go1 335	Lemma for proof of Mayet 8-variable "full" equation from 4-variable Godowski equation.
((a ∩ b) ∩ (a →1 b⊥ )) = 0
Theorem	i2or 336	Lemma for disjunction of →2 .
((a →2 c) ∪ (b →2 c)) ≤ ((a ∩ b) →2 c)
Theorem	i1or 337	Lemma for disjunction of →1 .
((c →1 a) ∪ (c →1 b)) ≤ (c →1 (a ∪ b))
Theorem	lei2 338	"Less than" analogue is equal to →2 implication.
(a ≤2 b) = (a →2 b)
Theorem	i5lei1 339	Relevance implication is l.e. Sasaki implication.
(a →5 b) ≤ (a →1 b)
Theorem	i5lei2 340	Relevance implication is l.e. Dishkant implication.
(a →5 b) ≤ (a →2 b)
Theorem	i5lei3 341	Relevance implication is l.e. Kalmbach implication.
(a →5 b) ≤ (a →3 b)
Theorem	i5lei4 342	Relevance implication is l.e. non-tollens implication.
(a →5 b) ≤ (a →4 b)
Axiom	ax-wom 343	2-variable WOML rule.
(a⊥ ∪ (a ∩ b)) = 1    ⇒   (b ∪ (a⊥ ∩ b⊥ )) = 1
Theorem	2vwomr2 344	2-variable WOML rule.
(b ∪ (a⊥ ∩ b⊥ )) = 1    ⇒   (a⊥ ∪ (a ∩ b)) = 1
Theorem	2vwomr1a 345	2-variable WOML rule.
(a →1 b) = 1    ⇒   (a →2 b) = 1
Theorem	2vwomr2a 346	2-variable WOML rule.
(a →2 b) = 1    ⇒   (a →1 b) = 1
Theorem	2vwomlem 347	Lemma from 2-variable WOML rule.
(a →2 b) = 1    &   (b →2 a) = 1    ⇒   (a ≡ b) = 1
Theorem	wr5-2v 348	WOML derived from 2-variable axioms.
(a ≡ b) = 1    ⇒   ((a ∪ c) ≡ (b ∪ c)) = 1
Theorem	wom3 349	Weak orthomodular law for study of weakly orthomodular lattices.
(a ≡ b) = 1    ⇒   a ≤ ((a ∪ c) ≡ (b ∪ c))
Theorem	wlor 350	Weak orthomodular law.
(a ≡ b) = 1    ⇒   ((c ∪ a) ≡ (c ∪ b)) = 1
Theorem	wran 351	Weak orthomodular law.
(a ≡ b) = 1    ⇒   ((a ∩ c) ≡ (b ∩ c)) = 1
Theorem	wlan 352	Weak orthomodular law.
(a ≡ b) = 1    ⇒   ((c ∩ a) ≡ (c ∩ b)) = 1
Theorem	wr2 353	Inference rule of AUQL.
(a ≡ b) = 1    &   (b ≡ c) = 1    ⇒   (a ≡ c) = 1
Theorem	w2or 354	Join both sides with disjunction.
(a ≡ b) = 1    &   (c ≡ d) = 1    ⇒   ((a ∪ c) ≡ (b ∪ d)) = 1
Theorem	w2an 355	Join both sides with conjunction.
(a ≡ b) = 1    &   (c ≡ d) = 1    ⇒   ((a ∩ c) ≡ (b ∩ d)) = 1
Theorem	w3tr1 356	Transitive inference useful for introducing definitions.
(a ≡ b) = 1    &   (c ≡ a) = 1    &   (d ≡ b) = 1    ⇒   (c ≡ d) = 1
Theorem	w3tr2 357	Transitive inference useful for eliminating definitions.
(a ≡ b) = 1    &   (a ≡ c) = 1    &   (b ≡ d) = 1    ⇒   (c ≡ d) = 1
Theorem	wleoa 358	Relation between two methods of expressing "less than or equal to".
((a ∪ c) ≡ b) = 1    ⇒   ((a ∩ b) ≡ a) = 1
Theorem	wleao 359	Relation between two methods of expressing "less than or equal to".
((c ∩ b) ≡ a) = 1    ⇒   ((a ∪ b) ≡ b) = 1
Theorem	wdf-le1 360	Define 'less than or equal to' analogue for ≡ analogue of =.
((a ∪ b) ≡ b) = 1    ⇒   (a ≤2 b) = 1
Theorem	wdf-le2 361	Define 'less than or equal to' analogue for ≡ analogue of =.
(a ≤2 b) = 1    ⇒   ((a ∪ b) ≡ b) = 1
Theorem	wom4 362	Orthomodular law. Kalmbach 83 p. 22.
(a ≤2 b) = 1    ⇒   ((a ∪ (a⊥ ∩ b)) ≡ b) = 1
Theorem	wom5 363	Orthomodular law. Kalmbach 83 p. 22.
(a ≤2 b) = 1    &   ((b ∩ a⊥ ) ≡ 0) = 1    ⇒   (a ≡ b) = 1
Theorem	wcomlem 364	Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22.
(a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1    ⇒   (b ≡ ((b ∩ a) ∪ (b ∩ a⊥ ))) = 1
Theorem	wdf-c1 365	Show that commutator is a 'commutes' analogue for ≡ analogue of =.
(a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1    ⇒    C (a, b) = 1
Theorem	wdf-c2 366	Show that commutator is a 'commutes' analogue for ≡ analogue of =.
C (a, b) = 1    ⇒   (a ≡ ((a ∩ b) ∪ (a ∩ b⊥ ))) = 1
Theorem	wdf2le1 367	Alternate definition of 'less than or equal to'.
((a ∩ b) ≡ a) = 1    ⇒   (a ≤2 b) = 1
Theorem	wdf2le2 368	Alternate definition of 'less than or equal to'.
(a ≤2 b) = 1    ⇒   ((a ∩ b) ≡ a) = 1
Theorem	wleo 369	L.e. absorption.
(a ≤2 (a ∪ b)) = 1
Theorem	wlea 370	L.e. absorption.
((a ∩ b) ≤2 a) = 1
Theorem	wle1 371	Anything is l.e. 1.
(a ≤2 1) = 1
Theorem	wle0 372	0 is l.e. anything.
(0 ≤2 a) = 1
Theorem	wler 373	Add disjunct to right of l.e.
(a ≤2 b) = 1    ⇒   (a ≤2 (b ∪ c)) = 1
Theorem	wlel 374	Add conjunct to left of l.e.
(a ≤2 b) = 1    ⇒   ((a ∩ c) ≤2 b) = 1
Theorem	wleror 375	Add disjunct to right of both sides
(a ≤2 b) = 1    ⇒   ((a ∪ c) ≤2 (b ∪ c)) = 1
Theorem	wleran 376	Add conjunct to right of both sides
(a ≤2 b) = 1    ⇒   ((a ∩ c) ≤2 (b ∩ c)) = 1
Theorem	wlecon 377	Contrapositive for l.e.
(a ≤2 b) = 1    ⇒   (b⊥ ≤2 a⊥ ) = 1
Theorem	wletr 378	Transitive law for l.e.
(a ≤2 b) = 1    &   (b ≤2 c) = 1    ⇒   (a ≤2 c) = 1
Theorem	wbltr 379	Transitive inference.
(a ≡ b) = 1    &   (b ≤2 c) = 1    ⇒   (a ≤2 c) = 1
Theorem	wlbtr 380	Transitive inference.
(a ≤2 b) = 1    &   (b ≡ c) = 1    ⇒   (a ≤2 c) = 1
Theorem	wle3tr1 381	Transitive inference useful for introducing definitions.
(a ≤2 b) = 1    &   (c ≡ a) = 1    &   (d ≡ b) = 1    ⇒   (c ≤2 d) = 1
Theorem	wle3tr2 382	Transitive inference useful for eliminating definitions.
(a ≤2 b) = 1    &   (a ≡ c) = 1    &   (b ≡ d) = 1    ⇒   (c ≤2 d) = 1
Theorem	wbile 383	Biconditional to l.e.
(a ≡ b) = 1    ⇒   (a ≤2 b) = 1
Theorem	wlebi 384	L.e. to biconditional.
(a ≤2 b) = 1    &   (b ≤2 a) = 1    ⇒   (a ≡ b) = 1
Theorem	wle2or 385	Disjunction of 2 l.e.'s
(a ≤2 b) = 1    &   (c ≤2 d) = 1    ⇒   ((a ∪ c) ≤2 (b ∪ d)) = 1
Theorem	wle2an 386	Conjunction of 2 l.e.'s
(a ≤2 b) = 1    &   (c ≤2 d) = 1    ⇒   ((a ∩ c) ≤2 (b ∩ d)) = 1
Theorem	wledi 387	Half of distributive law.
(((a ∩ b) ∪ (a ∩ c)) ≤2 (a ∩ (b ∪ c))) = 1
Theorem	wledio 388	Half of distributive law.
((a ∪ (b ∩ c)) ≤2 ((a ∪ b) ∩ (a ∪ c))) = 1
Theorem	wcom0 389	Commutation with 0. Kalmbach 83 p. 20.
C (a, 0) = 1
Theorem	wcom1 390	Commutation with 1. Kalmbach 83 p. 20.
C (1, a) = 1
Theorem	wlecom 391	Comparable elements commute. Beran 84 2.3(iii) p. 40.
(a ≤2 b) = 1    ⇒    C (a, b) = 1
Theorem	wbctr 392	Transitive inference.
(a ≡ b) = 1    &    C (b, c) = 1    ⇒    C (a, c) = 1
Theorem	wcbtr 393	Transitive inference.
C (a, b) = 1    &   (b ≡ c) = 1    ⇒    C (a, c) = 1
Theorem	wcomorr 394	Weak commutation law.
C (a, (a ∪ b)) = 1
Theorem	wcoman1 395	Weak commutation law.
C ((a ∩ b), a) = 1
Theorem	wcomcom 396	Commutation is symmetric. Kalmbach 83 p. 22.
C (a, b) = 1    ⇒    C (b, a) = 1
Theorem	wcomcom2 397	Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1    ⇒    C (a, b⊥ ) = 1
Theorem	wcomcom3 398	Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1    ⇒    C (a⊥ , b) = 1
Theorem	wcomcom4 399	Commutation equivalence. Kalmbach 83 p. 23.
C (a, b) = 1    ⇒    C (a⊥ , b⊥ ) = 1
Theorem	wcomd 400	Commutation dual. Kalmbach 83 p. 23.
C (a, b) = 1    ⇒   (a ≡ ((a ∪ b) ∩ (a ∪ b⊥ ))) = 1