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