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

Information

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

Files

Theorems

n. ¬(factorial n = 0)

m n. m n factorial m factorial n

Input Type Operators

Input Constants

Assumptions

T

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 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 T T

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