---

Step * 4 of Lemma lg-connected-remove

.....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 )))) ∈ ℕ+ ─→ ℙ
BY
{ (RepeatFor 4 (MemCD) THEN Try (Complete (Auto)) THEN RepeatFor 2 (MemCD) THEN Try (CompleteAuto))⋅ }

---

Latex:

---

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


By

---

Latex:
(RepeatFor  4  (MemCD)  THEN  Try  (Complete  (Auto))  THEN  RepeatFor  2  (MemCD)  THEN  Try  (CompleteAuto))\mcdot{}

---

Home Index