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

now

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Directed (I,l)) implies not b₁ destroys a )
A2: dom (Directed (I,l)) = dom I by FUNCT_4:99;
assume i in rng (Directed (I,l)) ; :: thesis: not b₁ destroys 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 3;

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

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

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

end;

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

then i = goto l by A3, A4, A2, FUNCT_4:106;
hence not i destroys a by SCMFSA7B:11; :: thesis: verum

end;

end;

end;

hence not Directed (I,l) destroys a by SCMFSA7B:def 4; :: thesis: verum