let aa be Int-Location; :: thesis: for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds
not I ';' J destroys aa
let I, J be MacroInstruction of SCM+FSA ; :: thesis: ( not I destroys aa & not J destroys aa implies not I ';' J destroys aa )
assume that
A1: not I destroys aa and
A2: not J destroys aa ; :: thesis: not I ';' J destroys aa
I <= I ;
then CutLastLoc I c= I ;
then A3: not CutLastLoc I destroys aa by A1, SCMFSA8A:45;
not Reloc (J,((card I) -' 1)) destroys aa by A2, SCMFSA8A:9;
hence not I ';' J destroys aa by A3, SCMFSA8A:11; :: thesis: verum