let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good Program of SCM+FSA st I is_halting_on Initialized s,P & I is_closed_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
set a = intloc 0;
let s be State of SCM+FSA; :: thesis: for I being good Program of SCM+FSA st I is_halting_on Initialized s,P & I is_closed_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
set A = NAT ;
let I be good Program of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P & I is_closed_on Initialized s,P implies ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of 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;
defpred S₁[ Nat] means for n being Element of NAT st n <= $1 holds
(Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0);
assume I is_halting_on Initialized s,P ; :: thesis: ( not I is_closed_on Initialized s,P or ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) ) )
then A2: P +* I halts_on Initialize (Initialized s) by SCMFSA7B:def 7;
A3: S₁[ 0 ]

proof

let n be Element of NAT ; :: thesis: ( n <= 0 implies (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) )
A4: for i being Element of NAT st i < 0 holds
IC (Comput ((P +* I),(Initialize (Initialized s)),i)) in dom I ;
assume n <= 0 ; :: thesis: (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0)
hence (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) by A4, Th95; :: thesis: verum

end;

assume A5: I is_closed_on Initialized s,P ; :: thesis: ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
let n be Element of NAT ; :: thesis: ( n <= k + 1 implies (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) )
assume A7: n <= k + 1 ; :: thesis: (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0)
for i being Element of NAT st i < k + 1 holds
IC (Comput ((P +* I),(Initialize (Initialized s)),i)) in dom I by A5, SCMFSA7B:def 6;
hence (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) by A7, Th95; :: thesis: verum

end;

A8: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A6);

A9: now

let k be Element of NAT ; :: thesis: (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
thus (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = (Initialized s) . (intloc 0) by A8
.= 1 by SCMFSA6A:38 ; :: thesis: verum

end;

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 A2, EXTPRO_1:23
.= 1 by A9 ; :: thesis: for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
thus for k being Element of NAT holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 by A9; :: thesis: verum