:: deftheorem defines while<0 SCMFSA_X:def 6 :
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) + 1),(goto 0));