let s be State of ; for I, J being Program of
for a being read-write Int-Location st s . a = 0 & Directed I is_pseudo-closed_on s holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
set D = Int-Locations \/ FinSeq-Locations ;
let I, J be Program of ; for a being read-write Int-Location st s . a = 0 & Directed I is_pseudo-closed_on s holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
let a be read-write Int-Location ; ( s . a = 0 & Directed I is_pseudo-closed_on s implies ( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 ) )
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA );
set s00 = s +* ((Directed I) +* (Start-At (insloc 0 )));
set s3 = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )));
set s4 = Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1;
set i = a =0_goto (insloc ((card J) + 3));
A1:
(Directed I) +* (Start-At (insloc 0 )) c= s +* ((Directed I) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
card (if=0 a,I,J) =
((card I) + (card J)) + (3 + 1)
by SCMFSA8B:14
.=
(((card I) + (card J)) + 3) + 1
;
then
((card I) + (card J)) + 3 < card (if=0 a,I,J)
by NAT_1:13;
then A2:
insloc (((card I) + (card J)) + 3) in dom (if=0 a,I,J)
by SCMFSA6A:15;
A3:
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
(if=0 a,I,J) +* (Start-At (insloc 0 )) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
then A4:
if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by A3, XBOOLE_1:1;
A5:
not a in dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by SCMFSA6B:12;
A6:
insloc 0 in dom (if=0 a,I,J)
by Th54;
if=0 a,I,J c= (if=0 a,I,J) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then
dom (if=0 a,I,J) c= dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
then A7: (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 ) =
((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (insloc 0 )
by A6, FUNCT_4:14
.=
(if=0 a,I,J) . (insloc 0 )
by A6, SCMFSA6B:7
.=
a =0_goto (insloc ((card J) + 3))
by Th55
;
A8: card (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) =
(card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))
by SCMFSA6A:61
.=
(card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1
by SCMFSA8A:29
.=
((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1
by SCMFSA6A:61
.=
((card J) + 2) + 1
by SCMFSA7B:6
.=
(card J) + (2 + 1)
;
IC SCM+FSA in dom ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by SF_MASTR:65;
then A9: IC (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) =
((if=0 a,I,J) +* (Start-At (insloc 0 ))) . (IC SCM+FSA )
by FUNCT_4:14
.=
insloc 0
by SF_MASTR:66
;
A10:
if=0 a,I,J c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by FUNCT_4:26, SCMFSA6B:5;
A11: Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),(0 + 1) =
Following (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 )
by AMI_1:14
.=
Following (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by AMI_1:13
.=
Exec (a =0_goto (insloc ((card J) + 3))),(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by A9, A7
;
A12:
if=0 a,I,J = ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) ';' (Stop SCM+FSA )
by SCMFSA8B:def 1;
then
if=0 a,I,J = (((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' (I ';' (Stop SCM+FSA ))
by SCMFSA6A:67;
then
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= if=0 a,I,J
by A8, FUNCT_4:26;
then
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by A4, XBOOLE_1:1;
then
ProgramPart [(ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)))] c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1
by AMI_1:99;
then A13:
ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3)) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1
by AMI_1:105;
ProgramPart (Relocated (Directed I),((card J) + 3)) c= ProgramPart (Relocated (I ';' (Stop SCM+FSA )),((card J) + 3))
by Th12, SCMFSA6A:55;
then A14:
ProgramPart (Relocated (Directed I),((card J) + 3)) c= Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1
by A13, XBOOLE_1:1;
A15:
DataPart (s +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by SCMFSA6A:39, SCMFSA8A:14;
A16:
now let f be
FinSeq-Location ;
(s +* ((Directed I) +* (Start-At (insloc 0 )))) . f = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . fthus (s +* ((Directed I) +* (Start-At (insloc 0 )))) . f =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . f
by A15, SCMFSA6A:38
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . f
by A11, SCMFSA_2:96
;
verum end;
now let a be
Int-Location ;
(s +* ((Directed I) +* (Start-At (insloc 0 )))) . a = (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . athus (s +* ((Directed I) +* (Start-At (insloc 0 )))) . a =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a
by A15, SCMFSA6A:38
.=
(Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) . a
by A11, SCMFSA_2:96
;
verum end;
then A17:
DataPart (s +* ((Directed I) +* (Start-At (insloc 0 )))) = DataPart (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1)
by A16, SCMFSA6A:38;
assume
s . a = 0
; ( not Directed I is_pseudo-closed_on s or ( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 ) )
then
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . a = 0
by A5, FUNCT_4:12;
then A18:
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1) = insloc ((card J) + 3)
by A11, SCMFSA_2:96;
assume A19:
Directed I is_pseudo-closed_on s
; ( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
then A20:
pseudo-LifeSpan s,(Directed I) = LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))
by Th58;
DataPart s = DataPart (s +* ((Directed I) +* (Start-At (insloc 0 ))))
by SCMFSA8A:11;
then A21:
Directed I is_pseudo-closed_on s +* ((Directed I) +* (Start-At (insloc 0 )))
by A19, Th52;
A22: IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) =
IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)))
by AMI_1:51
.=
(IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)))) + ((card J) + 3)
by A1, A21, A14, A18, A17, Th51
.=
(IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),(pseudo-LifeSpan s,(Directed I)))) + ((card J) + 3)
by A19, Th50
.=
(insloc (card (ProgramPart (Directed I)))) + ((card J) + 3)
by A19, SCMFSA8A:def 5
.=
(insloc (card (Directed I))) + ((card J) + 3)
by AMI_1:105
.=
insloc ((card I) + ((card J) + 3))
by SCMFSA8A:34
.=
insloc (((card I) + (card J)) + 3)
;
then A23: CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),((pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1)) =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc (((card I) + (card J)) + 3))
by AMI_1:54
.=
(if=0 a,I,J) . (insloc (((card I) + (card J)) + 3))
by A10, A2, GRFUNC_1:8
.=
halt SCM+FSA
by Th61
;
then A24:
ProgramPart (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) halts_on s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by AMI_1:146;
hence
if=0 a,I,J is_halting_on s
by SCMFSA7B:def 8; ( if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1 )
now let k be
Element of
NAT ;
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)per cases
( k = 0 or ( 0 < k & k < (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 ) or ( 0 < k & (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k ) )
;
suppose
k = 0
;
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J)then
Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),
k = s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))
by AMI_1:13;
then
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = insloc 0
by Th31;
hence
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J)
by Th54;
verum end; suppose A25:
(
0 < k &
k < (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 )
;
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),b1) in dom (if=0 a,I,J) card (if=0 a,I,J) =
((card I) + (card J)) + (3 + 1)
by SCMFSA8B:14
.=
(((card I) + (card J)) + 3) + 1
;
then A26:
((card I) + (card J)) + 3
< card (if=0 a,I,J)
by XREAL_1:31;
0 + 1
<= k
by A25, INT_1:20;
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 13;
reconsider n =
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1) as
Element of
NAT by ORDINAL1:def 13;
A28:
k1 < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),
(Directed I)
by A25, A27, XREAL_1:8;
then
k1 < pseudo-LifeSpan s,
(Directed I)
by A19, Th50;
then
insloc n in dom (Directed I)
by A19, SCMFSA8A:31;
then
n < card (Directed I)
by SCMFSA6A:15;
then
n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3)
by XREAL_1:8;
then
n + ((card J) + 3) < (card I) + ((card J) + 3)
by SCMFSA8A:34;
then A29:
n + ((card J) + 3) < card (if=0 a,I,J)
by A26, XXREAL_0:2;
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) =
IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),k1)
by A27, AMI_1:51
.=
(IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1)) + ((card J) + 3)
by A1, A21, A14, A18, A17, A28, Th51
;
hence
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J)
by A29, SCMFSA6A:15;
verum end; end;
hence
if=0 a,I,J is_closed_on s
by SCMFSA7B:def 7; LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1
now set J1 =
(((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I;
let k be
Element of
NAT ;
( CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA implies (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= k )assume A30:
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) = halt SCM+FSA
;
(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1 <= kassume
not
(pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1
<= k
;
contradictionthen A31:
k <= pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),
(Directed I)
by NAT_1:13;
A32:
insloc 0 in dom (if=0 a,I,J)
by Th54;
A33:
InsCode (a =0_goto (insloc ((card J) + 3))) = 7
by SCMFSA_2:48;
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),0 ) =
CurInstr (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 ))))
by AMI_1:13
.=
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (insloc 0 )
by Th31
.=
(if=0 a,I,J) . (insloc 0 )
by A32, Th26
.=
a =0_goto (insloc ((card J) + 3))
by Th55
;
then consider k1 being
Nat such that A34:
k1 + 1
= k
by A30, A33, NAT_1:6, SCMFSA_2:124;
reconsider k1 =
k1 as
Element of
NAT by ORDINAL1:def 13;
reconsider n =
IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1) as
Element of
NAT by ORDINAL1:def 13;
k1 < k
by A34, XREAL_1:31;
then A35:
k1 < pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),
(Directed I)
by A31, XXREAL_0:2;
then
k1 < pseudo-LifeSpan s,
(Directed I)
by A19, Th50;
then
insloc n in dom (Directed I)
by A19, SCMFSA8A:31;
then
n < card (Directed I)
by SCMFSA6A:15;
then
n + ((card J) + 3) < (card (Directed I)) + ((card J) + 3)
by XREAL_1:8;
then A36:
n + ((card J) + 3) < (card I) + ((card J) + 3)
by SCMFSA8A:34;
A37:
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) =
IC (Computation (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),1),k1)
by A34, AMI_1:51
.=
(IC (Computation (s +* ((Directed I) +* (Start-At (insloc 0 )))),k1)) + ((card J) + 3)
by A1, A21, A14, A18, A17, A35, Th51
;
card ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) =
(card (((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J) ';' (Goto (insloc ((card I) + 1))))) + (card I)
by SCMFSA6A:61
.=
((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + (card (Goto (insloc ((card I) + 1))))) + (card I)
by SCMFSA6A:61
.=
((card ((Macro (a =0_goto (insloc ((card J) + 3)))) ';' J)) + 1) + (card I)
by SCMFSA8A:29
.=
(((card (Macro (a =0_goto (insloc ((card J) + 3))))) + (card J)) + 1) + (card I)
by SCMFSA6A:61
.=
((2 + (card J)) + 1) + (card I)
by SCMFSA7B:6
.=
((card I) + (card J)) + 3
;
then
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)
by A37, A36, SCMFSA6A:15;
then A38:
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I))
by FUNCT_4:105;
then A39:
(Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) in rng (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I))
by FUNCT_1:def 5;
card (if=0 a,I,J) =
((card I) + (card J)) + (3 + 1)
by SCMFSA8B:14
.=
(((card I) + (card J)) + 3) + 1
;
then
((card I) + (card J)) + 3
< card (if=0 a,I,J)
by XREAL_1:31;
then
n + ((card J) + 3) < card (if=0 a,I,J)
by A36, XXREAL_0:2;
then A40:
IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) in dom (if=0 a,I,J)
by A37, SCMFSA6A:15;
A41:
CurInstr (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k) =
(s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k))
by AMI_1:54
.=
(if=0 a,I,J) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k))
by A40, Th26
;
Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I) c= if=0 a,
I,
J
by A12, SCMFSA6A:55;
then
(if=0 a,I,J) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k)) = (Directed ((((a =0_goto (insloc ((card J) + 3))) ';' J) ';' (Goto (insloc ((card I) + 1)))) ';' I)) . (IC (Computation (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))),k))
by A38, GRFUNC_1:8;
hence
contradiction
by A30, A39, A41, AMI_1:def 53;
verum end;
then
LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (pseudo-LifeSpan (s +* ((Directed I) +* (Start-At (insloc 0 )))),(Directed I)) + 1
by A23, A24, AMI_1:def 46;
hence
LifeSpan (s +* ((if=0 a,I,J) +* (Start-At (insloc 0 )))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) + 1
by A19, A20, Th50; verum