:: deftheorem defines while=0 SCMFSA_X:def 3 :
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));