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 holds
DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss)
set D = Int-Locations \/ FinSeq-Locations ;
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 holds
DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss)
let a be read-write Int-Location ; ( ss . (intloc 0 ) = 1 & ss . a <= 0 & Directed J is_pseudo-closed_on ss implies DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss) )
set J0 = Directed J;
set s = Initialize ss;
set s0 = Initialize (Initialize ss);
set J9 = J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )));
set s00 = (Initialize ss) +* ((Directed J) +* (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 s5 = 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 ))),2;
set i = a >0_goto ((card J) + 3);
assume A1:
ss . (intloc 0 ) = 1
; ( not ss . a <= 0 or not Directed J is_pseudo-closed_on ss or DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss) )
set s1 = (Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
assume
ss . a <= 0
; ( not Directed J is_pseudo-closed_on ss or DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss) )
then
(Initialize ss) . a <= 0
by SCMFSA6C:3;
then A2:
(Initialize (Initialize ss)) . a <= 0
by SCMFSA6C:3;
A3:
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 A4: ((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 A3, FUNCT_4:14
.=
(if>0 a,I,J) . 0
by A3, SCMFSA6B:7
.=
a >0_goto ((card J) + 3)
by Th55
;
(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 A5:
(Initialize ss) +* (Initialized (if>0 a,I,J)) = (Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by Th15;
A6:
if>0 a,I,J c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:26, SCMFSA6B:5;
if>0 a,I,J c= (if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A7:
dom (if>0 a,I,J) c= dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
A8:
(Directed J) ';' (Stop SCM+FSA ) = J ';' (Stop SCM+FSA )
by SCMFSA8A:41;
IC SCM+FSA in dom ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by SF_MASTR:65;
then A9: 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
;
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 A10:
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 SCMFSA7B:6;
then A11:
ProgramPart (Relocated (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )))),2) c= if>0 a,I,J
by A10, FUNCT_4:26;
A12:
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
if>0 a,I,J c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by A12, XBOOLE_1:1;
then
ProgramPart (Relocated (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )))),2) c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by A11, XBOOLE_1:1;
then
ProgramPart (ProgramPart (Relocated (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )))),2)) 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 ))),2
by AMI_1:99;
then A13:
ProgramPart (Relocated (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )))),2) 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 ))),2
by AMI_1:105;
ProgramPart (Relocated (Directed J),2) c= ProgramPart (Relocated (J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )))),2)
by Th12, SCMFSA6A:55;
then A14:
ProgramPart (Relocated (Directed J),2) 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 ))),2
by A13, XBOOLE_1:1;
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;
A15: 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 A9, A4, Y
;
assume
Directed J is_pseudo-closed_on ss
; DataPart (IExec (if>0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss)
then A16:
Directed J is_pseudo-closed_on Initialize ss
by A1, Th53;
then
J ';' (Stop SCM+FSA ) is_halting_on Initialize ss
by Th58;
then A17:
ProgramPart ((Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA7B:def 8;
DataPart (Initialize ss) = DataPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))
by SCMFSA8A:11;
then A18:
Directed J is_pseudo-closed_on (Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))
by A16, Th52;
(Initialize ss) +* (Initialized (J ';' (Stop SCM+FSA ))) = (Initialize (Initialize ss)) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA8A:13;
then A19:
(Initialize ss) +* (Initialized (J ';' (Stop SCM+FSA ))) = (Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by Th15;
A20:
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 A21:
(card J) + 2 in dom (if>0 a,I,J)
by SCMFSA6A:15;
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 A22:
((card I) + (card J)) + 3 in dom (if>0 a,I,J)
by SCMFSA6A:15;
A23:
if>0 a,I,J c= (Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:26, SCMFSA6B:5;
set s9 = 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2);
A24:
(Directed J) +* (Start-At 0 ,SCM+FSA ) c= (Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:26;
LifeSpan ((Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = pseudo-LifeSpan (Initialize ss),(Directed J)
by A16, Th58;
then A25:
DataPart (Comput (ProgramPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialize ss),(Directed J))) = DataPart (Comput (ProgramPart ((Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))))
by A16, A20, A8, Th58;
A26:
1 in dom (if>0 a,I,J)
by Th54;
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a =
(Initialize ss) . a
by Th28
.=
(Initialize (Initialize ss)) . a
by SCMFSA6C:3
;
then A27: 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) =
succ (IC ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))))
by A2, A15, SCMFSA_2:97
.=
0 + 1
by A9
;
A28: (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) . 1 =
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 1
by AMI_1:54
.=
((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )) . 1
by A26, A7, FUNCT_4:14
.=
(if>0 a,I,J) . 1
by A26, SCMFSA6B:7
.=
goto 2
by Th55
;
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 ))),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 ))),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 ))),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 ))),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;
A29: 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 + 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 ))),1)
by AMI_1:14
.=
Exec (goto 2),(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 A27, A28, Y, T
;
then A30:
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 ))),2) = 2
by SCMFSA_2:95;
A31:
DataPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) = DataPart ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA )))
by SCMFSA6A:39, SCMFSA8A:14;
A32:
now let f be
FinSeq-Location ;
((Initialize ss) +* ((Directed J) +* (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 ))),2) . fthus ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) . f =
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . f
by A31, 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 A15, SCMFSA_2:97
.=
(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 ))),2) . f
by A29, SCMFSA_2:95
;
verum end;
now let a be
Int-Location ;
((Initialize ss) +* ((Directed J) +* (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 ))),2) . athus ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) . a =
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a
by A31, 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 A15, SCMFSA_2:97
.=
(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 ))),2) . a
by A29, SCMFSA_2:95
;
verum end;
then A33:
DataPart ((Initialize ss) +* ((Directed J) +* (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 ))),2)
by A32, SCMFSA6A:38;
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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) /. (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) = (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) . (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)))
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 ))),2)
by AMI_1:144;
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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) =
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 ))),2),(pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)))
by AMI_1:51
.=
(IC (Comput (ProgramPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)))) + 2
by A24, A18, A14, A30, A33, T, Th51
.=
(IC (Comput (ProgramPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialize ss),(Directed J)))) + 2
by A16, Th50
.=
(card (ProgramPart (Directed J))) + 2
by A16, SCMFSA8A:def 5
.=
(card (Directed J)) + 2
by AMI_1:105
.=
(card J) + 2
by SCMFSA8A:34
;
then A35: 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) =
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . ((card J) + 2)
by Y, AMI_1:54
.=
(if>0 a,I,J) . ((card J) + 2)
by A23, A21, GRFUNC_1:8
.=
goto (((card I) + (card J)) + 3)
by Th64
;
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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))
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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1)) =
IC (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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)))
by AMI_1:14
.=
((card I) + (card J)) + 3
by A35, T, SCMFSA_2:95
;
then A36: 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 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 A6, A22, GRFUNC_1:8
.=
halt SCM+FSA
by Th62
;
then A37:
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;
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;
A38:
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 ))) = a >0_goto ((card J) + 3)
by A9, A4, Y;
now A39:
0 + 2
< ((card I) + (card J)) + 3
by XREAL_1:10;
then A40:
2
in dom (if>0 a,I,J)
by Th57;
A41:
(if>0 a,I,J) . 2
<> halt SCM+FSA
by A39, Th57;
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 ))),2)) /. (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 ))),2)) = (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 ))),2) . (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 ))),2))
by AMI_1:150;
A42:
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 ))),2)),
(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 ))),2) =
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 2
by A30, Y, AMI_1:54
.=
(if>0 a,I,J) . 2
by A40, Th26
;
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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + (1 + 2) <= k )assume A43:
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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + (1 + 2) <= kY:
(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;
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;
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 ) = a >0_goto ((card J) + 3)
by A38, u;
then A44:
k <> 0
by A43, SCMFSA_2:49, SCMFSA_2:124;
xx:
k <> 1
by A27, A28, A43, Y, SCMFSA_2:47, SCMFSA_2:124;
2
<> k
by A43, A41, A42;
then
2
< k
by A44, xx, NAT_1:27;
then consider k2 being
Nat such that A45:
2
+ k2 = k
by NAT_1:10;
reconsider k2 =
k2 as
Element of
NAT by ORDINAL1:def 13;
reconsider n =
IC (Comput (ProgramPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),k2) as
Element of
NAT ;
assume
not
(pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + (1 + 2) <= k
;
contradictionthen
k < ((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 1) + 2
;
then
k2 < (pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 1
by A45, XREAL_1:8;
then A46:
k2 <= pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),
(Directed J)
by NAT_1:13;
then A47:
k2 <= pseudo-LifeSpan (Initialize ss),
(Directed J)
by A16, Th50;
then A52:
n + 2
in dom (if>0 a,I,J)
by Th57;
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 ))),2)
by AMI_1:144;
A53:
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 ))),2),k2)
by A45, AMI_1:51
.=
n + 2
by A24, A18, A14, A30, A33, A46, Th51, T
;
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;
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 A53, A52, Th26
;
hence
contradiction
by A43, A53, A48, Th57;
verum end;
then A54:
LifeSpan ((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1
by A36, A37, AMI_1:def 46;
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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) /. (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) = (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) . (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)))
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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) =
((Initialize ss) +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . ((card J) + 2)
by A34, Y, AMI_1:54
.=
(if>0 a,I,J) . ((card J) + 2)
by A21, Th26
.=
goto (((card I) + (card J)) + 3)
by Th64
;
then
InsCode (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) = 6
by SCMFSA_2:47;
then
InsCode (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) in {0 ,6,7,8}
by ENUMSET1:def 2;
then A55:
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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) = DataPart (Following (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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(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 J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)))
by Th32;
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 ))),2)
by AMI_1:144;
A56: 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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) =
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 ))),2),(pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)))
by AMI_1:51
.=
DataPart (Comput (ProgramPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)))
by A24, A18, A14, A30, T, A33, Th51
;
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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))
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 A5, 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 A37, AMI_1:122
.=
DataPart (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 ))),((pseudo-LifeSpan ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)))
by A54, AMI_1:14
.=
DataPart (Comput (ProgramPart ((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialize ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialize ss),(Directed J)))
by A16, A56, A55, Th50, T
.=
DataPart (Result ((Initialize ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))))
by A17, A25, AMI_1:122
.=
DataPart ((Result ((Initialize ss) +* (Initialized (J ';' (Stop SCM+FSA ))))) +* ((Initialize ss) | NAT ))
by A19, Th35
.=
DataPart (IExec (J ';' (Stop SCM+FSA )),(Initialize ss))
by SCMFSA6B:def 1
.=
DataPart (IExec (J ';' (Stop SCM+FSA )),ss)
by Th17
; verum