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 AMISTD_2:70;
then A5: 0 + (card I) in dom (ProgramPart (Relocated (Stop SCM+FSA ),(card I))) by AMISTD_2:69;
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, AMISTD_2:76
.= 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 AMI_1:146; :: 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, AMI_1:def 46; :: thesis: