---

Step * 1 2 1 1 of Lemma fast-fib

.....antecedent..... 
1. n : ℕ
2. ∀n1:ℕn. ∀a,b:ℤ.
     (∃c:ℤ [(∀m:ℕ
               ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n1 then fib(n1 + m) else fib(m) fi  ∈ ℤ)))])
3. a : ℤ
4. b : ℤ
5. ¬(n = 0 ∈ ℤ)
6. s : ℤ
7. s = (a + b) ∈ ℤ
8. n' : ℤ
9. n' = (n - 1) ∈ ℤ
10. c : ℤ
11. ∀m:ℕ. ((s = fib(m + 1) ∈ ℤ) ⇒ (a = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n' then fib(n' + m) else fib(m) fi  ∈ ℤ))
12. m : ℕ
13. a = fib(m + 1) ∈ ℤ
14. b = fib(m) ∈ ℤ
⊢ s = fib((m + 1) + 1) ∈ ℤ
BY
{ RecUnfold `fib` 0
THEN RepeatFor 2 (AutoSplit)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  n  :  \mBbbN{}
2.  \mforall{}n1:\mBbbN{}n.  \mforall{}a,b:\mBbbZ{}.
          (\mexists{}c:\mBbbZ{}  [(\mforall{}m:\mBbbN{}
                              ((a  =  fib(m  +  1))
                              {}\mRightarrow{}  (b  =  fib(m))
                              {}\mRightarrow{}  (c  =  if  0  \mleq{}z  n1  then  fib(n1  +  m)  else  fib(m)  fi  )))])
3.  a  :  \mBbbZ{}
4.  b  :  \mBbbZ{}
5.  \mneg{}(n  =  0)
6.  s  :  \mBbbZ{}
7.  s  =  (a  +  b)
8.  n'  :  \mBbbZ{}
9.  n'  =  (n  -  1)
10.  c  :  \mBbbZ{}
11.  \mforall{}m:\mBbbN{}.  ((s  =  fib(m  +  1))  {}\mRightarrow{}  (a  =  fib(m))  {}\mRightarrow{}  (c  =  if  0  \mleq{}z  n'  then  fib(n'  +  m)  else  fib(m)  fi  ))
12.  m  :  \mBbbN{}
13.  a  =  fib(m  +  1)
14.  b  =  fib(m)
\mvdash{}  s  =  fib((m  +  1)  +  1)


By

---

Latex:
RecUnfold  `fib`  0
THEN  RepeatFor  2  (AutoSplit)\mcdot{}

---

Home Index