---

Step * 2 1 of Lemma fibs_wf


1. f : ⋂n:ℕ. (primrec(n;Top;λ,T. (ℕ × T)) ⟶ primrec(n;Top;λ,T. (ℕ × T)))
⊢ fix((λfibs.1.f fibs)) ∈ stream(ℕ)
BY
{ (RepUR ``stream corec`` 0
   THEN Auto
   THEN NatInd(-1)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN ProveWfLemma
   THEN With ⌜n - 1⌝ (D 1)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mcap{}n:\mBbbN{}.  (primrec(n;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T))  {}\mrightarrow{}  primrec(n;Top;\mlambda{},T.  (\mBbbN{}  \mtimes{}  T)))
\mvdash{}  fix((\mlambda{}fibs.1.f  fibs))  \mmember{}  stream(\mBbbN{})


By

---

Latex:
(RepUR  ``stream  corec``  0
  THEN  Auto
  THEN  NatInd(-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  ProveWfLemma
  THEN  With  \mkleeneopen{}n  -  1\mkleeneclose{}  (D  1)\mcdot{}
  THEN  Auto)

---

Home Index