let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds IC (IExec I,s) = IC (Result (s +* (Initialized (stop I))))
let I be Program of SCMPDS ; :: 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 ;
not IC SCMPDS in dom (s | NAT ) by A2, AMI_1:48;
hence IC (IExec I,s) = IC (Result (s +* (Initialized (stop I)))) by FUNCT_4:12; :: thesis: verum