for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being Program of SCMPDS
for a being Int_position
for i being Integer st s . (DataLoc ((s . a),i)) >= 0 holds
IC (IExec ((while<0 (a,i,I)),P,s)) = (card I) + 2