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

now

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

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

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

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

end;

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

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

end;

end;

end;

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