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 ) by SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:50, SCMFSA_2:52, SCMFSA_2:124;
hence not halt SCM+FSA destroys a by Def3; :: thesis: verum