let I be really-closed Program of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) & P +* (I ";" ()) halts_on Initialize s & LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P )

let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_halting_on s,P holds
( IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) & P +* (I ";" ()) halts_on Initialize s & LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P )

let s be State of SCM+FSA; :: thesis: ( I is_halting_on s,P implies ( IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) & P +* (I ";" ()) halts_on Initialize s & LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P ) )
card () = 1 by COMPOS_1:4;
then card (I ";" ()) = (card I) + 1 by SCMFSA6A:21;
then card I < card (I ";" ()) by NAT_1:13;
then A1: card I in dom (I ";" ()) by AFINSQ_1:66;
A2: 0 in dom () by COMPOS_1:3;
0 + (card I) in { (m + (card I)) where m is Nat : m in dom () } by A2;
then A3: 0 + (card I) in dom (Reloc ((),(card I))) by COMPOS_1:33;
set s2 = Initialize s;
set s1 = Initialize s;
A4: 0 in dom () by COMPOS_1:3;
A5: (Stop SCM+FSA) . 0 = halt SCM+FSA ;
assume A6: I is_halting_on s,P ; :: thesis: ( IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) & P +* (I ";" ()) halts_on Initialize s & LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P )
then A7: IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) by Th17;
A8: (P +* (I ";" ())) . (card I) = (I ";" ()) . (card I) by
.= (Reloc ((),(card I))) . (0 + (card I)) by
.= IncAddr ((),(card I)) by
.= halt SCM+FSA by COMPOS_0:4 ;
DataPart (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) by ;
hence ( IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) = card I & DataPart (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) = DataPart (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1))) ) by A6, A7, Th13; :: thesis: ( P +* (I ";" ()) halts_on Initialize s & LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P )
dom (P +* (I ";" ())) = NAT by PARTFUN1:def 2;
then A9: (P +* (I ";" ())) /. (IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1)))) = (P +* (I ";" ())) . (IC (Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1)))) by PARTFUN1:def 6;
A10: CurInstr ((P +* (I ";" ())),(Comput ((P +* (I ";" ())),(),((LifeSpan ((P +* I),())) + 1)))) = halt SCM+FSA by A8, A6, A7, Th13, A9;
hence A11: P +* (I ";" ()) halts_on Initialize s by EXTPRO_1:29; :: thesis: ( LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 & I ";" () is_halting_on s,P )
now :: thesis: for k being Nat st k < (LifeSpan ((P +* I),())) + 1 holds
CurInstr ((P +* (I ";" ())),(Comput ((P +* (I ";" ())),(),k))) <> halt SCM+FSA
let k be Nat; :: thesis: ( k < (LifeSpan ((P +* I),())) + 1 implies CurInstr ((P +* (I ";" ())),(Comput ((P +* (I ";" ())),(),k))) <> halt SCM+FSA )
assume k < (LifeSpan ((P +* I),())) + 1 ; :: thesis: CurInstr ((P +* (I ";" ())),(Comput ((P +* (I ";" ())),(),k))) <> halt SCM+FSA
then A12: k <= LifeSpan ((P +* I),()) by NAT_1:13;
then CurInstr ((P +* ()),(Comput ((P +* ()),(),k))) <> halt SCM+FSA by ;
hence CurInstr ((P +* (I ";" ())),(Comput ((P +* (I ";" ())),(),k))) <> halt SCM+FSA by ; :: thesis: verum
end;
then for k being Nat st CurInstr ((P +* (I ";" ())),(Comput ((P +* (I ";" ())),(),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),())) + 1 <= k ;
hence LifeSpan ((P +* (I ";" ())),()) = (LifeSpan ((P +* I),())) + 1 by ; :: thesis: I ";" () is_halting_on s,P
thus I ";" () is_halting_on s,P by ; :: thesis: verum