as:T1 List, bs:T2 List, i:
.
Thm* i<||zip(as;bs)||
zip(as;bs)[i] = <as[i],bs[i]>a:T, as:T List, i:
. 0<i i
||as|| [a / as][i] = as[(i-1)]as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||| Theorem | Name |
| as:T1 List, bs:T2 List, i:.
Thm* i<||zip(as;bs)|| zip(as;bs)[i] = <as[i],bs[i]> | [select_zip] |
| cites the following: | |
| a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |
| as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs|| | [zip_length] |