---

Step * 1 1 of Lemma lg-filter_wf


1. T : Type
2. P : T ─→ 𝔹
3. G : LabeledGraph(T)
4. G ∈ (T × Top) List
5. ∀x:ℕlg-size(G). ((x ∈ upto(lg-size(G))) ∈ Type)
6. i : ℕlg-size(G)@i
7. (i ∈ upto(lg-size(G)))@i
⊢ i < ||G||
BY
{ (Fold `lg-size` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  G  :  LabeledGraph(T)
4.  G  \mmember{}  (T  \mtimes{}  Top)  List
5.  \mforall{}x:\mBbbN{}lg-size(G).  ((x  \mmember{}  upto(lg-size(G)))  \mmember{}  Type)
6.  i  :  \mBbbN{}lg-size(G)@i
7.  (i  \mmember{}  upto(lg-size(G)))@i
\mvdash{}  i  <  ||G||


By

---

Latex:
(Fold  `lg-size`  0  THEN  Auto)\mcdot{}

---

Home Index