let ss be State of SCM+FSA; :: thesis:
set A = NAT ;
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 s = Initialized ss;
set I1 = I ';' (Stop SCM+FSA);
set s00 = (Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)));
set s3 = (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)));
set s4 = Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1);
set i = a >0_goto ((card J) + 3);
assume A1: ss . (intloc 0) = 1 ; :: thesis:
set s1 = (Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)));
assume ss . a > 0 ; :: thesis:
then A2: (Initialized ss) . a > 0 by SCMFSA6C:3;
IC SCM+FSA in dom ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
then A3: IC ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = IC ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A4: 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 A5: ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . 0 = ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) . 0 by A4, FUNCT_4:14
.= (if>0 (a,I,J)) . 0 by A4, SCMFSA6B:7
.= a >0_goto ((card J) + 3) by Th55 ;
Y: (ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) /. (IC ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) = ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . (IC ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
A6: Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),(0 + 1)) = Following ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by EXTPRO_1:3
.= Exec ((a >0_goto ((card J) + 3)),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by A3, A5, Y ;
not a in dom ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
then ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . a = (Initialized ss) . a by FUNCT_4:12;
then A7: IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) = (card J) + 3 by A2, A6, SCMFSA_2:97;
assume Directed I is_pseudo-closed_on ss ; :: thesis:
then A8: Directed I is_pseudo-closed_on Initialized ss by A1, Th53;
then A9: LifeSpan ((ProgramPart ((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) = pseudo-LifeSpan ((Initialized ss),(Directed I)) by Th58;
DataPart (Initialized ss) = DataPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;
then A10: Directed I is_pseudo-closed_on (Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))) by A8, Th52;
A11: DataPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))) = DataPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) by SCMFSA6A:39, SCMFSA8A:14;

A12: now

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

end;

now

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

end;

then A13: DataPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))) = DataPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) by A12, SCMFSA6A:38;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:15
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if>0 (a,I,J)) by NAT_1:13;
then A14: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:70;
A15: 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 COMPOS_1:150
.= (card J) + (2 + 1) ;
(Initialized ss) +* (Initialized (if>0 (a,I,J))) = (Initialized (Initialized ss)) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
then A16: (Initialized ss) +* (Initialized (if>0 (a,I,J))) = (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by Th15;
A17: if>0 (a,I,J) c= (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26, SCMFSA6B:5;
A18: 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= (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then A19: if>0 (a,I,J) c= (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by A18, XBOOLE_1:1;
A20: (Directed I) +* (Start-At (0,SCM+FSA)) c= (Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
A21: if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) by SCMFSA8B:def 2;
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 A15, FUNCT_4:26;
then ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3))) c= (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by A19, XBOOLE_1:1;
then ProgramPart (ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3)))) c= Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1) by AMI_1:99;
then A22: ProgramPart (Relocated ((I ';' (Stop SCM+FSA)),((card J) + 3))) c= Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((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 A23: ProgramPart (Relocated ((Directed I),((card J) + 3))) c= Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1) by A22, XBOOLE_1:1;
Y: (ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1)))) /. (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1)))) = (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1))) . (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1)))) by COMPOS_1:38;
T: ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
TX3: ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1))) by AMI_1:123;
IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1))) = IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)),(pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))))) by EXTPRO_1:5
.= (IC (Comput ((ProgramPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)))))) + ((card J) + 3) by A20, A10, A23, A7, A13, Th51, T
.= (IC (Comput ((ProgramPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan ((Initialized ss),(Directed I)))))) + ((card J) + 3) by A8, Th50
.= (card (ProgramPart (Directed I))) + ((card J) + 3) by A8, 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 A24: CurInstr ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),((pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1)))) = ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . (((card I) + (card J)) + 3) by Y, TX3, AMI_1:54
.= (if>0 (a,I,J)) . (((card I) + (card J)) + 3) by A17, A14, GRFUNC_1:8
.= halt SCM+FSA by Th62 ;
then A25: ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) halts_on (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;

now

set J1 = (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I;
let k be Element of NAT ; :: thesis:
assume A26: CurInstr ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) = halt SCM+FSA ; :: thesis:
assume not (pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1 <= k ; :: thesis:
then A27: k <= pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) by NAT_1:13;
A28: 0 in dom (if>0 (a,I,J)) by Th54;
u: Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),0) = (Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by EXTPRO_1:3;
Y: (ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) /. (IC ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) = ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . (IC ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
CurInstr ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),0))) = CurInstr ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by u
.= ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . 0 by Th31, Y
.= (if>0 (a,I,J)) . 0 by A28, Th26
.= a >0_goto ((card J) + 3) by Th55 ;
then k <> 0 by A26;
then consider k1 being Nat such that
A30: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput ((ProgramPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k1)) as Element of NAT ;
k1 < k by A30, XREAL_1:31;
then A31: k1 < pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I)) by A27, XXREAL_0:2;
then k1 < pseudo-LifeSpan ((Initialized ss),(Directed I)) by A8, Th50;
then n in dom (Directed I) by A8, 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 A32: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
T: ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
A33: IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) = IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)),k1)) by A30, EXTPRO_1:5
.= (IC (Comput ((ProgramPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),k1))) + ((card J) + 3) by A20, A10, A23, A7, A13, A31, 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 COMPOS_1:150
.= ((card I) + (card J)) + 3 ;
then IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((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 A33, A32, AFINSQ_1:70;
then A34: IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((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 A35: (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((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:15
.= (((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 A32, XXREAL_0:2;
then A36: IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) in dom (if>0 (a,I,J)) by A33, AFINSQ_1:70;
Y: (ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) /. (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) = (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) . (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) by COMPOS_1:38;
TX3: ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k)) by AMI_1:123;
A37: CurInstr ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) = ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) by Y, TX3, AMI_1:54
.= (if>0 (a,I,J)) . (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) by A36, Th26 ;
Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) c= if>0 (a,I,J) by A21, SCMFSA6A:55;
then (if>0 (a,I,J)) . (IC (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((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 ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),k))) by A34, GRFUNC_1:8;
hence contradiction by A26, A35, A37, COMPOS_1:def 7; :: thesis:

end;

then A38: LifeSpan ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) = (pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))) + 1 by A24, A25, EXTPRO_1:def 14;
(Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA))) = (Initialized (Initialized ss)) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
then A39: (Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA))) = (Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by Th15;
A40: (Directed I) ';' (Stop SCM+FSA) = I ';' (Stop SCM+FSA) by SCMFSA8A:41;
Directed (Directed I) = Directed I by SCMFSA6A:63;
then A41: DataPart (Comput ((ProgramPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan ((Initialized ss),(Directed I))))) = DataPart (Comput ((ProgramPart ((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan ((Initialized ss),(Directed I))))) by A8, A40, Th58;
I ';' (Stop SCM+FSA) is_halting_on Initialized ss by A8, Th58;
then A42: ProgramPart ((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))) halts_on (Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
T: ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
thus DataPart (IExec ((if>0 (a,I,J)),ss)) = DataPart (IExec ((if>0 (a,I,J)),(Initialized ss))) by Th17
.= DataPart ((Result ((ProgramPart ((Initialized ss) +* (Initialized (if>0 (a,I,J))))),((Initialized ss) +* (Initialized (if>0 (a,I,J)))))) +* ((Initialized ss) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))))) by A16, Th35
.= DataPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))))))) by A25, EXTPRO_1:23
.= DataPart (Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),1)),(pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))))) by A38, EXTPRO_1:5
.= DataPart (Comput ((ProgramPart ((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (((Initialized ss) +* ((Directed I) +* (Start-At (0,SCM+FSA)))),(Directed I))))) by A20, A10, A23, A7, A13, T, Th51
.= DataPart (Comput ((ProgramPart ((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))))) by A8, A9, A41, Th50
.= DataPart (Result ((ProgramPart ((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),((Initialized ss) +* ((I ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) by A42, EXTPRO_1:23
.= DataPart ((Result ((ProgramPart ((Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA))))),((Initialized ss) +* (Initialized (I ';' (Stop SCM+FSA)))))) +* ((Initialized ss) | NAT)) by A39, Th35
.= DataPart (IExec ((I ';' (Stop SCM+FSA)),(Initialized ss))) by SCMFSA6B:def 1
.= DataPart (IExec ((I ';' (Stop SCM+FSA)),ss)) by Th17 ; :: thesis: