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 COMPOS_1:3, FUNCOP_1:19;
then A2: not x in dom (Start-At l,SCMPDS ) by TARSKI:def 1;
A3: dom (ProgramPart s) = NAT by COMPOS_1:34;
thus (IExec I,s) . x = ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (s | NAT )) . x
.= (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