let aa, bb be Int-Location ; :: thesis: for I being Program of {INT,(INT *)} st not I destroys aa holds
not while>0 (bb,I) destroys aa
let I be Program of {INT,(INT *)}; :: 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:86;
A2: not Stop SCM+FSA destroys aa by SCMFSA8C:85;
assume not I destroys aa ; :: thesis: not while>0 (bb,I) destroys aa
then not I ';' (Goto 0) destroys aa by A1, SCMFSA8C:81;
then A3: not if>0 (bb,(I ';' (Goto 0)),(Stop SCM+FSA)) destroys aa by A2, SCMFSA8C:121;
( 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:35, SCMFSA_9:def 2;
hence not while>0 (bb,I) destroys aa by A3, SCMFSA8A:25; :: thesis: verum