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

now :: thesis: 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; :: thesis: 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; :: 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:1; :: 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:18;
hence AddTo (e,aa) <> cc := bb by SCMFSA_2:19; :: 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:20; :: 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:21; :: 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:22; :: 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 ; :: 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 ; :: 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:26; :: 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:27; :: thesis: f :=<0,...,0> aa <> cc := bb
thus f :=<0,...,0> aa <> cc := bb by A2, SCMFSA_2:29; :: thesis: verum

end;

hence not cc := bb refers aa ; :: thesis: verum