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