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 0 ,SCM+FSA ;
A1: IExec (Stop SCM+FSA ),s = (Initialize s) +* (Start-At 0 ,SCM+FSA ) by SCMFSA8C:38
.= ((s +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) by SCMFSA6C:def 3
.= (s +* ((intloc 0 ) .--> 1)) +* ((Start-At 0 ,SCM+FSA ) +* (Start-At 0 ,SCM+FSA )) 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