let a be Int-Location ; :: thesis: not halt SCM+FSA destroys a
for b being Int-Location
for l being Element of NAT
for f being FinSeq-Location holds
( a := b <> halt SCM+FSA & AddTo (a,b) <> halt SCM+FSA & SubFrom (a,b) <> halt SCM+FSA & MultBy (a,b) <> halt SCM+FSA & Divide (a,b) <> halt SCM+FSA & Divide (b,a) <> halt SCM+FSA & a := (f,b) <> halt SCM+FSA & a :=len f <> halt SCM+FSA ) ;
hence not halt SCM+FSA destroys a by Def3; :: thesis: verum