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