---

Step * 2 of Lemma fast-fib


1. ∀n:ℕ. ∀a,b:ℤ.
     (∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ)))])
⊢ ∀n:ℕ. (∃m:ℕ [(m = fib(n) ∈ ℕ)])
BY
{ xxx(ParallelLast THENA Auto)
THEN ((InstHyp [⌜n⌝;⌜1⌝;⌜1⌝] 1⋅ THENA Auto)
      THEN ParallelLast
      THEN (InstHyp [⌜0⌝] (-1)⋅ THENA Auto)
      THEN SplitOnHypITE -1 
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  \mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbZ{}.
          (\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  )))])
\mvdash{}  \mforall{}n:\mBbbN{}.  (\mexists{}m:\mBbbN{}  [(m  =  fib(n))])


By

---

Latex:
xxx(ParallelLast  THENA  Auto)
THEN  ((InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  1\mcdot{}  THENA  Auto)
            THEN  ParallelLast
            THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
            THEN  SplitOnHypITE  -1 
            THEN  Auto)xxx

---

Home Index