let I be Program of SCM+FSA ; :: thesis: for j 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 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
Macro j does_not_destroy a by A2, Th77;
hence I ';' j does_not_destroy a by A1, Th81; :: thesis: verum