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