let I, J be NAT -defined the InstructionsF of SCM+FSA -valued Function; :: thesis: ( I c= J implies for a being Int-Location st not J destroys a holds

not I destroys a )

assume A1: I c= J ; :: thesis: for a being Int-Location st not J destroys a holds

not I destroys a

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

assume A2: not J destroys a ; :: thesis: not I destroys a

let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def 4 :: thesis: ( not i in rng I or not i destroys a )

assume A3: i in rng I ; :: thesis: not i destroys a

rng I c= rng J by A1, RELAT_1:11;

then i in rng J by A3;

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

not I destroys a )

assume A1: I c= J ; :: thesis: for a being Int-Location st not J destroys a holds

not I destroys a

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

assume A2: not J destroys a ; :: thesis: not I destroys a

let i be Instruction of SCM+FSA; :: according to SCMFSA7B:def 4 :: thesis: ( not i in rng I or not i destroys a )

assume A3: i in rng I ; :: thesis: not i destroys a

rng I c= rng J by A1, RELAT_1:11;

then i in rng J by A3;

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