let I be really-closed Program of SCM+FSA; :: thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
( 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))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA st I is_halting_on Initialized s,P holds
( 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))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
let P be Instruction-Sequence of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P implies ( 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))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ) )
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 = s +* (Initialize ((intloc 0) .--> 1));
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A4: I is_halting_on Initialized s,P ; :: thesis: ( 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))) & P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
then A5: 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 Th18;
A6: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
A7: (Stop SCM+FSA) . 0 = halt SCM+FSA ;
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 A7, A6, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
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 A4, Th18;
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 A4, A5, Th20; :: thesis: ( P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 )
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))),(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;
A10: 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 A8, A4, A5, Th20, A9;
hence A11: P +* (I ";" (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:29; :: thesis: LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1

now :: thesis: for k being Nat st k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 holds
CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA

let k be Nat; :: thesis: ( k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 implies CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
assume k < (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ; :: thesis: CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA
then A12: 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 A4, Th19;
hence CurInstr ((P +* (I ";" (Stop SCM+FSA))),(Comput ((P +* (I ";" (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A4, A12, Th18; :: thesis: verum

end;

then for k being 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 A10, A11, EXTPRO_1:def 15; :: thesis: verum