let a be Int-Location; :: thesis: a := 1 = <%(a := (intloc 0))%> ^ (Stop SCM+FSA)
A1: 0 + 1 = 1 ;
<%(a := (intloc 0))%> ^ (Stop SCM+FSA) = (<%(a := (intloc 0))%> ^ {}) ^ (Stop SCM+FSA)
.= (<%(a := (intloc 0))%> ^ (0 --> (AddTo (a,(intloc 0))))) ^ (Stop SCM+FSA) ;
hence a := 1 = <%(a := (intloc 0))%> ^ (Stop SCM+FSA) by Def1, A1; :: thesis: verum