theorem :: SFMASTR3:34

for s being State of SCM+FSA
for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )