:: deftheorem defines if=0 SCMFSA8B:def 3 :
for a, b being Int-Location
for I, J being MacroInstruction of SCM+FSA holds if=0 (a,b,I,J) = (SubFrom (a,b)) ";" (if=0 (a,I,J));