:: deftheorem defines insert-sort SCMISORT:def 2 :
for f being FinSeq-Location holds insert-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)) ";" (SubFrom ((intloc 1),(intloc 0)))) ";" (Times ((intloc 1),(((((((((intloc 2) :=len f) ";" (SubFrom ((intloc 2),(intloc 1)))) ";" ((intloc 3) := (intloc 2))) ";" (AddTo ((intloc 3),(intloc 0)))) ";" ((intloc 6) := (f,(intloc 3)))) ";" (SubFrom ((intloc 4),(intloc 4)))) ";" (while>0 ((intloc 2),((((intloc 5) := (f,(intloc 2))) ";" (SubFrom ((intloc 5),(intloc 6)))) ";" (if>0 ((intloc 5),(Macro (SubFrom ((intloc 2),(intloc 2)))),((AddTo ((intloc 4),(intloc 0))) ";" (SubFrom ((intloc 2),(intloc 0)))))))))) ";" (Times ((intloc 4),(((((((intloc 2) := (intloc 3)) ";" (SubFrom ((intloc 3),(intloc 0)))) ";" ((intloc 5) := (f,(intloc 2)))) ";" ((intloc 6) := (f,(intloc 3)))) ";" ((f,(intloc 2)) := (intloc 6))) ";" ((f,(intloc 3)) := (intloc 5))))))));