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

now

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

end;

hence b :=len f does_not_destroy a by Def3; :: thesis: verum