let s be State of SCMPDS; :: thesis: for P being the Instructions of SCMPDS -valued ManySortedSet of NAT
for I being Program of SCMPDS holds IC (IExec (I,P,s)) = IC (Result ((P +* (stop I)),(Initialize s)))
let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCMPDS holds IC (IExec (I,P,s)) = IC (Result ((P +* (stop I)),(Initialize s)))
let I be Program of SCMPDS; :: thesis: IC (IExec (I,P,s)) = IC (Result ((P +* (stop I)),(Initialize s)))
set SI = stop I;
A1: dom s = ({(IC )} \/ 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 in dom (s | NAT) by A2, COMPOS_1:3;
hence IC (IExec (I,P,s)) = IC (Result ((P +* (stop I)),(Initialize s))) by FUNCT_4:12; :: thesis: verum