---

Step * of Lemma better-fibs_wf

better-fibs() ∈ stream(ℕ)
BY
{ (Unfold `better-fibs` 0 THEN GenConclAtAddrType ⌜stream(ℕ × ℕ)⌝ [2;2]⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `better-fibs`  0  THEN  GenConclAtAddrType  \mkleeneopen{}stream(\mBbbN{}  \mtimes{}  \mBbbN{})\mkleeneclose{}  [2;2]\mcdot{}  THEN  Auto)

---

Home Index