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

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