let a be Int-Location ; :: thesis: not halt SCM+FSA refers a
for b being Int-Location
for l being Element of NAT
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 ) ;
hence not halt SCM+FSA refers a by SCMFSA7B:def 1; :: thesis: verum