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