let s be State of SCM+FSA ; for I being Program of SCM+FSA st I is_halting_on Initialize s holds
( ( for a being read-write Int-Location holds (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f ) )
set A = NAT ;
let I be Program of SCM+FSA ; ( I is_halting_on Initialize s implies ( ( for a being read-write Int-Location holds (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f ) ) )
set s0 = Initialize s;
set s1 = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ));
assume
I is_halting_on Initialize s
; ( ( for a being read-write Int-Location holds (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f ) )
then A1:
ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))
by SCMFSA7B:def 8;
hereby for f being FinSeq-Location holds (IExec I,s) . f = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f
let a be
read-write Int-Location ;
(IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a
not
a in NAT
by SCMFSA_2:84;
then
not
a in (dom s) /\ NAT
by XBOOLE_0:def 4;
then A3:
not
a in dom (s | NAT )
by RELAT_1:90;
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))
by SCMFSA8A:13;
hence (IExec I,s) . a =
((Result ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))) +* (s | NAT )) . a
by SCMFSA6B:def 1
.=
(Result ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))) . a
by A3, FUNCT_4:12
.=
(Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a
by A1, AMI_1:122
;
verum
end;
let f be FinSeq-Location ; (IExec I,s) . f = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f
not f in NAT
by SCMFSA_2:85;
then
not f in (dom s) /\ NAT
by XBOOLE_0:def 4;
then A5:
not f in dom (s | NAT )
by RELAT_1:90;
s +* (Initialized I) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))
by SCMFSA8A:13;
hence (IExec I,s) . f =
((Result ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))) +* (s | NAT )) . f
by SCMFSA6B:def 1
.=
(Result ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))) . f
by A5, FUNCT_4:12
.=
(Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f
by A1, AMI_1:122
;
verum