let a, b, c be Int-Location ; :: thesis: ( a <> b implies AddTo c,b does_not_refer a )
assume A1:
a <> b
; :: thesis: AddTo c,b does_not_refer a
now let e be
Int-Location ;
:: thesis: for l being Instruction-Location of SCM+FSA
for f being FinSeq-Location holds
( e := a <> AddTo c,b & AddTo e,a <> AddTo c,b & SubFrom e,a <> AddTo c,b & MultBy e,a <> AddTo c,b & Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )let l be
Instruction-Location of
SCM+FSA ;
:: thesis: for f being FinSeq-Location holds
( e := a <> AddTo c,b & AddTo e,a <> AddTo c,b & SubFrom e,a <> AddTo c,b & MultBy e,a <> AddTo c,b & Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )let f be
FinSeq-Location ;
:: thesis: ( e := a <> AddTo c,b & AddTo e,a <> AddTo c,b & SubFrom e,a <> AddTo c,b & MultBy e,a <> AddTo c,b & Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )A2:
( 2
<> 1 & 2
<> 3 & 2
<> 4 & 2
<> 5 & 2
<> 7 & 2
<> 8 & 2
<> 9 & 2
<> 10 & 2
<> 12 &
InsCode (AddTo c,b) = 2 )
by SCMFSA_2:43;
hence
e := a <> AddTo c,
b
by SCMFSA_2:42;
:: thesis: ( AddTo e,a <> AddTo c,b & SubFrom e,a <> AddTo c,b & MultBy e,a <> AddTo c,b & Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
AddTo e,
a <> AddTo c,
b
by A1, SF_MASTR:6;
:: thesis: ( SubFrom e,a <> AddTo c,b & MultBy e,a <> AddTo c,b & Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
SubFrom e,
a <> AddTo c,
b
by A2, SCMFSA_2:44;
:: thesis: ( MultBy e,a <> AddTo c,b & Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
MultBy e,
a <> AddTo c,
b
by A2, SCMFSA_2:45;
:: thesis: ( Divide a,e <> AddTo c,b & Divide e,a <> AddTo c,b & a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
(
Divide a,
e <> AddTo c,
b &
Divide e,
a <> AddTo c,
b )
by A2, SCMFSA_2:46;
:: thesis: ( a =0_goto l <> AddTo c,b & a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
a =0_goto l <> AddTo c,
b
by A2, SCMFSA_2:48;
:: thesis: ( a >0_goto l <> AddTo c,b & e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
a >0_goto l <> AddTo c,
b
by A2, SCMFSA_2:49;
:: thesis: ( e := f,a <> AddTo c,b & f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
e := f,
a <> AddTo c,
b
by A2, SCMFSA_2:50;
:: thesis: ( f,e := a <> AddTo c,b & f,a := e <> AddTo c,b & f :=<0,...,0> a <> AddTo c,b )thus
(
f,
e := a <> AddTo c,
b &
f,
a := e <> AddTo c,
b )
by A2, SCMFSA_2:51;
:: thesis: f :=<0,...,0> a <> AddTo c,bthus
f :=<0,...,0> a <> AddTo c,
b
by A2, SCMFSA_2:53;
:: thesis: verum end;
hence
AddTo c,b does_not_refer a
by SCMFSA7B:def 1; :: thesis: verum