theorem Th52: :: SCMPDS_6:61

for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 holds
IExec ((if<>0 (a,k1,I)),P,(Initialize s)) = s +* (Start-At (((card I) + 2),SCMPDS))