:: deftheorem defines Selection-sort SFMASTR3:def 6 :
for f being FinSeq-Location holds Selection-sort f = ((1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))) :=len f) ";" (for-up ((1 -stRWNotIn ({} Int-Locations)),(intloc 0),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),((FinSeqMin (f,(1 -stRWNotIn ({} Int-Locations)),(1 -stNotUsed (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations))))),(2 -ndRWNotIn ({} Int-Locations)))) ";" (swap (f,(1 -stRWNotIn ({} Int-Locations)),(2 -ndRWNotIn ({} Int-Locations)))))));