theorem Th44: :: SCMFSA_2:51

for i being Instruction of SCM
for ii being Instruction of SCM+FSA
for s being State of SCM
for ss being State of SCM+FSA st i = ii & s = ss | SCM-Memory holds
Exec (ii,ss) = ss +* (Exec (i,s))