let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I, J be Program of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
assume A1: I is_closed_on s,P ; :: thesis:
A2: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= 1 + (card J) by Lm1 ;
A3: card ((Goto ((card J) + 1)) ";" J) = (card (Goto ((card J) + 1))) + (card J) by SCMFSA6A:21
.= (card J) + 1 by Lm1 ;
A4: ((card I) + (card J)) + 1 = ((card J) + 1) + (card I) ;
A5: 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 A6: I is_halting_on s,P ; :: thesis:
dom (Reloc ((Stop SCM+FSA),((card J) + 1))) = { (m + ((card J) + 1)) where m is Element of NAT : m in dom (Stop SCM+FSA) } by COMPOS_1:33;
then A7: 0 + ((card J) + 1) in dom (Reloc ((Stop SCM+FSA),((card J) + 1))) by A5;
A8: dom (Goto ((card J) + 1)) c= dom ((Goto ((card J) + 1)) ";" J) by SCMFSA6A:17;
A9: 0 in dom (Goto ((card J) + 1)) by Lm1;
A10: ((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 A9, A8, Th14
.= ((Goto ((card J) + 1)) ";" (Directed J)) . 0 by SCMFSA6A:24
.= (Directed (Goto ((card J) + 1))) . 0 by A9, Th14
.= (Goto ((card J) + 1)) . 0 by SCMFSA6A:22
.= goto ((card J) + 1) by Lm1 ;
A11: ((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 A12: 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 A1, A6, Th26;
A13: 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 A14: 0 + 1 <= card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by NAT_1:11;
A15: 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 A14, XREAL_1:6;
then A16: card I in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A17: 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 A15, SCMFSA6A:25
.= (card I) + (((card J) + 1) + 1) by A3, A17, 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 A18: ((card I) + (card J)) + 1 in dom (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) by AFINSQ_1:66;
A19: 0 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A14, AFINSQ_1:66;
then 0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) } ;
then A20: 0 + (card I) in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by COMPOS_1:33;
A21: card (Stop SCM+FSA) = 1 by COMPOS_1:4;
A22: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:34;
card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) = 1 + ((card J) + (card (Stop SCM+FSA))) by A13, SCMFSA6A:21
.= (card J) + (1 + (card (Stop SCM+FSA))) ;
then (card J) + 1 < card ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by A21, XREAL_1:6;
then A23: (card J) + 1 in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) by AFINSQ_1:66;
A24: ((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 A2, A7, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),((card J) + 1)) by A5, A22, 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 Element of NAT : m in dom ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))) } by COMPOS_1:33;
then A25: ((card I) + (card J)) + 1 in dom (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) by A23, A4;
A26: 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 A1, A6, A11, Th26;
A27: 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 A1, A6, A11, Th26
.= (P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))) . (card I) by A1, A6, Th22
.= (I ";" ((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA)))) . (card I) by A11, A16, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (0 + (card I)) by A20, FUNCT_4:13
.= IncAddr ((goto ((card J) + 1)),(card I)) by A19, A10, COMPOS_1:35
.= goto (((card J) + 1) + (card I)) by SCMFSA_4:1
.= goto (((card I) + (card J)) + 1) ;

A28: 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 A27, 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 A27, SCMFSA_2:69 ; :: thesis:
then A29: 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 A11, A18, FUNCT_4:13
.= (Reloc (((Goto ((card J) + 1)) ";" (J ";" (Stop SCM+FSA))),(card I))) . (((card J) + 1) + (card I)) by A25, FUNCT_4:13
.= IncAddr ((halt SCM+FSA),(card I)) by A23, A24, 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 A27, 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 A28, 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 A1, A6, A12, Th22; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A31: k < (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis:

per cases ;

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

then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(Initialize s),k))) <> halt SCM+FSA by A1, A6, Th21;
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 A1, A6, A11, A32, Th26; :: thesis:

end;

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

k < ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 by A31;
then A34: k <= (LifeSpan ((P +* I),(Initialize s))) + 1 by NAT_1:13;
(LifeSpan ((P +* I),(Initialize s))) + 1 <= k by A33, 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 A27, A34, XXREAL_0:1; :: thesis:

end;

end;

end;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A35: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis:
then Comput ((P +* I),(Initialize s),k) = Comput ((P +* (Directed I)),(Initialize s),k) by A1, A6, Th21;
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 A1, A6, A11, A35, Th26; :: 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 A1, A6, A26, Th22; :: thesis:
thus A36: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by A29, EXTPRO_1:29; :: thesis:
for k being Element of 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 A30;
hence LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 by A29, A36, EXTPRO_1:def 15; :: thesis: