let s be State of SCMPDS ; :: thesis: for I being Program of SCMPDS holds IC (IExec I,s) = IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))
let I be Program of SCMPDS ; :: thesis: IC (IExec I,s) = IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (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, COMPOS_1:3;
hence IC (IExec I,s) = IC (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by FUNCT_4:12; :: thesis: verum