---

Step * of Lemma pairwise-map

∀[T,T2:Type].
  ∀L:T List. ∀[P:T2 ⟶ T2 ⟶ ℙ']. ∀[f:{x:T| (x ∈ L)}  ⟶ T2].  ((∀x,y∈map(f;L).  P[x;y]) ⇐⇒ (∀x,y∈L.  P[f x;f y]))
BY
{ (Intros
   THEN GenConcl ⌜L = LL ∈ ({x:T| (x ∈ L)}  List)⌝⋅
   THEN Auto
   THEN ParallelLast
   THEN (All (RWO "length-map") THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN (RWW "select-map" (-1) THENA Auto)
   THEN RWW "select-map" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,T2:Type].
    \mforall{}L:T  List
        \mforall{}[P:T2  {}\mrightarrow{}  T2  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  T2].
            ((\mforall{}x,y\mmember{}map(f;L).    P[x;y])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}x,y\mmember{}L.    P[f  x;f  y]))


By

---

Latex:
(Intros
  THEN  GenConcl  \mkleeneopen{}L  =  LL\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ParallelLast
  THEN  (All  (RWO  "length-map")  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (RWW  "select-map"  (-1)  THENA  Auto)
  THEN  RWW  "select-map"  0
  THEN  Auto)

---

Home Index