:: deftheorem defines Times SCMFSA8C:def 1 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds Times (a,I) = while>0 (a,(I ";" (SubFrom (a,(intloc 0)))));