---

Step * 1 1 1 of Lemma lg-connected-remove


1. [T] : Type
2. g : LabeledGraph(T)@i
3. a : ℕlg-size(g) - 1@i
4. n : ℕ+@i
5. λx,y. lg-edge(g;x;y) ∈ ℕlg-size(g) ⟶ ℕlg-size(g) ⟶ ℙ
6. i : ℕlg-size(g)@i
7. lg-size(lg-remove(g;i)) = (lg-size(g) - 1) ∈ ℤ@i
8. b : ℕlg-size(g) - 1@i
9. a λx,y. lg-edge(lg-remove(g;i);x;y)^1 b@i
⊢ lg-edge(lg-remove(g;i);a;b)
BY
{ ((RepeatFor 2 ((RecUnfold `rel_exp` (-1) THEN Reduce (-1)))⋅ THEN ExRepD) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  g  :  LabeledGraph(T)@i
3.  a  :  \mBbbN{}lg-size(g)  -  1@i
4.  n  :  \mBbbN{}\msupplus{}@i
5.  \mlambda{}x,y.  lg-edge(g;x;y)  \mmember{}  \mBbbN{}lg-size(g)  {}\mrightarrow{}  \mBbbN{}lg-size(g)  {}\mrightarrow{}  \mBbbP{}
6.  i  :  \mBbbN{}lg-size(g)@i
7.  lg-size(lg-remove(g;i))  =  (lg-size(g)  -  1)@i
8.  b  :  \mBbbN{}lg-size(g)  -  1@i
9.  a  rel\_exp(\mBbbN{}lg-size(lg-remove(g;i));  \mlambda{}x,y.  lg-edge(lg-remove(g;i);x;y);  1)  b@i
\mvdash{}  lg-edge(lg-remove(g;i);a;b)


By

---

Latex:
((RepeatFor  2  ((RecUnfold  `rel\_exp`  (-1)  THEN  Reduce  (-1)))\mcdot{}  THEN  ExRepD)  THEN  Auto)\mcdot{}

---

Home Index