---

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

.....wf..... 
1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. 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
{ (DVar `g' THEN All (Fold `labeled-graph`) THEN All (Fold `lg-size`)) }

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. 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)

---

Latex:

---

Latex:
.....wf..... 
1.  [T]  :  Type
2.  g  :  LabeledGraph(T)@i
3.  i  :  \mBbbN{}lg-size(g)@i
4.  a  :  \mBbbN{}lg-size(g)  -  1@i
5.  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:
(DVar  `g'  THEN  All  (Fold  `labeled-graph`)  THEN  All  (Fold  `lg-size`))

---

Home Index