reconsider J = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) as good Program of SCM+FSA ;
if>0 a,(loop J),(Stop SCM+FSA ) is good ;
hence Times a,I is good by SCMFSA8C:def 5; :: thesis: verum