Package natural-factorial-thm: Properties of natural number factorial

Information

namenatural-factorial-thm
version1.21
descriptionProperties of natural number factorial
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2012-06-15
requiresbool
natural-add
natural-def
natural-factorial-def
natural-mult
natural-numeral
natural-order
showData.Bool
Number.Natural

Files

Theorems

n. ¬(factorial n = 0)

m n. m n factorial m factorial n

Input Type Operators

Input Constants

Assumptions

bit0 0 = 0

n. 0 n

n. n n

factorial 0 = 1

n. 0 < suc n

t. (x. t) t

() = λp. p = λx.

t. t t

t. t t

t. t

m. m + 0 = m

n. bit1 n = suc (bit0 n)

m. 1 * m = m

() = λp q. p q p

n. 0 < n ¬(n = 0)

n. factorial (suc n) = suc n * factorial n

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

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

m n. m + suc n = suc (m + n)

m n. suc m suc n m n

m n. m n d. n = m + d

m n p. m n n p m p

m n. 0 < m * n 0 < m 0 < n

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

m n p. m * p n * p m n p = 0