Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* P:(AAProp), f:(BA), x,y:B List. Thm* (x swap adjacent[P(f(x),f(y))] y) Thm*  Thm* (map(f;x) swap adjacent[P(x,y)] map(f;y))	[swap_adjacent_map]
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* P:(AAProp), X,Y:A List, a,b:A. Thm* P(a,b)  ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))	[swap_adjacent_instance]
Thm* P:(AAProp).  Thm* (Sym x,y:A. P(x,y))  (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)	[symmetric_swap_adjacent]
Thm* L:T List, P:(TTProp). Thm* (x,y:T. Dec(P(x,y))) Thm*  Thm* (x,y:T. P(x,y)  P(y,x)) Thm*  Thm* (L':T List.  Thm* ((L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)])))	[partial_sort]
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* n,m:, f:(nm), p:(nn), q:(mm). Thm* Bij(n; n; p) Thm*  Thm* Bij(m; m; q) Thm*  Thm* sum(f(p(x),q(y)) | x < n; y < m) = sum(f(x,y) | x < n; y < m)	[permute_double_sum]
Thm* n:, f:(n), p:(nn). Thm* Bij(n; n; p)  sum(f(p(x)) | x < n) = sum(f(x) | x < n)	[permute_sum]
Thm* k:, p:(kk). Bij(k; k; p)  (L:(k-1) List. p = compose_flips(L))	[permute_by_flips]
Thm* k:, x,y:k. L:(k-1) List. (x, y) = compose_flips(L)	[flip_adjacent]
Thm* k:, L1,L2:(k-1) List. Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)	[compose_flips_append]
Thm* k:, L:(k-1) List. compose_flips(L)  kk	[compose_flips_wf]
Thm* k:, x,y,z:k. Thm* y = z  x = y  (x, y) = compose_list([(x, z); (y, z); (x, z)])	[flip_lemma]
Thm* L1,L2:(TT) List. Thm* compose_list(L1) o compose_list(L2) = compose_list(L1 @ L2)	[compose_append]
Thm* n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i (R^*) j))	[decidable__rel_star]
Thm* n:, R:(nnProp), x,y:n. (x (R^*) y)  (k:(n+1). x R^k y)	[rel_star_finite]
Thm* R:(TTProp), k:, x,y:T. Thm* (x R^k y) Thm*  Thm* (L:T List.  Thm* (||L|| = k+1   & L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))	[rel_exp_list]
Thm* f,g:(TT). Bij(T; T; f)  Bij(T; T; g)  Bij(T; T; f o g)	[compose_bij]
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* f:(AB), L1,L2:A List. L1  L2  map(f;L1)  map(f;L2)	[iseg_map]
Thm* T:Type, L:T List, P:(TT). count(x < y in L | P(x,y))	[count_pairs_wf]
Thm* P:(L:(T List)(||L||-1)Prop).  Thm* Trans(T List)(_1 guarded_permutation(T;P) _2)	[guarded_permutation_transitivity]
Thm* f:(BA), x:B List, i,j:||x||. map(f;swap(x;i;j)) = swap(map(f;x);i;j)	[map_swap]
Thm* L:T List, i:(||L||-1), a,b:T. Thm* a before b  swap(L;i;i+1)  a before b  L  a = L[(i+1)] & b = L[i]	[l_before_swap]
Thm* i:, L:A List. Thm* i+1<||L|| Thm*  Thm* (X,Y:A List. Thm* (L = (X @ [L[i]; L[(i+1)]] @ Y) Thm* (& swap(L;i;i+1) = (X @ [L[(i+1)]; L[i]] @ Y))	[swap_adjacent_decomp]
Thm* L:T List, x:T, i,j:{1..(||L||+1)}. Thm* swap([x / L];i;j) = [x / swap(L;i-1;j-1)]	[swap_cons]
Thm* L1,L2:T List, i,j:||L1||. Thm* L2 = swap(L1;i;j) Thm*  Thm* L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||   & L1 = swap(L2;i;j) Thm* & (x:||L2||. x = i  x = j  L2[x] = L1[x])	[swapped_select]
Thm* L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1	[swap_swap]
Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||	[swap_length]
Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))]	[swap_select]
Thm* L:T List, f:(||L||||L||). ||(L o f)|| = ||L||	[permute_list_length]
Thm* L:T List, f:(||L||||L||), i:||L||. (L o f)[i] = L[(f(i))]	[permute_list_select]
Thm* L:T List, P:(||L||Prop). Thm* (x:||L||. Dec(P(x))) Thm*  Thm* (i:||L||. P(i))  (i:||L||. P(i) & (j:||L||. i<j  P(j)))	[last_with_property]
Thm* L:T List, P:(||L||Prop). Thm* (x:||L||. Dec(P(x))) Thm*  Thm* (L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||). Thm* (interleaving_occurence(T;L1;L2;L;f1;f2) Thm* (& (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i))) Thm* (& (i:||L||.  Thm* (& ((P(i)  (j:||L1||. f1(j) = i)) Thm* (& (& (P(i)  (j:||L2||. f2(j) = i))))	[interleaving_split]
Thm* L,L1,L2:T List. interleaving(T;L1;L2;L)  L1  L	[interleaving_sublist]
Thm* L1,L:T List. interleaving(T;L1;nil;L)  L = L1	[nil_interleaving2]
Thm* L1,L:T List. interleaving(T;nil;L1;L)  L = L1	[nil_interleaving]
Thm* L1,L2,L:T List. disjoint_sublists(T;L1;L2;L)  L1  L & L2  L	[disjoint_sublists_sublist]
Thm* L:T List, n:, f:(n||L||). Thm* increasing(f;n) Thm*  Thm* (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))	[range_sublist]
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* F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))	[decidable__l_exists]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x)  (yL.P(y))	[l_exists_cons]
Thm* P:(TProp). (xnil.P(x))  False	[l_exists_nil]
Thm* F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))	[decidable__l_all]
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:(TProp). (xnil.P(x))	[l_all_nil]
Thm* f:(AB), L:A List, P:(BProp). (xmap(f;L).P(x))  (xL.P(f(x)))	[l_all_map]
Thm* L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List	[list_set_type]
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]
Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y))	[l_all_cons]
Def interleaving_occurence(T;L1;L2;L;f1;f2) Def == ||L|| = ||L1||+||L2||   Def == & increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T) Def == & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T) Def == & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2)  )	[interleaving_occurence]
Def disjoint_sublists(T;L1;L2;L) Def == f1:(||L1||||L||), f2:(||L2||||L||). Def == increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T) Def == & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T) Def == & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2))	[disjoint_sublists]
Def sublist_occurence(T;L1;L2;f) Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)	[sublist_occurence]
Def (xL.P(x)) == x:T. (x  L)  P(x)	[l_all]
Def l_disjoint(T;l1;l2) == x:T. ((x  l1) & (x  l2))	[l_disjoint]

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

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