---

Step * 1 1 2 1 1 of Lemma nth-fibs


1. n : {1...}
2. n - 1 ≠ 0
3. ∀n:ℕn. (s-nth(n;fibs()) = fib(n) ∈ ℤ)
⊢ s-nth(n - 1 - 1;s-tl(fibs()))
= let a,s' = fibs() 
  in if (n - 1 =z 0) then a else eval m = n - 1 - 1 in s-nth(m;s') fi 
∈ ℤ
BY
{ ((CallByValueReduce 0⋅ THENA Auto) THEN RecUnfold `fibs` 0 THEN Reduce 0 THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  n  -  1  \mneq{}  0
3.  \mforall{}n:\mBbbN{}n.  (s-nth(n;fibs())  =  fib(n))
\mvdash{}  s-nth(n  -  1  -  1;s-tl(fibs()))
=  let  a,s'  =  fibs() 
    in  if  (n  -  1  =\msubz{}  0)  then  a  else  eval  m  =  n  -  1  -  1  in  s-nth(m;s')  fi 


By

---

Latex:
((CallByValueReduce  0\mcdot{}  THENA  Auto)  THEN  RecUnfold  `fibs`  0  THEN  Reduce  0  THEN  AutoSplit)

---

Home Index