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 IC (IExec (I,P,s)) = IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds IC (IExec (I,P,s)) = IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))
let I be Program of SCM+FSA; :: thesis: IC (IExec (I,P,s)) = IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))
not IC in NAT by COMPOS_1:def 12;
then A1: not IC in dom (ProgramPart s) by COMPOS_1:34;
IExec (I,P,s) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1;
hence IC (IExec (I,P,s)) = IC (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) by A1, FUNCT_4:12; :: thesis: verum