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 = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set F = if>0 bb,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA );
A1: Goto (insloc 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 (insloc 0 )) does_not_destroy aa by A1, SCMFSA8C:81;
then A3: if>0 bb,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) does_not_destroy aa by A2, SCMFSA8C:121;
( (insloc ((card I) + 4)) .--> (goto (insloc 0 )) does_not_destroy aa & while>0 bb,I = (if>0 bb,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0 ))) ) by SCMFSA_9:35, SCMFSA_9:def 2;
hence while>0 bb,I does_not_destroy aa by A3, SCMFSA8A:25; :: thesis: verum