theorem Th51: :: SCMPDS_2:54

for s being State of SCMPDS
for k1 being Integer holds
( (Exec ((goto k1),s)) . (IC ) = ICplusConst (s,k1) & ( for a being Int_position holds (Exec ((goto k1),s)) . a = s . a ) )