Package natural-factorial: Natural number factorial

Information

namenatural-factorial
version1.17
descriptionNatural number factorial
authorJoe Hurd <joe@gilith.com>
licenseMIT
requiresbool
natural-def
natural-thm
natural-numeral
natural-order
natural-add
natural-mult
showData.Bool
Number.Natural

Files

Defined Constant

Theorems

factorial 0 = 1

n. ¬(factorial n = 0)

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

m n. m n factorial m factorial n

Input Type Operators

Input Constants

Assumptions

bit0 0 = 0

n. 0 n

n. n n

n. 0 < suc n

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

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)

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

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

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

P. P 0 (n. P n P (suc n)) n. P n

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

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

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