let P be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
set D = Data-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 = Initialize s;
set P00 = P +* (Directed J);
set s3 = Initialize s;
set P3 = P +* (if>0 (a,I,J));
A2: if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:25;
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialize s),1);
set s5 = Comput ((P +* (if>0 (a,I,J))),(Initialize s),2);
set i = a >0_goto ((card J) + 3);
A3: Directed J c= P +* (Directed J) by FUNCT_4:25;
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:25;
then if>0 (a,I,J) = ((Macro (a >0_goto ((card J) + 3))) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))) by SCMFSA6A:25;
then A6: if>0 (a,I,J) = (Macro (a >0_goto ((card J) + 3))) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))) by SCMFSA6A:25;
card (Macro (a >0_goto ((card J) + 3))) = 2 by COMPOS_1:56;
then A7: Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= if>0 (a,I,J) by A6, FUNCT_4:25;
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:13
.= a >0_goto ((card J) + 3) by Th55 ;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:12
.= ((card J) + 2) + ((card I) + 2) ;
then A10: ((card J) + 2) + 0 < card (if>0 (a,I,J)) by XREAL_1:8;
then A11: (card J) + 2 in dom (if>0 (a,I,J)) by AFINSQ_1:66;
X1: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A12: IC (Initialize s) = IC (Initialize s)
.= IC (Start-At (0,SCM+FSA)) by X1, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
set ss = Comput ((P +* (if>0 (a,I,J))),(Initialize s),((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2));
set PP = P +* (if>0 (a,I,J));
if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:25;
then A14: Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= P +* (if>0 (a,I,J)) by A7, XBOOLE_1:1;
Reloc ((Directed J),2) c= Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) by COMPOS_1:44, SCMFSA6A:16;
then A16: Reloc ((Directed J),2) c= P +* (if>0 (a,I,J)) by A14, XBOOLE_1:1;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:12
.= (((card I) + (card J)) + 3) + 1 ;
then ((card I) + (card J)) + 3 < card (if>0 (a,I,J)) by NAT_1:13;
then A18: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:66;
assume s . a <= 0 ; :: thesis:
then A19: (Initialized s) . a <= 0 by SCMFSA6C:3;
A20: 1 in dom (if>0 (a,I,J)) by Th54;
assume A21: Directed J is_pseudo-closed_on s,P ; :: thesis:
then A22: pseudo-LifeSpan (s,P,(Directed J)) = LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(Initialize s)) by Th58;
A23: (P +* (if>0 (a,I,J))) . 1 = (if>0 (a,I,J)) . 1 by A20, FUNCT_4:13
.= goto 2 by Th55 ;
DataPart s = DataPart (Initialize s) by MEMSTR_0:79;
then A24: Directed J is_pseudo-closed_on Initialize s,P +* (Directed J) by A21, Th52;
A26: Comput ((P +* (if>0 (a,I,J))),(Initialize s),(0 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),0))) by EXTPRO_1:3
.= Following ((P +* (if>0 (a,I,J))),(Initialize s)) by EXTPRO_1:2
.= Exec ((a >0_goto ((card J) + 3)),(Initialize s)) by A12, A9, PBOOLE:143 ;
X2: a <> IC by SCMFSA_2:56;
dom (Start-At (0,SCM+FSA)) = {(IC )} by FUNCOP_1:13;
then not a in dom (Start-At (0,SCM+FSA)) by X2, TARSKI:def 1;
then not a in dom (Start-At (0,SCM+FSA)) ;
then (Initialize s) . a = s . a by FUNCT_4:11
.= (Initialized s) . a by SCMFSA6C:3 ;
then A27: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) = succ (IC (Initialize s)) by A19, A26, SCMFSA_2:71
.= 0 + 1 by A12 ;
A29: Comput ((P +* (if>0 (a,I,J))),(Initialize s),(1 + 1)) = Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),1))) by A27, A23, PBOOLE:143 ;
then A30: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)) = 2 by SCMFSA_2:69;

A32: now

let f be FinSeq-Location ; :: thesis:
thus (Initialize s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) . f by A26, SCMFSA_2:71
.= (Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)) . f by A29, SCMFSA_2:69 ; :: thesis:

end;

now

let a be Int-Location ; :: thesis:
thus (Initialize s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) . a by A26, SCMFSA_2:71
.= (Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)) . a by A29, SCMFSA_2:69 ; :: thesis:

end;

then A33: DataPart (Initialize s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)) by A32, SCMFSA6A:7;
A35: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2))) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)),(pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))))) by EXTPRO_1:4
.= (IC (Comput ((P +* (Directed J)),(Initialize s),(pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J)))))) + 2 by A24, A16, A30, A33, Th51, A3
.= (IC (Comput ((P +* (Directed J)),(Initialize s),(pseudo-LifeSpan (s,P,(Directed J)))))) + 2 by A21, Th50
.= (card (Directed J)) + 2 by A21, SCMFSA8A:def 4
.= (card J) + 2 by SCMFSA8A:20 ;
then A36: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2)))) = (P +* (if>0 (a,I,J))) . ((card J) + 2) by PBOOLE:143
.= (if>0 (a,I,J)) . ((card J) + 2) by A11, A2, GRFUNC_1:2
.= goto (((card I) + (card J)) + 3) by Th64 ;
A38: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),(((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2) + 1))) = IC (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2))))) by EXTPRO_1:3
.= ((card I) + (card J)) + 3 by A36, SCMFSA_2:69 ;
then A39: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),(((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2) + 1)))) = (P +* (if>0 (a,I,J))) . (((card I) + (card J)) + 3) by PBOOLE:143
.= (if>0 (a,I,J)) . (((card I) + (card J)) + 3) by A18, A2, GRFUNC_1:2
.= halt SCM+FSA by Th62 ;
then A40: P +* (if>0 (a,I,J)) halts_on Initialize s by EXTPRO_1:29;
hence if>0 (a,I,J) is_halting_on s,P by SCMFSA7B:def 7; :: thesis:

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

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

end;

suppose ( 0 < k & k = 1 ) ; :: thesis:

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

end;

suppose A41: ( 0 < k & k <> 1 & k < (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2 ) ; :: thesis:

then 0 + 1 <= k by INT_1:7;
then 1 < k by A41, XXREAL_0:1;
then 0 + (1 + 1) <= k by INT_1:7;
then consider k2 being Nat such that
A42: 2 + k2 = k by NAT_1:10;
card (if>0 (a,I,J)) = ((card I) + (card J)) + (2 + 2) by SCMFSA8B:12
.= ((card J) + 2) + ((card I) + 2) ;
then A43: (card J) + 2 <= card (if>0 (a,I,J)) by NAT_1:12;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;
reconsider n = IC (Comput ((P +* (Directed J)),(Initialize s),k2)) as Element of NAT ;
A44: k2 < pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J)) by A41, A42, XREAL_1:6;
then k2 < pseudo-LifeSpan (s,P,(Directed J)) by A21, Th50;
then n in dom (Directed J) by A21, SCMFSA8A:17;
then n < card (Directed J) by AFINSQ_1:66;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:6;
then n + 2 < (card J) + 2 by SCMFSA8A:20;
then A45: n + 2 < card (if>0 (a,I,J)) by A43, XXREAL_0:2;
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)),k2)) by A42, EXTPRO_1:4
.= (IC (Comput ((P +* (Directed J)),(Initialize s),k2))) + 2 by A24, A16, A30, A33, A44, Th51, A3 ;
hence IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J)) by A45, AFINSQ_1:66; :: thesis:

end;

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

hereby :: thesis:

per cases ) + 2 = k or (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2 < k ) by A46, XXREAL_0:1;

suppose (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2 = k ; :: thesis:

hence IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J)) by A10, A35, AFINSQ_1:66; :: thesis:

end;

suppose (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2 < k ; :: thesis:

then ((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 2) + 1 <= k by INT_1:7;
hence IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J)) by A18, A38, A39, EXTPRO_1:5; :: thesis:

end;

end;

end;

end;

end;

end;

hence if>0 (a,I,J) is_closed_on s,P by SCMFSA7B:def 6; :: thesis:
A48: CurInstr ((P +* (if>0 (a,I,J))),(Initialize s)) = a >0_goto ((card J) + 3) by A12, A9, PBOOLE:143;

now

A49: 0 + 2 < ((card I) + (card J)) + 3 by XREAL_1:8;
then A50: 2 in dom (if>0 (a,I,J)) by Th57;
A53: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),2))) = (P +* (if>0 (a,I,J))) . 2 by A30, PBOOLE:143
.= (if>0 (a,I,J)) . 2 by A50, A2, GRFUNC_1:2 ;
let k be Element of NAT ; :: thesis:
assume A54: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) = halt SCM+FSA ; :: thesis:
A57: k <> 0 by A54, A48, EXTPRO_1:2;
A58: k <> 1 by A27, A54, A23, PBOOLE:143;
2 <> k by A54, A49, Th57, A53;
then 2 < k by A57, A58, NAT_1:26;
then consider k2 being Nat such that
A59: 2 + k2 = k by NAT_1:10;
reconsider k2 = k2 as Element of NAT by ORDINAL1:def 12;
reconsider n = IC (Comput ((P +* (Directed J)),(Initialize s),k2)) as Element of NAT ;
assume not (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k ; :: thesis:
then k < ((pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 1) + 2 ;
then k2 < (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 1 by A59, XREAL_1:6;
then A60: k2 <= pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J)) by NAT_1:13;
then A61: k2 <= pseudo-LifeSpan (s,P,(Directed J)) by A21, Th50;

A62: now

per cases by A61, XXREAL_0:1;

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

((card I) + (card J)) + (2 + 1) = (((card J) + 2) + 1) + (card I) ;
then A64: ((card J) + 2) + 1 <= ((card I) + (card J)) + 3 by NAT_1:11;
IC (Comput ((P +* (Directed J)),(Initialize s),k2)) = card (Directed J) by A21, A63, SCMFSA8A:def 4;
then n = card J by SCMFSA8A:20;
hence n + 2 < ((card I) + (card J)) + 3 by A64, NAT_1:13; :: thesis:

end;

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

then n in dom (Directed J) by A21, SCMFSA8A:17;
then n < card (Directed J) by AFINSQ_1:66;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:6;
then A65: n + 2 < (card J) + 2 by SCMFSA8A:20;
((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 A65, XXREAL_0:2; :: thesis:

end;

end;

end;

then A66: n + 2 in dom (if>0 (a,I,J)) by Th57;
A67: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),2)),k2)) by A59, EXTPRO_1:4
.= n + 2 by A24, A16, A30, A33, A60, Th51, A3 ;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) = (P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) by PBOOLE:143
.= (if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) by A67, A66, A2, GRFUNC_1:2 ;
hence contradiction by A54, A67, A62, Th57; :: thesis:

end;

then LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 3 by A39, A40, EXTPRO_1:def 15;
hence LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Start-At (0,SCM+FSA)))) = (LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(Initialize s))) + 3 by A21, A22, Th50; :: thesis: