---

Step * of Lemma lg-all-map

∀[A,T:Type].  ∀f:A ⟶ T. ∀[P:T ⟶ ℙ]. ∀g:LabeledGraph(A). (∀x∈lg-map(f;g).P[x] ⇐⇒ ∀x∈g.P[f x])
BY
{ (Auto
   THEN ParallelLast
   THEN (Assert lg-size(lg-map(f;g)) ~ lg-size(g) BY
               (RepUR ``lg-map lg-size`` 0 THEN RWO "length-map-sq" 0 THEN Auto))
   THEN HypSubst (-1) 0
   THEN HypSubst (-1) (-2)
   THEN ParallelOp -2
   THEN MoveToConcl (-1)
   THEN RepUR ``lg-label lg-map`` 0
   THEN (RWO  "select-map" 0 THENA (Auto THEN Fold `lg-size` 0 THEN Auto))
   THEN Reduce 0
   THEN Dlg 5
   THEN (GenConcl ⌜g[n] = tr ∈ (A × ℕlg-size(g) List × (ℕlg-size(g) List))⌝⋅
         THENA (Auto THEN Fold `lg-size` 0 THEN Auto)
         )
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,T:Type].    \mforall{}f:A  {}\mrightarrow{}  T.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}g:LabeledGraph(A).  (\mforall{}x\mmember{}lg-map(f;g).P[x]  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x\mmember{}g.P[f  x])


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  (Assert  lg-size(lg-map(f;g))  \msim{}  lg-size(g)  BY
                          (RepUR  ``lg-map  lg-size``  0  THEN  RWO  "length-map-sq"  0  THEN  Auto))
  THEN  HypSubst  (-1)  0
  THEN  HypSubst  (-1)  (-2)
  THEN  ParallelOp  -2
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``lg-label  lg-map``  0
  THEN  (RWO    "select-map"  0  THENA  (Auto  THEN  Fold  `lg-size`  0  THEN  Auto))
  THEN  Reduce  0
  THEN  Dlg  5
  THEN  (GenConcl  \mkleeneopen{}g[n]  =  tr\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  Fold  `lg-size`  0  THEN  Auto))
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index