Home	Quantum Logic Explorer Theorem List (p. 4 of 13)	< Previous  Next >
		Browser slow? Try the Unicode version.
Mirrors  >  Metamath Home Page  >  QLE Home Page  >  Theorem List Contents       This page: Page List

---

Theorem List for Quantum Logic Explorer - 301-400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nomcon0 301	Lemma for "Non-Orthomodular Models..." paper.
Theorem	nomcon1 302	Lemma for "Non-Orthomodular Models..." paper.
Theorem	nomcon2 303	Lemma for "Non-Orthomodular Models..." paper.
Theorem	nomcon3 304	Lemma for "Non-Orthomodular Models..." paper.
Theorem	nomcon4 305	Lemma for "Non-Orthomodular Models..." paper.
Theorem	nomcon5 306	Lemma for "Non-Orthomodular Models..." paper.
Theorem	nom10 307	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom11 308	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom12 309	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom13 310	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom14 311	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom15 312	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom20 313	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom21 314	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom22 315	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom23 316	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom24 317	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom25 318	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom30 319	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom31 320	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom32 321	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom33 322	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom34 323	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom35 324	Part of Lemma 3.3(14) from "Non-Orthomodular Models..." paper.
Theorem	nom40 325	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom41 326	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom42 327	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom43 328	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom44 329	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom45 330	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom50 331	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom51 332	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom52 333	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom53 334	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom54 335	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom55 336	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom60 337	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom61 338	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom62 339	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom63 340	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom64 341	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	nom65 342	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
Theorem	go1 343	Lemma for proof of Mayet 8-variable "full" equation from 4-variable Godowski equation.
Theorem	i2or 344	Lemma for disjunction of .
Theorem	i1or 345	Lemma for disjunction of .
Theorem	lei2 346	"Less than" analogue is equal to implication.
Theorem	i5lei1 347	Relevance implication is l.e. Sasaki implication.
Theorem	i5lei2 348	Relevance implication is l.e. Dishkant implication.
Theorem	i5lei3 349	Relevance implication is l.e. Kalmbach implication.
Theorem	i5lei4 350	Relevance implication is l.e. non-tollens implication.
Theorem	id5leid0 351	Quantum identity is less than classical identity.
Theorem	id5id0 352	Show that classical identity follows from quantum identity in OL.
Theorem	k1-6 353	Statement (6) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-7 354	Statement (7) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-8a 355	First part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-8b 356	Second part of statement (8) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-2 357	Statement (2) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-3 358	Statement (3) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-4 359	Statement (4) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
Theorem	k1-5 360	Statement (5) in proof of Theorem 1 of Kalmbach, Orthomodular Lattices, p. 21.
0.2  Weakly orthomodular lattices
0.2.1  Weak orthomodular law
Axiom	ax-wom 361	2-variable WOML rule.
Theorem	2vwomr2 362	2-variable WOML rule.
Theorem	2vwomr1a 363	2-variable WOML rule.
Theorem	2vwomr2a 364	2-variable WOML rule.
Theorem	2vwomlem 365	Lemma from 2-variable WOML rule.
Theorem	wr5-2v 366	WOML derived from 2-variable axioms.
0.2.2  Weakly orthomodular lattices
Theorem	wom3 367	Weak orthomodular law for study of weakly orthomodular lattices.
Theorem	wlor 368	Weak orthomodular law.
Theorem	wran 369	Weak orthomodular law.
Theorem	wlan 370	Weak orthomodular law.
Theorem	wr2 371	Inference rule of AUQL.
Theorem	w2or 372	Join both sides with disjunction.
Theorem	w2an 373	Join both sides with conjunction.
Theorem	w3tr1 374	Transitive inference useful for introducing definitions.
Theorem	w3tr2 375	Transitive inference useful for eliminating definitions.
0.2.3  Relationship analogues (ordering; commutation) in WOML
Theorem	wleoa 376	Relation between two methods of expressing "less than or equal to".
Theorem	wleao 377	Relation between two methods of expressing "less than or equal to".
Theorem	wdf-le1 378	Define 'less than or equal to' analogue for analogue of .
Theorem	wdf-le2 379	Define 'less than or equal to' analogue for analogue of .
Theorem	wom4 380	Orthomodular law. Kalmbach 83 p. 22.
Theorem	wom5 381	Orthomodular law. Kalmbach 83 p. 22.
Theorem	wcomlem 382	Analogue of commutation is symmetric. Similar to Kalmbach 83 p. 22.
Theorem	wdf-c1 383	Show that commutator is a 'commutes' analogue for analogue of .
Theorem	wdf-c2 384	Show that commutator is a 'commutes' analogue for analogue of .
Theorem	wdf2le1 385	Alternate definition of 'less than or equal to'.
Theorem	wdf2le2 386	Alternate definition of 'less than or equal to'.
Theorem	wleo 387	L.e. absorption.
Theorem	wlea 388	L.e. absorption.
Theorem	wle1 389	Anything is l.e. 1.
Theorem	wle0 390	0 is l.e. anything.
Theorem	wler 391	Add disjunct to right of l.e.
Theorem	wlel 392	Add conjunct to left of l.e.
Theorem	wleror 393	Add disjunct to right of both sides.
Theorem	wleran 394	Add conjunct to right of both sides.
Theorem	wlecon 395	Contrapositive for l.e.
Theorem	wletr 396	Transitive law for l.e.
Theorem	wbltr 397	Transitive inference.
Theorem	wlbtr 398	Transitive inference.
Theorem	wle3tr1 399	Transitive inference useful for introducing definitions.
Theorem	wle3tr2 400	Transitive inference useful for eliminating definitions.

< Previous  Next >

---

Page List 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-1200 13 1201-1215

---

Copyright terms: Public domain

< Previous  Next >