let s be State of ; :: thesis: for I being Program of holds IC (IExec I,s) = IC (Result (s +* (Initialized (stop I))))
let I be Program of ; :: thesis: IC (IExec I,s) = IC (Result (s +* (Initialized (stop I))))
set SI = stop I;
A1: dom s = ({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT by SCMPDS_4:19;
A2: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= NAT by A1, XBOOLE_1:21 ;

now

assume IC SCMPDS in dom (s | NAT ) ; :: thesis: contradiction
then reconsider l = IC SCMPDS as Instruction-Location of SCMPDS by A2, AMI_1:def 4;
l = IC SCMPDS ;
hence contradiction by AMI_1:48; :: thesis: verum

end;

hence IC (IExec I,s) = IC (Result (s +* (Initialized (stop I)))) by FUNCT_4:12; :: thesis: verum