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 Reloc (J,(card I)) destroys a by A2, SCMFSA8A:9;
not Directed I destroys a by A1, SCMFSA8A:13;
hence not I ';' J destroys a by A3, SCMFSA8A:11; :: thesis: verum