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` THEN Auto) THEN BackThruHyp'' 4) THEN Auto) }

1
1. [T] Type
2. [P] (T List) ⟶ ℙ
3. T ⟶ 𝔹
4. tr1 List
5. tr2 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