---

Step * of Lemma fpf-join-wf

∀[A:Type]. ∀[B,C,D:A ─→ Type]. ∀[f:a:A fp-> B[a]]. ∀[g:a:A fp-> C[a]]. ∀[eq:EqDecider(A)].
  (f ⊕ g ∈ a:A fp-> D[a]) supposing 
     ((∀a:A. ((↑a ∈ dom(g)) ⇒ (C[a] ⊆r D[a]))) and 
     (∀a:A. ((↑a ∈ dom(f)) ⇒ (B[a] ⊆r D[a]))))
BY
{ ((UnivCD THENA Auto)
   THEN DVar `f'
   THEN DVar `g'
   THEN (RepUR ``fpf-join fpf fpf-dom fpf-cap`` 0 THEN All (RepUR ``fpf-dom``))
   THEN Auto
   THEN Thin (-1)
   THEN ((RWW "member_append member_filter" (-1) THENM Reduce (-1)) THENA Auto)
   THEN D -1
   THEN Auto) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[B,C,D:A  {}\mrightarrow{}  Type].  \mforall{}[f:a:A  fp->  B[a]].  \mforall{}[g:a:A  fp->  C[a]].  \mforall{}[eq:EqDecider(A)].
    (f  \moplus{}  g  \mmember{}  a:A  fp->  D[a])  supposing 
          ((\mforall{}a:A.  ((\muparrow{}a  \mmember{}  dom(g))  {}\mRightarrow{}  (C[a]  \msubseteq{}r  D[a])))  and 
          (\mforall{}a:A.  ((\muparrow{}a  \mmember{}  dom(f))  {}\mRightarrow{}  (B[a]  \msubseteq{}r  D[a]))))


By

((UnivCD  THENA  Auto)
  THEN  DVar  `f'
  THEN  DVar  `g'
  THEN  (RepUR  ``fpf-join  fpf  fpf-dom  fpf-cap``  0  THEN  All  (RepUR  ``fpf-dom``))
  THEN  Auto
  THEN  Thin  (-1)
  THEN  ((RWW  "member\_append  member\_filter"  (-1)  THENM  Reduce  (-1))  THENA  Auto)
  THEN  D  -1
  THEN  Auto)

---

Home Index