---

Step * 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
⊢ lg-edge(lg-add(g;i;j);a;b) ⇐⇒ lg-edge(g;a;b) ∨ ((a = i ∈ ℤ) ∧ (b = j ∈ ℤ))
BY
{ (RepUR ``lg-edge lg-in-edges lg-add`` 0
   THEN ((RWO "select-mklist" 0⋅ THENM Reduce 0) THENA (Fold `lg-size` 0 THEN Auto))
   THEN (GenConcl ⌈g[b] = X ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List))⌉⋅
         THENA (QuickAuto
               ORELSE Try ((DVar `g'
                            THEN All (Fold `labeled-graph`)
                            THEN All (Fold `lg-size`)
                            THEN Auto
                            THEN RepeatFor 2 (Thin 3)
                            THEN Auto
                            THEN Fold `lg-size` 0
                            THEN Complete (Auto))⋅)
               )
         )
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0)⋅ }

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
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 ∈ ℤ))

---

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
\mvdash{}  lg-edge(lg-add(g;i;j);a;b)  \mLeftarrow{}{}\mRightarrow{}  lg-edge(g;a;b)  \mvee{}  ((a  =  i)  \mwedge{}  (b  =  j))


By

---

Latex:
(RepUR  ``lg-edge  lg-in-edges  lg-add``  0
  THEN  ((RWO  "select-mklist"  0\mcdot{}  THENM  Reduce  0)  THENA  (Fold  `lg-size`  0  THEN  Auto))
  THEN  (GenConcl  \mkleeneopen{}g[b]  =  X\mkleeneclose{}\mcdot{}
              THENA  (QuickAuto
                          ORELSE  Try  ((DVar  `g'
                                                    THEN  All  (Fold  `labeled-graph`)
                                                    THEN  All  (Fold  `lg-size`)
                                                    THEN  Auto
                                                    THEN  RepeatFor  2  (Thin  3)
                                                    THEN  Auto
                                                    THEN  Fold  `lg-size`  0
                                                    THEN  Complete  (Auto))\mcdot{})
                          )
              )
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0)\mcdot{}

---

Home Index