theorem Th21: :: SCMPDS_6:30

for P being Instruction-Sequence of SCMPDS
for I, J being Program of
for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )