let a be Int-Location ; :: thesis: halt SCM+FSA does_not_destroy a
for b being Int-Location
for l being Instruction-Location of SCM+FSA
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 halt SCM+FSA does_not_destroy a by Def3; :: thesis: verum