let I be Program of SCM+FSA; :: thesis: for j 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 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
not Macro j destroys a by A2, Th39;
hence not I ";" j destroys a by A1, Th43; :: thesis: verum