let i be Instruction of SCM; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum