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