set J = (insloc ((card I) + 4)) .--> (goto (insloc 0 ));
set F = if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA );
A1: (insloc ((card I) + 4)) .--> (goto (insloc 0 )) does_not_destroy intloc 0 by Th35;
if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA ) does_not_destroy intloc 0 by SCMFSA7B:def 5;
then while>0 a,I does_not_destroy intloc 0 by A1, SCMFSA8A:25;
hence while>0 a,I is good by SCMFSA7B:def 5; :: thesis: verum