theorem :: SCMFSA_7:2

for a being Int-Location holds a := 1 = <%(a := (intloc 0))%> ^ (Stop SCM+FSA)