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. T1
4. 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