Package function: Function operators and combinators

Information

namefunction
version1.13
descriptionFunction operators and combinators
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
showData.Bool
Function

Files

Defined Constants

Theorems

id = λx. x

x. id x = x

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

f. surjective f y. x. y = f x

f. (id f) = f (f id) = f

f g x. (f g) x = f (g x)

f g h. (f (g h)) = (f g h)

f. injective f x1 x2. f x1 = f x2 x1 = x2

f g. (x. y. g y = f x) h. f = (g h)

f. (y. x. f x = y) P. (x. P (f x)) y. P y

f. (y. x. f x = y) P. (x. P (f x)) y. P y

f g. (x y. g x = g y f x = f y) h. f = (h g)

Input Type Operators

Input Constants

Assumptions

T

() = λP. P ((select) P)

t. (x. t) t

() = λp. p = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

(¬T F) (¬F T)

f y. (let x y in f x) = f y

x y. x = y y = x

x y. x = y y = x

() = λp q. (λf. f p q) = λf. f T T

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

f g. f = g x. f x = g x

() = λp q. r. (p r) (q r) r

P. (x. y. P x y) y. x. P x (y x)

(t. ¬¬t t) (¬T F) (¬F T)

t. ((T t) t) ((t T) t) ((F t) ¬t) ((t F) ¬t)

t. (T t t) (t T T) (F t T) (t t T) (t F ¬t)