Def A == A  False

is mentioned by

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* k:, x,y,z:k. Thm* y = z  x = y  (x, y) = compose_list([(x, z); (y, z); (x, z)])	[flip_lemma]
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* 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* 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* P:(T), L:T List. (xL.P(x))  (filter(P;L) ~ nil)	[filter_is_nil]
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 l_disjoint(T;l1;l2) == x:T. ((x  l1) & (x  l2))	[l_disjoint]

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