let aa, bb, cc be Int-Location; :: thesis: for I, J being really-closed MacroInstruction of SCM+FSA st cc <> aa & not I destroys cc & not J destroys cc holds
not if>0 (aa,bb,I,J) destroys cc
let I, J be really-closed MacroInstruction of SCM+FSA ; :: thesis: ( cc <> aa & not I destroys cc & not J destroys cc implies not if>0 (aa,bb,I,J) destroys cc )
assume that
A1: cc <> aa and
A2: ( not I destroys cc & not J destroys cc ) ; :: thesis: not if>0 (aa,bb,I,J) destroys cc
( if>0 (aa,bb,I,J) = (SubFrom (aa,bb)) ";" (if>0 (aa,I,J)) & not if>0 (aa,I,J) destroys cc ) by A2, SCMFSA8B:def 5, SCMFSA8C:88;
hence not if>0 (aa,bb,I,J) destroys cc by A1, SCMFSA7B:8, SCMFSA8C:53; :: thesis: verum