Theory combin

⊢ ∀x f. (x :> f) = f x

⊢ ∀f. ASSOC f ⇔ ∀x y z. f x (f y z) = f (f x y) z

⊢ ∀f. COMM f ⇔ ∀x y. f x y = f y x

⊢ flip = (λf x y. f y x)

⊢ ∀s f. EXTENSIONAL s f ⇔ ∀x. x ∉ s ⇒ f x = ARB

⊢ FAIL = (λx y. x)

⊢ ∀f g. FCOMM f g ⇔ ∀x y z. g x (f y z) = f (g x y) z

⊢ I = S K K

⊢ K = (λx y. x)

⊢ ∀f e. LEFT_ID f e ⇔ ∀x. f e x = x

⊢ ∀f e. MONOID f e ⇔ ASSOC f ∧ RIGHT_ID f e ∧ LEFT_ID f e

⊢ ∀s f x. RESTRICTION s f x = if x ∈ s then f x else ARB

⊢ ∀f e. RIGHT_ID f e ⇔ ∀x. f x e = x

⊢ S = (λf g x. f x (g x))

⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)

⊢ W = (λf x. f x x)

⊢ ∀f g. f ∘ g = (λx. f (g x))

⊢ ∀f a. f⦇a ↦ f a⦈ = f

⊢ ∀f a b c. f⦇a ↦ b⦈ c = if a = c then b else f c

⊢ ASSOC $/\

⊢ ASSOC $\/

⊢ ∀f. ASSOC f ⇔ ∀x y z. f (f x y) z = f x (f y z)

⊢ flip (λx. f x) y = (λx. f x y)

⊢ ∀f x y. flip f x y = f y x

⊢ ∀s f. EXTENSIONAL s (RESTRICTION s f)

⊢ FAIL x y = x

⊢ ∀f. FCOMM f f ⇔ ASSOC f

⊢ P (LET f v) = LET (P ∘ f) v

⊢ LET f v x = LET (flip f x) v

⊢ P (literal_case f v) = literal_case (P ∘ f) v

⊢ literal_case f v x = literal_case (flip f x) v

⊢ ∀s f. f ∈ EXTENSIONAL s ⇔ ∀x. x ∉ s ⇒ f x = ARB

⊢ ∀s f x. f ∈ EXTENSIONAL s ∧ x ∉ s ⇒ f x = ARB

⊢ I = (λx. x)

⊢ ∀x. I x = x

⊢ ∀f. I ∘ f = f ∧ f ∘ I = f

⊢ ∀x. K x = (λz. x)

⊢ ∀x y. K x y = x

⊢ (∀f v. K v ∘ f = K v) ∧ ∀f v. f ∘ K v = K (f v)

⊢ LET f v ⇔ $! (S ($==> ∘ Abbrev ∘ flip $= v) f)

⊢ MONOID $/\ T

⊢ MONOID $\/ F

⊢ ∀s f x. x ∈ s ⇒ RESTRICTION s f x = f x

⊢ ∀s f x y. x ∈ s ∧ f x = y ⇒ RESTRICTION s f x = y

⊢ ∀s f. RESTRICTION s f = (λx. if x ∈ s then f x else ARB)

⊢ ∀s f x. x ∉ s ⇒ RESTRICTION s f x = ARB

⊢ ∀f1 f2 a b c. b ≠ c ⇒ f⦇a ↦ b⦈ ≠ f⦇a ↦ c⦈

⊢ S (λx. f x) g = (λx. f x (g x))

⊢ S f (λx. g x) = (λx. f x (g x))

⊢ ∀f g x. S f g x = f x (g x)

⊢ ∀f a b c d.
    f⦇a ↦ c⦈ = f⦇b ↦ d⦈ ⇔
    a = b ∧ c = d ∨ a ≠ b ∧ f⦇a ↦ c⦈ = f ∧ f⦇b ↦ d⦈ = f

⊢ ∀f a b c. f⦇a ↦ b⦈ = f⦇a ↦ c⦈ ⇔ b = c

⊢ (∀a x f. f⦇a ↦ x⦈ a = x) ∧ ∀a b x f. a ≠ b ⇒ f⦇a ↦ x⦈ b = f b

⊢ ∀a x f. f⦇a ↦ x⦈ a = x

⊢ ∀f a b. f a = b ⇔ f⦇a ↦ b⦈ = f

⊢ (∀f a b. f⦇a ↦ b⦈ = f ⇔ f a = b) ∧ ∀f a b. f = f⦇a ↦ b⦈ ⇔ f a = b

⊢ ∀f b a. f a = b ⇒ f⦇a ↦ b⦈ = f

⊢ ∀f a b c d. a ≠ b ⇒ f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈

⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈

⊢ ∀f1 f2 a b c. f1⦇a ↦ b⦈ = f2⦇a ↦ c⦈ ⇒ b = c ∧ ∀v. f1⦇a ↦ v⦈ = f2⦇a ↦ v⦈

⊢ ∀f x. W f x = f x x

⊢ literal_case f v ⇔ $! (S ($==> ∘ Abbrev ∘ flip $= v) f)

⊢ (λx. f x) ∘ g = (λx. f (g x))

⊢ f ∘ (λx. g x) = (λx. f (g x))

⊢ ∀f g h. f ∘ g ∘ h = (f ∘ g) ∘ h

⊢ ∀f g h. (f ∘ g) ∘ h = f ∘ g ∘ h

⊢ ∀a1 a2 g1 g2 f1 f2.
    a1 = a2 ∧ (∀x. x = a2 ⇒ g1 x = g2 x) ∧ (∀y. y = g2 a2 ⇒ f1 y = f2 y) ⇒
    (f1 ∘ g1) a1 = (f2 ∘ g2) a2

⊢ ∀f g x. (f ∘ g) x = f (g x)