---

Step * of Lemma lg-edge-remove

∀[T:Type]
  ∀g:LabeledGraph(T). ∀i:ℕlg-size(g). ∀a,b:ℕlg-size(g) - 1.
    (lg-edge(lg-remove(g;i);a;b) ⇐⇒ lg-edge(g;if a <z i then a else a + 1 fi ;if b <z i then b else b + 1 fi ))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``lg-edge lg-in-edges lg-remove`` 0
   THEN (RWO "select-map" 0 THENM Reduce 0)
   THEN Try (Complete (Auto))) }

1
.....wf..... 
1. T : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. b : ℕlg-size(g) - 1@i
⊢ b ∈ ℕ||firstn(i;g) @ nth_tl(i + 1;g)||

2
1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. a : ℕlg-size(g) - 1@i
5. b : ℕlg-size(g) - 1@i
⊢ (a ∈ fst(snd(let lbl,in,out = firstn(i;g) @ nth_tl(i + 1;g)[b] in 
   <lbl
   , map(λx.if x ≤z i then x else x - 1 fi ;filter(λx.(¬b(x =z i));in))
   , map(λx.if x ≤z i then x else x - 1 fi ;filter(λx.(¬b(x =z i));out))>)))
⇐⇒ (if a <z i then a else a + 1 fi  ∈ fst(snd(g[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-edge(lg-remove(g;i);a;b)
        \mLeftarrow{}{}\mRightarrow{}  lg-edge(g;if  a  <z  i  then  a  else  a  +  1  fi  ;if  b  <z  i  then  b  else  b  +  1  fi  ))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``lg-edge  lg-in-edges  lg-remove``  0
  THEN  (RWO  "select-map"  0  THENM  Reduce  0)
  THEN  Try  (Complete  (Auto)))

---

Home Index