let s be State of SCM+FSA ; :: thesis: for f being FinSeq-Location
for a being read-write Int-Location holds
( (IExec (Stop SCM+FSA ),s) . a = s . a & (IExec (Stop SCM+FSA ),s) . f = s . f )
let f be FinSeq-Location ; :: thesis: for a being read-write Int-Location holds
( (IExec (Stop SCM+FSA ),s) . a = s . a & (IExec (Stop SCM+FSA ),s) . f = s . f )
let a be read-write Int-Location ; :: thesis: ( (IExec (Stop SCM+FSA ),s) . a = s . a & (IExec (Stop SCM+FSA ),s) . f = s . f )
set SA0 = Start-At (insloc 0 );
A1: IExec (Stop SCM+FSA ),s = (Initialize s) +* (Start-At (insloc 0 )) by SCMFSA8C:38
.= ((s +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ))) +* (Start-At (insloc 0 )) by SCMFSA6C:def 3
.= (s +* ((intloc 0 ) .--> 1)) +* ((Start-At (insloc 0 )) +* (Start-At (insloc 0 ))) by FUNCT_4:15
.= Initialize s by SCMFSA6C:def 3 ;
hence (IExec (Stop SCM+FSA ),s) . a = s . a by SCMFSA6C:3; :: thesis: (IExec (Stop SCM+FSA ),s) . f = s . f
thus (IExec (Stop SCM+FSA ),s) . f = s . f by A1, SCMFSA6C:3; :: thesis: verum