---

Step * of Lemma fpf-join-dom

∀[A:Type]. ∀[B:A ─→ Type].
  ∀eq:EqDecider(A). ∀f,g:a:A fp-> B[a]. ∀x:A.  (↑x ∈ dom(f ⊕ g) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
BY
{ (((((((((Unfolds ``fpf fpf-join fpf-dom`` 0 THEN Unfold `fpf-dom` 0 THEN Reduce 0 THEN UnivCD) THENA Auto)
         THEN RWO "assert-deq-member" 0
         )
        THENA Auto
        )
       THEN RWO "member_append" 0
       )
      THENA Auto
      )
     THEN RWO "member_filter" 0
     )
    THENA (Reduce 0 THEN Auto)
    )
   THEN Reduce 0
   THEN AutoBoolCase ⌈x ∈b fst(f))⌉⋅) }

---

Latex:


\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}eq:EqDecider(A).  \mforall{}f,g:a:A  fp->  B[a].  \mforall{}x:A.    (\muparrow{}x  \mmember{}  dom(f  \moplus{}  g)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}x  \mmember{}  dom(f))  \mvee{}  (\muparrow{}x  \mmember{}  dom(g)))


By

(((((((((Unfolds  ``fpf  fpf-join  fpf-dom``  0  THEN  Unfold  `fpf-dom`  0  THEN  Reduce  0  THEN  UnivCD)
                THENA  Auto
                )
              THEN  RWO  "assert-deq-member"  0
              )
            THENA  Auto
            )
          THEN  RWO  "member\_append"  0
          )
        THENA  Auto
        )
      THEN  RWO  "member\_filter"  0
      )
    THENA  (Reduce  0  THEN  Auto)
    )
  THEN  Reduce  0
  THEN  AutoBoolCase  \mkleeneopen{}x  \mmember{}\msubb{}  fst(f))\mkleeneclose{}\mcdot{})

---

Home Index