---

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
{ xxx(((((((((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)⌝⋅)xxx }

---

Latex:

---

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

---

Latex:
xxx(((((((((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{})xxx

---

Home Index