A1: not goto 0 destroys intloc 0 by SCMFSA7B:11;
not I destroys intloc 0 by SCMFSA7B:def 5;
then not if>0 (a,(I ';' (goto 0))) destroys intloc 0 by SCMFSA8C:98;
then not while>0 (a,I) destroys intloc 0 by SCMFSA8A:42, A1;
hence while>0 (a,I) is good by SCMFSA7B:def 5; :: thesis: verum