---

Step * of Lemma fibs_wf

fibs() ∈ stream(ℕ)
BY
{ ((RepUR ``fibs`` 0
    THEN Subst' λfibs.1.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs)) 
    ~ λfibs.1.(λfibs.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs))) fibs 0
    THEN Try ((Reduce 0 THEN Trivial)))⋅
   THEN GenConcl⌜(λfibs.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs)))
                 = f
                 ∈ (⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T))))⌝⋅
   THEN skip{(Auto THEN Auto')}) }

1
.....wf..... 
λfibs.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs)) ∈ ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))

2
1. f : ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))
2. (λfibs.1.stream-zip(λx,y. (x + y);fibs;s-tl(fibs))) = f ∈ (⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (\000Cℕ × T))))
⊢ fix((λfibs.1.f fibs)) ∈ stream(ℕ)

---

Latex:

---

Latex:
fibs()  \mmember{}  stream(\mBbbN{})


By

---

Latex:
((RepUR  ``fibs``  0
    THEN  Subst'  \mlambda{}fibs.1.1.stream-zip(\mlambda{}x,y.  (x  +  y);fibs;s-tl(fibs)) 
    \msim{}  \mlambda{}fibs.1.(\mlambda{}fibs.1.stream-zip(\mlambda{}x,y.  (x  +  y);fibs;s-tl(fibs)))  fibs  0
    THEN  Try  ((Reduce  0  THEN  Trivial)))\mcdot{}
  THEN  GenConcl\mkleeneopen{}(\mlambda{}fibs.1.stream-zip(\mlambda{}x,y.  (x  +  y);fibs;s-tl(fibs)))  =  f\mkleeneclose{}\mcdot{}
  THEN  skip\{(Auto  THEN  Auto')\})

---

Home Index