let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I be really-closed Program of SCM+FSA; :: thesis:
let J be Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
A1: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= 1 + (card J) by Lm1 ;
A2: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= (card J) + 1 by Lm1 ;
A3: ((card I) + (card J)) + 1 = ((card J) + 1) + (card I) ;
A4: 0 in dom (Stop SCM+FSA) by COMPOS_1:3;
set J2 = (Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA));
set s2 = Initialize s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
set s1 = Initialize s;
assume A5: I is_halting_on s,P ; :: thesis:
dom (Reloc ((Stop SCM+FSA),((card J) + 1))) = { (m + ((card J) + 1)) where m is Nat : m in dom (Stop SCM+FSA) } by COMPOS_1:33;
then A6: 0 + ((card J) + 1) in dom (Reloc ((Stop SCM+FSA),((card J) + 1))) by A4;
A7: dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ";" J) by SCMFSA6A:17;
A8: 0 in dom (Goto ((card J) + 1)) by Lm1;
A9: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . 0 = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . 0 by SCMFSA6A:25
.= (Directed ((Goto ((card J) + 1)) ";" J)) . 0 by A8, A7, Th7
.= ((Goto ((card J) + 1)) ";" (Directed J)) . 0 by SCMFSA6A:24
.= (Directed (Goto ((card J) + 1))) . 0 by A8, Th7
.= (Goto ((card J) + 1)) . 0 by SCMFSA6A:22
.= goto ((card J) + 1) ;
A10: ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) = (I ";" (Goto ((card J) + 1))) ";" (J ";" (Stop SCM+FSA)) by SCMFSA6A:25
.= I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by SCMFSA6A:25 ;
then A11: DataPart (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A5, Th17;
A12: card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = (card (Goto ((card J) + 1))) + (card (J ";" (Stop SCM+FSA))) by SCMFSA6A:21
.= 1 + (card (J ";" (Stop SCM+FSA))) by Lm1 ;
then A13: 0 + 1 <= card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by NAT_1:11;
A14: card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by SCMFSA6A:21;
then (card I) + 0 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by A13, XREAL_1:6;
then A15: card I in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A16: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) = (card I) + (card (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA))) by A14, SCMFSA6A:25
.= (card I) + (((card J) + 1) + 1) by A2, A16, SCMFSA6A:21
.= (((card I) + (card J)) + 1) + 1 ;
then ((card I) + (card J)) + 1 < card (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by NAT_1:13;
then A17: ((card I) + (card J)) + 1 in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A18: 0 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A13, AFINSQ_1:66;
then 0 + (card I) in { (m + (card I)) where m is Nat : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) } ;
then A19: 0 + (card I) in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by COMPOS_1:33;
A20: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A21: (Stop SCM+FSA) . 0 = halt SCM+FSA ;
card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = 1 + ((card J) + (card (Stop SCM+FSA))) by A12, SCMFSA6A:21
.= (card J) + (1 + (card (Stop SCM+FSA))) ;
then (card J) + 1 < card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A20, XREAL_1:6;
then A22: (card J) + 1 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by AFINSQ_1:66;
A23: ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) . ((card J) + 1) = (((Goto ((card J) + 1)) ";" J) ";" (Stop SCM+FSA)) . ((card J) + 1) by SCMFSA6A:25
.= (Reloc ((Stop SCM+FSA),((card J) + 1))) . (0 + ((card J) + 1)) by A1, A6, SCMFSA6A:40
.= IncAddr ((halt SCM+FSA),((card J) + 1)) by A4, A21, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;
dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) = { (m + (card I)) where m is Nat : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) } by COMPOS_1:33;
then A24: ((card I) + (card J)) + 1 in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by A22, A3;
A25: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) by A5, A10, Th17;
A26: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by PBOOLE:143
.= (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1)))) by A5, A10, Th17
.= (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (card I) by A5, Th13
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (card I) by A10, A15, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (0 + (card I)) by A19, SCMFSA6A:40
.= IncAddr ((goto ((card J) + 1)),(card I)) by A18, A9, COMPOS_1:35
.= goto (((card J) + 1) + (card I)) by SCMFSA_4:1
.= goto (((card I) + (card J)) + 1) ;

A27: now :: thesis:

let f be FinSeq-Location ; :: thesis:
thus (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . f = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 1) + 1))) . f
.= (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) . f by EXTPRO_1:3
.= (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . f by A26, SCMFSA_2:69 ; :: thesis:

end;

thus IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 1) + 1)))
.= IC (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 1 by A26, SCMFSA_2:69 ; :: thesis:
then A28: CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2)))) = (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (((card I) + (card J)) + 1) by PBOOLE:143
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (((card I) + (card J)) + 1) by A10, A17, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (((card J) + 1) + (card I)) by A24, SCMFSA6A:40
.= IncAddr ((halt SCM+FSA),(card I)) by A22, A23, COMPOS_1:35
.= halt SCM+FSA by COMPOS_0:4 ;

now :: thesis:

let a be Int-Location; :: thesis:
thus (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + (1 + 1)))) . a = (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),(((LifeSpan ((P +* I),(Initialize s))) + 1) + 1))) . a
.= (Following ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))))) . a by EXTPRO_1:3
.= (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) . a by A26, SCMFSA_2:69 ; :: thesis:

end;

then DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) by A27, SCMFSA_M:2;
hence DataPart (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s))))) = DataPart (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) by A5, A11, Th13; :: thesis:

hereby :: thesis:

let k be Nat; :: thesis:
assume A30: k < (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis:

per cases ;

suppose A31: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis:

then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA by A5, Th12;
hence CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A5, A10, A31, Th17; :: thesis:

end;

suppose A32: LifeSpan ((P +* I),(Initialize s)) < k ; :: thesis:

k < ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 by A30;
then A33: k <= (LifeSpan ((P +* I),(Initialize s))) + 1 by NAT_1:13;
(LifeSpan ((P +* I),(Initialize s))) + 1 <= k by A32, NAT_1:13;
hence CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) <> halt SCM+FSA by A26, A33, XXREAL_0:1; :: thesis:

end;

end;

end;

hereby :: thesis:

let k be Nat; :: thesis:
assume A34: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
then Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) by A5, Th12;
then IC (Comput ((P +* I),(Initialize s),k)) = IC (Comput ((P +* (Directed I)),(Initialize s),k)) ;
hence IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A5, A10, A34, Th17; :: thesis:

end;

thus IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card I by A5, A25, Th13; :: thesis:
thus A35: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by A28, EXTPRO_1:29; :: thesis:
for k being Nat st CurInstr ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(Initialize s))) + 2 <= k by A29;
hence LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 by A28, A35, EXTPRO_1:def 15; :: thesis: