let a, b be Int-Location ; :: thesis: for l being Element of NAT holds b >0_goto l does_not_destroy a
let l be Element of NAT ; :: thesis: b >0_goto l does_not_destroy 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 )
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 )
A1: InsCode (b >0_goto l) = 8 by SCMFSA_2:49;
hence a := e <> b >0_goto l by SCMFSA_2:42; :: 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 )
thus AddTo a,e <> b >0_goto l by A1, SCMFSA_2:43; :: 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 )
thus SubFrom a,e <> b >0_goto l by A1, SCMFSA_2:44; :: 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 )
thus MultBy a,e <> b >0_goto l by A1, SCMFSA_2:45; :: 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 )
thus ( Divide a,e <> b >0_goto l & Divide e,a <> b >0_goto l ) by A1, SCMFSA_2:46; :: thesis: ( a := f,e <> b >0_goto l & a :=len f <> b >0_goto l )
thus a := f,e <> b >0_goto l by A1, SCMFSA_2:50; :: thesis: a :=len f <> b >0_goto l
thus a :=len f <> b >0_goto l by A1, SCMFSA_2:52; :: thesis: verum

end;

hence b >0_goto l does_not_destroy a by Def3; :: thesis: verum