---

Step * 2 of Lemma filter_iseg


1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀L1:T List. (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
⊢ ∀L1:T List. (L1 ≤ [u / v] ⇒ filter(P;L1) ≤ if P u then [u / filter(P;v)] else filter(P;v) fi )
BY
{ ((((((D 0 THENA Auto) THEN ListInd (-1)) THEN Reduce 0) THEN All (Unfold `let`)) THEN All Reduce) THEN Auto) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀L1:T List. (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
6. u1 : T
7. v1 : T List
8. v1 ≤ [u / v] ⇒ filter(P;v1) ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 
9. [u1 / v1] ≤ [u / v]
⊢ if P u1 then [u1 / filter(P;v1)] else filter(P;v1) fi  ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}L1:T  List.  (L1  \mleq{}  v  {}\mRightarrow{}  filter(P;L1)  \mleq{}  filter(P;v))
\mvdash{}  \mforall{}L1:T  List.  (L1  \mleq{}  [u  /  v]  {}\mRightarrow{}  filter(P;L1)  \mleq{}  if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi  )


By

---

Latex:
((((((D  0  THENA  Auto)  THEN  ListInd  (-1))  THEN  Reduce  0)  THEN  All  (Unfold  `let`))  THEN  All  Reduce)
  THEN  Auto
  )

---

Home Index