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