let R be good Ring; :: thesis: for s being State of
for I being Instruction of
for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of st S = s holds
Exec I,s = SCM-Exec-Res i,S
let s be State of ; :: thesis: for I being Instruction of
for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of st S = s holds
Exec I,s = SCM-Exec-Res i,S
let I be Instruction of ; :: thesis: for i being Element of SCM-Instr R st i = I holds
for S being SCM-State of st S = s holds
Exec I,s = SCM-Exec-Res i,S
let i be Element of SCM-Instr R; :: thesis: ( i = I implies for S being SCM-State of st S = s holds
Exec I,s = SCM-Exec-Res i,S )
assume A1: i = I ; :: thesis: for S being SCM-State of st S = s holds
Exec I,s = SCM-Exec-Res i,S
let S be SCM-State of ; :: thesis: ( S = s implies Exec I,s = SCM-Exec-Res i,S )
assume S = s ; :: thesis: 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 ;
:: thesis: verum