let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds
DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,s))
let ss be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P holds
DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
set D = Data-Locations SCM+FSA;
set A = NAT ;
let I, J be Program of SCM+FSA; :: thesis: for a being read-write Int-Location st ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P holds
DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
let a be read-write Int-Location ; :: thesis: ( ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P implies DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) )
set J0 = Directed J;
A1: ProgramPart (Directed J) = Directed J by RELAT_1:209;
set s = Initialized ss;
set s0 = Initialized (Initialized ss);
set J9 = J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)));
set s00 = (Initialized ss) +* (Initialize (Directed J));
set P00 = P +* (Directed J);
set s3 = (Initialized ss) +* (Initialize (if>0 (a,I,J)));
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1);
set s5 = Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2);
set i = a >0_goto ((card J) + 3);
A2: if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:26;
A3: Directed J c= P +* (Directed J) by FUNCT_4:26;
assume A4: ss . (intloc 0) = 1 ; :: thesis: ( not ss . a <= 0 or not Directed J is_pseudo-closed_on ss,P or DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) )
set s1 = (Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA)));
set P1 = P +* (J ';' (Stop SCM+FSA));
A5: ProgramPart (J ';' (Stop SCM+FSA)) = J ';' (Stop SCM+FSA) by RELAT_1:209;
assume ss . a <= 0 ; :: thesis: ( not Directed J is_pseudo-closed_on ss,P or DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) )
then (Initialized ss) . a <= 0 by SCMFSA6C:3;
then A6: (Initialized (Initialized ss)) . a <= 0 by SCMFSA6C:3;
A7: 0 in dom (if>0 (a,I,J)) by Th54;
A8: (P +* (if>0 (a,I,J))) . 0 = (if>0 (a,I,J)) . 0 by A7, FUNCT_4:14
.= (if>0 (a,I,J)) . 0
.= a >0_goto ((card J) + 3) by Th55 ;
(Initialized ss) +* (Initialized (if>0 (a,I,J))) = (Initialized (Initialized ss)) +* (Initialize (if>0 (a,I,J))) by SCMFSA8A:13;
then A9: (Initialized ss) +* (Initialized (if>0 (a,I,J))) = (Initialized ss) +* (Initialize (if>0 (a,I,J))) by Th15;
A10: (Directed J) ';' (Stop SCM+FSA) = J ';' (Stop SCM+FSA) by SCMFSA8A:41;
IC in dom (Initialize (if>0 (a,I,J))) by COMPOS_1:141;
then A11: IC ((Initialized ss) +* (Initialize (if>0 (a,I,J)))) = IC (Initialize (if>0 (a,I,J))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
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 A12: 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 A13: Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= if>0 (a,I,J) by A12, FUNCT_4:26;
A14: if>0 (a,I,J) c= Initialize (if>0 (a,I,J)) by SCMFSA8A:9;
Initialize (if>0 (a,I,J)) c= (Initialized ss) +* (Initialize (if>0 (a,I,J))) by FUNCT_4:26;
then if>0 (a,I,J) c= (Initialized ss) +* (Initialize (if>0 (a,I,J))) by A14, XBOOLE_1:1;
then Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= (Initialized ss) +* (Initialize (if>0 (a,I,J))) by A13, XBOOLE_1:1;
then Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2) by AMI_1:81;
then A15: Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2) ;
A16: Reloc ((Directed J),2) c= Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) by COMPOS_1:156, SCMFSA6A:55;
then A17: Reloc ((Directed J),2) c= Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2) by A15, XBOOLE_1:1;
Reloc ((Directed J),2) c= if>0 (a,I,J) by A13, A16, XBOOLE_1:1;
then A18: Reloc ((Directed J),2) c= P +* (if>0 (a,I,J)) by XBOOLE_1:1, A2;
A19: (P +* (if>0 (a,I,J))) /. (IC ((Initialized ss) +* (Initialize (if>0 (a,I,J))))) = (P +* (if>0 (a,I,J))) . (IC ((Initialized ss) +* (Initialize (if>0 (a,I,J))))) by PBOOLE:158;
A20: Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(0 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),0))) by EXTPRO_1:4
.= Following ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J))))) by EXTPRO_1:3
.= Exec ((a >0_goto ((card J) + 3)),((Initialized ss) +* (Initialize (if>0 (a,I,J))))) by A11, A8, A19 ;
assume Directed J is_pseudo-closed_on ss,P ; :: thesis: DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
then A21: Directed J is_pseudo-closed_on Initialized ss,P by A4, Th53;
then J ';' (Stop SCM+FSA) is_halting_on Initialized ss,P by Th58;
then A22: P +* (J ';' (Stop SCM+FSA)) halts_on (Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA))) by SCMFSA7B:def 8, A5;
DataPart (Initialized ss) = DataPart ((Initialized ss) +* (Initialize (Directed J))) by SCMFSA8A:11;
then A23: Directed J is_pseudo-closed_on (Initialized ss) +* (Initialize (Directed J)),P +* (Directed J) by A21, Th52;
(Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA))) = (Initialized (Initialized ss)) +* (Initialize (J ';' (Stop SCM+FSA))) by SCMFSA8A:13;
then A24: (Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA))) = (Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA))) by Th15;
A25: Directed (Directed J) = Directed J by SCMFSA6A:63;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:15
.= ((card J) + 2) + ((card I) + 2) ;
then ((card J) + 2) + 0 < card (if>0 (a,I,J)) by XREAL_1:10;
then A26: (card J) + 2 in dom (if>0 (a,I,J)) by AFINSQ_1:70;
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 A27: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:70;
set s9 = Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2));
A28: Initialize (Directed J) c= (Initialized ss) +* (Initialize (Directed J)) by FUNCT_4:26;
LifeSpan ((P +* (J ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA))))) = pseudo-LifeSpan ((Initialized ss),P,(Directed J)) by A21, Th58;
then A29: DataPart (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),(pseudo-LifeSpan ((Initialized ss),P,(Directed J))))) = DataPart (Comput ((P +* (J ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (J ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA)))))))) by A21, A25, A10, Th58;
A30: 1 in dom (if>0 (a,I,J)) by Th54;
((Initialized ss) +* (Initialize (if>0 (a,I,J)))) . a = (Initialized ss) . a by Th28
.= (Initialized (Initialized ss)) . a by SCMFSA6C:3 ;
then A31: IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1)) = succ (IC ((Initialized ss) +* (Initialize (if>0 (a,I,J))))) by A6, A20, SCMFSA_2:97
.= 0 + 1 by A11 ;
A32: (P +* (if>0 (a,I,J))) . 1 = (if>0 (a,I,J)) . 1 by A30, FUNCT_4:14
.= (if>0 (a,I,J)) . 1
.= goto 2 by Th55 ;
A33: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1))) by PBOOLE:158;
A34: Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(1 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1))) by A31, A32, A33 ;
then A35: IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)) = 2 by SCMFSA_2:95;
A36: DataPart ((Initialized ss) +* (Initialize (Directed J))) = DataPart ((Initialized ss) +* (Initialize (if>0 (a,I,J)))) by COMPOS_1:138, SCMFSA8A:14;

A37: now

let f be FinSeq-Location ; :: thesis: ((Initialized ss) +* (Initialize (Directed J))) . f = (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)) . f
thus ((Initialized ss) +* (Initialize (Directed J))) . f = ((Initialized ss) +* (Initialize (if>0 (a,I,J)))) . f by A36, SCMFSA6A:38
.= (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1)) . f by A20, SCMFSA_2:97
.= (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)) . f by A34, SCMFSA_2:95 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: ((Initialized ss) +* (Initialize (Directed J))) . a = (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)) . a
thus ((Initialized ss) +* (Initialize (Directed J))) . a = ((Initialized ss) +* (Initialize (if>0 (a,I,J)))) . a by A36, SCMFSA6A:38
.= (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),1)) . a by A20, SCMFSA_2:97
.= (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)) . a by A34, SCMFSA_2:95 ; :: thesis: verum

end;

then A38: DataPart ((Initialized ss) +* (Initialize (Directed J))) = DataPart (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)) by A37, SCMFSA6A:38;
A39: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2)))) by PBOOLE:158;
A40: IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))))) by EXTPRO_1:5
.= (IC (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J)))))) + 2 by A28, A23, A17, A35, A38, Th51, A3, A18
.= (IC (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),(pseudo-LifeSpan ((Initialized ss),P,(Directed J)))))) + 2 by A21, Th50
.= (card (Directed J)) + 2 by A21, SCMFSA8A:def 5, A1
.= (card J) + 2 by SCMFSA8A:34 ;
then A41: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . ((card J) + 2) by A39
.= (if>0 (a,I,J)) . ((card J) + 2) by A26, GRFUNC_1:8, A2
.= goto (((card I) + (card J)) + 3) by Th64 ;
A42: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2) + 1)))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2) + 1)))) by PBOOLE:158;
IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2) + 1))) = IC (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))))) by EXTPRO_1:4
.= ((card I) + (card J)) + 3 by A41, SCMFSA_2:95 ;
then A43: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2) + 1)))) = (P +* (if>0 (a,I,J))) . (((card I) + (card J)) + 3) by A42
.= (if>0 (a,I,J)) . (((card I) + (card J)) + 3) by A27, GRFUNC_1:8, A2
.= halt SCM+FSA by Th62 ;
then A44: P +* (if>0 (a,I,J)) halts_on (Initialized ss) +* (Initialize (if>0 (a,I,J))) by EXTPRO_1:30;
A45: (P +* (if>0 (a,I,J))) /. (IC ((Initialized ss) +* (Initialize (if>0 (a,I,J))))) = (P +* (if>0 (a,I,J))) . (IC ((Initialized ss) +* (Initialize (if>0 (a,I,J))))) by PBOOLE:158;
A46: CurInstr ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J))))) = a >0_goto ((card J) + 3) by A11, A8, A45;

now

A47: 0 + 2 < ((card I) + (card J)) + 3 by XREAL_1:10;
then A48: 2 in dom (if>0 (a,I,J)) by Th57;
A49: (if>0 (a,I,J)) . 2 <> halt SCM+FSA by A47, Th57;
A50: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2))) by PBOOLE:158;
A51: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2))) = (P +* (if>0 (a,I,J))) . 2 by A35, A50
.= (if>0 (a,I,J)) . 2 by A48, GRFUNC_1:8, A2 ;
let k be Element of NAT ; :: thesis: ( CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) = halt SCM+FSA implies (pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k )
assume A52: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k
A53: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) by PBOOLE:158;
A54: Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),0) = (Initialized ss) +* (Initialize (if>0 (a,I,J))) by EXTPRO_1:3;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),0))) = a >0_goto ((card J) + 3) by A46, A54;
then A55: k <> 0 by A52;
A56: k <> 1 by A31, A32, A52, A53;
2 <> k by A52, A49, A51;
then 2 < k by A55, A56, NAT_1:27;
then consider k2 being Nat such that
A57: 2 + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),k2)) as Element of NAT ;
assume not (pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k ; :: thesis: contradiction
then k < ((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 1) + 2 ;
then k2 < (pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 1 by A57, XREAL_1:8;
then A58: k2 <= pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J)) by NAT_1:13;
then A59: k2 <= pseudo-LifeSpan ((Initialized ss),P,(Directed J)) by A21, Th50;

A60: now

per cases ( k2 = pseudo-LifeSpan ((Initialized ss),P,(Directed J)) or k2 < pseudo-LifeSpan ((Initialized ss),P,(Directed J)) ) by A59, XXREAL_0:1;

suppose A61: k2 = pseudo-LifeSpan ((Initialized ss),P,(Directed J)) ; :: thesis: n + 2 < ((card I) + (card J)) + 3

((card I) + (card J)) + (2 + 1) = (((card J) + 2) + 1) + (card I) ;
then A62: ((card J) + 2) + 1 <= ((card I) + (card J)) + 3 by NAT_1:11;
IC (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),k2)) = card (Directed J) by A21, A61, SCMFSA8A:def 5, A1;
then n = card J by SCMFSA8A:34;
hence n + 2 < ((card I) + (card J)) + 3 by A62, NAT_1:13; :: thesis: verum

end;

suppose k2 < pseudo-LifeSpan ((Initialized ss),P,(Directed J)) ; :: thesis: n + 2 < ((card I) + (card J)) + 3

then n in dom (Directed J) by A21, SCMFSA8A:31, A1;
then n < card (Directed J) by AFINSQ_1:70;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:8;
then A63: 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 A63, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then A64: n + 2 in dom (if>0 (a,I,J)) by Th57;
A65: IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k)) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)),k2)) by A57, EXTPRO_1:5
.= n + 2 by A28, A23, A17, A35, A38, A58, Th51, A3, A18 ;
A66: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) by PBOOLE:158;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) by A66
.= (if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),k))) by A65, A64, GRFUNC_1:8, A2 ;
hence contradiction by A52, A65, A60, Th57; :: thesis: verum

end;

then A67: LifeSpan ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J))))) = ((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2) + 1 by A43, A44, EXTPRO_1:def 14;
A68: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2)))) by PBOOLE:158;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . ((card J) + 2) by A40, A68
.= (if>0 (a,I,J)) . ((card J) + 2) by A26, A2, GRFUNC_1:8
.= goto (((card I) + (card J)) + 3) by Th64 ;
then InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))))) = 6 by SCMFSA_2:47;
then InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))))) in {0,6,7,8} by ENUMSET1:def 2;
then A69: DataPart (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))) = DataPart (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))))) by Th32;
A70: DataPart (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),2)),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))))) by EXTPRO_1:5
.= DataPart (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),(pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))))) by A28, A23, A17, A35, A38, Th51, A3, A18 ;
thus DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((if>0 (a,I,J)),P,(Initialized ss))) by Th17
.= DataPart ((Result ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialized (if>0 (a,I,J)))))) +* ((Initialized ss) | NAT))
.= DataPart (Result ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))))) by A9, COMPOS_1:82
.= DataPart (Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),(LifeSpan ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))))))) by A44, EXTPRO_1:23
.= DataPart (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),((Initialized ss) +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan (((Initialized ss) +* (Initialize (Directed J))),(P +* (Directed J)),(Directed J))) + 2))))) by A67, EXTPRO_1:4
.= DataPart (Comput ((P +* (Directed J)),((Initialized ss) +* (Initialize (Directed J))),(pseudo-LifeSpan ((Initialized ss),P,(Directed J))))) by A21, A70, A69, Th50
.= DataPart (Result ((P +* (J ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialize (J ';' (Stop SCM+FSA)))))) by A22, A29, EXTPRO_1:23
.= DataPart ((Result ((P +* (J ';' (Stop SCM+FSA))),((Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA)))))) +* ((Initialized ss) | NAT)) by A24, COMPOS_1:82
.= DataPart (IExec ((J ';' (Stop SCM+FSA)),P,(Initialized ss)))
.= DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) by Th17 ; :: thesis: verum