---

Step * of Lemma implies-filter-equal

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List].
  (filter(P;L1) = L2 ∈ (T List)) supposing 
     (((∀x:T. ((x ∈ L2) ⇐⇒ (x ∈ L1) ∧ (↑(P x)))) ∧ (∀x,y:T.  (x before y ∈ L2 ⇒ x before y ∈ L1))) and 
     no_repeats(T;L1))
BY
{ (Auto THEN BLemma `filter-equals` THEN Try (Trivial) THEN Try ((D 0 THEN Trivial))) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. L1 : T List
4. L2 : T List
5. no_repeats(T;L1)
6. ∀x:T. ((x ∈ L2) ⇐⇒ (x ∈ L1) ∧ (↑(P x)))
7. ∀x,y:T.  (x before y ∈ L2 ⇒ x before y ∈ L1)
⊢ no_repeats(T;L2)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L1,L2:T  List].
    (filter(P;L1)  =  L2)  supposing 
          (((\mforall{}x:T.  ((x  \mmember{}  L2)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L1)  \mwedge{}  (\muparrow{}(P  x))))
          \mwedge{}  (\mforall{}x,y:T.    (x  before  y  \mmember{}  L2  {}\mRightarrow{}  x  before  y  \mmember{}  L1)))  and 
          no\_repeats(T;L1))


By

---

Latex:
(Auto  THEN  BLemma  `filter-equals`  THEN  Try  (Trivial)  THEN  Try  ((D  0  THEN  Trivial)))

---

Home Index