---

Step * 1 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 ∈ ℤ
⊢ ∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z 0 then fib(0 + m) else fib(m) fi  ∈ ℤ)))]
BY
{ (Reduce 0 THEN UseWitness ⌜b⌝ ⋅ THEN MemTypeCD THEN Auto) }

---

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


By

---

Latex:
(Reduce  0  THEN  UseWitness  \mkleeneopen{}b\mkleeneclose{}  \mcdot{}  THEN  MemTypeCD  THEN  Auto)

---

Home Index