let s be State of SCM+FSA; :: thesis: for I being parahalting Program of SCM+FSA holds IC (IExec (I,s)) = IC (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))
let I be parahalting Program of SCM+FSA; :: thesis: 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 PARTFUN1:def 4, SCMFSA_2:8;
dom (s | NAT) = (dom s) /\ NAT by RELAT_1:90
.= NAT by A1, XBOOLE_1:21 ;
hence IC (IExec (I,s)) = IC (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) by Lm1, FUNCT_4:12; :: thesis: verum