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