let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds
DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,s))
let ss be State of SCM+FSA; for I, J being Program of SCM+FSA
for a being read-write Int-Location st ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P holds
DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
set D = Data-Locations SCM+FSA;
set A = NAT ;
let I, J be Program of SCM+FSA; for a being read-write Int-Location st ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P holds
DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
let a be read-write Int-Location ; ( ss . (intloc 0) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss,P implies DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) )
set J0 = Directed J;
A1:
ProgramPart (Directed J) = Directed J
by RELAT_1:209;
set s = Initialized ss;
set s0 = Initialized (Initialized ss);
set J9 = J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)));
set s00 = Initialize (Initialized ss);
set P00 = P +* (Directed J);
set s3 = Initialize (Initialized ss);
set P3 = P +* (if>0 (a,I,J));
set s4 = Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1);
set s5 = Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2);
set i = a >0_goto ((card J) + 3);
A2:
if>0 (a,I,J) c= P +* (if>0 (a,I,J))
by FUNCT_4:26;
A3:
Directed J c= P +* (Directed J)
by FUNCT_4:26;
assume A4:
ss . (intloc 0) = 1
; ( not ss . a <= 0 or not Directed J is_pseudo-closed_on ss,P or DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) )
set s1 = Initialize (Initialized ss);
set P1 = P +* (J ';' (Stop SCM+FSA));
assume
ss . a <= 0
; ( not Directed J is_pseudo-closed_on ss,P or DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss)) )
then A6:
(Initialized (Initialized ss)) . a <= 0
by SCMFSA6C:3;
A7:
0 in dom (if>0 (a,I,J))
by Th54;
A8: (P +* (if>0 (a,I,J))) . 0 =
(if>0 (a,I,J)) . 0
by A7, FUNCT_4:14
.=
a >0_goto ((card J) + 3)
by Th55
;
(Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized (Initialized ss))
by SCMFSA8A:13;
then A9:
(Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized ss)
;
A10:
(Directed J) ';' (Stop SCM+FSA) = J ';' (Stop SCM+FSA)
by SCMFSA8A:41;
X1:
IC in dom (Start-At (0,SCM+FSA))
by COMPOS_1:52;
A11: IC (Initialize (Initialized ss)) =
IC (Initialize (Initialized ss))
.=
IC (Start-At (0,SCM+FSA))
by X1, FUNCT_4:14
.=
0
by COMPOS_1:64
;
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:67;
then
if>0 (a,I,J) = ((Macro (a >0_goto ((card J) + 3))) ';' J) ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))
by SCMFSA6A:67;
then A12:
if>0 (a,I,J) = (Macro (a >0_goto ((card J) + 3))) ';' (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA))))
by SCMFSA6A:67;
card (Macro (a >0_goto ((card J) + 3))) = 2
by COMPOS_1:150;
then A13:
Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2) c= if>0 (a,I,J)
by A12, FUNCT_4:26;
A16:
Reloc ((Directed J),2) c= Reloc ((J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA)))),2)
by COMPOS_1:156, SCMFSA6A:55;
Reloc ((Directed J),2) c= if>0 (a,I,J)
by A13, A16, XBOOLE_1:1;
then A18:
Reloc ((Directed J),2) c= P +* (if>0 (a,I,J))
by A2, XBOOLE_1:1;
A20: Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(0 + 1)) =
Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),0)))
by EXTPRO_1:4
.=
Following ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)))
by EXTPRO_1:3
.=
Exec ((a >0_goto ((card J) + 3)),(Initialize (Initialized ss)))
by A11, A8, PBOOLE:158
;
assume
Directed J is_pseudo-closed_on ss,P
; DataPart (IExec ((if>0 (a,I,J)),P,ss)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
then A21:
Directed J is_pseudo-closed_on Initialized ss,P
by A4, Th53;
then
J ';' (Stop SCM+FSA) is_halting_on Initialized ss,P
by Th58;
then A22:
P +* (J ';' (Stop SCM+FSA)) halts_on Initialize (Initialized ss)
by SCMFSA7B:def 8;
DataPart (Initialized ss) = DataPart (Initialize (Initialized ss))
by SCMFSA8A:10;
then A23:
Directed J is_pseudo-closed_on Initialize (Initialized ss),P +* (Directed J)
by A21, Th52;
(Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized (Initialized ss))
by SCMFSA8A:13;
then A24:
(Initialized ss) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized ss)
;
A25:
Directed (Directed J) = Directed J
by SCMFSA6A:63;
card (if>0 (a,I,J)) =
((card I) + (card J)) + (2 + 2)
by SCMFSA8B:15
.=
((card J) + 2) + ((card I) + 2)
;
then
((card J) + 2) + 0 < card (if>0 (a,I,J))
by XREAL_1:10;
then A26:
(card J) + 2 in dom (if>0 (a,I,J))
by AFINSQ_1:70;
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 A27:
((card I) + (card J)) + 3 in dom (if>0 (a,I,J))
by AFINSQ_1:70;
set s9 = Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2));
A28:
Start-At (0,SCM+FSA) c= Initialize (Initialized ss)
by FUNCT_4:26;
LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(Initialize (Initialized ss))) = pseudo-LifeSpan ((Initialized ss),P,(Directed J))
by A21, Th58;
then A29:
DataPart (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialized ss),P,(Directed J))))) = DataPart (Comput ((P +* (J ';' (Stop SCM+FSA))),(Initialize (Initialized ss)),(LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(Initialize (Initialized ss))))))
by A21, A25, A10, Th58;
A30:
1 in dom (if>0 (a,I,J))
by Th54;
X2:
a <> IC
by SCMFSA_2:81;
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
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 (Initialized ss)) . a = (Initialized (Initialized ss)) . a
by FUNCT_4:12;
then A31: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)) =
succ (IC (Initialize (Initialized ss)))
by A6, A20, SCMFSA_2:97
.=
0 + 1
by A11
;
A32: (P +* (if>0 (a,I,J))) . 1 =
(if>0 (a,I,J)) . 1
by A30, FUNCT_4:14
.=
goto 2
by Th55
;
A34: Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(1 + 1)) =
Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)))
by EXTPRO_1:4
.=
Exec ((goto 2),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)))
by A31, A32, PBOOLE:158
;
then A35:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) = 2
by SCMFSA_2:95;
A37:
now let f be
FinSeq-Location ;
(Initialize (Initialized ss)) . f = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . fthus (Initialize (Initialized ss)) . f =
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)) . f
by A20, SCMFSA_2:97
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . f
by A34, SCMFSA_2:95
;
verum end;
now let a be
Int-Location ;
(Initialize (Initialized ss)) . a = (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . athus (Initialize (Initialized ss)) . a =
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),1)) . a
by A20, SCMFSA_2:97
.=
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)) . a
by A34, SCMFSA_2:95
;
verum end;
then A38:
DataPart (Initialize (Initialized ss)) = DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2))
by A37, SCMFSA6A:38;
A40: IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))) =
IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J)))))
by EXTPRO_1:5
.=
(IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J)))))) + 2
by A28, A23, A35, A38, Th51, A3, A18
.=
(IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialized ss),P,(Directed J)))))) + 2
by A21, Th50
.=
(card (Directed J)) + 2
by A21, A1, SCMFSA8A:def 5
.=
(card J) + 2
by SCMFSA8A:34
;
then A41: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))) =
(P +* (if>0 (a,I,J))) . ((card J) + 2)
by PBOOLE:158
.=
(if>0 (a,I,J)) . ((card J) + 2)
by A26, A2, GRFUNC_1:8
.=
goto (((card I) + (card J)) + 3)
by Th64
;
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2) + 1))) =
IC (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))))
by EXTPRO_1:4
.=
((card I) + (card J)) + 3
by A41, SCMFSA_2:95
;
then A43: CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2) + 1)))) =
(P +* (if>0 (a,I,J))) . (((card I) + (card J)) + 3)
by PBOOLE:158
.=
(if>0 (a,I,J)) . (((card I) + (card J)) + 3)
by A27, A2, GRFUNC_1:8
.=
halt SCM+FSA
by Th62
;
then A44:
P +* (if>0 (a,I,J)) halts_on Initialize (Initialized ss)
by EXTPRO_1:30;
A46:
CurInstr ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss))) = a >0_goto ((card J) + 3)
by A11, A8, PBOOLE:158;
now A47:
0 + 2
< ((card I) + (card J)) + 3
by XREAL_1:10;
then A48:
2
in dom (if>0 (a,I,J))
by Th57;
A51:
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2))) =
(P +* (if>0 (a,I,J))) . 2
by A35, PBOOLE:158
.=
(if>0 (a,I,J)) . 2
by A48, A2, GRFUNC_1:8
;
let k be
Element of
NAT ;
( CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) = halt SCM+FSA implies (pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k )assume A52:
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k)))
= halt SCM+FSA
;
(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= kA55:
k <> 0
by A52, A46, EXTPRO_1:3;
A56:
k <> 1
by A31, A32, A52, PBOOLE:158;
2
<> k
by A52, A47, Th57, A51;
then
2
< k
by A55, A56, NAT_1:27;
then consider k2 being
Nat such that A57:
2
+ k2 = k
by NAT_1:10;
reconsider k2 =
k2 as
Element of
NAT by ORDINAL1:def 13;
reconsider n =
IC (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),k2)) as
Element of
NAT ;
assume
not
(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + (1 + 2) <= k
;
contradictionthen
k < ((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 1) + 2
;
then
k2 < (pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 1
by A57, XREAL_1:8;
then A58:
k2 <= pseudo-LifeSpan (
(Initialize (Initialized ss)),
(P +* (Directed J)),
(Directed J))
by NAT_1:13;
then A59:
k2 <= pseudo-LifeSpan (
(Initialized ss),
P,
(Directed J))
by A21, Th50;
then A64:
n + 2
in dom (if>0 (a,I,J))
by Th57;
A65:
IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k)) =
IC (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)),k2))
by A57, EXTPRO_1:5
.=
n + 2
by A28, A23, A35, A38, A58, Th51, A3, A18
;
CurInstr (
(P +* (if>0 (a,I,J))),
(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k))) =
(P +* (if>0 (a,I,J))) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k)))
by PBOOLE:158
.=
(if>0 (a,I,J)) . (IC (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),k)))
by A65, A64, A2, GRFUNC_1:8
;
hence
contradiction
by A52, A65, A60, Th57;
verum end;
then A67:
LifeSpan ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss))) = ((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2) + 1
by A43, A44, EXTPRO_1:def 14;
CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))) =
(P +* (if>0 (a,I,J))) . ((card J) + 2)
by A40, PBOOLE:158
.=
(if>0 (a,I,J)) . ((card J) + 2)
by A26, A2, GRFUNC_1:8
.=
goto (((card I) + (card J)) + 3)
by Th64
;
then
InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) = 6
by SCMFSA_2:47;
then
InsCode (CurInstr ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))))) in {0,6,7,8}
by ENUMSET1:def 2;
then A69:
DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))) = DataPart (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))))
by Th32;
A70: DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2))) =
DataPart (Comput ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),2)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J)))))
by EXTPRO_1:5
.=
DataPart (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J)))))
by A28, A23, A35, A38, Th51, A3, A18
;
thus DataPart (IExec ((if>0 (a,I,J)),P,ss)) =
DataPart (IExec ((if>0 (a,I,J)),P,(Initialized ss)))
by Th17
.=
DataPart (Result ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss))))
by A9, COMPOS_1:82
.=
DataPart (Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),(LifeSpan ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss))))))
by A44, EXTPRO_1:23
.=
DataPart (Following ((P +* (if>0 (a,I,J))),(Comput ((P +* (if>0 (a,I,J))),(Initialize (Initialized ss)),((pseudo-LifeSpan ((Initialize (Initialized ss)),(P +* (Directed J)),(Directed J))) + 2)))))
by A67, EXTPRO_1:4
.=
DataPart (Comput ((P +* (Directed J)),(Initialize (Initialized ss)),(pseudo-LifeSpan ((Initialized ss),P,(Directed J)))))
by A21, A70, A69, Th50
.=
DataPart (Result ((P +* (J ';' (Stop SCM+FSA))),(Initialize (Initialized ss))))
by A22, A29, EXTPRO_1:23
.=
DataPart (IExec ((J ';' (Stop SCM+FSA)),P,(Initialized ss)))
by A24, COMPOS_1:82
.=
DataPart (IExec ((J ';' (Stop SCM+FSA)),P,ss))
by Th17
; verum