---

Step * of Lemma filter_before

∀[A:Type]. ∀L:A List. ∀P:A ⟶ 𝔹. ∀x,y:A.  (x before y ∈ filter(P;L) ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ L)
BY
{ ((RepeatFor 2 (D 0 THENA Auto) THEN ListInd (-1)) THEN Reduce 0) }

1
1. [A] : Type
⊢ ∀P:A ⟶ 𝔹. ∀x,y:A.  (x before y ∈ [] ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ [])

2
1. [A] : Type
2. u : A
3. v : A List
4. ∀P:A ⟶ 𝔹. ∀x,y:A.  (x before y ∈ filter(P;v) ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ v)
⊢ ∀P:A ⟶ 𝔹. ∀x,y:A.
    (x before y ∈ if P u then [u / filter(P;v)] else filter(P;v) fi  ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ [u / v])

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}L:A  List.  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,y:A.    (x  before  y  \mmember{}  filter(P;L)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(P  x))  \mwedge{}  (\muparrow{}(P  y))  \mwedge{}  x  before  y  \mmember{}  L)


By

---

Latex:
((RepeatFor  2  (D  0  THENA  Auto)  THEN  ListInd  (-1))  THEN  Reduce  0)

---

Home Index