---

Step * 2 1 1 of Lemma less-fast-fib


1. f : ∀n,a,b:ℕ.
         {m:ℕ| 
          ∀k:ℕ
            ((a = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))} 
⊢ λn.(f n 1 0) ∈ ∀n:ℕ. {m:ℕ| m = fib(n) ∈ ℕ} 
BY
{ TACTIC:RepeatFor 1 ((MemCD THENA Auto)) }

1
.....subterm..... T:t
1:n
1. f : ∀n,a,b:ℕ.
         {m:ℕ| 
          ∀k:ℕ
            ((a = fib(k) ∈ ℤ) ⇒ ((k ≤ 0) ⇒ (b = 0 ∈ ℤ)) ⇒ (0 < k ⇒ (b = fib(k - 1) ∈ ℤ)) ⇒ (m = fib(n + k) ∈ ℕ))} 
2. n : ℕ@i
⊢ f n 1 0 ∈ {m:ℕ| m = fib(n) ∈ ℕ} 

---

Latex:

---

Latex:

1.  f  :  \mforall{}n,a,b:\mBbbN{}.
                  \{m:\mBbbN{}| 
                    \mforall{}k:\mBbbN{}
                        ((a  =  fib(k))
                        {}\mRightarrow{}  ((k  \mleq{}  0)  {}\mRightarrow{}  (b  =  0))
                        {}\mRightarrow{}  (0  <  k  {}\mRightarrow{}  (b  =  fib(k  -  1)))
                        {}\mRightarrow{}  (m  =  fib(n  +  k)))\} 
\mvdash{}  \mlambda{}n.(f  n  1  0)  \mmember{}  \mforall{}n:\mBbbN{}.  \{m:\mBbbN{}|  m  =  fib(n)\} 


By

---

Latex:
TACTIC:RepeatFor  1  ((MemCD  THENA  Auto))

---

Home Index