---

Step * of Lemma fpf-join-dom2

∀[A:Type]. ∀eq:EqDecider(A). ∀f,g:a:A fp-> Top. ∀x:A.  (↑x ∈ dom(f ⊕ g) ⇐⇒ (↑x ∈ dom(f)) ∨ (↑x ∈ dom(g)))
BY
{ xxx((((UnivCD THENA Auto) THEN (InstLemma `fpf-join-dom` [⌜A⌝; ⌜λ2a.Top⌝; ⌜eq⌝; ⌜f⌝; ⌜g⌝; ⌜x⌝])⋅) THENA Auto)
      THEN Try (Trivial)
      )xxx }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}eq:EqDecider(A).  \mforall{}f,g:a:A  fp->  Top.  \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((((UnivCD  THENA  Auto)  THEN  (InstLemma  `fpf-join-dom`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}a.Top\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}g\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{})
          THENA  Auto
          )
        THEN  Try  (Trivial)
        )xxx

---

Home Index