---

Step * 2 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||))
⊢ ∀[bs:T2 List]. ((||zip([u / v];bs)|| ≤ ||[u / v]||) ∧ (||zip([u / v];bs)|| ≤ ||bs||))
BY
{ (InductionOnList⋅ THEN RecUnfold `zip` 0 THEN Reduce 0 THEN Try (Complete (Auto'))) }

1
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))

---

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||))
\mvdash{}  \mforall{}[bs:T2  List].  ((||zip([u  /  v];bs)||  \mleq{}  ||[u  /  v]||)  \mwedge{}  (||zip([u  /  v];bs)||  \mleq{}  ||bs||))


By

---

Latex:
(InductionOnList\mcdot{}  THEN  RecUnfold  `zip`  0  THEN  Reduce  0  THEN  Try  (Complete  (Auto')))

---

Home Index