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