Package natural-cases: natural-cases

Information

namenatural-cases
version1.0
descriptionnatural-cases
authorJoe Hurd <joe@gilith.com>
licenseHOLLight
provenanceHOL Light theory extracted on 2011-02-19
showData.Bool

Files

Theorems

m. m = Number.Numeral.zero n. m = Number.Natural.suc n

e f.
    fn.
      fn Number.Numeral.zero = e
      n. fn (Number.Natural.suc n) = f (fn n) n

e f.
    fn.
      fn Number.Numeral.zero = e
      n. fn (Number.Natural.suc n) = f n (fn n)

Input Type Operators

Input Constants

Assumptions

T

t. (λx. t x) = t

() = λP. P = λx. T

x. x = x T

() = λp q. p q p

t. (t T) (t F)

(¬T F) (¬F T)

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

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

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

P.
    P Number.Numeral.zero (n. P n P (Number.Natural.suc n)) n. P n

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

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

e f.
    ∃!fn.
      fn Number.Numeral.zero = e
      n. fn (Number.Natural.suc n) = f (fn n) n

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)