let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCM+FSA; :: thesis:
set D = Data-Locations SCM+FSA;
let I, J be Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
set I0 = Directed I;
A1: ProgramPart (Directed I) = Directed I by RELAT_1:209;
set I1 = I ';' (Stop SCM+FSA);
set s00 = s +* (Initialize (Directed I));
set P00 = P +* (Directed I);
set s3 = s +* (Initialize (if>0 (a,I,J)));
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1);
set i = a >0_goto ((card J) + 3);
A2: Directed I c= P +* (Directed I) by FUNCT_4:26;
A3: ProgramPart (if>0 (a,I,J)) = if>0 (a,I,J) by RELAT_1:209;
A4: Initialize (Directed I) c= s +* (Initialize (Directed I)) by FUNCT_4:26;
A5: if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:26;
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 A6: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:70;
IC in dom (Initialize (if>0 (a,I,J))) by COMPOS_1:141;
then A7: IC (s +* (Initialize (if>0 (a,I,J)))) = IC (Initialize (if>0 (a,I,J))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A8: 0 in dom (if>0 (a,I,J)) by Th54;
A9: (P +* (if>0 (a,I,J))) . 0 = (if>0 (a,I,J)) . 0 by A8, FUNCT_4:14
.= (if>0 (a,I,J)) . 0
.= a >0_goto ((card J) + 3) by Th55 ;
A10: 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) ;
A11: (P +* (if>0 (a,I,J))) /. (IC (s +* (Initialize (if>0 (a,I,J))))) = (P +* (if>0 (a,I,J))) . (IC (s +* (Initialize (if>0 (a,I,J))))) by PBOOLE:158;
A12: Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),(0 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),0))) by EXTPRO_1:4
.= Following ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J))))) by EXTPRO_1:3
.= Exec ((a >0_goto ((card J) + 3)),(s +* (Initialize (if>0 (a,I,J))))) by A7, A9, A11 ;
A13: if>0 (a,I,J) c= Initialize (if>0 (a,I,J)) by SCMFSA8A:9;
Initialize (if>0 (a,I,J)) c= s +* (Initialize (if>0 (a,I,J))) by FUNCT_4:26;
then A14: if>0 (a,I,J) c= s +* (Initialize (if>0 (a,I,J))) by A13, XBOOLE_1:1;
A15: 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 A16: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= if>0 (a,I,J) by A10, FUNCT_4:26;
then Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= s +* (Initialize (if>0 (a,I,J))) by A14, XBOOLE_1:1;
then Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1) by AMI_1:81;
then A17: Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) c= Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1) ;
A18: Reloc ((Directed I),((card J) + 3)) c= Reloc ((I ';' (Stop SCM+FSA)),((card J) + 3)) by COMPOS_1:156, SCMFSA6A:55;
then A19: Reloc ((Directed I),((card J) + 3)) c= Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1) by A17, XBOOLE_1:1;
Reloc ((Directed I),((card J) + 3)) c= if>0 (a,I,J) by A16, A18, XBOOLE_1:1;
then A20: Reloc ((Directed I),((card J) + 3)) c= P +* (if>0 (a,I,J)) by A5, XBOOLE_1:1;
A21: DataPart (s +* (Initialize (Directed I))) = DataPart (s +* (Initialize (if>0 (a,I,J)))) by COMPOS_1:138, SCMFSA8A:14;

A22: now

let f be FinSeq-Location ; :: thesis:
thus (s +* (Initialize (Directed I))) . f = (s +* (Initialize (if>0 (a,I,J)))) . f by A21, SCMFSA6A:38
.= (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) . f by A12, SCMFSA_2:97 ; :: thesis:

end;

now

let a be Int-Location ; :: thesis:
thus (s +* (Initialize (Directed I))) . a = (s +* (Initialize (if>0 (a,I,J)))) . a by A21, SCMFSA6A:38
.= (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) . a by A12, SCMFSA_2:97 ; :: thesis:

end;

then A23: DataPart (s +* (Initialize (Directed I))) = DataPart (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) by A22, SCMFSA6A:38;
not a in dom (Initialize (if>0 (a,I,J))) by SCMFSA6B:12;
then A24: (s +* (Initialize (if>0 (a,I,J)))) . a = s . a by FUNCT_4:12;
assume s . a > 0 ; :: thesis:
then A25: IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)) = (card J) + 3 by A12, A24, SCMFSA_2:97;
assume A26: Directed I is_pseudo-closed_on s,P ; :: thesis:
then A27: pseudo-LifeSpan (s,P,(Directed I)) = LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) by Th58;
DataPart s = DataPart (s +* (Initialize (Directed I))) by SCMFSA8A:11;
then A28: Directed I is_pseudo-closed_on s +* (Initialize (Directed I)),P +* (Directed I) by A26, Th52;
A29: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1)))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1)))) by PBOOLE:158;
A30: IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1))) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)),(pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))))) by EXTPRO_1:5
.= (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)))))) + ((card J) + 3) by A4, A28, A19, A25, A23, Th51, A2, A20
.= (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),(pseudo-LifeSpan (s,P,(Directed I)))))) + ((card J) + 3) by A26, Th50
.= (card (Directed I)) + ((card J) + 3) by A26, SCMFSA8A:def 5, A1
.= (card I) + ((card J) + 3) by SCMFSA8A:34
.= ((card I) + (card J)) + 3 ;
then A31: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),((pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1)))) = (P +* (if>0 (a,I,J))) . (((card I) + (card J)) + 3) by A29
.= (if>0 (a,I,J)) . (((card I) + (card J)) + 3) by A6, GRFUNC_1:8, A5
.= halt SCM+FSA by Th62 ;
then A32: P +* (if>0 (a,I,J)) halts_on s +* (Initialize (if>0 (a,I,J))) by EXTPRO_1:30;
hence if>0 (a,I,J) is_halting_on s,P by SCMFSA7B:def 8, A3; :: thesis:

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

then Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k) = s +* (Initialize (if>0 (a,I,J))) by EXTPRO_1:3;
then IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) = 0 by Th31;
hence IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (if>0 (a,I,J)) by Th54; :: thesis:

end;

suppose A33: ( 0 < k & k < (pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1 ) ; :: thesis:

card (if>0 (a,I,J)) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:15
.= (((card I) + (card J)) + 3) + 1 ;
then A34: ((card I) + (card J)) + 3 < card (if>0 (a,I,J)) by XREAL_1:31;
0 + 1 <= k by A33, INT_1:20;
then consider k1 being Nat such that
A35: 1 + k1 = k by NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k1)) as Element of NAT ;
A36: k1 < pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) by A33, A35, XREAL_1:8;
then k1 < pseudo-LifeSpan (s,P,(Directed I)) by A26, Th50;
then n in dom (Directed I) by A26, SCMFSA8A:31, A1;
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 A37: n + ((card J) + 3) < card (if>0 (a,I,J)) by A34, XXREAL_0:2;
IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)),k1)) by A35, EXTPRO_1:5
.= (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k1))) + ((card J) + 3) by A4, A28, A19, A25, A23, A36, Th51, A2, A20 ;
hence IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (if>0 (a,I,J)) by A37, AFINSQ_1:70; :: thesis:

end;

suppose ( 0 < k & (pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1 <= k ) ; :: thesis:

hence IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (if>0 (a,I,J)) by A6, A30, A31, EXTPRO_1:6; :: thesis:

end;

hence if>0 (a,I,J) is_closed_on s,P by SCMFSA7B:def 7, A3; :: thesis:

now

set J1 = (((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I;
let k be Element of NAT ; :: thesis:
assume A38: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) = halt SCM+FSA ; :: thesis:
assume not (pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1 <= k ; :: thesis:
then A39: k <= pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) by NAT_1:13;
A40: 0 in dom (if>0 (a,I,J)) by Th54;
A41: Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),0) = s +* (Initialize (if>0 (a,I,J))) by EXTPRO_1:3;
A42: (P +* (if>0 (a,I,J))) /. (IC (s +* (Initialize (if>0 (a,I,J))))) = (P +* (if>0 (a,I,J))) . (IC (s +* (Initialize (if>0 (a,I,J))))) by PBOOLE:158;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),0))) = (P +* (if>0 (a,I,J))) . 0 by Th31, A42, A41
.= (if>0 (a,I,J)) . 0 by A40, A5, GRFUNC_1:8
.= a >0_goto ((card J) + 3) by Th55 ;
then k <> 0 by A38;
then consider k1 being Nat such that
A43: k1 + 1 = k by NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 13;
reconsider n = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k1)) as Element of NAT ;
k1 < k by A43, XREAL_1:31;
then A44: k1 < pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I)) by A39, XXREAL_0:2;
then k1 < pseudo-LifeSpan (s,P,(Directed I)) by A26, Th50;
then n in dom (Directed I) by A26, SCMFSA8A:31, A1;
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 A45: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:34;
A46: IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),1)),k1)) by A43, EXTPRO_1:5
.= (IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k1))) + ((card J) + 3) by A4, A28, A19, A25, A23, A44, Th51, A2, A20 ;
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 ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) by A46, A45, AFINSQ_1:70;
then A47: IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) by FUNCT_4:105;
then A48: (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),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 A45, XXREAL_0:2;
then A49: IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k)) in dom (if>0 (a,I,J)) by A46, AFINSQ_1:70;
A50: (P +* (if>0 (a,I,J))) /. (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) by PBOOLE:158;
A51: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) by A50
.= (if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) by A49, GRFUNC_1:8, A5 ;
Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) c= if>0 (a,I,J) by A15, SCMFSA6A:55;
then (if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) = (Directed ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I)) . (IC (Comput ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J)))),k))) by A47, GRFUNC_1:8;
hence contradiction by A38, A48, A51, COMPOS_1:def 7; :: thesis:

end;

then LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J))))) = (pseudo-LifeSpan ((s +* (Initialize (Directed I))),(P +* (Directed I)),(Directed I))) + 1 by A31, A32, EXTPRO_1:def 14;
hence LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J))))) = (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) + 1 by A26, A27, Th50; :: thesis: