---

Step * 1 of Lemma lg-connected-remove

.....basecase..... 
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) ⟶ ℙ
⊢ ∀i:ℕlg-size(g)
    ((lg-size(lg-remove(g;i)) = (lg-size(g) - 1) ∈ ℤ)
    ⇒ (∀b:ℕlg-size(g) - 1
          ((a λx,y. lg-edge(lg-remove(g;i);x;y)^1 b)
          ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^1 if b <z i then b else b + 1 fi ))))
BY
{ (Auto
   THEN RepeatFor 2 ((RecUnfold `rel_exp` 0 THEN Reduce 0))
   THEN With ⌜if b <z i then b else b + 1 fi ⌝ (D 0)⋅
   THEN Auto) }

1
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(g;if a <z i then a else a + 1 fi ;if b <z i then b else b + 1 fi )

---

Latex:

---

Latex:
.....basecase..... 
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{}
\mvdash{}  \mforall{}i:\mBbbN{}lg-size(g)
        ((lg-size(lg-remove(g;i))  =  (lg-size(g)  -  1))
        {}\mRightarrow{}  (\mforall{}b:\mBbbN{}lg-size(g)  -  1
                    ((a  rel\_exp(\mBbbN{}lg-size(lg-remove(g;i));  \mlambda{}x,y.  lg-edge(lg-remove(g;i);x;y);  1)  b)
                    {}\mRightarrow{}  (if  a  <z  i  then  a  else  a  +  1  fi    \mlambda{}x,y.  lg-edge(g;x;y)\^{}1  if  b  <z  i  then  b  else  b  +  1  fi  \000C))))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((RecUnfold  `rel\_exp`  0  THEN  Reduce  0))
  THEN  With  \mkleeneopen{}if  b  <z  i  then  b  else  b  +  1  fi  \mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index