let I be preProgram of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA
for a being Int-Location st I does_not_destroy a holds
Directed I,l does_not_destroy a
let l be Instruction-Location of SCM+FSA ; :: thesis: for a being Int-Location st I does_not_destroy a holds
Directed I,l does_not_destroy a
let a be Int-Location ; :: thesis: ( I does_not_destroy a implies Directed I,l does_not_destroy a )
assume A1: I does_not_destroy a ; :: thesis: Directed I,l does_not_destroy a

now

let i be Instruction of SCM+FSA ; :: thesis: ( i in rng (Directed I,l) implies b₁ does_not_destroy a )
assume i in rng (Directed I,l) ; :: thesis: b₁ does_not_destroy a
then consider x being set such that
A2: ( x in dom (Directed I,l) & i = (Directed I,l) . x ) by FUNCT_1:def 5;
A3: dom (Directed I,l) = dom I by FUNCT_4:105;

per cases ( I . x <> halt SCM+FSA or I . x = halt SCM+FSA ) ;

suppose I . x <> halt SCM+FSA ; :: thesis: b₁ does_not_destroy a

then i = I . x by A2, FUNCT_4:111;
then i in rng I by A2, A3, FUNCT_1:def 5;
hence i does_not_destroy a by A1, SCMFSA7B:def 4; :: thesis: verum

end;

suppose I . x = halt SCM+FSA ; :: thesis: b₁ does_not_destroy a

then i = goto l by A2, A3, FUNCT_4:112;
hence i does_not_destroy a by SCMFSA7B:17; :: thesis: verum

end;

end;

end;

hence Directed I,l does_not_destroy a by SCMFSA7B:def 4; :: thesis: verum