---

Step * 1 of Lemma l_disjoint-fpf-join-dom


1. A : Type
2. eq : EqDecider(A)
3. f : a:A fp-> Top
4. g : a:A fp-> Top
5. L : A List
6. ∀[a:A]. ¬(a ∈ L) supposing ↑a ∈ dom(f ⊕ g) supposing l_disjoint(A;fst(f ⊕ g);L)
7. l_disjoint(A;fst(f ⊕ g);L) supposing ∀[a:A]. ¬(a ∈ L) supposing ↑a ∈ dom(f ⊕ g)
8. l_disjoint(A;fst(f);L)
9. l_disjoint(A;fst(g);L)
10. ∀[a:A]. ¬(a ∈ L) supposing ↑a ∈ dom(g)
11. ∀[a:A]. ¬(a ∈ L) supposing ↑a ∈ dom(f)
12. l_disjoint(A;fst(g);L)
13. l_disjoint(A;fst(f);L)
⊢ l_disjoint(A;fst(f ⊕ g);L)
BY
{ (BackThruSomeHyp
   THEN Auto
   THEN (RWO "fpf-join-dom" (-1))
   THEN Auto
   THEN (D (-1))
   THEN AllHyps h.(BHyp h THEN Complete (Auto)) ) }

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  f  :  a:A  fp->  Top
4.  g  :  a:A  fp->  Top
5.  L  :  A  List
6.  \mforall{}[a:A].  \mneg{}(a  \mmember{}  L)  supposing  \muparrow{}a  \mmember{}  dom(f  \moplus{}  g)  supposing  l\_disjoint(A;fst(f  \moplus{}  g);L)
7.  l\_disjoint(A;fst(f  \moplus{}  g);L)  supposing  \mforall{}[a:A].  \mneg{}(a  \mmember{}  L)  supposing  \muparrow{}a  \mmember{}  dom(f  \moplus{}  g)
8.  l\_disjoint(A;fst(f);L)
9.  l\_disjoint(A;fst(g);L)
10.  \mforall{}[a:A].  \mneg{}(a  \mmember{}  L)  supposing  \muparrow{}a  \mmember{}  dom(g)
11.  \mforall{}[a:A].  \mneg{}(a  \mmember{}  L)  supposing  \muparrow{}a  \mmember{}  dom(f)
12.  l\_disjoint(A;fst(g);L)
13.  l\_disjoint(A;fst(f);L)
\mvdash{}  l\_disjoint(A;fst(f  \moplus{}  g);L)


By

(BackThruSomeHyp
  THEN  Auto
  THEN  (RWO  "fpf-join-dom"  (-1))
  THEN  Auto
  THEN  (D  (-1))
  THEN  AllHyps  h.(BHyp  h  THEN  Complete  (Auto))  )

---

Home Index