let I, J be Program of ; :: thesis: for s being State of st I is_closed_on s & I is_halting_on s holds
( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )
let s be State of ; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 ) )
assume A1: I is_closed_on s ; :: thesis: ( not I is_halting_on s or ( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 ) )
A2: card ((Goto (insloc ((card J) + 1))) ';' J) = (card (Goto (insloc ((card J) + 1)))) + (card J) by SCMFSA6A:61
.= 1 + (card J) by Lm1 ;
A3: ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1)) c= Relocated (Stop SCM+FSA ),((card J) + 1) by RELAT_1:88;
A4: card ((Goto (insloc ((card J) + 1))) ';' J) = (card (Goto (insloc ((card J) + 1)))) + (card J) by SCMFSA6A:61
.= (card J) + 1 by Lm1 ;
A5: insloc (((card I) + (card J)) + 1) = insloc (((card J) + 1) + (card I)) ;
A6: insloc 0 in dom (ProgramPart (Stop SCM+FSA )) by Th15, AMI_1:105;
set J2 = (Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ));
set s2 = s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
set s1 = s +* (I +* (Start-At (insloc 0 )));
assume A7: I is_halting_on s ; :: thesis: ( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = insloc (((card I) + (card J)) + 1) & DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )
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;
then A8: insloc (0 + ((card J) + 1)) in dom (ProgramPart (Relocated (Stop SCM+FSA ),((card J) + 1))) by A6;
A9: dom (Goto (insloc ((card J) + 1))) c= dom ((Goto (insloc ((card J) + 1))) ';' J) by SCMFSA6A:56;
A10: insloc 0 in dom (Goto (insloc ((card J) + 1))) by Lm1;
A11: ((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 A10, A9, Th28
.= ((Goto (insloc ((card J) + 1))) ';' (Directed J)) . (insloc 0 ) by SCMFSA6A:66
.= (Directed (Goto (insloc ((card J) + 1)))) . (insloc 0 ) by A10, Th28
.= (Goto (insloc ((card J) + 1))) . (insloc 0 ) by SCMFSA6A:63
.= goto (insloc ((card J) + 1)) by Lm1 ;
A12: 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;
A13: ((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 ;
then A14: DataPart (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) by A1, A7, Th42;
I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) c= (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At (insloc 0 )) by Th9;
then A15: dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) c= dom ((I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) c= (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At (insloc 0 )) by Th9;
then A16: dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) c= dom ((I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At (insloc 0 ))) by GRFUNC_1:8;
A17: 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 A18: 0 + 1 <= card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) by NAT_1:11;
A19: 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;
then (card I) + 0 < card (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by A18, XREAL_1:8;
then A20: insloc (card I) in dom (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by SCMFSA6A:15;
card (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) = (card I) + (card (((Goto (insloc ((card J) + 1))) ';' J) ';' (Stop SCM+FSA ))) by A19, 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 A21: insloc (((card I) + (card J)) + 1) 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 A22: insloc 0 in dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by A18, 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 A23: insloc (0 + (card I)) in dom (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) by SCMFSA_5:3;
card ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))) = 1 + ((card J) + (card (Stop SCM+FSA ))) by A17, 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 A24: insloc ((card J) + 1) in dom (ProgramPart ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) by AMI_1:105;
A25: ((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 A2, A8, FUNCT_4:14
.= (Relocated (Stop SCM+FSA ),((card J) + 1)) . (insloc (0 + ((card J) + 1))) by A3, A8, GRFUNC_1:8
.= IncAddr (halt SCM+FSA ),((card J) + 1) by A6, Th16, SCMFSA_5:7
.= halt SCM+FSA by SCMFSA_4:8 ;
A26: 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;
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;
then A27: insloc (((card I) + (card J)) + 1) in dom (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) by A24, A5;
A28: IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) by A1, A7, A13, Th42;
then A29: CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) . (insloc (card I)) by A1, A7, Th36
.= (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (insloc (card I)) by AMI_1:54
.= ((I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At (insloc 0 ))) . (insloc (card I)) by A13, A16, A20, FUNCT_4:14
.= (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) . (insloc (card I)) by A20, SCMFSA6B:7
.= (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) . (insloc (card I)) by A23, FUNCT_4:14
.= (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I)) . (insloc (0 + (card I))) by A23, A12, GRFUNC_1:8
.= IncAddr (goto (insloc ((card J) + 1))),(card I) by A22, A11, SCMFSA_5:7
.= goto ((insloc ((card J) + 1)) + (card I)) by SCMFSA_4:14
.= goto (insloc (((card I) + (card J)) + 1)) ;

A30: now

let f be FinSeq-Location ; :: thesis: (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + (1 + 1))) . f = (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) . f
thus (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + (1 + 1))) . f = (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 1)) . f
.= (Following (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1))) . f by AMI_1:14
.= (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) . f by A29, SCMFSA_2:95 ; :: thesis: verum

end;

thus IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),(((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 1))
.= IC (Following (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1))) by AMI_1:14
.= insloc (((card I) + (card J)) + 1) by A29, SCMFSA_2:95 ; :: thesis: ( DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) & ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )
then A31: CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) = (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . (insloc (((card I) + (card J)) + 1)) by AMI_1:54
.= ((I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) +* (Start-At (insloc 0 ))) . (insloc (((card I) + (card J)) + 1)) by A13, A21, A15, FUNCT_4:14
.= (I ';' ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA )))) . (insloc (((card I) + (card J)) + 1)) by A21, SCMFSA6B:7
.= (ProgramPart (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I))) . (insloc (((card I) + (card J)) + 1)) by A27, FUNCT_4:14
.= (Relocated ((Goto (insloc ((card J) + 1))) ';' (J ';' (Stop SCM+FSA ))),(card I)) . (insloc (((card J) + 1) + (card I))) by A27, A26, GRFUNC_1:8
.= IncAddr (halt SCM+FSA ),(card I) by A24, A25, SCMFSA_5:7
.= halt SCM+FSA by SCMFSA_4:8 ;

now

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

end;

then DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) by A30, SCMFSA6A:38;
hence DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 )))))) = DataPart (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2)) by A1, A7, A14, Th36; :: thesis: ( ( for k being Element of NAT st k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 holds
CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA ) & ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )

hereby :: thesis: ( ( for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) ) & IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )

let k be Element of NAT ; :: thesis: ( k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 implies CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) <> halt SCM+FSA )
assume A33: k < (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 ; :: thesis: CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) <> halt SCM+FSA

per cases ( k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) or LifeSpan (s +* (I +* (Start-At (insloc 0 )))) < k ) ;

suppose A34: k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) <> halt SCM+FSA

then CurInstr (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA by A1, A7, Th35;
hence CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA by A1, A7, A13, A34, Th42; :: thesis: verum

end;

suppose A35: LifeSpan (s +* (I +* (Start-At (insloc 0 )))) < k ; :: thesis: CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),b₁) <> halt SCM+FSA

A36: InsCode (goto (insloc (((card I) + (card J)) + 1))) = 6 by SCMFSA_2:47;
k < ((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1) + 1 by A33;
then A37: k <= (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 by NAT_1:13;
(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1 <= k by A35, NAT_1:13;
hence CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) <> halt SCM+FSA by A29, A37, A36, SCMFSA_2:124, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hereby :: thesis: ( IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) & ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )

let k be Element of NAT ; :: thesis: ( k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) implies IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) )
assume A38: k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) ; :: thesis: IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k)
then IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k) by A1, A7, Th35, AMI_1:121;
hence IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = IC (Computation (s +* (I +* (Start-At (insloc 0 )))),k) by A1, A7, A13, A38, Th42; :: thesis: verum

end;

thus IC (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 1)) = insloc (card I) by A1, A7, A28, Th36; :: thesis: ( ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) & LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 )
thus A39: ProgramPart (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) halts_on s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) by A31, AMI_1:146; :: thesis: LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2
for k being Element of NAT st CurInstr (Computation (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA holds
(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 <= k by A32;
hence LifeSpan (s +* ((((I ';' (Goto (insloc ((card J) + 1)))) ';' J) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 2 by A31, A39, AMI_1:def 46; :: thesis: verum