---

Step * of Lemma lg-edge-add

∀[T:Type]
  ∀g:LabeledGraph(T). ∀i,j,a,b:ℕlg-size(g).
    (lg-edge(lg-add(g;i;j);a;b) ⇐⇒ lg-edge(g;a;b) ∨ ((a = i ∈ ℤ) ∧ (b = j ∈ ℤ)))
BY
{ ((UnivCD THENA Auto)
   THEN skip{(RepUR ``lg-edge lg-in-edges lg-add`` 0
              THEN ((RWO "select-mklist" 0⋅ THENM Reduce 0) THENA Auto)
              THEN Try ((Fold `lg-size` 0 THEN Auto)⋅)
              THEN (((GenConcl ⌜g[b] = X ∈ (T × ℕlg-size(g) List × (ℕlg-size(g) List))⌝⋅ THEN Try (Complete (Auto)))
                     THENA (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 Auto)⋅
                     )
                    THEN RepeatFor 2 (D -2)
                    THEN Reduce 0
                    THEN RepeatFor 2 (AutoSplit)
                    THEN (RWW "cons_member" 0 THEN MaAuto THEN SplitOrHyps THEN Auto)⋅)⋅)}
   ) }

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
⊢ lg-edge(lg-add(g;i;j);a;b) ⇐⇒ lg-edge(g;a;b) ∨ ((a = i ∈ ℤ) ∧ (b = j ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}g:LabeledGraph(T).  \mforall{}i,j,a,b:\mBbbN{}lg-size(g).
        (lg-edge(lg-add(g;i;j);a;b)  \mLeftarrow{}{}\mRightarrow{}  lg-edge(g;a;b)  \mvee{}  ((a  =  i)  \mwedge{}  (b  =  j)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  skip\{(RepUR  ``lg-edge  lg-in-edges  lg-add``  0
                        THEN  ((RWO  "select-mklist"  0\mcdot{}  THENM  Reduce  0)  THENA  Auto)
                        THEN  Try  ((Fold  `lg-size`  0  THEN  Auto)\mcdot{})
                        THEN  (((GenConcl  \mkleeneopen{}g[b]  =  X\mkleeneclose{}\mcdot{}  THEN  Try  (Complete  (Auto)))
                                      THENA  (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  Auto)\mcdot{}
                                      )
                                    THEN  RepeatFor  2  (D  -2)
                                    THEN  Reduce  0
                                    THEN  RepeatFor  2  (AutoSplit)
                                    THEN  (RWW  "cons\_member"  0  THEN  MaAuto  THEN  SplitOrHyps  THEN  Auto)\mcdot{})\mcdot{})\}
  )

---

Home Index