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) = (Initialized s) +* (Start-At (0,SCM+FSA)) by SCMFSA8C:38
.= ((s +* ((intloc 0) .--> 1)) +* (Start-At (0,SCM+FSA))) +* (Start-At (0,SCM+FSA)) by SCMFSA6A:def 4
.= (s +* ((intloc 0) .--> 1)) +* ((Start-At (0,SCM+FSA)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= Initialized s by SCMFSA6A:def 4 ;
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