let I, J be Program of SCM+FSA ; :: thesis: for a being Int-Location st not I destroysdestroy a & not J destroysdestroy a holds
not I ';' J destroysdestroy a
let a be Int-Location ; :: thesis: ( not I destroysdestroy a & not J destroysdestroy a implies not I ';' J destroysdestroy a )
assume that
A1: not I destroysdestroy a and
A2: not J destroysdestroy a ; :: thesis: not I ';' J destroysdestroy a
A3: not ProgramPart (Relocated J,(card I)) destroysdestroy a by A2, SCMFSA8A:23;
not Directed I destroysdestroy a by A1, SCMFSA8A:27;
hence not I ';' J destroysdestroy a by A3, SCMFSA8A:25; :: thesis: verum