mb collection Sections GenAutomata Doc

Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

is mentioned by

Thm* l:Collection(T) List, x:T List. x col_list_prod(l) ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])[member_col_list_prod]
Def col_list_prod(l)(x) == ||x|| = ||l|| & (i:. i < ||x|| x[i] l[i])[col_list_prod]

In prior sections: list 1

Try larger context: GenAutomata

mb collection Sections GenAutomata Doc