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 Element of NAT
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 Element of NAT ; :: 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: 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,b
thus 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