let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA holds IExec (I,P,s) = IExec (I,P,(Initialized s))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds IExec (I,P,s) = IExec (I,P,(Initialized s))
set A = NAT ;
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: IExec (I,P,s) = IExec (I,P,(Initialized s))
A1: for x being set st x in NAT holds
s . x = (Initialized s) . x by SCMFSA6C:3;
dom (Initialized s) = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
then A2: NAT c= dom (Initialized s) by XBOOLE_1:7;
dom s = ((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT by COMPOS_1:172;
then B3: NAT c= dom s by XBOOLE_1:7;
A4: (Initialized s) +* (Initialize ((intloc 0) .--> 1)) = s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:99;
thus IExec (I,P,s) = IExec (I,P,(Initialized s)) by B3, A4, A2, A1, FUNCT_1:165; :: thesis: verum