let cc, aa, bb be Int-Location ; :: thesis: for I, J being Program of SCM+FSA st cc <> aa & I does_not_destroy cc & J does_not_destroy cc holds
if>0 aa,bb,I,J does_not_destroy cc
let I, J be Program of SCM+FSA ; :: thesis: ( cc <> aa & I does_not_destroy cc & J does_not_destroy cc implies if>0 aa,bb,I,J does_not_destroy cc )
assume that
A1: cc <> aa and
A2: I does_not_destroy cc and
A3: J does_not_destroy cc ; :: thesis: if>0 aa,bb,I,J does_not_destroy cc
A4: if>0 aa,bb,I,J = (SubFrom aa,bb) ';' (if>0 aa,I,J) by SCMFSA8B:def 5;
if>0 aa,I,J does_not_destroy cc by A2, A3, SCMFSA8C:121;
hence if>0 aa,bb,I,J does_not_destroy cc by A1, A4, SCMFSA7B:14, SCMFSA8C:82; :: thesis: verum