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