:: deftheorem defines while>0 SCMFSA_X:def 4 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds while>0 (a,I) = (if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));