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