let a, b be Int-Location ; :: thesis:
let l be Element of NAT ; :: thesis:

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

end;

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