theorem Th19: :: SCMPDS_5:31

for m, n being Nat
for P, P1 being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for s1 being 0 -started State of SCMPDS
for J being parahalting shiftable Program of st stop J c= P & s = Comput ((P1 +* (stop J)),s1,m) holds
Exec ((CurInstr (P,s)),(IncIC (s,n))) = IncIC ((Following (P,s)),n)