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

let b be Int-Location ; :: thesis:
let r be Element of NAT ; :: thesis:
let f be FinSeq-Location ; :: thesis:
thus a := b <> goto l ; :: thesis:
thus AddTo (a,b) <> goto l ; :: thesis:
thus SubFrom (a,b) <> goto l ; :: thesis:
thus MultBy (a,b) <> goto l ; :: thesis:
thus ( Divide (a,b) <> goto l & Divide (b,a) <> goto l ) ; :: thesis:
thus a := (f,b) <> goto l ; :: thesis:
thus a :=len f <> goto l ; :: thesis:
thus a :==1 <> goto l ; :: thesis:

end;

hence not goto l destroys a by Def3; :: thesis: