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 1030 | 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 1033 | ((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 1045 | (((a →1 b) →1 (c →1 b)) ∩ ((a
→1 c) ∩ (b →1 a))) ≤ (c
→1 a) |
df-id5 1047 | (a ≡5 b) = ((a ∩
b) ∪ (a⊥ ∩ b⊥ )) |
df-b1 1048 | (a ↔1 b) = ((a
→1 b) ∩ (b →1 a)) |
ax-wdol 1104 | ((a ≡ b)
∪ (a ≡ b⊥ )) = 1 |
ax-ml 1122 | ((a ∪ b) ∩
(a ∪ c)) ≤ (a
∪ (b ∩ (a ∪ c))) |
ax-arg 1153 | ((a0 ∪ b0) ∩ (a1 ∪ b1)) ≤ (a2 ∪ b2) ⇒ ((a0 ∪ a1) ∩ (b0 ∪ b1)) ≤ (((a0 ∪ a2) ∩ (b0 ∪ b2)) ∪ ((a1 ∪ a2) ∩ (b1 ∪ b2))) |