let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT
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),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT
set A = NAT ;
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),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT )
A1: ProgramPart I = I by RELAT_1:209;
set s1 = s +* (Initialize I);
set P1 = P +* I;
A2: I c= P +* I by FUNCT_4:26;
set s2 = s +* (Initialize (loop I));
set P2 = P +* (loop I);
A3: loop I c= P +* (loop I) by FUNCT_4:26;
assume A4: 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),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT )
defpred S₁[ Nat] means ( $1 <= LifeSpan ((P +* I),(s +* (Initialize I))) implies Comput ((P +* I),(s +* (Initialize I)),$1), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),$1) equal_outside NAT );
assume I is_halting_on s,P ; :: thesis: for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT
then A5: P +* I halts_on s +* (Initialize I) by SCMFSA7B:def 8, A1;
A6: 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 A7: ( m <= LifeSpan ((P +* I),(s +* (Initialize I))) implies Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT ) ; :: thesis: S₁[m + 1]
A8: Comput ((P +* I),(s +* (Initialize I)),(m + 1)) = Following ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m)))),(Comput ((P +* I),(s +* (Initialize I)),m))) ;
A9: Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(m + 1)) = Following ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) by EXTPRO_1:4
.= Exec ((CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m)))),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) ;
A10: IC (Comput ((P +* I),(s +* (Initialize I)),m)) in dom I by A4, SCMFSA7B:def 7, A1;
A11: (P +* I) /. (IC (Comput ((P +* I),(s +* (Initialize I)),m))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by PBOOLE:158;
A12: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A10, A11, GRFUNC_1:8, A2;
assume A13: m + 1 <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: Comput ((P +* I),(s +* (Initialize I)),(m + 1)), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(m + 1)) equal_outside NAT
then m < LifeSpan ((P +* I),(s +* (Initialize I))) by NAT_1:13;
then I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) <> halt SCM+FSA by A5, A12, EXTPRO_1:def 14;
then A14: I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) = (loop I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by FUNCT_4:111;
A15: (P +* (loop I)) /. (IC (Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) = (P +* (loop I)) . (IC (Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) by PBOOLE:158;
A16: IC (Comput ((P +* I),(s +* (Initialize I)),m)) in dom (loop I) by A10, FUNCT_4:105;
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by PBOOLE:158
.= I . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by GRFUNC_1:8, A2, A10
.= (loop I) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by A14
.= (P +* (loop I)) . (IC (Comput ((P +* I),(s +* (Initialize I)),m))) by GRFUNC_1:8, A3, A16
.= CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) by A7, A13, A15, COMPOS_1:24, NAT_1:13 ;
hence Comput ((P +* I),(s +* (Initialize I)),(m + 1)), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(m + 1)) equal_outside NAT by A7, A13, A8, A9, NAT_1:13, AMISTD_2:def 20; :: thesis: verum

end;

A17: S₁[ 0 ]

proof

assume 0 <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: Comput ((P +* I),(s +* (Initialize I)),0), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),0) equal_outside NAT
A18: s,s +* (loop I) equal_outside NAT by FUNCT_7:132;
s +* I,s equal_outside NAT by FUNCT_7:28, FUNCT_7:132;
then s +* I,s +* (loop I) equal_outside NAT by A18, FUNCT_7:29;
then Initialize (s +* I), Initialize (s +* (loop I)) equal_outside NAT by FUNCT_7:106;
then Initialize (s +* I),s +* (Initialize (loop I)) equal_outside NAT by FUNCT_4:15;
then s +* (Initialize I),s +* (Initialize (loop I)) equal_outside NAT by FUNCT_4:15;
then s +* (Initialize I), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),0) equal_outside NAT by EXTPRO_1:3;
hence Comput ((P +* I),(s +* (Initialize I)),0), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),0) equal_outside NAT by EXTPRO_1:3; :: thesis: verum

end;

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