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