---

Step * of Lemma fpf-join-list-domain

∀[A:Type]
  ∀eq:EqDecider(A)
    ∀[B:A ⟶ Type]. ∀L:a:A fp-> B[a] List. ∀x:A.  ((x ∈ fpf-domain(⊕(L))) ⇐⇒ (∃f∈L. (x ∈ fpf-domain(f))))
BY
{ (InstLemma `fpf-join-list-dom` []
   THEN RepeatFor 5 ((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:

---

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


By

---

Latex:
(InstLemma  `fpf-join-list-dom`  []
  THEN  RepeatFor  5  ((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