theorem Th13: :: SCPINVAR:13

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