let a be Int-Location ; :: thesis: a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%>
( 0 + 1 = 1 & <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> = (<%(a := (intloc 0))%> ^ (0 --> (AddTo (a,(intloc 0))))) ^ <%(halt SCM+FSA)%> ) by AFINSQ_1:29;
hence a := 1 = <%(a := (intloc 0))%> ^ <%(halt SCM+FSA)%> by Def2; :: thesis: verum