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