---

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 \p. AutoBoolCase (subtermn 2 (concl p)) p
   THEN Auto'
   THEN \p. AutoBoolCase (subtermn 3 (concl p)) p
   THEN Auto') }

---

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

((RWO  "length-append"  0  THENA  Auto)
  THEN  \mbackslash{}p.  AutoBoolCase  (subtermn  2  (concl  p))  p
  THEN  Auto'
  THEN  \mbackslash{}p.  AutoBoolCase  (subtermn  3  (concl  p))  p
  THEN  Auto')

---

Home Index