let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of S
for i being Instruction of S holds (Exec (s . (IC s)),s) . (IC S) = IC (Following (ProgramPart s),s)
let S be non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N; :: thesis: for s being State of S
for i being Instruction of S holds (Exec (s . (IC s)),s) . (IC S) = IC (Following (ProgramPart s),s)
let s be State of S; :: thesis: for i being Instruction of S holds (Exec (s . (IC s)),s) . (IC S) = IC (Following (ProgramPart s),s)
let i be Instruction of S; :: thesis: (Exec (s . (IC s)),s) . (IC S) = IC (Following (ProgramPart s),s)
(ProgramPart s) /. (IC s) = s . (IC s) by BWL1;
hence (Exec (s . (IC s)),s) . (IC S) = IC (Following (ProgramPart s),s) ; :: thesis: verum