---

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
{ ((((UnivCD THENA Auto) THEN (InstLemma `fpf-join-dom` [⌈A⌉; ⌈λ2a.Top⌉; ⌈eq⌉; ⌈f⌉; ⌈g⌉; ⌈x⌉])⋅) THENA Auto)
   THEN Try (Trivial)
   ) }

---

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

((((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)
  )

---

Home Index