---

Step * 1 2 of Lemma lg-remove-noop


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
10. ||L|| ≤ x
⊢ lg-remove(L;x) ~ L
BY
{ (MoveToConcl (-1)
   THEN Thin (-1)
   THEN MoveToConcl (-2)
   THEN MoveToConcl (-1)
   THEN RepeatFor 2 (Thin 3)
   THEN (GenConclAtAddr [1;1;2;1;1;2]⋅ THENA Auto)
   THEN All Thin) }

1
1. T : Type
2. x : ℕ
3. v : ℕ@i
⊢ ∀L:(T × ℕv List × (ℕv List)) List. ((v ≤ x) ⇒ (||L|| ≤ x) ⇒ (lg-remove(L;x) ~ L))

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  g  \mmember{}  Top  List
4.  g  \mmember{}  (T  \mtimes{}  \mBbbN{}lg-size(g)  List  \mtimes{}  (\mBbbN{}lg-size(g)  List))  List
5.  lg-size(g)  \mmember{}  \mBbbN{}
6.  x  :  \mBbbN{}
7.  lg-size(g)  \mleq{}  x
8.  L  :  (T  \mtimes{}  \mBbbN{}lg-size(g)  List  \mtimes{}  (\mBbbN{}lg-size(g)  List))  List@i
9.  g  =  L@i
10.  ||L||  \mleq{}  x
\mvdash{}  lg-remove(L;x)  \msim{}  L


By

---

Latex:
(MoveToConcl  (-1)
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-2)
  THEN  MoveToConcl  (-1)
  THEN  RepeatFor  2  (Thin  3)
  THEN  (GenConclAtAddr  [1;1;2;1;1;2]\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index