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