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