:: deftheorem defines FinSeqMin SFMASTR3:def 4 :
for start, finish, minpos being Int-Location
for f being FinSeq-Location holds FinSeqMin (f,start,finish,minpos) = (minpos := start) ";" (for-up ((3 -rdRWNotIn {start,finish,minpos}),start,finish,((((1 -stRWNotIn {start,finish,minpos}) := (f,(3 -rdRWNotIn {start,finish,minpos}))) ";" ((2 -ndRWNotIn {start,finish,minpos}) := (f,minpos))) ";" (if>0 ((2 -ndRWNotIn {start,finish,minpos}),(1 -stRWNotIn {start,finish,minpos}),(Macro (minpos := (3 -rdRWNotIn {start,finish,minpos}))),(Stop SCM+FSA))))));