let aa, bb be Int-Location ; :: thesis: for I being Program of SCM+FSA st not I destroysdestroy aa holds
not while>0 bb,I destroysdestroy aa
let I be Program of SCM+FSA ; :: thesis: ( not I destroysdestroy aa implies not while>0 bb,I destroysdestroy aa )
set J = ((card I) + 4) .--> (goto 0 );
set F = if>0 bb,(I ';' (Goto 0 )),(Stop SCM+FSA );
A1: not Goto 0 destroysdestroy aa by SCMFSA8C:86;
A2: not Stop SCM+FSA destroysdestroy aa by SCMFSA8C:85;
assume not I destroysdestroy aa ; :: thesis: not while>0 bb,I destroysdestroy aa
then not I ';' (Goto 0 ) destroysdestroy aa by A1, SCMFSA8C:81;
then A3: not if>0 bb,(I ';' (Goto 0 )),(Stop SCM+FSA ) destroysdestroy aa by A2, SCMFSA8C:121;
( not ((card I) + 4) .--> (goto 0 ) destroysdestroy 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 destroysdestroy aa by A3, SCMFSA8A:25; :: thesis: verum