let I, J be Program 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: ProgramPart (Relocated J,(card I)) does_not_destroy a by A2, SCMFSA8A:23;
Directed I does_not_destroy a by A1, SCMFSA8A:27;
hence I ';' J does_not_destroy a by A3, SCMFSA8A:25; :: thesis: verum