Package bool: Basic boolean theory

Information

namebool
version1.5
descriptionBasic boolean theory
authorJoe Hurd <joe@gilith.com>
licenseMIT
showData.Bool

Files

Defined Constants

Theorems

T

x. x = x

F p. p

t. t ¬t

(~) = λp. p F

() = λ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

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

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

x. x = x T

t1 t2. (let xt2t1) = t1

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

() = λp q. p q p

t. (t T) (t F)

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

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

(¬T F) (¬F T)

f y. (let xyf 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 T P F

P. (b. P b) P T P F

P. P F P T x. P 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. ¬(x. P x) x. ¬P x

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

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

A B. (B A) ¬A ¬B

t1 t2. ¬(t1 t2) t1 ¬t2

t1 t2. ¬t1 ¬t2 t2 t1

a b. f. f F = a f T = b

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

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

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

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

p q r. p q r p q r

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

p q r. p q r p q r

p q r. p q r q p r

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

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

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

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

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

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

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 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 T) x = t1) ((t F) x = t2)

A B C D. (A B) (C D) A C B D

A B C D. (A B) (C D) A C B D

A B C D. (B A) (C D) (A C) B D

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'

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

b A B C D. (A B) (C D) (if b then A else C) if b then B else D

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

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

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

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

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

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

Input Type Operators

Input Constants

Assumptions

let a d ← (λe. d e) = da = λb. (λc. c) = λc. c

let a d
      let e g
          (let hd g
           λi.
             (let jh
              λk. (λl. l j k) = λm. m ((λc. c) = λc. c) ((λc. c) = λc. c))
               i h) (d ((select) d)) ∈
      e = (λf. (λc. c) = λc. c) ∈
  a = λb. (λc. c) = λc. c