let I be Program of SCM+FSA ; :: thesis: for s being State of SCM+FSA holds IExec I,s = IExec I,(Initialized s)
let s be State of SCM+FSA ; :: thesis: IExec I,s = IExec I,(Initialized s)
set sp = s | NAT ;
X: s +* (Initialized I) = (Initialized s) +* (Initialized I) by SCMFSA8A:8;
thus IExec I,s = (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Result (ProgramPart ((Initialized s) +* (Initialized I))),((Initialized s) +* (Initialized I))) +* (s | NAT ) by X
.= (Result (ProgramPart ((Initialized s) +* (Initialized I))),((Initialized s) +* (Initialized I))) +* ((Initialized s) | NAT ) by SCMFSA8C:36
.= IExec I,(Initialized s) by SCMFSA6B:def 1 ; :: thesis: verum