let J be Program of SCM+FSA; :: thesis: for i being Instruction of SCM+FSA
for a being Int-Location st not i destroys a & not J destroys a holds
not i ";" J destroys a
let i be Instruction of SCM+FSA; :: thesis: for a being Int-Location st not i destroys a & not J destroys a holds
not i ";" J destroys a
let a be Int-Location; :: thesis: ( not i destroys a & not J destroys a implies not i ";" J destroys a )
assume that
A1: not i destroys a and
A2: not J destroys a ; :: thesis: not i ";" J destroys a
not Macro i destroys a by A1, Th39;
hence not i ";" J destroys a by A2, Th43; :: thesis: verum