---

Step * of Lemma filter_strong_safety

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ∀f:T ⟶ 𝔹. (strong_safety(T;L.P L) ⇒ strong_safety(T;L.P filter(f;L)))
BY
{ (((Unfold `strong_safety` 0 THEN Auto) THEN BackThruHyp'' 4) THEN Auto) }

1
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. f : T ⟶ 𝔹
4. tr1 : T List
5. tr2 : T List
6. tr1 ⊆ tr2
7. ∀tr1,tr2:T List.  (tr1 ⊆ tr2 ⇒ {(P tr2) ⇒ (P tr1)})
⊢ filter(f;tr1) ⊆ filter(f;tr2)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}f:T  {}\mrightarrow{}  \mBbbB{}.  (strong\_safety(T;L.P  L)  {}\mRightarrow{}  strong\_safety(T;L.P  filter(f;L)))


By

---

Latex:
(((Unfold  `strong\_safety`  0  THEN  Auto)  THEN  BackThruHyp''  4)  THEN  Auto)

---

Home Index