let a, b be Int-Location ; :: thesis: ( a <> b implies not b :==1 destroys a )
assume A1: a <> b ; :: thesis: not b :==1 destroys a

now

let c be Int-Location ; :: thesis: for g being FinSeq-Location holds
( a := c <> b :==1 & AddTo (a,c) <> b :==1 & SubFrom (a,c) <> b :==1 & MultBy (a,c) <> b :==1 & Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 & a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
let g be FinSeq-Location ; :: thesis: ( a := c <> b :==1 & AddTo (a,c) <> b :==1 & SubFrom (a,c) <> b :==1 & MultBy (a,c) <> b :==1 & Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 & a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
A2: InsCode (b :==1) = 13 by SCMFSA_2:137;
hence a := c <> b :==1 by SCMFSA_2:42; :: thesis: ( AddTo (a,c) <> b :==1 & SubFrom (a,c) <> b :==1 & MultBy (a,c) <> b :==1 & Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 & a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
thus AddTo (a,c) <> b :==1 by A2, SCMFSA_2:43; :: thesis: ( SubFrom (a,c) <> b :==1 & MultBy (a,c) <> b :==1 & Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 & a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
thus SubFrom (a,c) <> b :==1 by A2, SCMFSA_2:44; :: thesis: ( MultBy (a,c) <> b :==1 & Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 & a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
thus MultBy (a,c) <> b :==1 by A2, SCMFSA_2:45; :: thesis: ( Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 & a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
thus ( Divide (a,c) <> b :==1 & Divide (c,a) <> b :==1 ) by A2, SCMFSA_2:46; :: thesis: ( a := (g,c) <> b :==1 & a :=len g <> b :==1 & a :==1 <> b :==1 )
thus a := (g,c) <> b :==1 by A2, SCMFSA_2:50; :: thesis: ( a :=len g <> b :==1 & a :==1 <> b :==1 )
thus a :=len g <> b :==1 by A2, SCMFSA_2:52; :: thesis: a :==1 <> b :==1
thus a :==1 <> b :==1 by A1, SF_MASTR:74; :: thesis: verum

end;

hence not b :==1 destroys a by Def3; :: thesis: verum