---

Step * 2 1 of Lemma lg-connected-remove


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
8. i : ℕlg-size(g)@i
9. lg-size(lg-remove(g;i)) = (lg-size(g) - 1) ∈ ℤ@i
10. b : ℕlg-size(g) - 1@i
11. a λx,y. lg-edge(lg-remove(g;i);x;y)^n + 1 b@i
⊢ 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 
BY
{ ((BLemma `rel_exp_iff` THENA Auto)
   THEN (FLemma `rel_exp_iff` [-1] THENA Auto)
   THEN All Reduce
   THEN ParallelLast
   THEN Auto
   THEN ExRepD
   THEN RenameVar `c' (-4)
   THEN (With ⌜if c <z i then c else c + 1 fi ⌝ (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 Auto
   THEN BLemma `lg-edge-remove`
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  g  :  LabeledGraph(T)@i
3.  a  :  \mBbbN{}lg-size(g)  -  1@i
4.  \mlambda{}x,y.  lg-edge(g;x;y)  \mmember{}  \mBbbN{}lg-size(g)  {}\mrightarrow{}  \mBbbN{}lg-size(g)  {}\mrightarrow{}  \mBbbP{}
5.  n  :  \mBbbZ{}@i
6.  0  <  n
7.  \mforall{}i:\mBbbN{}lg-size(g)
          ((lg-size(lg-remove(g;...))  =  (lg-size(g)  -  1))
          {}\mRightarrow{}  (\mforall{}b:\mBbbN{}lg-size(g)  -  1
                      ((a  \mlambda{}x,y.  lg-edge(lg-remove(g;i);x;y)\^{}n  b)
                      {}\mRightarrow{}  (if  a  <z  i  then  a  else  a  +  1  fi   
                              \mlambda{}x,y.  lg-edge(g;x;y)\^{}n 
                              if  b  <z  i  then  b  else  b  +  1  fi  ))))@i
8.  i  :  \mBbbN{}lg-size(g)@i
9.  lg-size(lg-remove(g;i))  =  (lg-size(g)  -  1)@i
10.  b  :  \mBbbN{}lg-size(g)  -  1@i
11.  a  rel\_exp(\mBbbN{}lg-size(lg-remove(g;i));  \mlambda{}x,y.  lg-edge(lg-remove(g;i);x;y);  n  +  1)  b@i
\mvdash{}  if  a  <z  i  then  a  else  a  +  1  fi   
    \mlambda{}x,y.  lg-edge(g;x;y)\^{}n  +  1 
    if  b  <z  i  then  b  else  b  +  1  fi 


By

---

Latex:
((BLemma  `rel\_exp\_iff`  THENA  Auto)
  THEN  (FLemma  `rel\_exp\_iff`  [-1]  THENA  Auto)
  THEN  All  Reduce
  THEN  ParallelLast
  THEN  Auto
  THEN  ExRepD
  THEN  RenameVar  `c'  (-4)
  THEN  (With  \mkleeneopen{}if  c  <z  i  then  c  else  c  +  1  fi  \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  Auto
  THEN  BLemma  `lg-edge-remove`
  THEN  Auto)\mcdot{}

---

Home Index