---

Step * of Lemma lg-connected-remove

∀[T:Type]
  ∀g:LabeledGraph(T). ∀i:ℕlg-size(g). ∀a,b:ℕlg-size(g) - 1.
    (lg-connected(lg-remove(g;i);a;b)
    ⇒ lg-connected(g;if a <z i then a else a + 1 fi ;if b <z i then b else b + 1 fi ))
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN InstLemma `lg-size-remove` [⌜T⌝;⌜g⌝;⌜i⌝]⋅
   THEN Auto
   THEN (Assert λx,y. lg-edge(g;x;y) ∈ ℕlg-size(g) ⟶ ℕlg-size(g) ⟶ ℙ BY
               Auto)
   THEN All (RepUR ``lg-connected rel_plus``)
   THEN ExRepD
   THEN (With ⌜n⌝ (D 0)⋅
         THENA ((GenConcl ⌜if a <z i then a else a + 1 fi  = A ∈ ℕlg-size(g)⌝⋅ THENA Auto)
                THEN GenConcl ⌜if b <z i then b else b + 1 fi  = B ∈ ℕlg-size(g)⌝⋅
                THEN Auto)
         )
   THEN RepeatFor 2 (MoveToConcl (-5))
   THEN NatPlusInd (-2)
   THEN Try (CompleteAuto)) }

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

2
.....upcase..... 
1. [T] : Type
2. g : LabeledGraph(T)@i
3. a : ℕlg-size(g) - 1@i
4. λx,y. lg-edge(g;x;y) ∈ ℕlg-size(g) ⟶ ℕlg-size(g) ⟶ ℙ
5. n : ℤ@i
6. 0 < n
7. ∀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)^n b)
           ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^n if b <z i then b else b + 1 fi ))))@i
⊢ ∀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)^n + 1 b)
          ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^n + 1 if b <z i then b else b + 1 fi ))))

3
.....wf..... 
1. T : Type
2. g : LabeledGraph(T)@i
3. a : ℕlg-size(g) - 1@i
4. λx,y. lg-edge(g;x;y) ∈ ℕlg-size(g) ⟶ ℕlg-size(g) ⟶ ℙ
5. n : ℤ@i
6. 0 < n
⊢ ∀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)^n b)
          ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^n if b <z i then b else b + 1 fi )))) ∈ ℙ

4
.....wf..... 
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)
     ((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 ))))
7. ∀n:ℕ+
     ((∀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)^n b)
               ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^n if b <z i then b else b + 1 fi )))))
     ⇒ (∀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)^n + 1 b)
                 ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^n + 1 if b <z i then b else b + 1 fi ))))))
⊢ λn.∀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)^n b)
             ⇒ (if a <z i then a else a + 1 fi  λx,y. lg-edge(g;x;y)^n if b <z i then b else b + 1 fi )))) ∈ ℕ+ ⟶ ℙ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}g:LabeledGraph(T).  \mforall{}i:\mBbbN{}lg-size(g).  \mforall{}a,b:\mBbbN{}lg-size(g)  -  1.
        (lg-connected(lg-remove(g;i);a;b)
        {}\mRightarrow{}  lg-connected(g;if  a  <z  i  then  a  else  a  +  1  fi  ;if  b  <z  i  then  b  else  b  +  1  fi  ))


By

---

Latex:
(RepeatFor  5  ((D  0  THENA  Auto))
  THEN  InstLemma  `lg-size-remove`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Assert  \mlambda{}x,y.  lg-edge(g;x;y)  \mmember{}  \mBbbN{}lg-size(g)  {}\mrightarrow{}  \mBbbN{}lg-size(g)  {}\mrightarrow{}  \mBbbP{}  BY
                          Auto)
  THEN  All  (RepUR  ``lg-connected  rel\_plus``)
  THEN  ExRepD
  THEN  (With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
              THENA  ((GenConcl  \mkleeneopen{}if  a  <z  i  then  a  else  a  +  1  fi    =  A\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  GenConcl  \mkleeneopen{}if  b  <z  i  then  b  else  b  +  1  fi    =  B\mkleeneclose{}\mcdot{}
                            THEN  Auto)
              )
  THEN  RepeatFor  2  (MoveToConcl  (-5))
  THEN  NatPlusInd  (-2)
  THEN  Try  (CompleteAuto))

---

Home Index