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 J0 = Directed J;
set s0 = Initialized s;
set J9 = J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)));
set s00 = s +* ((Directed J) +* (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 s5 = Comput ((ProgramPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),2);
set i = a >0_goto ((card J) + 3);
A1: (Directed J) +* (Start-At (0,SCM+FSA)) c= s +* ((Directed J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
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) = (((Macro (a >0_goto ((card J) + 3))) ';' J) ';' (Goto ((card I) + 1))) ';' (I ';' (Stop SCM+FSA)) by SCMFSA6A:67;
then if>0 (a,I,J) = ((Macro (a >0_goto ((card J) + 3))) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))) by SCMFSA6A:67;
then A2: if>0 (a,I,J) = (Macro (a >0_goto ((card J) + 3))) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) by SCMFSA6A:67;
card (Macro (a >0_goto ((card J) + 3))) = 2 by COMPOS_1:150;
then A3: ProgramPart (Relocated ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2)) c= if>0 (a,I,J) by A2, FUNCT_4:26;
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: (s +* ((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 ;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:15
.= ((card J) + 2) + ((card I) + 2) ;
then A6: ((card J) + 2) + 0 < card (if>0 (a,I,J)) by XREAL_1:10;
then A7: (card J) + 2 in dom (if>0 (a,I,J)) by AFINSQ_1:70;
IC SCM+FSA in dom ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
then A8: IC (s +* ((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 ;
set ss = 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2));
A9: if>0 (a,I,J) c= (if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
A10: if>0 (a,I,J) c= s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26, SCMFSA6B:5;
(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 if>0 (a,I,J) c= s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by A9, XBOOLE_1:1;
then ProgramPart (Relocated ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2)) c= s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by A3, XBOOLE_1:1;
then ProgramPart (ProgramPart (Relocated ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2))) 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)))),2) by AMI_1:99;
then A11: ProgramPart (Relocated ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2)) 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)))),2) by RELAT_1:209;
ProgramPart (Relocated ((Directed J),2)) c= ProgramPart (Relocated ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2)) by Th12, SCMFSA6A:55;
then A12: ProgramPart (Relocated ((Directed J),2)) 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)))),2) by A11, XBOOLE_1:1;
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 A13: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:70;
assume s . a <= 0 ; :: thesis:
then A14: (Initialized s) . a <= 0 by SCMFSA6C:3;
A15: 1 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 A16: dom (if>0 (a,I,J)) c= dom ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
A17: if>0 (a,I,J) c= s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26, SCMFSA6B:5;
assume A18: Directed J is_pseudo-closed_on s ; :: thesis:
then A19: pseudo-LifeSpan (s,(Directed J)) = LifeSpan ((ProgramPart (s +* ((J ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((J ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))) by Th58;
A20: (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)) . 1 = (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . 1 by AMI_1:54
.= ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))) . 1 by A15, A16, FUNCT_4:14
.= (if>0 (a,I,J)) . 1 by A15, SCMFSA6B:7
.= goto 2 by Th55 ;
DataPart s = DataPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;
then A21: Directed J is_pseudo-closed_on s +* ((Directed J) +* (Start-At (0,SCM+FSA))) by A18, Th52;
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;
A22: 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 EXTPRO_1:4
.= 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 EXTPRO_1:3
.= Exec ((a >0_goto ((card J) + 3)),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by A8, A5, Y ;
(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . a = s . a by Th28
.= (Initialized s) . a by SCMFSA6C:3 ;
then A23: 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)) = succ (IC (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) by A14, A22, SCMFSA_2:97
.= 0 + 1 by A8 ;
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)))),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)))),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)))),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)))),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;
A24: 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 + 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)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(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 A23, A20, Y, T ;
then A25: 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)))),2)) = 2 by SCMFSA_2:95;
A26: DataPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA)))) = DataPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) by SCMFSA6A:39, SCMFSA8A:14;

A27: now

let f be FinSeq-Location ; :: thesis:
thus (s +* ((Directed J) +* (Start-At (0,SCM+FSA)))) . f = (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . f by A26, 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 A22, SCMFSA_2:97
.= (Comput ((ProgramPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),2)) . f by A24, SCMFSA_2:95 ; :: thesis:

end;

now

let a be Int-Location ; :: thesis:
thus (s +* ((Directed J) +* (Start-At (0,SCM+FSA)))) . a = (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . a by A26, 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 A22, SCMFSA_2:97
.= (Comput ((ProgramPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),2)) . a by A24, SCMFSA_2:95 ; :: thesis:

end;

then A28: DataPart (s +* ((Directed J) +* (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)))),2)) by A27, SCMFSA6A:38;
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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2)))) /. (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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2)))) = (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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2))) . (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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2)))) 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)))),2)) by AMI_1:123;
A29: 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2))) = 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)))),2)),(pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))))) by EXTPRO_1:5
.= (IC (Comput ((ProgramPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J)))))) + 2 by A1, A21, A12, A25, A28, T, Th51
.= (IC (Comput ((ProgramPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,(Directed J)))))) + 2 by A18, Th50
.= (card (ProgramPart (Directed J))) + 2 by A18, SCMFSA8A:def 5
.= (card (Directed J)) + 2 by RELAT_1:209
.= (card J) + 2 by SCMFSA8A:34 ;
then A30: 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)))),((pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2)))),(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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2)))) = (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . ((card J) + 2) by Y, AMI_1:54
.= (if>0 (a,I,J)) . ((card J) + 2) by A10, A7, GRFUNC_1:8
.= goto (((card I) + (card J)) + 3) by Th64 ;
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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 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)))),((pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2))) 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 1))) by AMI_1:123;
A31: 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 1))) = IC (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)))),((pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2))))) by EXTPRO_1:4
.= ((card I) + (card J)) + 3 by A30, T, SCMFSA_2:95 ;
then A32: 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 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 A17, A13, GRFUNC_1:8
.= halt SCM+FSA by Th62 ;
then A33: 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 EXTPRO_1:30;
hence if>0 (a,I,J) is_halting_on s by SCMFSA7B:def 8; :: thesis:

now

let k be Element of NAT ; :: thesis:

per cases ;

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 EXTPRO_1: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)) = 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 ( 0 < k & k = 1 ) ; :: 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 A23, Th54; :: thesis:

end;

suppose A34: ( 0 < k & k <> 1 & k < (pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2 ) ; :: thesis:

then 0 + 1 <= k by INT_1:20;
then 1 < k by A34, XXREAL_0:1;
then 0 + (1 + 1) <= k by INT_1:20;
then consider k2 being Nat such that
A35: 2 + k2 = k by NAT_1:10;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:15
.= ((card J) + 2) + ((card I) + 2) ;
then A36: (card J) + 2 <= card (if>0 (a,I,J)) by NAT_1:12;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput ((ProgramPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),k2)) as Element of NAT ;
A37: k2 < pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J)) by A34, A35, XREAL_1:8;
then k2 < pseudo-LifeSpan (s,(Directed J)) by A18, Th50;
then n in dom (Directed J) by A18, SCMFSA8A:31;
then n < card (Directed J) by AFINSQ_1:70;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:8;
then n + 2 < (card J) + 2 by SCMFSA8A:34;
then A38: n + 2 < card (if>0 (a,I,J)) by A36, 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)))),2)) 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)))),2)),k2)) by A35, EXTPRO_1:5
.= (IC (Comput ((ProgramPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),k2))) + 2 by A1, A21, A12, A25, A28, A37, Th51, T ;
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 A38, AFINSQ_1:70; :: thesis:

end;

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

hereby :: thesis:

per cases ) + 2 = k or (pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2 < k ) by A39, XXREAL_0:1;

suppose (pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2 = 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 A6, A29, AFINSQ_1:70; :: thesis:

end;

suppose (pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2 < k ; :: thesis:

then ((pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 2) + 1 <= k by INT_1:20;
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 A13, A31, A32, EXTPRO_1:6; :: thesis:

end;

end;

end;

end;

end;

end;

hence if>0 (a,I,J) is_closed_on s by SCMFSA7B:def 7; :: thesis:
V: (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;
A40: CurInstr ((ProgramPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))) = a >0_goto ((card J) + 3) by A8, A5, V;

now

A41: 0 + 2 < ((card I) + (card J)) + 3 by XREAL_1:10;
then A42: 2 in dom (if>0 (a,I,J)) by Th57;
A43: (if>0 (a,I,J)) . 2 <> halt SCM+FSA by A41, Th57;
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)))),2))) /. (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)))),2))) = (Comput ((ProgramPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),2)) . (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)))),2))) by COMPOS_1:38;
A44: 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)))),2))),(Comput ((ProgramPart (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA))))),(s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))),2))) = (s +* ((if>0 (a,I,J)) +* (Start-At (0,SCM+FSA)))) . 2 by A25, Y, AMI_1:54
.= (if>0 (a,I,J)) . 2 by A42, Th26 ;
let k be Element of NAT ; :: 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 A45: 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:
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 EXTPRO_1:3;
U: (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 (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))) = a >0_goto ((card J) + 3) by A40, u;
then A46: k <> 0 by A45;
xx: k <> 1 by A23, A20, A45, U, TX3;
2 <> k by A45, A43, A44, TX3;
then 2 < k by A46, xx, NAT_1:27;
then consider k2 being Nat such that
A47: 2 + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput ((ProgramPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),k2)) as Element of NAT ;
assume not (pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + (1 + 2) <= k ; :: thesis:
then k < ((pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 1) + 2 ;
then k2 < (pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 1 by A47, XREAL_1:8;
then A48: k2 <= pseudo-LifeSpan ((s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),(Directed J)) by NAT_1:13;
then A49: k2 <= pseudo-LifeSpan (s,(Directed J)) by A18, Th50;

A50: now

per cases by A49, XXREAL_0:1;

suppose A51: k2 = pseudo-LifeSpan (s,(Directed J)) ; :: thesis:

((card I) + (card J)) + (2 + 1) = (((card J) + 2) + 1) + (card I) ;
then A52: ((card J) + 2) + 1 <= ((card I) + (card J)) + 3 by NAT_1:11;
IC (Comput ((ProgramPart (s +* ((Directed J) +* (Start-At (0,SCM+FSA))))),(s +* ((Directed J) +* (Start-At (0,SCM+FSA)))),k2)) = card (ProgramPart (Directed J)) by A18, A51, SCMFSA8A:def 5
.= card (Directed J) by RELAT_1:209 ;
then n = card J by SCMFSA8A:34;
hence n + 2 < ((card I) + (card J)) + 3 by A52, NAT_1:13; :: thesis:

end;

suppose k2 < pseudo-LifeSpan (s,(Directed J)) ; :: thesis:

then n in dom (Directed J) by A18, SCMFSA8A:31;
then n < card (Directed J) by AFINSQ_1:70;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:8;
then A53: n + 2 < (card J) + 2 by SCMFSA8A:34;
((card I) + (card J)) + (1 + 2) = ((card J) + 2) + ((card I) + 1) ;
then (card J) + 2 <= ((card I) + (card J)) + 3 by NAT_1:11;
hence n + 2 < ((card I) + (card J)) + 3 by A53, XXREAL_0:2; :: thesis:

end;

end;

end;

then A54: n + 2 in dom (if>0 (a,I,J)) by Th57;
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)))),2)) by AMI_1:123;
A55: 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)))),2)),k2)) by A47, EXTPRO_1:5
.= n + 2 by A1, A21, A12, A25, A28, A48, Th51, T ;
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)))),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;
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;
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))) = (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 Y, TX3, 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 A55, A54, Th26 ;
hence contradiction by A45, A55, A50, Th57; :: 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 J) +* (Start-At (0,SCM+FSA)))),(Directed J))) + 3 by A32, A33, EXTPRO_1:def 14;
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 +* ((J ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA))))),(s +* ((J ';' (Stop SCM+FSA)) +* (Start-At (0,SCM+FSA)))))) + 3 by A18, A19, Th50; :: thesis: