Step * 1 of Lemma zip_unzip


[T1,T2:Type]. ∀[as:(T1 × T2) List].
  (zip(fst(<map(λp.(fst(p));as), map(λp.(snd(p));as)>);snd(<map(λp.(fst(p));as), map(λp.(snd(p));as)>)) as ∈ ((T1 × T2\000C) List))
BY
(InductionOnList THEN All Reduce THEN Try (Complete (Auto{1,3}-1))) }

1
1. T1 Type
2. T2 Type
3. T1 × T2
4. (T1 × T2) List
5. zip(map(λp.(fst(p));v);map(λp.(snd(p));v)) v ∈ ((T1 × T2) List)
⊢ [<fst(u), snd(u)> zip(map(λp.(fst(p));v);map(λp.(snd(p));v))] [u v] ∈ ((T1 × T2) List)


Latex:


Latex:

\mforall{}[T1,T2:Type].  \mforall{}[as:(T1  \mtimes{}  T2)  List].
    (zip(fst(<map(\mlambda{}p.(fst(p));as),  map(\mlambda{}p.(snd(p));as)>);snd(<map(\mlambda{}p.(fst(p));as),  map(\mlambda{}p.(snd(p));as)\000C>))  =  as)


By


Latex:
(InductionOnList  THEN  All  Reduce  THEN  Try  (Complete  (Auto\{1,3\}-1)))




Home Index