for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting shiftable Program of
for a being Int_position
for k1 being Integer holds IC (IExec ((if=0 (a,k1,I)),P,s)) = (card I) + 1