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