let s be State of SCM+FSA; for I being Program of SCM+FSA holds IC (IExec (I,s)) = IC (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))
let I be Program of SCM+FSA; IC (IExec (I,s)) = IC (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))
A1:
dom s = ((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT
by SCMFSA6A:34;
A2: dom (s | NAT) =
(dom s) /\ NAT
by RELAT_1:90
.=
NAT
by A1, XBOOLE_1:21
;
A3:
not IC SCM+FSA in dom (s | NAT)
by A2, COMPOS_1:3;
IExec (I,s) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)
by SCMFSA6B:def 1;
hence
IC (IExec (I,s)) = IC (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))
by A3, FUNCT_4:12; verum