let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I, J being MacroInstruction 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 & 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; for I, J being MacroInstruction 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 & 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 MacroInstruction 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 & 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; ( s . a > 0 & Directed I is_pseudo-closed_on s,P implies ( if>0 (a,I,J) is_halting_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 AFINSQ_1:65;
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 Th18
;
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;
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, SCMFSA6A:38;
then A11:
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 A12:
Reloc ((Directed I),((card J) + 3)) c= P +* (if>0 (a,I,J))
by A11, XBOOLE_1:1;
A13:
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 A14:
DataPart (Initialize s) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1))
by A13, SCMFSA_M:2;
A15:
a <> IC
by SCMFSA_2:56;
not a in dom (Start-At (0,SCM+FSA))
by A15, TARSKI:def 1;
then
not a in dom (Start-At (0,SCM+FSA))
;
then A16:
(Initialize s) . a = s . a
by FUNCT_4:11;
assume
s . a > 0
; ( not Directed I is_pseudo-closed_on s,P or ( if>0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 ) )
then A17:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),1)) = (card J) + 3
by A9, A16, SCMFSA_2:71;
assume A18:
Directed I is_pseudo-closed_on s,P
; ( if>0 (a,I,J) is_halting_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1 )
then A19:
pseudo-LifeSpan (s,P,(Directed I)) = LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))
by Th21;
A20:
Directed I is_pseudo-closed_on Initialize s,P +* (Directed I)
by A18;
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 A20, A12, A17, A14, Th14, A1
.=
(IC (Comput ((P +* (Directed I)),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))) + ((card J) + 3)
by A18, Th13
.=
(card (Directed I)) + ((card J) + 3)
by A18, SCMFSA8A:def 4
.=
(card I) + ((card J) + 3)
by SCMFSA6A:36
.=
((card I) + (card J)) + 3
;
then A21: 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 Th25
;
then A22:
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
; LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1
now for k being 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 <= kset J1 =
(((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I;
let k be
Nat;
( 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 A23:
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)))
= halt SCM+FSA
;
(pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1 <= kassume
not
(pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1
<= k
;
contradictionthen A24:
k <= pseudo-LifeSpan (
(Initialize s),
(P +* (Directed I)),
(Directed I))
by NAT_1:13;
A25:
0 in dom (if>0 (a,I,J))
by AFINSQ_1:65;
A26:
(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 A26, MEMSTR_0:16
.=
(if>0 (a,I,J)) . 0
by A25, A2, GRFUNC_1:2
.=
a >0_goto ((card J) + 3)
by Th18
;
then consider k1 being
Nat such that A27:
k1 + 1
= k
by A23, 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 A27, XREAL_1:29;
then A28:
k1 < pseudo-LifeSpan (
(Initialize s),
(P +* (Directed I)),
(Directed I))
by A24, XXREAL_0:2;
then
k1 < pseudo-LifeSpan (
s,
P,
(Directed I))
by A18, Th13;
then
n in dom (Directed I)
by A18, 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 A29:
n + ((card J) + 3) < (card I) + ((card J) + 3)
by SCMFSA6A:36;
A30:
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 A20, A12, A17, A14, A28, Th14, 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 A30, A29, AFINSQ_1:66;
then A31:
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 A32:
(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 A29, XXREAL_0:2;
then A33:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize s),k)) in dom (if>0 (a,I,J))
by A30, AFINSQ_1:66;
A34:
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 A33, A2, GRFUNC_1:2
;
Directed ((((a >0_goto ((card J) + 3)) ";" J) ";" (Goto ((card I) + 1))) ";" I) c= if>0 (
a,
I,
J)
by 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 A31, GRFUNC_1:2;
hence
contradiction
by A23, A32, A34, COMPOS_1:def 11;
verum end;
then
LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (pseudo-LifeSpan ((Initialize s),(P +* (Directed I)),(Directed I))) + 1
by A21, A22, EXTPRO_1:def 15;
hence
LifeSpan ((P +* (if>0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) + 1
by A18, A19, Th13; verum