let s be State of SCMPDS; :: thesis: for I being Program of SCMPDS
for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for x, l being Element of NAT holds (IExec (I,P,s)) . x = (s +* (Start-At (l,SCMPDS))) . x
let I be Program of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for x, l being Element of NAT holds (IExec (I,P,s)) . x = (s +* (Start-At (l,SCMPDS))) . x
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for x, l being Element of NAT holds (IExec (I,P,s)) . x = (s +* (Start-At (l,SCMPDS))) . x
let x, l be Element of NAT ; :: thesis: (IExec (I,P,s)) . x = (s +* (Start-At (l,SCMPDS))) . x
( dom (Start-At (l,SCMPDS)) = {(IC )} & x <> IC ) by COMPOS_1:3, FUNCOP_1:19;
then A1: not x in dom (Start-At (l,SCMPDS)) by TARSKI:def 1;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then B2: x in dom (s | NAT) ;
thus (IExec (I,P,s)) . x = ((Result ((P +* (stop I)),(Initialize s))) +* (s | NAT)) . x
.= (s | NAT) . x by FUNCT_4:14, B2
.= s . x by FUNCT_1:72
.= (s +* (Start-At (l,SCMPDS))) . x by A1, FUNCT_4:12 ; :: thesis: verum