---

Step * of Lemma fpf-join-list-domain2

∀[A:Type]. ∀eq:EqDecider(A). ∀L:a:A fp-> Top List. ∀x:A.  ((x ∈ fpf-domain(⊕(L))) ⇐⇒ (∃f∈L. (x ∈ fpf-domain(f))))
BY
{ (InstLemma `fpf-join-list-dom2` []
   THEN RepeatFor 4 ((ParallelLast THEN Thin (-3)))
   THEN (RWO "member-fpf-domain" (-1) THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN (All (RWO "member-fpf-domain")⋅ THEN Auto)⋅) }

---

Latex:


\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A).  \mforall{}L:a:A  fp->  Top  List.  \mforall{}x:A.
        ((x  \mmember{}  fpf-domain(\moplus{}(L)))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}f\mmember{}L.  (x  \mmember{}  fpf-domain(f))))


By

(InstLemma  `fpf-join-list-dom2`  []
  THEN  RepeatFor  4  ((ParallelLast  THEN  Thin  (-3)))
  THEN  (RWO  "member-fpf-domain"  (-1)  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  (All  (RWO  "member-fpf-domain")\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index