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