- o_THM
-
|- ∀f g x. (f o g) x = f (g x)
- o_ASSOC
-
|- ∀f g h. f o g o h = (f o g) o h
- o_ABS_L
-
|- (λx. f x) o g = (λx. f (g x))
- o_ABS_R
-
|- f o (λx. g x) = (λx. f (g x))
- K_THM
-
|- ∀x y. K x y = x
- S_THM
-
|- ∀f g x. S f g x = f x (g x)
- S_ABS_L
-
|- S (λx. f x) g = (λx. f x (g x))
- S_ABS_R
-
|- S f (λx. g x) = (λx. f x (g x))
- C_THM
-
|- ∀f x y. combin$C f x y = f y x
- C_ABS_L
-
|- combin$C (λx. f x) y = (λx. f x y)
- W_THM
-
|- ∀f x. W f x = f x x
- I_THM
-
|- ∀x. I x = x
- I_o_ID
-
|- ∀f. (I o f = f) ∧ (f o I = f)
- K_o_THM
-
|- (∀f v. K v o f = K v) ∧ ∀f v. f o K v = K (f v)
- UPDATE_APPLY
-
|- (∀a x f. (a =+ x) f a = x) ∧ ∀a b x f. a ≠ b ⇒ ((a =+ x) f b = f b)
- APPLY_UPDATE_THM
-
|- ∀f a b c. (a =+ b) f c = if a = c then b else f c
- UPDATE_COMMUTES
-
|- ∀f a b c d. a ≠ b ⇒ ((a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f))
- UPDATE_EQ
-
|- ∀f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f
- UPDATE_APPLY_ID
-
|- ∀f a b. (f a = b) ⇔ ((a =+ b) f = f)
- UPDATE_APPLY_IMP_ID
-
|- ∀f b a. (f a = b) ⇒ ((a =+ b) f = f)
- APPLY_UPDATE_ID
-
|- ∀f a. (a =+ f a) f = f
- UPD11_SAME_BASE
-
|- ∀f a b c d.
((a =+ c) f = (b =+ d) f) ⇔
(a = b) ∧ (c = d) ∨ a ≠ b ∧ ((a =+ c) f = f) ∧ ((b =+ d) f = f)
- SAME_KEY_UPDATE_DIFFER
-
|- ∀f1 f2 a b c. b ≠ c ⇒ (a =+ b) f ≠ (a =+ c) f
- UPD11_SAME_KEY_AND_BASE
-
|- ∀f a b c. ((a =+ b) f = (a =+ c) f) ⇔ (b = c)
- UPD_SAME_KEY_UNWIND
-
|- ∀f1 f2 a b c.
((a =+ b) f1 = (a =+ c) f2) ⇒ (b = c) ∧ ∀v. (a =+ v) f1 = (a =+ v) f2
- GEN_LET_RAND
-
|- P (LET f v) = LET (P o f) v
- GEN_LET_RATOR
-
|- LET f v x = LET (combin$C f x) v
- LET_FORALL_ELIM
-
|- LET f v ⇔ $! (S ($==> o Abbrev o combin$C $= v) f)
- GEN_literal_case_RAND
-
|- P (literal_case f v) = literal_case (P o f) v
- GEN_literal_case_RATOR
-
|- literal_case f v x = literal_case (combin$C f x) v
- literal_case_FORALL_ELIM
-
|- literal_case f v ⇔ $! (S ($==> o Abbrev o combin$C $= v) f)
- FAIL_THM
-
|- FAIL x y = x