let aa, bb be Int-Location ; :: thesis: for I being Program of st not I destroys aa holds
not while>0 (bb,I) destroys aa
let I be Program of ; :: thesis: ( not I destroys aa implies not while>0 (bb,I) destroys aa )
set J = ((card I) + 4) .--> (goto 0);
set F = if>0 (bb,(I ';' (Goto 0)),(Stop SCM+FSA));
A1: not Goto 0 destroys aa by SCMFSA8C:57;
A2: not Stop SCM+FSA destroys aa by SCMFSA8C:56;
assume not I destroys aa ; :: thesis: not while>0 (bb,I) destroys aa
then not I ';' (Goto 0) destroys aa by A1, SCMFSA8C:52;
then A3: not if>0 (bb,(I ';' (Goto 0)),(Stop SCM+FSA)) destroys aa by A2, SCMFSA8C:88;
( not ((card I) + 4) .--> (goto 0) destroys aa & while>0 (bb,I) = (if>0 (bb,(I ';' (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)) ) by SCMFSA_9:30, SCMFSA_9:def 2;
hence not while>0 (bb,I) destroys aa by A3, SCMFSA8A:11; :: thesis: verum