---

Step * 2 2 1 1 of Lemma lg-edge-remove


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. i : ℕlg-size(g)@i
7. a : ℕlg-size(g) - 1@i
8. b : ℕlg-size(g) - 1@i
⊢ g[if b <z i then b else b + 1 fi ] ∈ T × ℕlg-size(g) List × (ℕlg-size(g) List)
BY
{ (Auto THEN RepeatFor 2 (Thin 3) THEN Auto THEN Try (Fold `lg-size` 0⋅) THEN AutoSplit) }

---

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.  i  :  \mBbbN{}lg-size(g)@i
7.  a  :  \mBbbN{}lg-size(g)  -  1@i
8.  b  :  \mBbbN{}lg-size(g)  -  1@i
\mvdash{}  g[if  b  <z  i  then  b  else  b  +  1  fi  ]  \mmember{}  T  \mtimes{}  \mBbbN{}lg-size(g)  List  \mtimes{}  (\mBbbN{}lg-size(g)  List)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (Thin  3)  THEN  Auto  THEN  Try  (Fold  `lg-size`  0\mcdot{})  THEN  AutoSplit)

---

Home Index