---

Step * 1 of Lemma safety_induced


1. [A] : Type
2. [B] : Type
3. f : A ⟶ B
4. [P] : (B List) ⟶ ℙ
5. ∀tr1,tr2:B List.  (tr1 ≤ tr2 ⇒ P[tr2] ⇒ P[tr1])
6. tr1 : A List
7. tr2 : A List
8. tr1 ≤ tr2
9. P[map(f;tr2)]
⊢ map(f;tr1) ≤ map(f;tr2)
BY
{ Easy }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  [P]  :  (B  List)  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}tr1,tr2:B  List.    (tr1  \mleq{}  tr2  {}\mRightarrow{}  P[tr2]  {}\mRightarrow{}  P[tr1])
6.  tr1  :  A  List
7.  tr2  :  A  List
8.  tr1  \mleq{}  tr2
9.  P[map(f;tr2)]
\mvdash{}  map(f;tr1)  \mleq{}  map(f;tr2)


By

---

Latex:
Easy

---

Home Index