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