let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds IC (IExec I,s) = IC (Result (s +* (Initialized I)))
let I be Program of SCM+FSA ; :: thesis: IC (IExec I,s) = IC (Result (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, AMI_1:48;
IExec I,s = (Result (s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1;
hence IC (IExec I,s) = IC (Result (s +* (Initialized I))) by A3, FUNCT_4:12; :: thesis: verum