theorem Th31: :: SCMPDS_6:40

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for J being shiftable Program of
for a being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) = 0 & I is_closed_on s,P & I is_halting_on s,P holds
IExec ((if=0 (a,k1,I,J)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 2),SCMPDS))