---

Step * of Lemma lg-filter_wf

∀[T:Type]. ∀[P:T ─→ 𝔹]. ∀[G:LabeledGraph(T)].  (lg-filter(P;G) ∈ LabeledGraph(T))
BY
{ (Auto THEN Unfold `lg-filter` 0 THEN (Assert G ∈ (T × Top) List BY (Dlg 3 THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[G:LabeledGraph(T)].    (lg-filter(P;G)  \mmember{}  LabeledGraph(T))


By

---

Latex:
(Auto  THEN  Unfold  `lg-filter`  0  THEN  (Assert  G  \mmember{}  (T  \mtimes{}  Top)  List  BY  (Dlg  3  THEN  Auto)))

---

Home Index