---

Step * 2 of Lemma lg-edge-remove


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 ])))
BY
{ Subst' firstn(i;g) @ nth_tl(i + 1;g)[b] = g[if b <z i then b else b + 1 fi ] ∈ (T × ℕ||g|| List × (ℕ||g|| List)) 0 }

1
.....equality..... 
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
⊢ firstn(i;g) @ nth_tl(i + 1;g)[b] = g[if b <z i then b else b + 1 fi ] ∈ (T × ℕ||g|| List × (ℕ||g|| List))

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 = g[if b <z i then b else b + 1 fi ] 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 ])))

3
.....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
6. z : T × ℕ||g|| List × (ℕ||g|| List)
⊢ (a ∈ fst(snd(let lbl,in,out = z 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:

1.  [T]  :  Type
2.  g  :  LabeledGraph(T)@i
3.  i  :  \mBbbN{}lg-size(g)@i
4.  a  :  \mBbbN{}lg-size(g)  -  1@i
5.  b  :  \mBbbN{}lg-size(g)  -  1@i
\mvdash{}  (a  \mmember{}  fst(snd(let  lbl,in,out  =  firstn(i;g)  @  nth\_tl(i  +  1;g)[b]  in 
      <lbl
      ,  map(\mlambda{}x.if  x  \mleq{}z  i  then  x  else  x  -  1  fi  ;filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  i));in))
      ,  map(\mlambda{}x.if  x  \mleq{}z  i  then  x  else  x  -  1  fi  ;filter(\mlambda{}x.(\mneg{}\msubb{}(x  =\msubz{}  i));out))>)))
\mLeftarrow{}{}\mRightarrow{}  (if  a  <z  i  then  a  else  a  +  1  fi    \mmember{}  fst(snd(g[if  b  <z  i  then  b  else  b  +  1  fi  ])))


By

---

Latex:
Subst'  firstn(i;g)  @  nth\_tl(i  +  1;g)[b]  =  g[if  b  <z  i  then  b  else  b  +  1  fi  ]  0

---

Home Index