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 J 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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )
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 J 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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )
set D = Data-Locations ;
let I, J be MacroInstruction of SCM+FSA ; for a being read-write Int-Location st s . a <> 0 & Directed J 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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )
let a be read-write Int-Location; ( s . a <> 0 & Directed J 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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 ) )
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));
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);
A1:
if=0 (a,I,J) c= P +* (if=0 (a,I,J))
by FUNCT_4:25;
A2:
Directed J c= P +* (Directed J)
by FUNCT_4:25;
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 A3:
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 A4:
Reloc ((J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))),2) c= if=0 (a,I,J)
by A3, SCMFSA6A:38;
A5:
0 in dom (if=0 (a,I,J))
by AFINSQ_1:65;
A6: (P +* (if=0 (a,I,J))) . 0 =
(if=0 (a,I,J)) . 0
by A5, FUNCT_4:13
.=
a =0_goto ((card J) + 3)
by Th18
;
card (if=0 (a,I,J)) =
((card I) + (card J)) + (2 + 2)
by SCMFSA8B:11
.=
((card J) + 2) + ((card I) + 2)
;
then
((card J) + 2) + 0 < card (if=0 (a,I,J))
by XREAL_1:8;
then A7:
(card J) + 2 in dom (if=0 (a,I,J))
by AFINSQ_1:66;
A8:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
A9: IC (Initialize s) =
IC (Initialize s)
.=
IC (Start-At (0,SCM+FSA))
by A8, 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 A10:
Reloc ((J ";" ((Goto ((card I) + 1)) ";" (I ";" (Stop SCM+FSA)))),2) c= P +* (if=0 (a,I,J))
by A4, 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 A11:
Reloc ((Directed J),2) c= P +* (if=0 (a,I,J))
by A10, XBOOLE_1:1;
card (if=0 (a,I,J)) =
((card I) + (card J)) + (3 + 1)
by SCMFSA8B:11
.=
(((card I) + (card J)) + 3) + 1
;
then
((card I) + (card J)) + 3 < card (if=0 (a,I,J))
by NAT_1:13;
then A12:
((card I) + (card J)) + 3 in dom (if=0 (a,I,J))
by AFINSQ_1:66;
assume
s . a <> 0
; ( not Directed J 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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 ) )
then A13:
(Initialized s) . a <> 0
by SCMFSA_M:37;
A14:
1 in dom (if=0 (a,I,J))
by Th17;
assume A15:
Directed J 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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3 )
then A16:
pseudo-LifeSpan (s,P,(Directed J)) = LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))
by Th21;
A17: (P +* (if=0 (a,I,J))) . 1 =
(if=0 (a,I,J)) . 1
by A14, FUNCT_4:13
.=
goto 2
by Th18
;
A18:
Directed J is_pseudo-closed_on Initialize s,P +* (Directed J)
by A15;
A19: 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 A9, A6, PBOOLE:143
;
A20:
a <> IC
by SCMFSA_2:56;
not a in dom (Start-At (0,SCM+FSA))
by A20, 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 SCMFSA_M:37
;
then A21: IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) =
(IC (Initialize s)) + 1
by A13, A19, SCMFSA_2:70
.=
0 + 1
by A9
;
A22: 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 A21, A17, PBOOLE:143
;
then A23:
IC (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) = 2
by SCMFSA_2:69;
A24:
now for f being FinSeq-Location holds (Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . flet f be
FinSeq-Location ;
(Initialize s) . f = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . fthus (Initialize s) . f =
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . f
by A19, SCMFSA_2:70
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . f
by A22, SCMFSA_2:69
;
verum end;
now for a being Int-Location holds (Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . alet a be
Int-Location;
(Initialize s) . a = (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . athus (Initialize s) . a =
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),1)) . a
by A19, SCMFSA_2:70
.=
(Comput ((P +* (if=0 (a,I,J))),(Initialize s),2)) . a
by A22, SCMFSA_2:69
;
verum end;
then A25:
DataPart (Initialize s) = DataPart (Comput ((P +* (if=0 (a,I,J))),(Initialize s),2))
by A24, SCMFSA_M:2;
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 A18, A11, A23, A25, Th14, A2
.=
(IC (Comput ((P +* (Directed J)),(Initialize s),(pseudo-LifeSpan (s,P,(Directed J)))))) + 2
by A15, Th13
.=
(card (Directed J)) + 2
by A15, SCMFSA8A:def 4
.=
(card J) + 2
by SCMFSA6A:36
;
then A26: 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 A7, A1, GRFUNC_1:2
.=
goto (((card I) + (card J)) + 3)
by Th26
;
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 A26, SCMFSA_2:69
;
then A27: 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 A12, A1, GRFUNC_1:2
.=
halt SCM+FSA
by Th24
;
then A28:
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 +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3
A29:
CurInstr ((P +* (if=0 (a,I,J))),(Initialize s)) = a =0_goto ((card J) + 3)
by A9, A6, PBOOLE:143;
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 J)),(Directed J))) + (1 + 2) <= kA30:
0 + 2
< ((card I) + (card J)) + 3
by XREAL_1:8;
then A31:
2
in dom (if=0 (a,I,J))
by Th19;
A32:
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 A23, PBOOLE:143
.=
(if=0 (a,I,J)) . 2
by A31, A1, GRFUNC_1:2
;
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 J)),(Directed J))) + (1 + 2) <= k )assume A33:
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 J)),(Directed J))) + (1 + 2) <= kA34:
k <> 0
by A33, A29;
A35:
k <> 1
by A21, A33, A17, PBOOLE:143;
k <> 2
by A33, A30, Th19, A32;
then
k <> 0 & ... &
k <> 2
by A34, A35;
then
2
< k
;
then consider k2 being
Nat such that A36:
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
;
contradictionthen
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 A36, XREAL_1:6;
then A37:
k2 <= pseudo-LifeSpan (
(Initialize s),
(P +* (Directed J)),
(Directed J))
by NAT_1:13;
then A38:
k2 <= pseudo-LifeSpan (
s,
P,
(Directed J))
by A15, Th13;
then A43:
n + 2
in dom (if=0 (a,I,J))
by Th19;
A44:
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 A36, EXTPRO_1:4
.=
n + 2
by A18, A11, A23, A25, A37, Th14, A2
;
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 A44, A43, A1, GRFUNC_1:2
;
hence
contradiction
by A33, A44, A39, Th19;
verum end;
then
LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (pseudo-LifeSpan ((Initialize s),(P +* (Directed J)),(Directed J))) + 3
by A27, A28, EXTPRO_1:def 15;
hence
LifeSpan ((P +* (if=0 (a,I,J))),(Initialize s)) = (LifeSpan ((P +* (J ";" (Stop SCM+FSA))),(Initialize s))) + 3
by A15, A16, Th13; verum