---

Step * 1 1 of Lemma lg-edge-add


1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. j : ℕlg-size(g)@i
5. a : ℕlg-size(g)@i
6. b : ℕlg-size(g)@i
7. X1 : T@i
8. X3 : ℕlg-size(g) List@i
9. X4 : ℕlg-size(g) List@i
10. g[b] = <X1, X3, X4> ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List))@i
⊢ (a ∈ fst(if (b =z i) then if (b =z j) then <[b / X3], [b / X4]> else <X3, [j / X4]> fi 
   if (b =z j) then <[i / X3], X4>
   else <X3, X4>
   fi ))
⇐⇒ (a ∈ X3) ∨ ((a = i ∈ ℤ) ∧ (b = j ∈ ℤ))
BY
{ Thin (-1) }

1
1. [T] : Type
2. g : LabeledGraph(T)@i
3. i : ℕlg-size(g)@i
4. j : ℕlg-size(g)@i
5. a : ℕlg-size(g)@i
6. b : ℕlg-size(g)@i
7. X1 : T@i
8. X3 : ℕlg-size(g) List@i
9. X4 : ℕlg-size(g) List@i
⊢ (a ∈ fst(if (b =z i) then if (b =z j) then <[b / X3], [b / X4]> else <X3, [j / X4]> fi 
   if (b =z j) then <[i / X3], X4>
   else <X3, X4>
   fi ))
⇐⇒ (a ∈ X3) ∨ ((a = i ∈ ℤ) ∧ (b = j ∈ ℤ))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  g  :  LabeledGraph(T)@i
3.  i  :  \mBbbN{}lg-size(g)@i
4.  j  :  \mBbbN{}lg-size(g)@i
5.  a  :  \mBbbN{}lg-size(g)@i
6.  b  :  \mBbbN{}lg-size(g)@i
7.  X1  :  T@i
8.  X3  :  \mBbbN{}lg-size(g)  List@i
9.  X4  :  \mBbbN{}lg-size(g)  List@i
10.  g[b]  =  <X1,  X3,  X4>@i
\mvdash{}  (a  \mmember{}  fst(if  (b  =\msubz{}  i)  then  if  (b  =\msubz{}  j)  then  <[b  /  X3],  [b  /  X4]>  else  <X3,  [j  /  X4]>  fi 
      if  (b  =\msubz{}  j)  then  <[i  /  X3],  X4>
      else  <X3,  X4>
      fi  ))
\mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  X3)  \mvee{}  ((a  =  i)  \mwedge{}  (b  =  j))


By

---

Latex:
Thin  (-1)

---

Home Index