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