Package natural-fibonacci-exists: Existence of Fibonacci numbers

Information

namenatural-fibonacci-exists
version1.1
descriptionExistence of Fibonacci numbers
authorJoe Hurd <joe@gilith.com>
licenseMIT
provenanceHOL Light theory extracted on 2012-03-07
requiresbase
showData.Bool
Function
Number.Natural
Relation

Files

Theorems

p. p 0 p 1 (n. p n p (n + 1) p (n + 2)) n. p n

f. f 0 = 0 f 1 = 1 n. f (n + 2) = f (n + 1) + f n

h.
    (f g n. (m. m + 1 = n m + 2 = n f m = g m) h f n = h g n)
    f. n. f n = h f n

Input Type Operators

Input Constants

Assumptions

wellFounded (<)

¬

¬

bit0 0 = 0

t. t t

n. 0 n

n. n n

p. p

x. id x = x

n. n < suc n

n. n suc n

(¬) = λp. p

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 t

t. t

t. t t

t. t

t. t t

t. t

t. t t

t. t

n. ¬(suc n = 0)

n. 0 + n = n

m. m + 0 = m

t. ( t) ¬t

t. (t ) ¬t

t. t ¬t

n. bit1 n = suc (bit0 n)

m n. n m + n

() = λp q. p q p

t. (t ) (t )

m. suc m = m + 1

n. even (suc n) ¬even n

m. m 0 m = 0

t1 t2. (if then t1 else t2) = t2

t1 t2. (if then t1 else t2) = t1

n. bit0 (suc n) = suc (suc (bit0 n))

f y. (let x y in f x) = f y

x y. x = y y = x

t1 t2. t1 t2 t2 t1

m n. m + n - n = m

n. 2 * n = n + n

m n. ¬(m < n n m)

m n. ¬(m n n < m)

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. suc m n m < n

m. m = 0 n. m = suc n

p. (b. p b) p p

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

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

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

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

t1 t2. ¬(t1 t2) t1 ¬t2

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

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

m n. suc m = suc n m = n

m n. suc m suc n m n

r s. subrelation r s wellFounded s wellFounded r

t1 t2. ¬(t1 t2) ¬t1 ¬t2

m n. even (m * n) even m even n

m n. even (m + n) even m even n

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

m n. m n m < n m = n

m n. n m m - n + n = m

m n. m n n m m = n

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

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

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

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

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

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

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

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

t1 t2 t3. (t1 t2) t3 t1 t2 t3

t1 t2 t3. (t1 t2) t3 t1 t2 t3

m n p. m + p = n + p m = n

m n p. m + n m + p n p

m n p. m < n n < p m < p

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

m n. m suc n m = suc n m n

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

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

r s. subrelation r s x y. r x y s x y

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

P. (n. (m. m < n P m) P n) n. P n

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

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

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

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

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

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

m n p. m * n < m * p ¬(m = 0) n < p

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

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

r. wellFounded r p. (x. (y. r y x p y) p x) x. p x