theorem Th31: :: SFMASTR3:33

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 . f) +* ((s . aa),((s . f) . (s . bb)))) +* ((s . bb),((s . f) . (s . aa)))