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