---

Step * of Lemma lg-remove-noop

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕ].  lg-remove(g;x) ~ g supposing lg-size(g) ≤ x
BY
{ ((UnivCD THENA Auto)
   THEN DVar `g'
   THEN All (Fold `labeled-graph`)
   THEN All (Fold `lg-size`)
   THEN (GenConcl ⌜g = L ∈ ((T × ℕlg-size(g) List × (ℕlg-size(g) List)) List)⌝⋅
         THENA (Auto THEN RepeatFor 2 (Thin 3⋅) THEN Auto)
         )) }

1
1. T : Type
2. g : LabeledGraph(T)
3. g ∈ Top List
4. g ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List)) List
5. lg-size(g) ∈ ℕ
6. x : ℕ
7. lg-size(g) ≤ x
8. L : (T × ℕlg-size(g) List × (ℕlg-size(g) List)) List@i
9. g = L ∈ ((T × ℕlg-size(g) List × (ℕlg-size(g) List)) List)@i
⊢ lg-remove(L;x) ~ L

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].  \mforall{}[x:\mBbbN{}].    lg-remove(g;x)  \msim{}  g  supposing  lg-size(g)  \mleq{}  x


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  DVar  `g'
  THEN  All  (Fold  `labeled-graph`)
  THEN  All  (Fold  `lg-size`)
  THEN  (GenConcl  \mkleeneopen{}g  =  L\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  RepeatFor  2  (Thin  3\mcdot{})  THEN  Auto)))

---

Home Index