Step
*
1
1
of Lemma
length-list-diff
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. ||filter(λa.(¬ba ∈b bs);as)|| ≤ ||as||
6. (∃a∈as. (a ∈ bs))
⊢ (∃x∈as. ¬↑((λa.(¬ba ∈b bs)) x))
BY
{ (Reduce 0 THEN (RWO "l_exists_iff" (-1) THENA Auto)) }
1
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. ||filter(λa.(¬ba ∈b bs);as)|| ≤ ||as||
6. ∃a:T. ((a ∈ as) ∧ (a ∈ bs))
⊢ (∃x∈as. ¬↑¬bx ∈b bs)
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. ||filter(\mlambda{}a.(\mneg{}\msubb{}a \mmember{}\msubb{} bs);as)|| \mleq{} ||as||
6. (\mexists{}a\mmember{}as. (a \mmember{} bs))
\mvdash{} (\mexists{}x\mmember{}as. \mneg{}\muparrow{}((\mlambda{}a.(\mneg{}\msubb{}a \mmember{}\msubb{} bs)) x))
By
Latex:
(Reduce 0 THEN (RWO "l\_exists\_iff" (-1) THENA Auto))
Home
Index