let aa, bb, cc be Int-Location ; :: thesis: ( aa <> bb implies not cc := bb refersrefer aa )
assume A1: aa <> bb ; :: thesis: not cc := bb refersrefer aa

now

let e be Int-Location ; :: thesis: for l being Element of 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 Element of NAT ; :: thesis: 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 ; :: thesis: ( 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:5; :: thesis: ( 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:42;
hence AddTo e,aa <> cc := bb by SCMFSA_2:43; :: thesis: ( 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:44; :: thesis: ( 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:45; :: thesis: ( 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:46; :: thesis: ( 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 by A2, SCMFSA_2:48; :: thesis: ( 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 by A2, SCMFSA_2:49; :: thesis: ( 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:50; :: thesis: ( 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:51; :: thesis: f :=<0,...,0> aa <> cc := bb
thus f :=<0,...,0> aa <> cc := bb by A2, SCMFSA_2:53; :: thesis: verum

end;

hence not cc := bb refersrefer aa by SCMFSA7B:def 1; :: thesis: verum