let P be Instruction-Sequence of SCM+FSA; :: 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 . a > 0 & Directed I is_pseudo-closed_on s,P holds
( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
let s be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & Directed I is_pseudo-closed_on s,P holds
( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
set D = Data-Locations ;
let I, J be Program of SCM+FSA; :: thesis: for a being read-write Int-Location st s . a > 0 & Directed I is_pseudo-closed_on s,P holds
( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
let a be read-write Int-Location; :: thesis: ( s . a > 0 & Directed I is_pseudo-closed_on s,P implies ( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 ) )
set I0 = Directed I;
set I1 = I ";" (Stop SCM+FSA);
set s00 = Initialize s;
set P00 = P +* (Directed I);
set s3 = Initialize s;
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialize s),1);
set i = a >0_goto ((card J) + 3);
A1: Directed I c= P +* (Directed I) by FUNCT_4:25;
A2: if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:25;
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 A3: ((card I) + (card J)) + 3 in dom (if>0 (a,I,J)) by AFINSQ_1:66;
A4: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A5: IC (Initialize s) = IC (Initialize s)
.= IC (Start-At (0,SCM+FSA)) by A4, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A6: 0 in dom (if>0 (a,I,J)) by Th25;
A7: (P +* (if>0 (a,I,J))) . 0 = (if>0 (a,I,J)) . 0 by A6, FUNCT_4:13
.= a >0_goto ((card J) + 3) by Th26 ;
A8: 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:21
.= (card ((Macro (a >0_goto ((card J) + 3))) ";" J)) + 1 by SCMFSA8A:15
.= ((card (Macro (a >0_goto ((card J) + 3)))) + (card J)) + 1 by SCMFSA6A:21
.= ((card J) + 2) + 1 by COMPOS_1:56
.= (card J) + (2 + 1) ;
A9: 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))
.= Exec ((a >0_goto ((card J) + 3)),(Initialize s)) by A5, A7, PBOOLE:143 ;
A10: if>0 (a,I,J) c= P +* (if>0 (a,I,J)) by FUNCT_4:25;
A11: 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:25;
then Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= if>0 (a,I,J) by A8, FUNCT_4:25;
then A12: Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) c= P +* (if>0 (a,I,J)) by A10, XBOOLE_1:1;
Reloc ((Directed I),((card J) + 3)) c= Reloc ((I ";" (Stop SCM+FSA)),((card J) + 3)) by COMPOS_1:44, SCMFSA6A:16;
then A13: Reloc ((Directed I),((card J) + 3)) c= P +* (if>0 (a,I,J)) by A12, XBOOLE_1:1;
A14: for f being FinSeq-Location holds (Initialize s) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) . f by A9, SCMFSA_2:71;
for a being Int-Location holds (Initialize s) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) . a by A9, SCMFSA_2:71;
then A15: DataPart (Initialize s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) by A14, SCMFSA_M:2;
A16: 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 A16, TARSKI:def 1;
then not a in dom (Start-At (0,SCM+FSA)) ;
then A17: (Initialize s) . a = s . a by FUNCT_4:11;
assume s . a > 0 ; :: thesis: ( not Directed I is_pseudo-closed_on s,P or ( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 ) )
then A18: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) = (card J) + 3 by A9, A17, SCMFSA_2:71;
assume A19: Directed I is_pseudo-closed_on s,P ; :: thesis: ( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
then A20: pseudo-LifeSpan (s,P,(Directed I)) = LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) by Th29;
DataPart s = DataPart (Initialize s) by MEMSTR_0:79;
then A21: Directed I is_pseudo-closed_on Initialize s,P +* (Directed I) by A19, Th23;
A22: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),((pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1))) = IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)),(pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))))) by EXTPRO_1:4
.= (IC (Comput ((P +* (Directed I)),(Initialize s),(pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)))))) + ((card J) + 3) by A21, A13, A18, A15, Th22, A1
.= (IC (Comput ((P +* (Directed I)),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))) + ((card J) + 3) by A19, Th21
.= (card (Directed I)) + ((card J) + 3) by A19, SCMFSA8A:def 4
.= (card I) + ((card J) + 3) by SCMFSA8A:20
.= ((card I) + (card J)) + 3 ;
then A23: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),((pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 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 A3, A2, GRFUNC_1:2
.= halt SCM+FSA by Th33 ;
then A24: 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: ( if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )

now :: thesis: for k being Element of NAT holds IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J))

let k be Element of NAT ; :: thesis: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),b₁)) in dom (if>0 (a,I,J))

per cases ( k = 0 or ( 0 < k & k < (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 ) or ( 0 < k & (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= k ) ) ;

suppose k = 0 ; :: thesis: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),b₁)) in dom (if>0 (a,I,J))

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 Th25; :: thesis: verum

end;

suppose A25: ( 0 < k & k < (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 ) ; :: thesis: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),b₁)) in dom (if>0 (a,I,J))

card (if>0 (a,I,J)) = ((card I) + (card J)) + (3 + 1) by SCMFSA8B:12
.= (((card I) + (card J)) + 3) + 1 ;
then A26: ((card I) + (card J)) + 3 < card (if>0 (a,I,J)) by XREAL_1:29;
0 + 1 <= k by A25, INT_1:7;
then consider k1 being Nat such that
A27: 1 + k1 = k by NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
reconsider n = IC (Comput ((P +* (Directed I)),(Initialize s),k1)) as Element of NAT ;
A28: k1 < pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) by A25, A27, XREAL_1:6;
then k1 < pseudo-LifeSpan (s,P,(Directed I)) by A19, Th21;
then n in dom (Directed I) by A19, SCMFSA8A:17;
then n < card (Directed I) by AFINSQ_1:66;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:6;
then n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:20;
then A29: n + ((card J) + 3) < card (if>0 (a,I,J)) by A26, 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),1)),k1)) by A27, EXTPRO_1:4
.= (IC (Comput ((P +* (Directed I)),(Initialize s),k1))) + ((card J) + 3) by A21, A13, A18, A15, A28, Th22, A1 ;
hence IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J)) by A29, AFINSQ_1:66; :: thesis: verum

end;

suppose ( 0 < k & (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= k ) ; :: thesis: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),b₁)) in dom (if>0 (a,I,J))

hence IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J)) by A3, A22, A23, EXTPRO_1:5; :: thesis: verum

end;

end;

end;

hence if>0 (a,I,J) is_closed_on s,P by SCMFSA7B:def 6; :: thesis: LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1

now :: thesis: for k being Element of NAT st CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) = halt SCM+FSA holds
(pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= k

set J1 = (((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I;
let k be Element of NAT ; :: thesis: ( CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) = halt SCM+FSA implies (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= k )
assume A30: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= k
assume not (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= k ; :: thesis: contradiction
then A31: k <= pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) by NAT_1:13;
A32: 0 in dom (if>0 (a,I,J)) by Th25;
A33: (P +* (if>0 (a,I,J))) /. (IC (Initialize s)) = (P +* (if>0 (a,I,J))) . (IC (Initialize s)) by PBOOLE:143;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize s),0))) = (P +* (if>0 (a,I,J))) . 0 by A33, MEMSTR_0:16
.= (if>0 (a,I,J)) . 0 by A32, A2, GRFUNC_1:2
.= a >0_goto ((card J) + 3) by Th26 ;
then consider k1 being Nat such that
A34: k1 + 1 = k by A30, NAT_1:6;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
reconsider n = IC (Comput ((P +* (Directed I)),(Initialize s),k1)) as Element of NAT ;
k1 < k by A34, XREAL_1:29;
then A35: k1 < pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I)) by A31, XXREAL_0:2;
then k1 < pseudo-LifeSpan (s,P,(Directed I)) by A19, Th21;
then n in dom (Directed I) by A19, SCMFSA8A:17;
then n < card (Directed I) by AFINSQ_1:66;
then n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3) by XREAL_1:6;
then A36: n + ((card J) + 3) < (card I) + ((card J) + 3) by SCMFSA8A:20;
A37: 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),1)),k1)) by A34, EXTPRO_1:4
.= (IC (Comput ((P +* (Directed I)),(Initialize s),k1))) + ((card J) + 3) by A21, A13, A18, A15, A35, Th22, A1 ;
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:21
.= ((card ((Macro (a >0_goto ((card J) + 3))) ";" J)) + (card (Goto ((card I) + 1)))) + (card I) by SCMFSA6A:21
.= ((card ((Macro (a >0_goto ((card J) + 3))) ";" J)) + 1) + (card I) by SCMFSA8A:15
.= (((card (Macro (a >0_goto ((card J) + 3)))) + (card J)) + 1) + (card I) by SCMFSA6A:21
.= ((2 + (card J)) + 1) + (card I) by COMPOS_1:56
.= ((card I) + (card J)) + 3 ;
then IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) by A37, A36, AFINSQ_1:66;
then A38: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (Directed ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) by FUNCT_4:99;
then A39: (Directed ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) in rng (Directed ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) by FUNCT_1:def 3;
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 XREAL_1:29;
then n + ((card J) + 3) < card (if>0 (a,I,J)) by A36, XXREAL_0:2;
then A40: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J)) by A37, AFINSQ_1:66;
A41: 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 A40, A2, GRFUNC_1:2 ;
Directed ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) c= if>0 (a,I,J) by A11, SCMFSA6A:16;
then (if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) = (Directed ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I)) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k))) by A38, GRFUNC_1:2;
hence contradiction by A30, A39, A41, COMPOS_1:def 11; :: thesis: verum

end;

then LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 by A23, A24, EXTPRO_1:def 15;
hence LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 by A19, A20, Th21; :: thesis: verum