let p be Instruction-Sequence of SCM+FSA; :: 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;
thus IExec (I,p,s) = Result ((p +* I),(Initialized (Initialized s))) by SCMFSA6B:def 1
.= IExec (I,p,(Initialized s)) by SCMFSA6B:def 1 ; :: thesis: verum