let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCM+FSA
for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))
let I be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))
let s be State of SCM+FSA; :: thesis: IExec (I,p,s) = IExec (I,p,(Initialized s))
set sp = s | NAT;
A1: s +* (Initialize ((intloc 0) .--> 1)) = (Initialized s) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:99;
thus IExec (I,p,s) = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Result ((p +* I),((Initialized s) +* (Initialize ((intloc 0) .--> 1))))) +* ((Initialized s) | NAT) by A1, SCMFSA8C:36
.= IExec (I,p,(Initialized s)) by SCMFSA6B:def 1 ; :: thesis: verum