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

now

let e be Int-Location ; :: thesis: 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 & a :==1 <> b =0_goto l )
let f be FinSeq-Location ; :: thesis: ( 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 & a :==1 <> b =0_goto l )
thus a := e <> b =0_goto l ; :: thesis: ( 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 & a :==1 <> b =0_goto l )
thus AddTo (a,e) <> b =0_goto l ; :: thesis: ( 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 & a :==1 <> b =0_goto l )
thus SubFrom (a,e) <> b =0_goto l ; :: thesis: ( 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 & a :==1 <> b =0_goto l )
thus MultBy (a,e) <> b =0_goto l ; :: thesis: ( 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 & a :==1 <> b =0_goto l )
thus ( Divide (a,e) <> b =0_goto l & Divide (e,a) <> b =0_goto l ) ; :: thesis: ( a := (f,e) <> b =0_goto l & a :=len f <> b =0_goto l & a :==1 <> b =0_goto l )
thus a := (f,e) <> b =0_goto l ; :: thesis: ( a :=len f <> b =0_goto l & a :==1 <> b =0_goto l )
thus a :=len f <> b =0_goto l ; :: thesis: a :==1 <> b =0_goto l
thus a :==1 <> b =0_goto l ; :: thesis: verum

end;

hence not b =0_goto l destroys a by Def3; :: thesis: verum