take x = halt SCM+FSA ; :: thesis: ( x is parahalting & x is good )
thus x is parahalting ; :: thesis: x is good
not x destroysdestroy intloc 0 by SCMFSA7B:11;
hence x is good by Def6; :: thesis: verum