let R be Ring; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: 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