let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
set a = intloc 0;
let s be State of SCM+FSA; for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
set D = Data-Locations ;
let I be keeping_0 Program of SCM+FSA; ( I is_halting_on Initialized s,P implies ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) ) )
set s0 = Initialized s;
set s1 = Initialize (Initialized s);
set P1 = P +* I;
A1:
I c= P +* I
by FUNCT_4:25;
A2:
DataPart (Initialized s) = DataPart (Initialize (Initialized s))
by MEMSTR_0:79;
assume
I is_halting_on Initialized s,P
; ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
then A4:
P +* I halts_on Initialize (Initialized s)
;
thus (IExec (I,P,s)) . (intloc 0) =
(Result ((P +* I),(Initialize (Initialized s)))) . (intloc 0)
by MEMSTR_0:44
.=
(Result ((P +* I),(Initialize (Initialized s)))) . (intloc 0)
.=
(Comput ((P +* I),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . (intloc 0)
by A4, EXTPRO_1:23
.=
1
by A3
; for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
let k be Nat; (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
thus
(Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
by A3; verum