Theorem | Name |
Thm* l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i<||l1|| l1[i] = l2[i]) | [iseg_select] |
cites the following: |
Thm* a:T, as:T List, i:. i0 [a / as][i] = a | [select_cons_hd] |
Thm* a,b:T, l1,l2:T List. [a / l1] [b / l2] a = b & l1 l2 | [cons_iseg] |
Thm* a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |