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 v b) ->0 b) = (a ->2 b)
Theorem	nom41 318	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ->1 b) = (a ->2 b)
Theorem	nom42 319	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ->2 b) = (a ->2 b)
Theorem	nom43 320	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ->3 b) = (a ->2 b)
Theorem	nom44 321	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ->4 b) = (a ->2 b)
Theorem	nom45 322	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ->5 b) = (a ->2 b)
Theorem	nom50 323	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ==0 b) = (a ->2 b)
Theorem	nom51 324	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ==1 b) = (a ->2 b)
Theorem	nom52 325	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ==2 b) = (a ->2 b)
Theorem	nom53 326	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ==3 b) = (a ->2 b)
Theorem	nom54 327	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) ==4 b) = (a ->2 b)
Theorem	nom55 328	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
((a v b) == b) = (a ->2 b)
Theorem	nom60 329	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ==0 (a v b)) = (a ->2 b)
Theorem	nom61 330	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ==1 (a v b)) = (a ->2 b)
Theorem	nom62 331	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ==2 (a v b)) = (a ->2 b)
Theorem	nom63 332	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ==3 (a v b)) = (a ->2 b)
Theorem	nom64 333	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b ==4 (a v b)) = (a ->2 b)
Theorem	nom65 334	Part of Lemma 3.3(15) from "Non-Orthomodular Models..." paper.
(b == (a v 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) v (b ->2 c)) =< ((a ^ b) ->2 c)
Theorem	i1or 337	Lemma for disjunction of ->1.
((c ->1 a) v (c ->1 b)) =< (c ->1 (a v 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_|_ v (a ^ b)) = 1   =>   (b v (a_|_ ^ b_|_)) = 1
Theorem	2vwomr2 344	2-variable WOML rule.
(b v (a_|_ ^ b_|_)) = 1   =>   (a_|_ v (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 v c) == (b v c)) = 1
Theorem	wom3 349	Weak orthomodular law for study of weakly orthomodular lattices.
(a == b) = 1   =>   a =< ((a v c) == (b v c))
Theorem	wlor 350	Weak orthomodular law.
(a == b) = 1   =>   ((c v a) == (c v 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 v c) == (b v 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 v 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 v b) == b) = 1
Theorem	wdf-le1 360	Define 'less than or equal to' analogue for == analogue of =.
((a v 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 v b) == b) = 1
Theorem	wom4 362	Orthomodular law. Kalmbach 83 p. 22.
(a =<2 b) = 1   =>   ((a v (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) v (a ^ b_|_))) = 1   =>   (b == ((b ^ a) v (b ^ a_|_))) = 1
Theorem	wdf-c1 365	Show that commutator is a 'commutes' analogue for == analogue of =.
(a == ((a ^ b) v (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) v (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 v 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 v 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 v c) =<2 (b v 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 v c) =<2 (b v 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) v (a ^ c)) =<2 (a ^ (b v c))) = 1
Theorem	wledio 388	Half of distributive law.