Theory: combin

Parents

• bool

Types

Constants

• C  :('a -> 'b -> 'c) -> 'b -> 'a -> 'c
• I  :'a -> 'a
• K  :'a -> 'b -> 'a
• S  :('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
• W  :('a -> 'a -> 'b) -> 'a -> 'b
• o  :('c -> 'b) -> ('a -> 'c) -> 'a -> 'b

Definitions

C_DEF

|- C = (\f x y. f y x)

I_DEF

|- I = S K K

K_DEF

|- K = (\x y. x)

o_DEF

|- !f g. f o g = (\x. f (g x))

S_DEF

|- S = (\f g x. f x (g x))

W_DEF

|- W = (\f x. f x x)

Theorems

C_THM

|- !f x y. C f x y = f y x

I_o_ID

|- !f. (I o f = f) /\ (f o I = f)

I_THM

|- !x. I x = x

K_THM

|- !x y. K x y = x

o_ASSOC

|- !f g h. f o g o h = (f o g) o h

o_THM

|- !f g x. (f o g) x = f (g x)

S_THM

|- !f g x. S f g x = f x (g x)

W_THM

|- !f x. W f x = f x x