---

Step * 1 2 1 of Lemma fast-fib


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) ∈ ℤ
⊢ c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ
BY
{ xxxInstHyp [⌜m + 1⌝] (-4)⋅
THEN Autoxxx }

1
.....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) ∈ ℤ

2
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) ∈ ℤ
15. c = if 0 ≤z n' then fib(n' + m + 1) else fib(m + 1) fi  ∈ ℤ
⊢ c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ

---

Latex:

---

Latex:

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{}  c  =  if  0  \mleq{}z  n  then  fib(n  +  m)  else  fib(m)  fi 


By

---

Latex:
xxxInstHyp  [\mkleeneopen{}m  +  1\mkleeneclose{}]  (-4)\mcdot{}
THEN  Autoxxx

---

Home Index