Package natural-thm: Properties of natural numbers

Information

namenatural-thm
version1.17
descriptionProperties of natural numbers
authorJoe Leslie-Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-12-02
requiresbool
natural-def
showData.Bool
Number.Natural

Files

Theorems

m. m = 0 n. m = suc n

e f. ∃!fn. fn 0 = e n. fn (suc n) = f (fn n) n

External Type Operators

External Constants

Assumptions

¬

¬

p. p

(¬) = λp. p

a. ∃!x. x = a

t. (x. t) t

t. (λx. t x) = t

() = λp. p = λx.

t. ¬¬t t

t. t

t. t t

t. t t

t. t

t. t t

n. ¬(suc n = 0)

t. ( t) ¬t

t. t ¬t

() = λp q. p q p

t. (t ) (t )

x y. x = y y = x

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

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

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

m n. suc m = suc n m = n

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

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

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

p. p 0 (n. p n p (suc n)) n. p n

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

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

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

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

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