let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds
for a being Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a
let s be State of SCM+FSA; for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds
for a being Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a
let I be Program of SCM+FSA; ( I is_halting_on Initialized s,P implies for a being Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a )
set s0 = Initialized s;
set s1 = (Initialized s) +* (Initialize I);
set A = NAT ;
set P1 = P +* I;
A1:
ProgramPart I = I
by RELAT_1:209;
assume
I is_halting_on Initialized s,P
; for a being Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a
then A2:
P +* I halts_on (Initialized s) +* (Initialize I)
by SCMFSA7B:def 8, A1;
hereby verum
let a be
Int-Location ;
(IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . 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) = (Initialized s) +* (Initialize I)
by SCMFSA8A:13;
hence (IExec (I,P,s)) . a =
((Result ((P +* I),((Initialized s) +* (Initialize I)))) +* (s | NAT)) . a
by SCMFSA6B:def 1
.=
(Result ((P +* I),((Initialized s) +* (Initialize I)))) . a
by A3, FUNCT_4:12
.=
(Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a
by A2, EXTPRO_1:23
;
verum
end;