Step * 1 1 of Lemma select_zip


1. T1 Type
2. T2 Type
3. T1
4. T1 List
5. ∀[bs:T2 List]. ∀[i:ℕ].  zip(v;bs)[i] = <v[i], bs[i]> ∈ (T1 × T2) supposing i < ||zip(v;bs)||
6. u1 T2
7. v1 T2 List
8. ∀[i:ℕ]. zip([u v];v1)[i] = <[u v][i], v1[i]> ∈ (T1 × T2) supposing i < ||zip([u v];v1)||
9. : ℕ
10. i < ||zip(v;v1)|| 1
11. 0 ∈ ℤ
⊢ [<u, u1> zip(v;v1)][0] = <[u v][0], [u1 v1][0]> ∈ (T1 × T2)
BY
(Reduce THEN Auto{1,3}-1)⋅ }


Latex:


Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  u  :  T1
4.  v  :  T1  List
5.  \mforall{}[bs:T2  List].  \mforall{}[i:\mBbbN{}].    zip(v;bs)[i]  =  <v[i],  bs[i]>  supposing  i  <  ||zip(v;bs)||
6.  u1  :  T2
7.  v1  :  T2  List
8.  \mforall{}[i:\mBbbN{}].  zip([u  /  v];v1)[i]  =  <[u  /  v][i],  v1[i]>  supposing  i  <  ||zip([u  /  v];v1)||
9.  i  :  \mBbbN{}
10.  i  <  ||zip(v;v1)||  +  1
11.  i  =  0
\mvdash{}  [<u,  u1>  /  zip(v;v1)][0]  =  <[u  /  v][0],  [u1  /  v1][0]>


By


Latex:
(Reduce  0  THEN  Auto\{1,3\}-1)\mcdot{}




Home Index