Package bool: Boolean operators and quantifiers

Information

namebool
version1.37
descriptionBoolean operators and quantifiers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseMIT
checksum3ce9f58a6d6373bd7540fd16b482130ece4799b8
showData.Bool

Files

Defined Constants

Theorems

¬

¬

x. x = x

t. t t

p. p

t. t ¬t

(¬) = λp. p

() = λp. p ((select) p)

a. x. x = a

a. ∃!x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

(λp. p) = λp. p

() = λp. p = λx.

t. ¬¬t t

t. ( t) t

t. (t ) t

t. t

t. t t

t. t

t. t t

t. t t t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

t. t t t

t1 t2. (let x t2 in t1) = t1

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

x. (select y. y = x) = x

() = λp q. p q p

t. (t ) (t )

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

b t. (if b then t else t) = t

p x. p x p ((select) p)

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

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

t1 t2. t1 t2 t2 t1

a b. (a b) a b

p. (b. p b) p p

p. (b. p b) p p

p. p p x. p x

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

p. (x. ¬p x) ¬x. p x

p. (x. ¬p x) ¬x. p x

p. ¬(x. p x) x. ¬p x

p. ¬(x. p x) x. ¬p x

() = λp. q. (x. p x q) q

p q. (q p) ¬p ¬q

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. (¬t1 ¬t2) t1 t2

t1 t2. ¬t1 ¬t2 t2 t1

t1 t2. ¬(t1 t2) ¬t1 ¬t2

t1 t2. ¬(t1 t2) ¬t1 ¬t2

a b. f. f = a f = b

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

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

p a. (x. a = x p x) p a

p a. (x. x = a p x) p a

p a. (x. a = x p x) p a

p a. (x. x = a p x) p a

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

c x y. (if ¬c then x else y) = if c then y else x

p q. (x. p q) (x. p) x. q

p q. (x. p q) (x. p) x. q

p q. (x. p q) (x. p) x. q

p q. (x. p q) (x. p) x. q

p q. (x. p) (x. q) x. p q

p q. (x. p) (x. q) x. p q

p. (x y. p x y) y x. p x y

p. (x y. p x y) y x. p x y

p q. (x. p q x) p x. q x

p q. (x. p q x) p x. q x

p q. (x. p q x) p x. q x

p q. (x. p q x) p x. q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. p (x. q x) x. p q x

p q. (x. p x q) (x. p x) q

p q. (x. p x q) (x. p x) q

p q. (x. p x q) (x. p x) q

p q. (x. p x q) (x. p x) q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p q. (x. p x) q x. p x q

p. (∃!x. p x) x. y. p y x = y

x y z. x = y y = z x = z

p q r. p q r p q r

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

p x. (y. p y y = x) (select) p = x

r. (x. y. r x y) f. x. r x (f x)

p. (x. ∃!y. p x y) ∃!f. x. p x (f x)

b f g. (λx. if b then f x else g x) = if b then f else g

b t1 t2. (if b then t1 else t2) (¬b t1) (b t2)

p q r. p (q r) p q p r

p q r. p q r (p q) (p r)

p q r. p q r (p q) (p r)

p q r. (p q) r p r q r

p q r. p q r (p r) (q r)

p q r. p q r (p r) (q r)

(∃!) = λp. () p x y. p x p y x = y

b f x y. f (if b then x else y) = if b then f x else f y

b f g x. (if b then f else g) x = if b then f x else g x

p. (∃!x. p x) x. p x y. p y y = x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x q x) (x. p x) x. q x

p q. (x. p x) (x. q x) x. p x q x

p q. (x. p x) (x. q x) x. p x q x

cond = λt t1 t2. select x. ((t ) x = t1) ((t ) x = t2)

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p1 p2) (q1 q2) p1 q1 p2 q2

p1 p2 q1 q2. (p2 p1) (q1 q2) (p1 q1) p2 q2

p. (x. ∃!y. p x y) f. x y. p x y f x = y

p c x y. p (if c then x else y) (c p x) (¬c p y)

p. (∃!x. p x) (x. p x) x x'. p x p x' x = x'

p r. (x. p x y. r x y) f. x. p x r x (f x)

b p q r s. (p q) (r s) (if b then p else r) if b then q else s

r p.
    (x y. p x y p y x) (x y. r x y r y x) (x y. r x y p x y)
    x y. p x y

External Type Operators

External Constants

Assumptions

AXIOM OF EXTENSIONALITY

AXIOM OF CHOICE