theorem :: SCMFSA_X:9

for a being Int-Location
for I being MacroInstruction of SCM+FSA holds
( 1 in dom (while=0 (a,I)) & 1 in dom (while>0 (a,I)) ) by Th5, Th7;