---

Step * of Lemma zip_length

∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List].  ((||zip(as;bs)|| ≤ ||as||) ∧ (||zip(as;bs)|| ≤ ||bs||))
BY
{ InductionOnList }

1
1. T1 : Type
2. T2 : Type
⊢ ∀[bs:T2 List]. ((||zip([];bs)|| ≤ ||[]||) ∧ (||zip([];bs)|| ≤ ||bs||))

2
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||))
⊢ ∀[bs:T2 List]. ((||zip([u / v];bs)|| ≤ ||[u / v]||) ∧ (||zip([u / v];bs)|| ≤ ||bs||))

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[as:T1  List].  \mforall{}[bs:T2  List].
    ((||zip(as;bs)||  \mleq{}  ||as||)  \mwedge{}  (||zip(as;bs)||  \mleq{}  ||bs||))


By

---

Latex:
InductionOnList

---

Home Index