theorem :: SCMPDS_7:46

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) <= 0 holds
IC (IExec ((for-down (a,i,n,I)),P,(Initialize s))) = (card I) + 3