let a be Int-Location ; :: thesis: for l being Instruction-Location of SCM+FSA holds goto l does_not_destroy a
let l be Instruction-Location of SCM+FSA ; :: thesis: goto l does_not_destroy a

now

let b be Int-Location ; :: thesis: for r being Instruction-Location of SCM+FSA
for f being FinSeq-Location holds
( a := b <> goto l & AddTo a,b <> goto l & SubFrom a,b <> goto l & MultBy a,b <> goto l & Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
let r be Instruction-Location of SCM+FSA ; :: thesis: for f being FinSeq-Location holds
( a := b <> goto l & AddTo a,b <> goto l & SubFrom a,b <> goto l & MultBy a,b <> goto l & Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
let f be FinSeq-Location ; :: thesis: ( a := b <> goto l & AddTo a,b <> goto l & SubFrom a,b <> goto l & MultBy a,b <> goto l & Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
A1: ( 6 <> 1 & 6 <> 2 & 6 <> 3 & 6 <> 4 & 6 <> 5 & 6 <> 9 & 6 <> 11 & InsCode (goto l) = 6 ) by SCMFSA_2:47;
hence a := b <> goto l by SCMFSA_2:42; :: thesis: ( AddTo a,b <> goto l & SubFrom a,b <> goto l & MultBy a,b <> goto l & Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
thus AddTo a,b <> goto l by A1, SCMFSA_2:43; :: thesis: ( SubFrom a,b <> goto l & MultBy a,b <> goto l & Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
thus SubFrom a,b <> goto l by A1, SCMFSA_2:44; :: thesis: ( MultBy a,b <> goto l & Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
thus MultBy a,b <> goto l by A1, SCMFSA_2:45; :: thesis: ( Divide a,b <> goto l & Divide b,a <> goto l & a := f,b <> goto l & a :=len f <> goto l )
thus ( Divide a,b <> goto l & Divide b,a <> goto l ) by A1, SCMFSA_2:46; :: thesis: ( a := f,b <> goto l & a :=len f <> goto l )
thus a := f,b <> goto l by A1, SCMFSA_2:50; :: thesis: a :=len f <> goto l
thus a :=len f <> goto l by A1, SCMFSA_2:52; :: thesis: verum

end;

hence goto l does_not_destroy a by Def3; :: thesis: verum