let i, j 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
A3: not Macro j destroys a by A2, Th77;
not Macro i destroys a by A1, Th77;
hence not i ';' j destroys a by A3, Th81; :: thesis: verum