let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS
for x, l being Element of NAT holds (IExec I,s) . x = (s +* (Start-At l,SCMPDS )) . x
let I be Program of SCMPDS ; :: thesis: for x, l being Element of NAT holds (IExec I,s) . x = (s +* (Start-At l,SCMPDS )) . x
let x, l be Element of NAT ; :: thesis: (IExec I,s) . x = (s +* (Start-At l,SCMPDS )) . x
( dom (Start-At l,SCMPDS ) = {(IC SCMPDS )} & x <> IC SCMPDS ) by AMI_1:48, FUNCOP_1:19;
then A2: not x in dom (Start-At l,SCMPDS ) by TARSKI:def 1;
A3: dom (ProgramPart s) = NAT by AMI_1:143;
thus (IExec I,s) . x = ((Result (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I)))) +* (s | NAT )) . x by SCMPDS_4:def 8
.= (s | NAT ) . x by A3, FUNCT_4:14
.= s . x by FUNCT_1:72
.= (s +* (Start-At l,SCMPDS )) . x by A2, FUNCT_4:12 ; :: thesis: verum