let s be State of SCM+FSA ; :: thesis: for I being parahalting Program of SCM+FSA holds IC (IExec I,s) = IC (Result (s +* (Initialized I)))
let I be parahalting 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 AMI_1:79, 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 (s +* (Initialized I))) by Lm1, FUNCT_4:12; :: thesis: verum