let I be preProgram of SCM+FSA; :: thesis: for a being Int-Location st not I destroys a holds

not Directed I destroys a

let a be Int-Location; :: thesis: ( not I destroys a implies not Directed I destroys a )

assume A1: not I destroys a ; :: thesis: not Directed I destroys a

not Directed I destroys a

let a be Int-Location; :: thesis: ( not I destroys a implies not Directed I destroys a )

assume A1: not I destroys a ; :: thesis: not Directed I destroys a

now :: thesis: for i being Instruction of SCM+FSA st i in rng (Directed I) holds

not i destroys a

hence
not Directed I destroys a
by SCMFSA7B:def 4; :: thesis: verumnot i destroys a

let i be Instruction of SCM+FSA; :: thesis: ( i in rng (Directed I) implies not b_{1} destroys a )

A2: dom (Directed I) = dom I by FUNCT_4:99;

assume i in rng (Directed I) ; :: thesis: not b_{1} destroys a

then consider x being object such that

A3: x in dom (Directed I) and

A4: i = (Directed I) . x by FUNCT_1:def 3;

end;A2: dom (Directed I) = dom I by FUNCT_4:99;

assume i in rng (Directed I) ; :: thesis: not b

then consider x being object such that

A3: x in dom (Directed I) and

A4: i = (Directed I) . x by FUNCT_1:def 3;

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

end;

suppose
I . x <> halt SCM+FSA
; :: thesis: not b_{1} 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;then i in rng I by A3, A2, FUNCT_1:def 3;

hence not i destroys a by A1, SCMFSA7B:def 4; :: thesis: verum

suppose
I . x = halt SCM+FSA
; :: thesis: not b_{1} destroys a

then
i = goto (card I)
by A3, A4, A2, FUNCT_4:106;

hence not i destroys a by SCMFSA7B:11; :: thesis: verum

end;hence not i destroys a by SCMFSA7B:11; :: thesis: verum