let a, b be Int-Location ; for l being Element of NAT holds not b =0_goto l destroys a
let l be Element of NAT ; not b =0_goto l destroys a
now let e be
Int-Location ;
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 ;
( 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:
InsCode (b =0_goto l) = 7
by SCMFSA_2:48;
hence
a := e <> b =0_goto l
by SCMFSA_2:42;
( 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;
( 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;
( 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;
( 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;
( 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;
a :=len f <> b =0_goto lthus
a :=len f <> b =0_goto l
by A1, SCMFSA_2:52;
verum end;
hence
not b =0_goto l destroys a
by Def3; verum