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:
( 12
<> 1 & 12
<> 2 & 12
<> 3 & 12
<> 4 & 12
<> 5 & 12
<> 9 & 12
<> 11 &
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> bthus
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