---

Step * 1 2 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 ∈ ℤ)
⊢ ∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ)))]
BY
{ (((Evaluate ⌜s = (a + b) ∈ ℤ⌝⋅ THENM (Evaluate ⌜n' = (n - 1) ∈ ℤ⌝⋅ THENM InstHyp [⌜n'⌝;⌜s⌝;⌜a⌝] 2⋅)) THENA Auto)
   THEN (ParallelLast THENA Auto')
   )⋅ }

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

---

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)
\mvdash{}  \mexists{}c:\mBbbZ{}
[(\mforall{}m:\mBbbN{}.  ((a  =  fib(m  +  1))  {}\mRightarrow{}  (b  =  fib(m))  {}\mRightarrow{}  (c  =  if  0  \mleq{}z  n  then  fib(n  +  m)  else  fib(m)  fi  )))]


By

---

Latex:
(((Evaluate  \mkleeneopen{}s  =  (a  +  b)\mkleeneclose{}\mcdot{}  THENM  (Evaluate  \mkleeneopen{}n'  =  (n  -  1)\mkleeneclose{}\mcdot{}  THENM  InstHyp  [\mkleeneopen{}n'\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  2\mcdot{}))
    THENA  Auto
    )
  THEN  (ParallelLast  THENA  Auto')
  )\mcdot{}

---

Home Index