mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  == {i:| 0i }

is mentioned by

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* 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* 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* 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, n:, f:(n||L||).
Thm* increasing(f;n)
Thm* 
Thm* (L1:T List. ||L1|| = n   & sublist_occurence(T;L1;L;f))		[range_sublist]
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 interleaving(T;L1;L2;L)
Def == ||L|| = ||L1||+||L2||   & disjoint_sublists(T;L1;L2;L)		[interleaving]

In prior sections: int 1 bool 1 int 2 num thy 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