let a, b be Int-Location ; :: thesis: for l being Element of NAT holds not b =0_goto l destroys a
let l be Element of NAT ; :: thesis: not b =0_goto l destroys a
for e being Int-Location
for f being FinSeq-Location holds
( a := e <> b =0_goto l & AddTo (a,e) <> b =0_goto l & SubFrom (a,e) <> b =0_goto l & MultBy (a,e) <> b =0_goto l & Divide (a,e) <> b =0_goto l & Divide (e,a) <> b =0_goto l & a := (f,e) <> b =0_goto l & a :=len f <> b =0_goto l ) ;
hence not b =0_goto l destroys a by Def3; :: thesis: verum