:: deftheorem defines swap SFMASTR3:def 5 :
for f being FinSeq-Location
for a, b being Int-Location holds swap (f,a,b) = ((((1 -stRWNotIn {a,b}) := (f,a)) ";" ((2 -ndRWNotIn {a,b}) := (f,b))) ";" ((f,a) := (2 -ndRWNotIn {a,b}))) ";" ((f,b) := (1 -stRWNotIn {a,b}));