let R be Ring; for s being State of (SCM R)
for I being Instruction of (SCM R)
for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of R st S = s holds
Exec (I,s) = SCM-Exec-Res (i,S)
let s be State of (SCM R); for I being Instruction of (SCM R)
for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of R st S = s holds
Exec (I,s) = SCM-Exec-Res (i,S)
let I be Instruction of (SCM R); for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of R st S = s holds
Exec (I,s) = SCM-Exec-Res (i,S)
let i be Element of SCM-Instr R; ( i = I implies for S being SCM-State of R st S = s holds
Exec (I,s) = SCM-Exec-Res (i,S) )
assume A1:
i = I
; for S being SCM-State of R st S = s holds
Exec (I,s) = SCM-Exec-Res (i,S)
let S be SCM-State of R; ( S = s implies Exec (I,s) = SCM-Exec-Res (i,S) )
assume
S = s
; Exec (I,s) = SCM-Exec-Res (i,S)
hence Exec (I,s) =
((SCM-Exec R) . i) . S
by A1, Def1
.=
SCM-Exec-Res (i,S)
by SCMRING1:def 15
;
verum