---

Step * of Lemma fpf-domain-join

No Annotations
∀[A:Type]
  ∀f,g:a:A fp-> Top. ∀eq:EqDecider(A). ∀x:A.  ((x ∈ fpf-domain(f ⊕ g)) ⇐⇒ (x ∈ fpf-domain(f)) ∨ (x ∈ fpf-domain(g)))
BY
{ ((UnivCD THENA Auto)
   THEN ((InstLemma `member-fpf-domain` [⌜A⌝; ⌜f⌝; ⌜eq⌝; ⌜x⌝])⋅ THENA Auto)
   THEN ((InstLemma `member-fpf-domain` [⌜A⌝; ⌜g⌝; ⌜eq⌝; ⌜x⌝])⋅ THENA Auto)
   THEN ((InstLemma `member-fpf-domain` [⌜A⌝; ⌜f ⊕ g⌝; ⌜eq⌝; ⌜x⌝])⋅ THENA Auto)) }

1
1. [A] : Type
2. f : a:A fp-> Top
3. g : a:A fp-> Top
4. eq : EqDecider(A)
5. x : A
6. ↑x ∈ dom(f) ⇐⇒ (x ∈ fpf-domain(f))
7. ↑x ∈ dom(g) ⇐⇒ (x ∈ fpf-domain(g))
8. ↑x ∈ dom(f ⊕ g) ⇐⇒ (x ∈ fpf-domain(f ⊕ g))
⊢ (x ∈ fpf-domain(f ⊕ g)) ⇐⇒ (x ∈ fpf-domain(f)) ∨ (x ∈ fpf-domain(g))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type]
    \mforall{}f,g:a:A  fp->  Top.  \mforall{}eq:EqDecider(A).  \mforall{}x:A.
        ((x  \mmember{}  fpf-domain(f  \moplus{}  g))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  fpf-domain(f))  \mvee{}  (x  \mmember{}  fpf-domain(g)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ((InstLemma  `member-fpf-domain`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `member-fpf-domain`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}g\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `member-fpf-domain`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}f  \moplus{}  g\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index