let a, b, c be Int-Location ; :: thesis: ( a <> b implies not AddTo (c,b) refers a )
assume A1: a <> b ; :: thesis: not AddTo (c,b) refers 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) ; :: 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) ; :: 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 not AddTo (c,b) refers a by SCMFSA7B:def 1; :: thesis: verum