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