---

Step * 1 1 of Lemma lg-remove-noop

.....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
BY
{ (RepeatFor 2 (Thin 3) THEN RevHypSubst (-1) 0) }

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

2
.....wf..... 
1. T : Type
2. g : LabeledGraph(T)
3. lg-size(g) ∈ ℕ
4. x : ℕ
5. lg-size(g) ≤ x
6. L : (T × ℕlg-size(g) List × (ℕlg-size(g) List)) List@i
7. g = L ∈ ((T × ℕlg-size(g) List × (ℕlg-size(g) List)) List)@i
8. z : (T × ℕlg-size(g) List × (ℕlg-size(g) List)) List
⊢ ||z|| ≤ x ∈ ℙ

---

Latex:

---

Latex:
.....assertion..... 
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{}  ||L||  \mleq{}  x


By

---

Latex:
(RepeatFor  2  (Thin  3)  THEN  RevHypSubst  (-1)  0)

---

Home Index