---

Step * 1 of Lemma fast-fib

.....assertion..... 
∀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  ∈ ℤ)))])
BY
{ xxx(GeneralInductionOnNat THEN Auto' THEN CaseNat 0 `n')xxx }

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 ∈ ℤ
⊢ ∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z 0 then fib(0 + m) else fib(m) fi  ∈ ℤ)))]

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 ∈ ℤ)
⊢ ∃c:ℤ [(∀m:ℕ. ((a = fib(m + 1) ∈ ℤ) ⇒ (b = fib(m) ∈ ℤ) ⇒ (c = if 0 ≤z n then fib(n + m) else fib(m) fi  ∈ ℤ)))]

---

Latex:

---

Latex:
.....assertion..... 
\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  )))])


By

---

Latex:
xxx(GeneralInductionOnNat  THEN  Auto'  THEN  CaseNat  0  `n')xxx

---

Home Index