---

Step * of Lemma gamma-neighbourhood_wf

∀[beta:ℕ ⟶ ℕ]. ∀[n0:finite-nat-seq()].  (gamma-neighbourhood(beta;n0) ∈ finite-nat-seq() ⟶ (ℕ?))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``gamma-neighbourhood`` 0
   THEN (MemCD THENA Auto)
   THEN ((BoolCase ⌜init-seg-nat-seq(n;n0)⌝⋅ THENA Auto) THENL [Auto; Id])) }

1
1. beta : ℕ ⟶ ℕ
2. n0 : finite-nat-seq()
3. n : finite-nat-seq()
4. ¬↑init-seg-nat-seq(n;n0)
⊢ if TERMOF{extend-seq1-all-dec:o, 1:l} n n0 beta then inl 1 else inl 0 fi  ∈ ℕ?

---

Latex:

---

Latex:
\mforall{}[beta:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[n0:finite-nat-seq()].    (gamma-neighbourhood(beta;n0)  \mmember{}  finite-nat-seq()  {}\mrightarrow{}  (\mBbbN{}?))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``gamma-neighbourhood``  0
  THEN  (MemCD  THENA  Auto)
  THEN  ((BoolCase  \mkleeneopen{}init-seg-nat-seq(n;n0)\mkleeneclose{}\mcdot{}  THENA  Auto)  THENL  [Auto;  Id]))

---

Home Index