let I be Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
assume A1: I is_closed_on Initialized s ; :: thesis:
card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:61;
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:70;
x: 0 in dom (Stop SCM+FSA) by COMPOS_1:45;
A3: ProgramPart (Relocated ((Stop SCM+FSA),(card I))) c= Relocated ((Stop SCM+FSA),(card I)) by RELAT_1:88;
A4: dom (ProgramPart (Stop SCM+FSA)) = dom (Stop SCM+FSA) by RELAT_1:209;
then 0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA)) } by x;
then 0 + (card I) in dom (Reloc ((ProgramPart (Stop SCM+FSA)),(card I))) by COMPOS_1:117;
then A5: 0 + (card I) in dom (ProgramPart (Relocated ((Stop SCM+FSA),(card I)))) by COMPOS_1:116;
set s2 = s +* (Initialized (I ';' (Stop SCM+FSA)));
set s1 = s +* (Initialized I);
assume A6: I is_halting_on Initialized s ; :: thesis:
then A7: IC (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = IC (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) by A1, Th43;
x: 0 in dom (Stop SCM+FSA) by COMPOS_1:45;
y: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:38;
I ';' (Stop SCM+FSA) c= Initialized (I ';' (Stop SCM+FSA)) by SCMFSA6A:26;
then dom (I ';' (Stop SCM+FSA)) c= dom (Initialized (I ';' (Stop SCM+FSA))) by GRFUNC_1:8;
then A8: (s +* (Initialized (I ';' (Stop SCM+FSA)))) . (card I) = (Initialized (I ';' (Stop SCM+FSA))) . (card I) by A2, FUNCT_4:14
.= (I ';' (Stop SCM+FSA)) . (card I) by A2, SCMFSA6A:50
.= (ProgramPart (Relocated ((Stop SCM+FSA),(card I)))) . (card I) by A5, FUNCT_4:14
.= (Relocated ((Stop SCM+FSA),(card I))) . (0 + (card I)) by A5, A3, GRFUNC_1:8
.= IncAddr ((halt SCM+FSA),(card I)) by A4, y, x, COMPOS_1:122
.= halt SCM+FSA by SCMFSA_4:8 ;
DataPart (Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) by A1, A6, Th43;
hence ( IC (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) ) by A1, A6, A7, Th45; :: thesis:
TX: ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) by AMI_1:123;
Y: (ProgramPart (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))) /. (IC (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))) = (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) . (IC (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))) by COMPOS_1:38;
A9: CurInstr ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))) = (Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) . (card I) by A1, A6, A7, Th45, Y, TX
.= halt SCM+FSA by A8, AMI_1:54 ;
hence A10: ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA)))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA))) by EXTPRO_1:30; :: thesis:

let k be Element of NAT ; :: thesis:
assume k < (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1 ; :: thesis:
then A11: k <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) by NAT_1:13;
then CurInstr ((ProgramPart (s +* (Initialized (Directed I)))),(Comput ((ProgramPart (s +* (Initialized (Directed I)))),(s +* (Initialized (Directed I))),k))) <> halt SCM+FSA by A1, A6, Th44;
hence CurInstr ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),k))) <> halt SCM+FSA by A1, A6, A11, Th43; :: thesis:

end;

then for k being Element of NAT st CurInstr ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(Comput ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),k))) = halt SCM+FSA holds
(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1 <= k ;
hence LifeSpan ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA))))) = (LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1 by A9, A10, EXTPRO_1:def 14; :: thesis: