mmdefinitions - Quantum Logic Explorer

List of Syntax, Axioms (ax-) and Definitions (df-)

Ref	Expression (see link for any distinct variable requirements)
wb 1	wff  a = b
wle 2	wff  a ≤ b
wc 3	wff  a C b
wn 4	term  a⊥
tb 5	term  (a ≡ b)
wo 6	term  (a ∪ b)
wa 7	term  (a ∩ b)
wt 8	term  1
wf 9	term  0
wle2 10	term  (a ≤2 b)
wi0 11	term  (a →0 b)
wi1 12	term  (a →1 b)
wi2 13	term  (a →2 b)
wi3 14	term  (a →3 b)
wi4 15	term  (a →4 b)
wi5 16	term  (a →5 b)
wid0 17	term  (a ≡0 b)
wid1 18	term  (a ≡1 b)
wid2 19	term  (a ≡2 b)
wid3 20	term  (a ≡3 b)
wid4 21	term  (a ≡4 b)
wid5 22	term  (a ≡5 b)
wb3 23	term  (a ↔3 b)
wb1 24	term  (a ↔1 b)
wo3 25	term  (a ∪3 b)
wan3 26	term  (a ∩3 b)
wid3oa 27	term  (a ≡ c ≡OA b)
wid4oa 28	term  (a ≡ c, d ≡OA b)
wcmtr 29	term  C (a, b)
ax-a1 30	a = a⊥ ⊥
ax-a2 31	(a ∪ b) = (b ∪ a)
ax-a3 32	((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
ax-a4 33	(a ∪ (b ∪ b⊥ )) = (b ∪ b⊥ )
ax-a5 34	(a ∪ (a⊥ ∪ b)⊥ ) = a
ax-r1 35	a = b    ⇒   b = a
ax-r2 36	a = b    &   b = c    ⇒   a = c
ax-r4 37	a = b    ⇒   a⊥ = b⊥
ax-r5 38	a = b    ⇒   (a ∪ c) = (b ∪ c)
df-b 39	(a ≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
df-a 40	(a ∩ b) = (a⊥ ∪ b⊥ )⊥
df-t 41	1 = (a ∪ a⊥ )
df-f 42	0 = 1⊥
df-i0 43	(a →0 b) = (a⊥ ∪ b)
df-i1 44	(a →1 b) = (a⊥ ∪ (a ∩ b))
df-i2 45	(a →2 b) = (b ∪ (a⊥ ∩ b⊥ ))
df-i3 46	(a →3 b) = (((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )) ∪ (a ∩ (a⊥ ∪ b)))
df-i4 47	(a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
df-i5 48	(a →5 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ (a⊥ ∩ b⊥ ))
df-id0 49	(a ≡0 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ a))
df-id1 50	(a ≡1 b) = ((a ∪ b⊥ ) ∩ (a⊥ ∪ (a ∩ b)))
df-id2 51	(a ≡2 b) = ((a ∪ b⊥ ) ∩ (b ∪ (a⊥ ∩ b⊥ )))
df-id3 52	(a ≡3 b) = ((a⊥ ∪ b) ∩ (a ∪ (a⊥ ∩ b⊥ )))
df-id4 53	(a ≡4 b) = ((a⊥ ∪ b) ∩ (b⊥ ∪ (a ∩ b)))
df-o3 54	(a ∪3 b) = (a⊥ →3 (a⊥ →3 b))
df-a3 55	(a ∩3 b) = (a⊥ ∪3 b⊥ )⊥
df-b3 56	(a ↔3 b) = ((a →3 b) ∩ (b →3 a))
df-id3oa 57	(a ≡ c ≡OA b) = (((a →1 c) ∩ (b →1 c)) ∪ ((a⊥ →1 c) ∩ (b⊥ →1 c)))
df-id4oa 58	(a ≡ c, d ≡OA b) = ((a ≡ d ≡OA b) ∪ ((a ≡ d ≡OA c) ∩ (b ≡ d ≡OA c)))
df-le 129	(a ≤2 b) = ((a ∪ b) ≡ b)
df-le1 130	(a ∪ b) = b    ⇒   a ≤ b
df-le2 131	a ≤ b    ⇒   (a ∪ b) = b
df-c1 132	a = ((a ∩ b) ∪ (a ∩ b⊥ ))    ⇒   a C b
df-c2 133	a C b    ⇒   a = ((a ∩ b) ∪ (a ∩ b⊥ ))
df-cmtr 134	C (a, b) = (((a ∩ b) ∪ (a ∩ b⊥ )) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ b⊥ )))
ax-wom 361	(a⊥ ∪ (a ∩ b)) = 1    ⇒   (b ∪ (a⊥ ∩ b⊥ )) = 1
ax-r3 439	(c ∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )    ⇒   a = b
ax-oadist 994	e = (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d))))    &   f = (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ e)    &   h ≤ (a →1 d)    &   j ≤ f    &   k ≤ f    &   (h ∩ (b →1 d)) ≤ k    ⇒   (h ∩ (j ∪ k)) = ((h ∩ j) ∪ (h ∩ k))
ax-3oa 998	((a →1 c) ∩ ((a ∩ b) ∪ ((a →1 c) ∩ (b →1 c)))) ≤ (b →1 c)
ax-oal4 1026	a ≤ b⊥    &   c ≤ d⊥    ⇒   ((a ∪ b) ∩ (c ∪ d)) ≤ (b ∪ (a ∩ (c ∪ ((a ∪ c) ∩ (b ∪ d)))))
ax-oa6 1029	a ≤ b⊥    &   c ≤ d⊥    &   e ≤ f⊥    ⇒   (((a ∪ b) ∩ (c ∪ d)) ∩ (e ∪ f)) ≤ (b ∪ (a ∩ (c ∪ (((a ∪ c) ∩ (b ∪ d)) ∩ (((a ∪ e) ∩ (b ∪ f)) ∪ ((c ∪ e) ∩ (d ∪ f)))))))
ax-4oa 1032	((a →1 d) ∩ (((a ∩ b) ∪ ((a →1 d) ∩ (b →1 d))) ∪ (((a ∩ c) ∪ ((a →1 d) ∩ (c →1 d))) ∩ ((b ∩ c) ∪ ((b →1 d) ∩ (c →1 d)))))) ≤ (b →1 d)
ax-newstateeq 1044	(((a →1 b) →1 (c →1 b)) ∩ ((a →1 c) ∩ (b →1 a))) ≤ (c →1 a)
df-id5 1046	(a ≡5 b) = ((a ∩ b) ∪ (a⊥ ∩ b⊥ ))
df-b1 1047	(a ↔1 b) = ((a →1 b) ∩ (b →1 a))
ax-wdol 1101	((a ≡ b) ∪ (a ≡ b⊥ )) = 1

Copyright terms: Public domain