let I be Program of SCM+FSA ; :: thesis: for j 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 j 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 j destroysdestroy a by A2, Th77;
hence not I ';' j destroysdestroy a by A1, Th81; :: thesis: verum