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