let s be State of SCM+FSA ; :: thesis:
set D = Int-Locations \/ FinSeq-Locations ;
let I, J be Program of SCM+FSA ; :: thesis:
let a be read-write Int-Location ; :: thesis:
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA );
set s00 = s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ));
set s3 = s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ));
set s4 = Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1;
set i = a =0_goto ((card J) + 3);
A1: (Directed I) +* (Start-At 0 ,SCM+FSA ) c= s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by NAT_1:13;
then A2: ((card I) + (card J)) + 3 in dom (if=0 a,I,J) by AFINSQ_1:70;
A3: if=0 a,I,J c= (if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ) by SCMFSA8A:9;
(if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ) c= s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
then A4: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by A3, XBOOLE_1:1;
A5: not a in dom ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by SCMFSA6B:12;
A6: 0 in dom (if=0 a,I,J) by Th54;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ) by SCMFSA8A:9;
then dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by GRFUNC_1:8;
then A7: (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 0 = ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . 0 by A6, FUNCT_4:14
.= (if=0 a,I,J) . 0 by A6, SCMFSA6B:7
.= a =0_goto ((card J) + 3) by Th55 ;
A8: card (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) = (card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1))) by SCMFSA6A:61
.= (card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1 by SCMFSA8A:29
.= ((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1 by SCMFSA6A:61
.= ((card J) + 2) + 1 by SCMFSA7B:6
.= (card J) + (2 + 1) ;
IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by SF_MASTR:65;
then A9: IC (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . (IC SCM+FSA ) by FUNCT_4:14
.= 0 by SF_MASTR:66 ;
A10: if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26, SCMFSA6B:5;
Y: (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) /. (IC (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) = (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) by COMPOS_1:38;
A11: Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(0 + 1) = Following (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by AMI_1:13
.= Exec (a =0_goto ((card J) + 3)),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by A9, A7, Y ;
A12: if=0 a,I,J = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1;
then if=0 a,I,J = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA )) by SCMFSA6A:67;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if=0 a,I,J by A8, FUNCT_4:26;
then ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by A4, XBOOLE_1:1;
then ProgramPart (ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3))) c= Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1 by AMI_1:99;
then A13: ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1 by RELAT_1:209;
ProgramPart (Relocated (Directed I),((card J) + 3)) c= ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) by Th12, SCMFSA6A:55;
then A14: ProgramPart (Relocated (Directed I),((card J) + 3)) c= Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1 by A13, XBOOLE_1:1;
A15: DataPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))) = DataPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA6A:39, SCMFSA8A:14;

A16: now

let f be FinSeq-Location ; :: thesis:
thus (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))) . f = (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . f by A15, SCMFSA6A:38
.= (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . f by A11, SCMFSA_2:96 ; :: thesis:

end;

let a be Int-Location ; :: thesis:
thus (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))) . a = (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a by A15, SCMFSA6A:38
.= (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . a by A11, SCMFSA_2:96 ; :: thesis:

end;

then A17: DataPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))) = DataPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by A16, SCMFSA6A:38;
assume s . a = 0 ; :: thesis:
then (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a = 0 by A5, FUNCT_4:12;
then A18: IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) = (card J) + 3 by A11, SCMFSA_2:96;
assume A19: Directed I is_pseudo-closed_on s ; :: thesis:
then A20: pseudo-LifeSpan s,(Directed I) = LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) by Th58;
DataPart s = DataPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
then A21: Directed I is_pseudo-closed_on s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )) by A19, Th52;
Y: (ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1))) /. (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1))) = (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1)) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1))) by COMPOS_1:38;
T: ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by AMI_1:123;
TX: ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1)) by AMI_1:123;
A22: IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1)) = IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I))) by AMI_1:51
.= (IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)))) + ((card J) + 3) by A1, A21, T, A14, A18, A17, Th51
.= (IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I)))) + ((card J) + 3) by A19, Th50
.= (card (ProgramPart (Directed I))) + ((card J) + 3) by A19, SCMFSA8A:def 5
.= (card (Directed I)) + ((card J) + 3) by RELAT_1:209
.= (card I) + ((card J) + 3) by SCMFSA8A:34
.= ((card I) + (card J)) + 3 ;
then A23: CurInstr (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1)) = (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (((card I) + (card J)) + 3) by Y, TX, AMI_1:54
.= (if=0 a,I,J) . (((card I) + (card J)) + 3) by A10, A2, GRFUNC_1:8
.= halt SCM+FSA by Th61 ;
then A24: ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by AMI_1:146;
hence if=0 a,I,J is_halting_on s by SCMFSA7B:def 8; :: thesis:

let k be Element of NAT ; :: thesis:

suppose k = 0 ; :: thesis:

then Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k = s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by AMI_1:13;
then IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = 0 by Th31;
hence IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if=0 a,I,J) by Th54; :: thesis:

end;

suppose A25: ( 0 < k & k < (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1 ) ; :: thesis:

card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ;
then A26: ((card I) + (card J)) + 3 < card (if=0 a,I,J) by XREAL_1:31;
0 + 1 <= k by A25, INT_1:20;
then consider k1 being Nat such that
A27: 1 + k1 = k by NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k1) as Element of NAT ;
A28: k1 < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I) by A25, A27, XREAL_1:8;
then k1 < pseudo-LifeSpan s,(Directed I) by A19, Th50;
then n in dom (Directed I) by A19, SCMFSA8A:31;
then n < card (Directed I) by AFINSQ_1:70;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:8;
then n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
then A29: n + ((card J) + 3) < card (if=0 a,I,J) by A26, XXREAL_0:2;
T: ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by AMI_1:123;
IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),k1) by A27, AMI_1:51
.= (IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k1)) + ((card J) + 3) by A1, A21, A14, A18, A17, A28, T, Th51 ;
hence IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if=0 a,I,J) by A29, AFINSQ_1:70; :: thesis:

end;

suppose ( 0 < k & (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1 <= k ) ; :: thesis:

hence IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if=0 a,I,J) by A2, A22, A23, AMI_1:52; :: thesis:

end;

end;

end;

hence if=0 a,I,J is_closed_on s by SCMFSA7B:def 7; :: thesis:

set J1 = (((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I;
let k be Element of NAT ; :: thesis:
assume A30: CurInstr (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA ; :: thesis:
TX3: ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) by AMI_1:123;
assume not (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1 <= k ; :: thesis:
then A31: k <= pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I) by NAT_1:13;
A32: 0 in dom (if=0 a,I,J) by Th54;
A33: InsCode (a =0_goto ((card J) + 3)) = 7 by SCMFSA_2:48;
u: Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 = s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by AMI_1:13;
Y: (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) /. (IC (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) = (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) /. (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) = (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 )),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 ) = CurInstr (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by u
.= (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 0 by Th31, Y
.= (if=0 a,I,J) . 0 by A32, Th26
.= a =0_goto ((card J) + 3) by Th55 ;
then k <> 0 by A30, A33, TX3, SCMFSA_2:124;
then consider k1 being Nat such that
A34: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k1) as Element of NAT ;
k1 < k by A34, XREAL_1:31;
then A35: k1 < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I) by A31, XXREAL_0:2;
then k1 < pseudo-LifeSpan s,(Directed I) by A19, Th50;
then n in dom (Directed I) by A19, SCMFSA8A:31;
then n < card (Directed I) by AFINSQ_1:70;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:8;
then A36: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
T: ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by AMI_1:123;
A37: IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1),k1) by A34, AMI_1:51
.= (IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),k1)) + ((card J) + 3) by A1, A21, A14, A18, A17, A35, Th51, T ;
card ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) = (card (((Macro (a =0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + (card (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:61
.= ((card ((Macro (a =0_goto ((card J) + 3))) ';' J)) + 1) + (card I) by SCMFSA8A:29
.= (((card (Macro (a =0_goto ((card J) + 3)))) + (card J)) + 1) + (card I) by SCMFSA6A:61
.= ((2 + (card J)) + 1) + (card I) by SCMFSA7B:6
.= ((card I) + (card J)) + 3 ;
then IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) by A37, A36, AFINSQ_1:70;
then A38: IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) by FUNCT_4:105;
then A39: (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) in rng (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) by FUNCT_1:def 5;
card (if=0 a,I,J) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:14
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if=0 a,I,J) by XREAL_1:31;
then n + ((card J) + 3) < card (if=0 a,I,J) by A36, XXREAL_0:2;
then A40: IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) in dom (if=0 a,I,J) by A37, AFINSQ_1:70;
A41: CurInstr (ProgramPart (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by Z, AMI_1:54
.= (if=0 a,I,J) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by A40, Th26 ;
Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) c= if=0 a,I,J by A12, SCMFSA6A:55;
then (if=0 a,I,J) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) = (Directed ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by A38, GRFUNC_1:8;
hence contradiction by A30, A39, A41, TX3, COMPOS_1:def 7; :: thesis:

end;

then LifeSpan (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),(Directed I)) + 1 by A23, A24, AMI_1:def 46;
hence LifeSpan (ProgramPart (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1 by A19, A20, Th50; :: thesis: