---

Step * of Lemma lg-edge-map

∀[T,S:Type].  ∀f:T ⟶ S. ∀g:LabeledGraph(T). ∀a,b:ℕlg-size(g).  (lg-edge(lg-map(f;g);a;b) ⇐⇒ lg-edge(g;a;b))
BY
{ (RepUR ``lg-size lg-map lg-edge lg-in-edges`` 0
   THEN (UnivCD THENA (Auto THEN Fold `lg-size` 0 THEN Auto))
   THEN ((RWW "select-map" 0 THENM Reduce 0)⋅ THENA 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 5)
                 THEN Auto
                 THEN Fold `lg-size` 0
                 THEN Auto)⋅
          )⋅
         THEN RepeatFor 2 (D -2)
         THEN Reduce 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].
    \mforall{}f:T  {}\mrightarrow{}  S.  \mforall{}g:LabeledGraph(T).  \mforall{}a,b:\mBbbN{}lg-size(g).    (lg-edge(lg-map(f;g);a;b)  \mLeftarrow{}{}\mRightarrow{}  lg-edge(g;a;b))


By

---

Latex:
(RepUR  ``lg-size  lg-map  lg-edge  lg-in-edges``  0
  THEN  (UnivCD  THENA  (Auto  THEN  Fold  `lg-size`  0  THEN  Auto))
  THEN  ((RWW  "select-map"  0  THENM  Reduce  0)\mcdot{}  THENA  Auto)
  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  5)
                              THEN  Auto
                              THEN  Fold  `lg-size`  0
                              THEN  Auto)\mcdot{}
                )\mcdot{}
              THEN  RepeatFor  2  (D  -2)
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index