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