:: deftheorem defines refers SCMFSA7B:def 1 :
for i being Instruction of SCM+FSA
for a being Int-Location holds
( i refers a iff not for b being Int-Location
for l being Nat
for f being FinSeq-Location holds
( b := a <> i & AddTo (b,a) <> i & SubFrom (b,a) <> i & MultBy (b,a) <> i & Divide (b,a) <> i & Divide (a,b) <> i & a =0_goto l <> i & a >0_goto l <> i & b := (f,a) <> i & (f,b) := a <> i & (f,a) := b <> i & f :=<0,...,0> a <> i ) );