---

Step * 1 of Lemma fpf-join-is-empty


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)
BY
{ ((D (-2)) THEN Reduce 0) }

1
1. A : Type
2. eq : EqDecider(A)
3. d1 : A List
⊢ (||filter(λa.tt;d1)|| =z 0) = (||d1|| =z 0)

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

---

Latex:



1.  A  :  Type
2.  eq  :  EqDecider(A)
3.  d  :  A  List
4.  d1  :  A  List
\mvdash{}  (||d  @  filter(\mlambda{}a.(\mneg{}\msubb{}a  \mmember{}\msubb{}  d));d1)||  =\msubz{}  0)  =  (||d||  =\msubz{}  0)  \mwedge{}\msubb{}  (||d1||  =\msubz{}  0)


By

((D  (-2))  THEN  Reduce  0)

---

Home Index