let a, b be Int-Location ; :: thesis: for f being FinSeq-Location st a <> b holds
b :=len f does_not_destroy a
let f be FinSeq-Location ; :: thesis: ( a <> b implies b :=len f does_not_destroy a )
assume A1:
a <> b
; :: thesis: b :=len f does_not_destroy a
now let c be
Int-Location ;
:: thesis: for g being FinSeq-Location holds
( a := c <> b :=len f & AddTo a,c <> b :=len f & SubFrom a,c <> b :=len f & MultBy a,c <> b :=len f & Divide a,c <> b :=len f & Divide c,a <> b :=len f & a := g,c <> b :=len f & a :=len g <> b :=len f )let g be
FinSeq-Location ;
:: thesis: ( a := c <> b :=len f & AddTo a,c <> b :=len f & SubFrom a,c <> b :=len f & MultBy a,c <> b :=len f & Divide a,c <> b :=len f & Divide c,a <> b :=len f & a := g,c <> b :=len f & a :=len g <> b :=len f )A2:
( 11
<> 1 & 11
<> 2 & 11
<> 3 & 11
<> 4 & 11
<> 5 & 11
<> 9 &
InsCode (b :=len f) = 11 )
by SCMFSA_2:52;
hence
a := c <> b :=len f
by SCMFSA_2:42;
:: thesis: ( AddTo a,c <> b :=len f & SubFrom a,c <> b :=len f & MultBy a,c <> b :=len f & Divide a,c <> b :=len f & Divide c,a <> b :=len f & a := g,c <> b :=len f & a :=len g <> b :=len f )thus
AddTo a,
c <> b :=len f
by A2, SCMFSA_2:43;
:: thesis: ( SubFrom a,c <> b :=len f & MultBy a,c <> b :=len f & Divide a,c <> b :=len f & Divide c,a <> b :=len f & a := g,c <> b :=len f & a :=len g <> b :=len f )thus
SubFrom a,
c <> b :=len f
by A2, SCMFSA_2:44;
:: thesis: ( MultBy a,c <> b :=len f & Divide a,c <> b :=len f & Divide c,a <> b :=len f & a := g,c <> b :=len f & a :=len g <> b :=len f )thus
MultBy a,
c <> b :=len f
by A2, SCMFSA_2:45;
:: thesis: ( Divide a,c <> b :=len f & Divide c,a <> b :=len f & a := g,c <> b :=len f & a :=len g <> b :=len f )thus
(
Divide a,
c <> b :=len f &
Divide c,
a <> b :=len f )
by A2, SCMFSA_2:46;
:: thesis: ( a := g,c <> b :=len f & a :=len g <> b :=len f )thus
a := g,
c <> b :=len f
by A2, SCMFSA_2:50;
:: thesis: a :=len g <> b :=len fthus
a :=len g <> b :=len f
by A1, SF_MASTR:15;
:: thesis: verum end;
hence
b :=len f does_not_destroy a
by Def3; :: thesis: verum