---

Step * of Lemma l_member-iff-length-filter

∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀x:A.  (1 ≤ ||filter(eq x;L)|| ⇐⇒ (x ∈ L))
BY
{ (((UnivCD THENA Auto) THEN (InstLemma `assert-deq-member` [⌜A⌝;⌜eq⌝;⌜L⌝;⌜x⌝]⋅ THENA Auto))
   THEN (RWO "deq-member-length-filter2" (-1) THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN (RWO "-1<" 0 THENA Auto)
   THEN RepUR ``eqof`` 0) }

1
1. [A] : Type
2. eq : EqDecider(A)@i
3. L : A List@i
4. x : A@i
5. 0 < ||filter(λy.(eqof(eq) x y);L)|| ⇐⇒ (x ∈ L)
⊢ 1 ≤ ||filter(eq x;L)|| ⇐⇒ 0 < ||filter(λy.(eq x y);L)||

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}eq:EqDecider(A).  \mforall{}L:A  List.  \mforall{}x:A.    (1  \mleq{}  ||filter(eq  x;L)||  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  (InstLemma  `assert-deq-member`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (RWO  "deq-member-length-filter2"  (-1)  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  RepUR  ``eqof``  0)

---

Home Index