---

Step * 1 of Lemma lg-filter_wf


1. T : Type
2. P : T ─→ 𝔹
3. G : LabeledGraph(T)
4. G ∈ (T × Top) List
⊢ let rms = filter(λi.(¬b(P (fst(G[i]))));upto(lg-size(G))) in
      reduce(λx,g. lg-remove(g;x);G;rms) ∈ LabeledGraph(T)
BY
{ Auto }

1
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||

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  G  :  LabeledGraph(T)
4.  G  \mmember{}  (T  \mtimes{}  Top)  List
\mvdash{}  let  rms  =  filter(\mlambda{}i.(\mneg{}\msubb{}(P  (fst(G[i]))));upto(lg-size(G)))  in
            reduce(\mlambda{}x,g.  lg-remove(g;x);G;rms)  \mmember{}  LabeledGraph(T)


By

---

Latex:
Auto

---

Home Index