---

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


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)
BY
{ ((RWO "length-append" 0 THENA Auto)
   THEN AutoBoolCase (||v @ filter(λa.(¬b((eq u a) ∨ba ∈b v));d1)|| + 1 =z 0)⋅
   THEN Auto') }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "length-append"  0  THENA  Auto)
  THEN  AutoBoolCase  (||v  @  filter(\mlambda{}a.(\mneg{}\msubb{}((eq  u  a)  \mvee{}\msubb{}a  \mmember{}\msubb{}  v));d1)||  +  1  =\msubz{}  0)\mcdot{}
  THEN  Auto')

---

Home Index