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, Th77;
hence not i ';' J destroys a by A2, Th81; :: thesis: verum