let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N
for P being the Instructions of b₁ -valued ManySortedSet of NAT
for s being State of S
for i being Instruction of S holds (Exec (P . (IC s)),s) . (IC S) = IC (Following P,s)
let S be non empty stored-program IC-Ins-separated definite steady-programmed AMI-Struct of N; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT
for s being State of S
for i being Instruction of S holds (Exec (P . (IC s)),s) . (IC S) = IC (Following P,s)
let P be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: for s being State of S
for i being Instruction of S holds (Exec (P . (IC s)),s) . (IC S) = IC (Following P,s)
let s be State of S; :: thesis: for i being Instruction of S holds (Exec (P . (IC s)),s) . (IC S) = IC (Following P,s)
let i be Instruction of S; :: thesis: (Exec (P . (IC s)),s) . (IC S) = IC (Following P,s)
NAT = dom P by PARTFUN1:def 4;
then A: IC s in dom P ;
thus (Exec (P . (IC s)),s) . (IC S) = IC (Exec (P . (IC s)),s)
.= IC (Exec (CurInstr P,s),s) by A, PARTFUN1:def 8
.= IC (Following P,s) ; :: thesis: verum