let aa, bb, cc be Int-Location; ( aa <> bb implies not cc := bb refers aa )
assume A1:
aa <> bb
; not cc := bb refers aa
now for e being Int-Location
for l being Nat
for f being FinSeq-Location holds
( e := aa <> cc := bb & AddTo (e,aa) <> cc := bb & SubFrom (e,aa) <> cc := bb & MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )let e be
Int-Location;
for l being Nat
for f being FinSeq-Location holds
( e := aa <> cc := bb & AddTo (e,aa) <> cc := bb & SubFrom (e,aa) <> cc := bb & MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )let l be
Nat;
for f being FinSeq-Location holds
( e := aa <> cc := bb & AddTo (e,aa) <> cc := bb & SubFrom (e,aa) <> cc := bb & MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )let f be
FinSeq-Location ;
( e := aa <> cc := bb & AddTo (e,aa) <> cc := bb & SubFrom (e,aa) <> cc := bb & MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
e := aa <> cc := bb
by A1, SF_MASTR:1;
( AddTo (e,aa) <> cc := bb & SubFrom (e,aa) <> cc := bb & MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )A2:
InsCode (cc := bb) = 1
by SCMFSA_2:18;
hence
AddTo (
e,
aa)
<> cc := bb
by SCMFSA_2:19;
( SubFrom (e,aa) <> cc := bb & MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
SubFrom (
e,
aa)
<> cc := bb
by A2, SCMFSA_2:20;
( MultBy (e,aa) <> cc := bb & Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
MultBy (
e,
aa)
<> cc := bb
by A2, SCMFSA_2:21;
( Divide (aa,e) <> cc := bb & Divide (e,aa) <> cc := bb & aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
(
Divide (
aa,
e)
<> cc := bb &
Divide (
e,
aa)
<> cc := bb )
by A2, SCMFSA_2:22;
( aa =0_goto l <> cc := bb & aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
aa =0_goto l <> cc := bb
;
( aa >0_goto l <> cc := bb & e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
aa >0_goto l <> cc := bb
;
( e := (f,aa) <> cc := bb & (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
e := (
f,
aa)
<> cc := bb
by A2, SCMFSA_2:26;
( (f,e) := aa <> cc := bb & (f,aa) := e <> cc := bb & f :=<0,...,0> aa <> cc := bb )thus
( (
f,
e)
:= aa <> cc := bb & (
f,
aa)
:= e <> cc := bb )
by A2, SCMFSA_2:27;
f :=<0,...,0> aa <> cc := bbthus
f :=<0,...,0> aa <> cc := bb
by A2, SCMFSA_2:29;
verum end;
hence
not cc := bb refers aa
; verum