---

Step * 2 1 of Lemma zip_length


1. T1 : Type
2. T2 : Type
3. u : T1
4. v : T1 List
5. ∀[bs:T2 List]. ((||zip(v;bs)|| ≤ ||v||) ∧ (||zip(v;bs)|| ≤ ||bs||))
6. u1 : T2
7. v1 : T2 List
8. (||zip([u / v];v1)|| ≤ ||[u / v]||) ∧ (||zip([u / v];v1)|| ≤ ||v1||)
⊢ ((||zip(v;v1)|| + 1) ≤ (||v|| + 1)) ∧ ((||zip(v;v1)|| + 1) ≤ (||v1|| + 1))
BY
{ (AllHyps (InstHyp [v1]) THEN Auto) }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  u  :  T1
4.  v  :  T1  List
5.  \mforall{}[bs:T2  List].  ((||zip(v;bs)||  \mleq{}  ||v||)  \mwedge{}  (||zip(v;bs)||  \mleq{}  ||bs||))
6.  u1  :  T2
7.  v1  :  T2  List
8.  (||zip([u  /  v];v1)||  \mleq{}  ||[u  /  v]||)  \mwedge{}  (||zip([u  /  v];v1)||  \mleq{}  ||v1||)
\mvdash{}  ((||zip(v;v1)||  +  1)  \mleq{}  (||v||  +  1))  \mwedge{}  ((||zip(v;v1)||  +  1)  \mleq{}  (||v1||  +  1))


By

---

Latex:
(AllHyps  (InstHyp  [v1])  THEN  Auto)

---

Home Index