mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  == Unit+Unit

is mentioned by

Thm* P:(AAProp), f:(A), L1,L2:A List.
Thm* (L1 swap adjacent[P(x,y)] L2)
Thm* 
Thm* (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2))
Thm*  filter(f;L1) = filter(f;L2)		[filter_swap_adjacent]
Thm* L:T List, P:(TT).
Thm* (x,y:T. P(x,y)  P(y,x))
Thm* 
Thm* (L':T List. 
Thm* ((L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')
Thm* (& (i:(||L'||-1). P(L'[i],L'[(i+1)])))		[partial_sort_exists_2]
Thm* L:T List, P:(TT), n:(||L||-1).
Thm* count(x < y in swap(L;n;n+1) | P(x,y))
Thm* =
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P(L[(n+1)]
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if P,L[n])
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+if 1
Thm* count(x < y in L | P(x,y))+if P(L[n],L[(n+1)]) -1 else 0 fi+else 0 fi		[count_pairs_swap]
Thm* P:(L:(T List)(||L||-1)), m:((T List)).
Thm* (L:T List, i:(||L||-1).
Thm* (P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))
Thm* 
Thm* (L:T List. 
Thm* (L':T List. 
Thm* ((L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))		[partial_sort_exists]
Thm* T:Type, L:T List, P:(TT). count(x < y in L | P(x,y))  [count_pairs_wf]
Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x:T'.
Thm* (x  mapfilter(f;P;L))  (y:T. (y  L) & P(y) & x = f(y))		[member_map_filter]
Thm* T:Type, P:(T), T':Type, f:({x:T| P(x) }T'), L:T List.
Thm* mapfilter(f;P;L)  T' List		[mapfilter_wf]
Thm* P:(T), l:T List. no_repeats(T;l)  no_repeats(T;filter(P;l))[no_repeats_filter]
Thm* l:T List, P:(T), x,y:T.
Thm* x before y  filter(P;l)  P(x) & P(y) & x before y  l		[l_before_filter]
Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))[sublist_filter]
Thm* L:T List, P:(T). (xL.P(x))  reduce(x,y. P(x)y;true;L)[l_all_reduce]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ nil)[filter_is_nil]
Thm* P:(T), L:T List. (xL.P(x))  filter(P;L) = L[filter_trivial2]
Thm* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ L)[filter_trivial]

In prior sections: bool 1 rel 1 list 1 sqequal 1 mb nat mb list 1

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

mb list 2 Sections MarkB generic Doc