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

now

let b be Int-Location ; :: thesis: for r 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 )
let r be Element of NAT ; :: thesis: 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 )
let f be FinSeq-Location ; :: thesis: ( 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 )
A1: InsCode (goto l) = 6 by SCMFSA_2:47;
hence a := b <> goto l by SCMFSA_2:42; :: thesis: ( 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 )
thus AddTo (a,b) <> goto l by A1, SCMFSA_2:43; :: thesis: ( 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 )
thus SubFrom (a,b) <> goto l by A1, SCMFSA_2:44; :: thesis: ( 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 )
thus MultBy (a,b) <> goto l by A1, SCMFSA_2:45; :: thesis: ( Divide (a,b) <> goto l & Divide (b,a) <> goto l & a := (f,b) <> goto l & a :=len f <> goto l )
thus ( Divide (a,b) <> goto l & Divide (b,a) <> goto l ) by A1, SCMFSA_2:46; :: thesis: ( a := (f,b) <> goto l & a :=len f <> goto l )
thus a := (f,b) <> goto l by A1, SCMFSA_2:50; :: thesis: a :=len f <> goto l
thus a :=len f <> goto l by A1, SCMFSA_2:52; :: thesis: verum

end;

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