mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def AB == B<A

is mentioned by

Thm* as:T1 List, bs:T2 List. ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||[zip_length]
Thm* l1,l2:T List. l1  l2  ||l1||||l2||[iseg_length]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])[iseg_select]
Thm* L1,L2:T List. L1  L2  ||L1||||L2||[length_sublist]
Thm* L:T List, P:(||L||Prop).
Thm* (x:||L||. Dec(P(x)))
Thm* 
Thm* (i,j:||L||. P(i)  i<j  P(j))
Thm* 
Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:||L||. P(i)  ||L_1||i))		[append_split2]

In prior sections: int 1 bool 1 int 2 list 1 mb nat core

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb list 1 Sections MarkB generic Doc