let i be 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))
let ii be 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))
let s be 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))
let ss be State of SCM+FSA; ( i = ii & s = ss | SCM-Memory implies Exec (ii,ss) = ss +* (Exec (i,s)) )
assume that
A1:
i = ii
and
A2:
s = ss | SCM-Memory
; Exec (ii,ss) = ss +* (Exec (i,s))
reconsider SS = ss as SCM+FSA-State by CARD_3:107;
reconsider II = ii as Element of SCM+FSA-Instr ;
InsCode II <= 8
by A1, AMI_5:5;
then consider I being Element of SCM-Instr , S being SCM-State such that
A3:
( I = II & S = SS | SCM-Memory )
and
A4:
SCM+FSA-Exec-Res (II,SS) = SS +* (SCM-Exec-Res (I,S))
by SCMFSA_1:def 16;
Exec (i,s) = SCM-Exec-Res (I,S)
by A1, A2, A3, AMI_2:def 15;
hence
Exec (ii,ss) = ss +* (Exec (i,s))
by A4, SCMFSA_1:def 17; verum