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 A1: ( i does_not_destroy a & J does_not_destroy a ) ; :: thesis: i ';' J does_not_destroy a
then A2: Macro i does_not_destroy a by Th77;
thus i ';' J does_not_destroy a by A1, A2, Th81; :: thesis: verum