---

Step * of Lemma fpf-join-is-empty

∀[A:Type]. ∀[eq:EqDecider(A)]. ∀[f,g:x:A fp-> Top].  (fpf-is-empty(f ⊕ g) ~ fpf-is-empty(f) ∧b fpf-is-empty(g))
BY
{ (Auto
   THEN (D (-2))
   THEN (D (-1))
   THEN Repeat ((Unfolds ``fpf-is-empty fpf-join fpf-dom`` 0 THEN Reduce 0))
   THEN All Thin) }

1
1. A : Type
2. eq : EqDecider(A)
3. d : A List
4. d1 : A List
⊢ (||d @ filter(λa.(¬ba ∈b d));d1)|| =z 0) = (||d|| =z 0) ∧b (||d1|| =z 0)

---

Latex:


\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[f,g:x:A  fp->  Top].
    (fpf-is-empty(f  \moplus{}  g)  \msim{}  fpf-is-empty(f)  \mwedge{}\msubb{}  fpf-is-empty(g))


By

(Auto
  THEN  (D  (-2))
  THEN  (D  (-1))
  THEN  Repeat  ((Unfolds  ``fpf-is-empty  fpf-join  fpf-dom``  0  THEN  Reduce  0))
  THEN  All  Thin)

---

Home Index