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;
A4: I ";" J = (CutLastLoc (stop (Directed I))) +* (Reloc (J,((card (stop I)) -' 1))) by SCMFSA6A:37
.= (Directed I) +* (Reloc (J,(card I))) by COMPOS_1:71 ;
not Directed I destroys a by A1, SCMFSA8A:13;
hence not I ";" J destroys a by A3, A4, SCMFSA8A:11; :: thesis: verum