let a, b be Int-Location ; :: thesis: for f being FinSeq-Location holds f :=<0,...,0> b does_not_destroy a
let f be FinSeq-Location ; :: thesis: f :=<0,...,0> b does_not_destroy a

now

let e be Int-Location ; :: thesis: for h being FinSeq-Location holds
( a := e <> f :=<0,...,0> b & AddTo a,e <> f :=<0,...,0> b & SubFrom a,e <> f :=<0,...,0> b & MultBy a,e <> f :=<0,...,0> b & Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b & a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
let h be FinSeq-Location ; :: thesis: ( a := e <> f :=<0,...,0> b & AddTo a,e <> f :=<0,...,0> b & SubFrom a,e <> f :=<0,...,0> b & MultBy a,e <> f :=<0,...,0> b & Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b & a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
A1: InsCode (f :=<0,...,0> b) = 12 by SCMFSA_2:53;
hence a := e <> f :=<0,...,0> b by SCMFSA_2:42; :: thesis: ( AddTo a,e <> f :=<0,...,0> b & SubFrom a,e <> f :=<0,...,0> b & MultBy a,e <> f :=<0,...,0> b & Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b & a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus AddTo a,e <> f :=<0,...,0> b by A1, SCMFSA_2:43; :: thesis: ( SubFrom a,e <> f :=<0,...,0> b & MultBy a,e <> f :=<0,...,0> b & Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b & a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus SubFrom a,e <> f :=<0,...,0> b by A1, SCMFSA_2:44; :: thesis: ( MultBy a,e <> f :=<0,...,0> b & Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b & a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus MultBy a,e <> f :=<0,...,0> b by A1, SCMFSA_2:45; :: thesis: ( Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b & a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus ( Divide a,e <> f :=<0,...,0> b & Divide e,a <> f :=<0,...,0> b ) by A1, SCMFSA_2:46; :: thesis: ( a := h,e <> f :=<0,...,0> b & a :=len h <> f :=<0,...,0> b )
thus a := h,e <> f :=<0,...,0> b by A1, SCMFSA_2:50; :: thesis: a :=len h <> f :=<0,...,0> b
thus a :=len h <> f :=<0,...,0> b by A1, SCMFSA_2:52; :: thesis: verum

end;

hence f :=<0,...,0> b does_not_destroy a by Def3; :: thesis: verum