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