theorem :: SCMPDS_6:112

for P being Instruction-Sequence of SCMPDS
for s being 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,(Initialize s))) = (card I) + 1