let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m)
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m)
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m) )
set s1 = Initialize s;
set P1 = P +* I;
A1: I c= P +* I by FUNCT_4:25;
set s2 = Initialize s;
set P2 = P +* (loop I);
A2: loop I c= P +* (loop I) by FUNCT_4:25;
assume A3: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m) )
defpred S₁[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),$1) = Comput ((P +* (loop I)),(Initialize s),$1) );
assume I is_halting_on s,P ; :: thesis: for m being Element of NAT st m <= LifeSpan ((P +* I),(Initialize s)) holds
Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m)
then A4: P +* I halts_on Initialize s by SCMFSA7B:def 7;
A5: for m being Element of NAT st S₁[m] holds
S₁[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A6: ( m <= LifeSpan ((P +* I),(Initialize s)) implies Comput ((P +* I),(Initialize s),m) = Comput ((P +* (loop I)),(Initialize s),m) ) ; :: thesis: S₁[m + 1]
A7: Comput ((P +* I),(Initialize s),(m + 1)) = Following ((P +* I),(Comput ((P +* I),(Initialize s),m))) by EXTPRO_1:3;
A8: Comput ((P +* (loop I)),(Initialize s),(m + 1)) = Following ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) by EXTPRO_1:3;
A9: IC (Comput ((P +* I),(Initialize s),m)) in dom I by A3, SCMFSA7B:def 6;
A10: (P +* I) /. (IC (Comput ((P +* I),(Initialize s),m))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),m))) by PBOOLE:143;
A11: CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = I . (IC (Comput ((P +* I),(Initialize s),m))) by A9, A10, A1, GRFUNC_1:2;
assume A12: m + 1 <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: Comput ((P +* I),(Initialize s),(m + 1)) = Comput ((P +* (loop I)),(Initialize s),(m + 1))
then m < LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
then A13: I . (IC (Comput ((P +* I),(Initialize s),m))) <> halt SCM+FSA by A4, A11, EXTPRO_1:def 15;
A14: (P +* (loop I)) /. (IC (Comput ((P +* (loop I)),(Initialize s),m))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),(Initialize s),m))) by PBOOLE:143;
A15: IC (Comput ((P +* I),(Initialize s),m)) in dom (loop I) by A9, FUNCT_4:99;
CurInstr ((P +* I),(Comput ((P +* I),(Initialize s),m))) = (P +* I) . (IC (Comput ((P +* I),(Initialize s),m))) by PBOOLE:143
.= I . (IC (Comput ((P +* I),(Initialize s),m))) by A1, A9, GRFUNC_1:2
.= (loop I) . (IC (Comput ((P +* I),(Initialize s),m))) by A13, FUNCT_4:105
.= (P +* (loop I)) . (IC (Comput ((P +* I),(Initialize s),m))) by A2, A15, GRFUNC_1:2
.= CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(Initialize s),m))) by A6, A12, A14, NAT_1:13 ;
hence Comput ((P +* I),(Initialize s),(m + 1)) = Comput ((P +* (loop I)),(Initialize s),(m + 1)) by A6, A12, A7, A8, NAT_1:13; :: thesis: verum

end;

A16: S₁[ 0 ] ;
thus for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A16, A5); :: thesis: verum