let a be Int-Location ; :: thesis: halt SCM+FSA does_not_refer a
for b being Int-Location
for l being Instruction-Location of SCM+FSA
for f being FinSeq-Location holds
( b := a <> halt SCM+FSA & AddTo b,a <> halt SCM+FSA & SubFrom b,a <> halt SCM+FSA & MultBy b,a <> halt SCM+FSA & Divide a,b <> halt SCM+FSA & Divide b,a <> halt SCM+FSA & a =0_goto l <> halt SCM+FSA & a >0_goto l <> halt SCM+FSA & b := f,a <> halt SCM+FSA & f,b := a <> halt SCM+FSA & f,a := b <> halt SCM+FSA & f :=<0,...,0> a <> halt SCM+FSA ) by SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:53, SCMFSA_2:124;
hence halt SCM+FSA does_not_refer a by SCMFSA7B:def 1; :: thesis: verum