let I, J be Program of SCM+FSA ; :: thesis:
let s be State of SCM+FSA ; :: thesis:
assume A1: I is_closed_on Initialize s ; :: thesis:
assume A2: I is_halting_on Initialize s ; :: thesis:
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )));
set J2 = (Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ));
A3: ((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ) = (I ';' (Goto (insloc ((card J) + 1)))) ';' (J ';' (Stop SCM+FSA )) by SCMFSA6A:67
.= I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) by SCMFSA6A:67 ;
A4: card ((Goto (insloc ((card J) + 1))) ';' J) = (card (Goto (insloc ((card J) + 1)))) + (card J) by SCMFSA6A:61
.= (card J) + 1 by Lm1 ;
I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) c= Initialized (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by SCMFSA6A:26;
then A5: dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) c= dom (Initialized (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))))) by GRFUNC_1:8;
A6: card (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) = (card I) + (card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by SCMFSA6A:61;
A7: card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) = (card (Goto (insloc ((card J) + 1)))) + (card (J ';' (Stop SCM+FSA ))) by SCMFSA6A:61
.= 1 + (card (J ';' (Stop SCM+FSA ))) by Lm1 ;
then A8: 0 + 1 <= card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) by NAT_1:11;
then (card I) + 0 < card (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by A6, XREAL_1:8;
then A9: insloc (card I) in dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by SCMFSA6A:15;
dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) = dom ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) by AMI_1:105;
then A10: insloc 0 in dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by A8, SCMFSA6A:15;
then insloc (0 + (card I)) in { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) } ;
then A11: insloc (0 + (card I)) in dom (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) by SCMFSA_5:3;
A12: insloc 0 in dom (Goto (insloc ((card J) + 1))) by Lm1;
A13: dom (Goto (insloc ((card J) + 1))) c= dom ((Goto (insloc ((card J) + 1))) ';' J) by SCMFSA6A:56;
A14: ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) . (insloc 0 ) = (((Goto (insloc ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) . (insloc 0 ) by SCMFSA6A:67
.= (Directed ((Goto (insloc ((card J) + 1))) ';' J)) . (insloc 0 ) by A12, A13, Th28
.= ((Goto (insloc ((card J) + 1))) ';' (Directed J)) . (insloc 0 ) by SCMFSA6A:66
.= (Directed (Goto (insloc ((card J) + 1)))) . (insloc 0 ) by A12, Th28
.= (Goto (insloc ((card J) + 1))) . (insloc 0 ) by SCMFSA6A:63
.= goto (insloc ((card J) + 1)) by Lm1 ;
A15: ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I)) c= Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I) by RELAT_1:88;
A16: ( DataPart (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = DataPart (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) & IC (Computation (s +* (Initialized (Directed I))),((LifeSpan (s +* (Initialized I))) + 1)) = IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) ) by A1, A2, A3, Th43;
then A17: CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) . (insloc (card I)) by A1, A2, Th45
.= (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) . (insloc (card I)) by AMI_1:54
.= (Initialized (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))))) . (insloc (card I)) by A3, A5, A9, FUNCT_4:14
.= (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) . (insloc (card I)) by A9, SCMFSA6A:50
.= (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) . (insloc (card I)) by A11, FUNCT_4:14
.= (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I)) . (insloc (0 + (card I))) by A11, A15, GRFUNC_1:8
.= IncAddr (goto (insloc ((card J) + 1))),(card I) by A10, A14, SCMFSA_5:7
.= goto ((insloc ((card J) + 1)) + (card I)) by SCMFSA_4:14
.= goto (insloc (((card I) + (card J)) + 1)) ;
card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) = 1 + ((card J) + (card (Stop SCM+FSA ))) by A7, SCMFSA6A:61
.= (card J) + (1 + (card (Stop SCM+FSA ))) ;
then (card J) + 1 < card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) by Th17, XREAL_1:8;
then insloc ((card J) + 1) in dom ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) by SCMFSA6A:15;
then A18: insloc ((card J) + 1) in dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by AMI_1:105;
A19: dom (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) = { (m + (card I)) where m is Element of NAT : m in dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) } by SCMFSA_5:3;
card (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) = (card I) + (card (((Goto (insloc ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))) by A6, SCMFSA6A:67
.= (card I) + (((card J) + 1) + 1) by A4, Th17, SCMFSA6A:61
.= (((card I) + (card J)) + 1) + 1 ;
then ((card I) + (card J)) + 1 < card (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by NAT_1:13;
then A20: insloc (((card I) + (card J)) + 1) in dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by SCMFSA6A:15;
I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) c= Initialized (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by SCMFSA6A:26;
then A21: dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) c= dom (Initialized (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))))) by GRFUNC_1:8;
insloc (((card I) + (card J)) + 1) = insloc (((card J) + 1) + (card I)) ;
then A22: insloc (((card I) + (card J)) + 1) in dom (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) by A18, A19;
A23: ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1)) c= Relocated (Stop SCM+FSA ),((card J) + 1) by RELAT_1:88;
A24: card ((Goto (insloc ((card J) + 1))) ';' J) = (card (Goto (insloc ((card J) + 1)))) + (card J) by SCMFSA6A:61
.= 1 + (card J) by Lm1 ;
A25: dom (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) = { (m + ((card J) + 1)) where m is Element of NAT : m in dom (ProgramPart (Stop SCM+FSA )) } by SCMFSA_5:3;
A26: insloc 0 in dom (ProgramPart (Stop SCM+FSA )) by Th16, AMI_1:105;
then A27: insloc (0 + ((card J) + 1)) in dom (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) by A25;
A28: ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) . (insloc ((card J) + 1)) = (((Goto (insloc ((card J) + 1))) ';' J) ';' (Stop SCM+FSA )) . (insloc ((card J) + 1)) by SCMFSA6A:67
.= (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) . (insloc ((card J) + 1)) by A27, A24, FUNCT_4:14
.= (Relocated (Stop SCM+FSA ),((card J) + 1)) . (insloc (0 + ((card J) + 1))) by A23, A27, GRFUNC_1:8
.= IncAddr (halt SCM+FSA ),((card J) + 1) by A26, Th16A, SCMFSA_5:7
.= halt SCM+FSA by SCMFSA_4:8 ;
A29: ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I)) c= Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I) by RELAT_1:88;
thus IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) = IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),(((LifeSpan (s +* (Initialized I))) + 1) + 1))
.= IC (Following (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1))) by AMI_1:14
.= insloc (((card I) + (card J)) + 1) by A17, SCMFSA_2:95 ; :: thesis:
then A30: CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 2)) = (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) . (insloc (((card I) + (card J)) + 1)) by AMI_1:54
.= (Initialized (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))))) . (insloc (((card I) + (card J)) + 1)) by A3, A20, A21, FUNCT_4:14
.= (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) . (insloc (((card I) + (card J)) + 1)) by A20, SCMFSA6A:50
.= (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) . (insloc (((card I) + (card J)) + 1)) by A22, FUNCT_4:14
.= (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I)) . (insloc (((card J) + 1) + (card I))) by A22, A29, GRFUNC_1:8
.= IncAddr (halt SCM+FSA ),(card I) by A18, A28, SCMFSA_5:7
.= halt SCM+FSA by SCMFSA_4:8 ;

A31: now

let a be Int-Location ; :: thesis:
thus (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + (1 + 1))) . a = (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),(((LifeSpan (s +* (Initialized I))) + 1) + 1)) . a
.= (Following (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1))) . a by AMI_1:14
.= (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) . a by A17, SCMFSA_2:95 ; :: thesis:

end;

now

end;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A32: k < (LifeSpan (s +* (Initialized I))) + 2 ; :: thesis:

per cases ;

suppose A33: k <= LifeSpan (s +* (Initialized I)) ; :: thesis:

then CurInstr (Computation (s +* (Initialized (Directed I))),k) <> halt SCM+FSA by A1, A2, Th44;
hence CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) <> halt SCM+FSA by A1, A2, A3, A33, Th43; :: thesis:

end;

suppose LifeSpan (s +* (Initialized I)) < k ; :: thesis:

then A34: (LifeSpan (s +* (Initialized I))) + 1 <= k by NAT_1:13;
k < ((LifeSpan (s +* (Initialized I))) + 1) + 1 by A32;
then A35: k <= (LifeSpan (s +* (Initialized I))) + 1 by NAT_1:13;
InsCode (goto (insloc (((card I) + (card J)) + 1))) = 6 by SCMFSA_2:47;
hence CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) <> halt SCM+FSA by A17, A34, A35, SCMFSA_2:124, XXREAL_0:1; :: thesis:

end;

then A36: for k being Element of NAT st CurInstr (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) = halt SCM+FSA holds
(LifeSpan (s +* (Initialized I))) + 2 <= k ;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A37: k <= LifeSpan (s +* (Initialized I)) ; :: thesis:
then IC (Computation (s +* (Initialized I)),k) = IC (Computation (s +* (Initialized (Directed I))),k) by A1, A2, Th44, AMI_1:121;
hence IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),k) = IC (Computation (s +* (Initialized I)),k) by A1, A2, A3, A37, Th43; :: thesis:

end;

thus IC (Computation (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) by A1, A2, A16, Th45; :: thesis:
thus s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA ))) is halting by A30, AMI_1:def 20; :: thesis:
hence LifeSpan (s +* (Initialized (((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )))) = (LifeSpan (s +* (Initialized I))) + 2 by A30, A36, AMI_1:def 46; :: thesis: