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 :: thesis: for e being Int-Location
for l being 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 e be Int-Location; :: thesis: for l being 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 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:19;
hence e := a <> AddTo (c,b) by SCMFSA_2:18; :: 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:2; :: 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:20; :: 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:21; :: 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:22; :: 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:26; :: 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:27; :: thesis: f :=<0,...,0> a <> AddTo (c,b)
thus f :=<0,...,0> a <> AddTo (c,b) by A2, SCMFSA_2:29; :: thesis: verum

end;

hence not AddTo (c,b) refers a ; :: thesis: verum