theorem Th10: :: SCPINVAR:10

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds
( 0 in dom (while<>0 (a,i,I)) & 1 in dom (while<>0 (a,i,I)) )