:: deftheorem defines bubble-sort SCMBSORT:def 1 :
for f being FinSeq-Location holds bubble-sort f = (((((((intloc 2) := (intloc 0)) ";" ((intloc 3) := (intloc 0))) ";" ((intloc 4) := (intloc 0))) ";" ((intloc 5) := (intloc 0))) ";" ((intloc 6) := (intloc 0))) ";" ((intloc 1) :=len f)) ";" (Times ((intloc 1),(((((intloc 2) := (intloc 1)) ";" (SubFrom ((intloc 2),(intloc 0)))) ";" ((intloc 3) :=len f)) ";" (Times ((intloc 2),(((((((intloc 4) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 3)))) ";" ((intloc 6) := (f,(intloc 4)))) ";" (SubFrom ((intloc 6),(intloc 5)))) ";" (if>0 ((intloc 6),((((intloc 6) := (f,(intloc 4))) ";" ((f,(intloc 3)) := (intloc 6))) ";" ((f,(intloc 4)) := (intloc 5))),(Stop SCM+FSA)))))))));