mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Dec(P) == P  P

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* n:, R:(nnProp). (i,j:n. Dec(i R j))  (i,j:n. Dec(i (R^*) j))[decidable__rel_star]
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* F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))[decidable__l_exists]
Thm* F:(AProp), L:A List. (k:A. Dec(F(k)))  Dec((kL.F(k)))[decidable__l_all]

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

mb list 2 Sections MarkB generic Doc