let I be Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let P be Instruction-Sequence of SCM+FSA; :: thesis:
assume A1: I is_closed_on Initialized 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 = s +* (Initialize ((intloc 0) .--> 1));
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A5: I is_halting_on Initialized s,P ; :: thesis:
then A6: IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, Th43;
A7: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A8: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
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 A8, A7, COMPOS_1:35
.= halt SCM+FSA by COMPOS_1:11 ;
DataPart (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) by A1, A5, Th43;
hence ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) ) by A1, A5, A6, Th45; :: 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))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) by PARTFUN1:def 6;
A11: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)))) = halt SCM+FSA by A9, A1, A5, A6, Th45, A10;
hence A12: P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29; :: thesis:

let k be Element of NAT ; :: thesis:
assume k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ; :: thesis:
then A13: k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by NAT_1:13;
then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A1, A5, Th44;
hence CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A1, A5, A13, Th43; :: thesis:

end;

then for k being Element of NAT st CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 <= k ;
hence LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 by A11, A12, EXTPRO_1:def 15; :: thesis: