---

Step * of Lemma l_disjoint-fpf-join-dom

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:a:A fp-> Top]. ∀[L:A List].
  uiff(l_disjoint(A;fst(f ⊕ g);L);l_disjoint(A;fst(f);L) ∧ l_disjoint(A;fst(g);L))
BY
{ ((((((((UnivCD THENA Auto) THEN (InstLemma `l_disjoint-fpf-dom` [⌜A⌝; ⌜eq⌝; ⌜f⌝; ⌜L⌝])⋅) THENA Auto)
       THEN (D (-1))
       THEN (InstLemma `l_disjoint-fpf-dom` [⌜A⌝; ⌜eq⌝; ⌜g⌝; ⌜L⌝])⋅)
      THENA Auto
      )
     THEN (D (-1))
     THEN (InstLemma `l_disjoint-fpf-dom` [⌜A⌝; ⌜eq⌝; ⌜f ⊕ g⌝; ⌜L⌝])⋅)
    THENA Auto
    )
   THEN (D (-1))
   THEN Auto
   THEN ThinTrivial) }

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:a:A  fp->  Top].  \mforall{}[L:A  List].
    uiff(l\_disjoint(A;fst(f  \moplus{}  g);L);l\_disjoint(A;fst(f);L)  \mwedge{}  l\_disjoint(A;fst(g);L))


By

---

Latex:
((((((((UnivCD  THENA  Auto)  THEN  (InstLemma  `l\_disjoint-fpf-dom`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{})  THENA  Auto)
          THEN  (D  (-1))
          THEN  (InstLemma  `l\_disjoint-fpf-dom`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}g\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{})
        THENA  Auto
        )
      THEN  (D  (-1))
      THEN  (InstLemma  `l\_disjoint-fpf-dom`  [\mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}eq\mkleeneclose{};  \mkleeneopen{}f  \moplus{}  g\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{})
    THENA  Auto
    )
  THEN  (D  (-1))
  THEN  Auto
  THEN  ThinTrivial)

---

Home Index