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