---

Step * 1 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
⊢ lg-remove(L;x) ~ L
BY
{ Assert ⌈||L|| ≤ x⌉⋅ }

1
.....assertion..... 
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
⊢ ||L|| ≤ x

2
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

---

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
\mvdash{}  lg-remove(L;x)  \msim{}  L


By

---

Latex:
Assert  \mkleeneopen{}||L||  \mleq{}  x\mkleeneclose{}\mcdot{}

---

Home Index