let I be Program of SCM+FSA; :: thesis:
let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
assume A1: I is_closed_on s,P ; :: thesis:
card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:21;
then card I < card (I ';' (Stop SCM+FSA)) by NAT_1:13;
then A2: card I in dom (I ';' (Stop SCM+FSA)) by AFINSQ_1:66;
A3: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom (Stop SCM+FSA) } by A3;
then A4: 0 + (card I) in dom (Reloc ((Stop SCM+FSA),(card I))) by COMPOS_1:33;
set s2 = Initialize s;
set s1 = Initialize s;
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A6: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
assume A7: I is_halting_on s,P ; :: thesis:
then A8: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, Th42;
A9: (P +* (I ';' (Stop SCM+FSA))) . (card I) = (I ';' (Stop SCM+FSA)) . (card I) by A2, FUNCT_4:13
.= (Reloc ((Stop SCM+FSA),(card I))) . (0 + (card I)) by A4, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A6, A5, COMPOS_1:35
.= halt SCM+FSA by COMPOS_1:11 ;
DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A1, A7, Th42;
hence ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I & DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) ) by A1, A7, A8, Th36; :: thesis:
dom (P +* (I ';' (Stop SCM+FSA))) = NAT by PARTFUN1:def 2;
then A10: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by PARTFUN1:def 6;
A11: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = halt SCM+FSA by A9, A1, A7, A8, Th36, A10;
hence A12: P +* (I ';' (Stop SCM+FSA)) halts_on Initialize s by EXTPRO_1:29; :: thesis:

A13: now

let k be Element of NAT ; :: thesis:
assume A14: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
then Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) by A1, A7, Th35;
then IC (Comput ((P +* I),(Initialize s),k)) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) ;
then A15: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A1, A7, A14, Th42;
A17: IC (Comput ((P +* I),(Initialize s),k)) in dom I by A1, SCMFSA7B:def 6;
dom I c= dom (I ';' (Stop SCM+FSA)) by SCMFSA6A:17;
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k)) in dom (I ';' (Stop SCM+FSA)) by A15, A17; :: thesis:

end;

defpred S₁[ Nat] means ( ( LifeSpan ((P +* I),(Initialize s)) < $1 implies IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),$1)) = card I ) & IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),$1)) in dom (I ';' (Stop SCM+FSA)) );
card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:21;
then A18: (card I) + 0 < card (I ';' (Stop SCM+FSA)) by XREAL_1:6;
then A19: card I in dom (I ';' (Stop SCM+FSA)) by AFINSQ_1:66;

A20: now

let k be Element of NAT ; :: thesis:
assume A21: S₁[k] ; :: thesis:

per cases by XXREAL_0:1;

suppose k < LifeSpan ((P +* I),(Initialize s)) ; :: thesis:

then k + 1 <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
hence S₁[k + 1] by A13; :: thesis:

end;

suppose k = LifeSpan ((P +* I),(Initialize s)) ; :: thesis:

hence S₁[k + 1] by A1, A7, A8, A19, Th36; :: thesis:

end;

suppose A22: k > LifeSpan ((P +* I),(Initialize s)) ; :: thesis:

A23: now

assume k + 1 > LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
B24: dom (P +* (I ';' (Stop SCM+FSA))) = NAT by PARTFUN1:def 2;
A25: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA by A9, A21, A22, B24, PARTFUN1:def 6;
thus IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),(k + 1))) = IC (Following ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k)))) by EXTPRO_1:3
.= card I by A21, A22, A25, EXTPRO_1:def 3 ; :: thesis:

end;

k + 1 > k + 0 by XREAL_1:6;
hence S₁[k + 1] by A18, A22, A23, AFINSQ_1:66, XXREAL_0:2; :: thesis:

end;

end;

end;

let k be Element of NAT ; :: thesis:
assume k < (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis:
then A26: k <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;
then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA by A1, A7, Th35;
hence CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A1, A7, A26, Th42; :: thesis:

end;

then for k being Element of NAT st CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(Initialize s))) + 1 <= k ;
hence LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by A11, A12, EXTPRO_1:def 15; :: thesis:
A27: S₁[ 0 ] by A13, NAT_1:2;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A27, A20);
hence I ';' (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def 6; :: thesis:
thus I ';' (Stop SCM+FSA) is_halting_on s,P by A12, SCMFSA7B:def 7; :: thesis: