let a be Int-Location ; :: thesis: a := 0 = Load ((<*(a := (intloc 0 ))*> ^ <*(SubFrom a,(intloc 0 ))*>) ^ <*(halt SCM+FSA )*>)
( 1 |-> (SubFrom a,(intloc 0 )) = <*(SubFrom a,(intloc 0 ))*> & 1 + 0 = 1 ) by FINSEQ_2:73;
hence a := 0 = Load ((<*(a := (intloc 0 ))*> ^ <*(SubFrom a,(intloc 0 ))*>) ^ <*(halt SCM+FSA )*>) by Def2; :: thesis: verum