(65steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: partial sort exists 1

1. T : Type
2. P : L:(T List)(||L||-1)
3. m : (T List)
4. L:T List, i:(||L||-1).
4. P(L,i P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)
5. L : T List
  L':T List. 
  (L guarded_permutation(T;L,iP(L,i)) L') & (i:(||L'||-1). P(L',i))


By: Decide (0<||L||)


Generated subgoals:

1 6. 0<||L||
  L':T List. 
  (L guarded_permutation(T;L,iP(L,i)) L') & (i:(||L'||-1). P(L',i))

61 steps
2 6. 0<||L||
  L':T List. 
  (L guarded_permutation(T;L,iP(L,i)) L') & (i:(||L'||-1). P(L',i))

2 steps

About:
listboolassertnatural_numberaddsubtractless_thanlambdaapply
functionuniverseimpliesandallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(65steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc