reconsider J = if=0 a,(Goto (insloc 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