let I be really-closed Program of SCM+FSA; :: thesis:
let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: 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 A1: card I in dom (I ";" (Stop SCM+FSA)) by AFINSQ_1:66;
A2: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
0 + (card I) in { (m + (card I)) where m is Nat : m in dom (Stop SCM+FSA) } by A2;
then A3: 0 + (card I) in dom (Reloc ((Stop SCM+FSA),(card I))) by COMPOS_1:33;
set s2 = Initialize s;
set s1 = Initialize s;
A4: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A5: (Stop SCM+FSA) . 0 = halt SCM+FSA ;
assume A6: I is_halting_on s,P ; :: thesis:
then A7: 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 Th17;
A8: (P +* (I ";" (Stop SCM+FSA))) . (card I) = (I ";" (Stop SCM+FSA)) . (card I) by A1, FUNCT_4:13
.= (Reloc ((Stop SCM+FSA),(card I))) . (0 + (card I)) by A3, SCMFSA6A:40
.= IncAddr ((halt SCM+FSA),(card I)) by A5, A4, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
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 A6, Th17;
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 A6, A7, Th13; :: thesis:
dom (P +* (I ";" (Stop SCM+FSA))) = NAT by PARTFUN1:def 2;
then A9: (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;
A10: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = halt SCM+FSA by A8, A6, A7, Th13, A9;
hence A11: P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s by EXTPRO_1:29; :: thesis:

let k be Nat; :: thesis:
assume k < (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis:
then A12: 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 A6, Th12;
hence CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A6, A12, Th17; :: thesis:

end;

then for k being 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 A10, A11, EXTPRO_1:def 15; :: thesis:
thus I ";" (Stop SCM+FSA) is_halting_on s,P by A11, SCMFSA7B:def 7; :: thesis: