let i, j be 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 a be Int-Location; ( 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
; not i ";" j destroys a
A3:
not Macro j destroys a
by A2, Th39;
not Macro i destroys a
by A1, Th39;
hence
not i ";" j destroys a
by A3, Th43; verum