Def P  Q == PQ

is mentioned by

Thm* l:T List, x,y,z:T. Thm* no_repeats(T;l)  x before y  l  y before z  l  x before z  l	[l_before_transitivity]
Thm* L1,L2,L:T List, x:T. Thm* no_repeats(T;L)  L1 @ [x]  L  [x / L2]  L  L1 @ [x / L2]  L	[append_overlapping_sublists]
Thm* l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y)	[no_repeats_iff]
Thm* as:T1 List, bs:T2 List. ||as|| = ||bs||    unzip(zip(as;bs)) = <as,bs>	[unzip_zip]
Thm* as:T1 List, bs:T2 List. ||as|| = ||bs||    ||zip(as;bs)|| = ||as||	[length_zip]
Thm* as:T1 List, bs:T2 List, i:. Thm* i<||zip(as;bs)||  zip(as;bs)[i] = <as[i],bs[i]>	[select_zip]
Thm* L_1,L_2:T List. L_1  L_2  L_1  L_2	[iseg_is_sublist]
Thm* l1,l2:T List. l1  l2  ||l1||||l2||	[iseg_length]
Thm* P:(T), L2,L1:T List. L1  L2  filter(P;L1)  filter(P;L2)	[filter_iseg]
Thm* l1,l2:T List, x:T. l1  l2  (x  l1)  (x  l2)	[iseg_member]
Thm* l1,l2:T List. l1  l2  ||l1||||l2|| & (i:. i<||l1||  l1[i] = l2[i])	[iseg_select]
Thm* l1,l2,l3:T List. l2  l3  l1  l2  l1  l3	[iseg_transitivity2]
Thm* l1,l2,l3:T List. l1  l2  l1  l2 @ l3	[iseg_append]
Thm* l1,l2,l3:T List. l1  l2  l2  l3  l1  l3	[iseg_transitivity]
Thm* L:A List, f1,f2:(A). f1 = f2  (filter(f1;L) ~ filter(f2;L))	[filter_functionality]
Thm* L:T List, a,b:T. a before b  L  (a  L)	[l_before_member2]
Thm* L:T List, a,b:T. a before b  L  (b  L)	[l_before_member]
Thm* x,y:T, L:T List. Thm* (x  L)  (y  L)  x = y  x before y  L  y before x  L	[l_tricotomy]
Thm* L:T List, i,j:||L||. i<j  [L[i]; L[j]]  L	[sublist_pair]
Thm* L1,L2:T List. null(L2)  L1  tl(L2)  L1  L2	[sublist_tl]
Thm* L1,L2:T List. L1 = L2  L1  L2	[sublist_weakening]
Thm* L1,L2:T List. L1  L2  L2  L1  L1 = L2	[sublist_antisymmetry]
Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2	[proper_sublist_length]
Thm* L1,L2:T List. L1  L2  ||L1||||L2||	[length_sublist]
Thm* L1,L2,L3:T List. L1  L2  L2  L3  L1  L3	[sublist_transitivity]
Thm* L:T List, x:T. null(L)  last([x / L]) = last(L)	[last_cons]
Thm* T:Type, L:T List. null(L)  last(L)  T	[last_wf]
Thm* x:T, l:T List. (y:T. Dec(x = y))  Dec((x  l))	[l_member_decidable]
Thm* L:T List, x:T. (x  L)  null(L)	[member_null]
Thm* L:T List, x:T. null(L)  (x  L)	[null_member]
Thm* as:T List, x:T. 0<||as||  (x  tl(as))  (x  as)	[member_tl]
Thm* a:T List, f:(TT). (x:T. (x  a)  f(x) = x)  map(f;a) = a	[trivial_map]
Thm* a:T List, f,g:(TT'). Thm* (x:T. (x  a)  f(x) = g(x))  map(f;a) = map(g;a)	[map_equal2]
Thm* L:T List. L = nil  (x:T. (x  L))	[member_exists]
Thm* z:T List. ||z|| = 2    z = [z[0]; z[1]]	[list_2_decomp]
Thm* Q:((T List)Prop).  Thm* Q(nil)  (ys:T List, x:T. Q(ys)  Q(ys @ [x]))  (zs:T List. Q(zs))	[list_append_singleton_ind]
Thm* L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x]))	[list_decomp_reverse]
Thm* a:T List, f,g:(TT'). Thm* (i:. i<||a||  f(a[i]) = g(a[i]))  map(f;a) = map(g;a)	[map_equal]
Thm* a,b:T List. ||a|| = ||b||    (i:. i<||a||  a[i] = b[i])  a = b	[list_extensionality]
Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])	[nth_tl_decomp]
Thm* L:T List. 0<||L||  (L ~ [hd(L) / tl(L)])	[list_decomp]
Thm* L:T List. L = nil  0<||L||	[non_nil_length]
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]
Def no_repeats(T;l) == i,j:. i<||l||  j<||l||  i = j  l[i] = l[j]  T	[no_repeats]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 mb basic rel 1 mb nat

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