theorem Th17: :: SCMFSA8C:25

for a being Int-Location
for I, J being MacroInstruction of SCM+FSA holds
( 1 in dom (if=0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) )