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