let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being good really-closed 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; :: thesis: for I being good really-closed 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 ) )
let I be good really-closed Program of SCM+FSA; :: thesis: ( 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;
defpred S1[ Nat] means for n being 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: ( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 ) )
then A1: P +* I halts_on Initialize (Initialized s) ;
A2: S1[ 0 ]
proof
let n be Nat; :: thesis: ( n <= 0 implies (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) )
A3: for i being 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 A3, Th57; :: thesis: verum
end;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
let n be Nat; :: thesis: ( n <= k + 1 implies (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) )
assume A5: n <= k + 1 ; :: thesis: (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0)
A6: I c= P +* I by FUNCT_4:25;
IC (Initialize (Initialized s)) = 0 by MEMSTR_0:def 11;
then IC (Initialize (Initialized s)) in dom I by AFINSQ_1:65;
then for i being Nat st i < k + 1 holds
IC (Comput ((P +* I),(Initialize (Initialized s)),i)) in dom I by AMISTD_1:21, A6;
hence (Comput ((P +* I),(Initialize (Initialized s)),n)) . (intloc 0) = (Initialized s) . (intloc 0) by A5, Th57; :: thesis: verum
end;
A7: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A4);
A8: now :: thesis: for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
let k be 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 A7
.= 1 by SCMFSA_M:9 ; :: 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 A1, EXTPRO_1:23
.= 1 by A8 ; :: thesis: for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1
thus for k being Nat holds (Comput ((P +* I),(Initialize (Initialized s)),k)) . (intloc 0) = 1 by A8; :: thesis: verum