theorem Th25: :: SCMPDS_5:38

for i being Instruction of SCMPDS
for s1, s2 being State of SCMPDS st DataPart s1 = DataPart s2 & InsCode i <> 3 holds
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))