let a be Int-Location ; :: thesis: a := 1 = Load (<*(a := (intloc 0 ))*> ^ <*(halt SCM+FSA )*>)
( 0 |-> (AddTo a,(intloc 0 )) = {} & (<*(a := (intloc 0 ))*> ^ {} ) ^ <*(halt SCM+FSA )*> = <*(a := (intloc 0 ))*> ^ <*(halt SCM+FSA )*> ) by FINSEQ_1:47;
hence a := 1 = Load (<*(a := (intloc 0 ))*> ^ <*(halt SCM+FSA )*>) by Def2; :: thesis: verum