let a, b, c be Int-Location ; :: thesis: for f being FinSeq-Location st a <> b holds
not b := f,c destroysdestroy a
let f be FinSeq-Location ; :: thesis: ( a <> b implies not b := f,c destroysdestroy a )
assume A1: a <> b ; :: thesis: not b := f,c destroysdestroy a

now

let e be Int-Location ; :: thesis: for l being Element of NAT
for h being FinSeq-Location holds
( a := e <> b := f,c & AddTo a,e <> b := f,c & SubFrom a,e <> b := f,c & MultBy a,e <> b := f,c & Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
let l be Element of NAT ; :: thesis: for h being FinSeq-Location holds
( a := e <> b := f,c & AddTo a,e <> b := f,c & SubFrom a,e <> b := f,c & MultBy a,e <> b := f,c & Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
let h be FinSeq-Location ; :: thesis: ( a := e <> b := f,c & AddTo a,e <> b := f,c & SubFrom a,e <> b := f,c & MultBy a,e <> b := f,c & Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
A2: InsCode (b := f,c) = 9 by SCMFSA_2:50;
hence a := e <> b := f,c by SCMFSA_2:42; :: thesis: ( AddTo a,e <> b := f,c & SubFrom a,e <> b := f,c & MultBy a,e <> b := f,c & Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
thus AddTo a,e <> b := f,c by A2, SCMFSA_2:43; :: thesis: ( SubFrom a,e <> b := f,c & MultBy a,e <> b := f,c & Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
thus SubFrom a,e <> b := f,c by A2, SCMFSA_2:44; :: thesis: ( MultBy a,e <> b := f,c & Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
thus MultBy a,e <> b := f,c by A2, SCMFSA_2:45; :: thesis: ( Divide a,e <> b := f,c & Divide e,a <> b := f,c & a := h,e <> b := f,c & a :=len h <> b := f,c )
thus ( Divide a,e <> b := f,c & Divide e,a <> b := f,c ) by A2, SCMFSA_2:46; :: thesis: ( a := h,e <> b := f,c & a :=len h <> b := f,c )
thus a := h,e <> b := f,c by A1, SF_MASTR:13; :: thesis: a :=len h <> b := f,c
thus a :=len h <> b := f,c by A2, SCMFSA_2:52; :: thesis: verum

end;

hence not b := f,c destroysdestroy a by Def3; :: thesis: verum