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