let ss be State of SCM+FSA ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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 = Initialized ss;
set s0 = Initialized (Initialized ss);
set J9 = J ';' ((Goto ((card I) + 1)) ';' (I ';' (Stop SCM+FSA )));
set s00 = (Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ));
set s3 = (Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ));
set s4 = Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1;
set s5 = Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized 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 ; :: thesis: ( 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 = (Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
assume ss . a <> 0 ; :: thesis: ( 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 (Initialized ss) . a <> 0 by SCMFSA6C:3;
then A2: (Initialized (Initialized 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: ((Initialized 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 ;
(Initialized ss) +* (Initialized (if=0 a,I,J)) = (Initialized (Initialized ss)) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
then A5: (Initialized ss) +* (Initialized (if=0 a,I,J)) = (Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by Th15;
A6: if=0 a,I,J c= (Initialized 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 ((Initialized 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 1;
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= (Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
then if=0 a,I,J c= (Initialized 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= (Initialized 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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized 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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2 by RELAT_1:209;
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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2 by A13, XBOOLE_1:1;
Y: (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) /. (IC ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) by COMPOS_1:38;
A15: Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(0 + 1) = Following (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by AMI_1:13
.= Exec (a =0_goto ((card J) + 3)),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by A9, A4, Y ;
assume Directed J is_pseudo-closed_on ss ; :: thesis: DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (J ';' (Stop SCM+FSA )),ss)
then A16: Directed J is_pseudo-closed_on Initialized ss by A1, Th53;
then J ';' (Stop SCM+FSA ) is_halting_on Initialized ss by Th58;
then A17: ProgramPart ((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
DataPart (Initialized ss) = DataPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
then A18: Directed J is_pseudo-closed_on (Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )) by A16, Th52;
(Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA ))) = (Initialized (Initialized ss)) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
then A19: (Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA ))) = (Initialized 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:14
.= ((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 AFINSQ_1:70;
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 A22: ((card I) + (card J)) + 3 in dom (if=0 a,I,J) by AFINSQ_1:70;
A23: if=0 a,I,J c= (Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26, SCMFSA6B:5;
set s9 = Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2);
A24: (Directed J) +* (Start-At 0 ,SCM+FSA ) c= (Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
LifeSpan (ProgramPart ((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = pseudo-LifeSpan (Initialized ss),(Directed J) by A16, Th58;
then A25: DataPart (Comput (ProgramPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialized ss),(Directed J))) = DataPart (Comput (ProgramPart ((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialized 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;
((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a = (Initialized ss) . a by Th28
.= (Initialized (Initialized ss)) . a by SCMFSA6C:3 ;
then A27: IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) = succ (IC ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) by A2, A15, SCMFSA_2:96
.= 0 + 1 by A9 ;
A28: (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . 1 = ((Initialized 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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1)) by COMPOS_1:38;
T: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by AMI_1:123;
A29: Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(1 + 1) = Following (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by AMI_1:14
.= Exec (goto 2),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) by A27, A28, Y, T ;
then A30: IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) = 2 by SCMFSA_2:95;
A31: DataPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) = DataPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA6A:39, SCMFSA8A:14;

A32: now

let f be FinSeq-Location ; :: thesis: ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) . f = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . f
thus ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) . f = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . f by A31, SCMFSA6A:38
.= (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . f by A15, SCMFSA_2:96
.= (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . f by A29, SCMFSA_2:95 ; :: thesis: verum

end;

now

let a be Int-Location ; :: thesis: ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) . a = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . a
thus ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) . a = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . a by A31, SCMFSA6A:38
.= (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),1) . a by A15, SCMFSA_2:96
.= (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . a by A29, SCMFSA_2:95 ; :: thesis: verum

end;

then A33: DataPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))) = DataPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) by A32, SCMFSA6A:38;
Y: (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) by COMPOS_1:38;
T: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) by AMI_1:123;
A34: IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) = IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2),(pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J))) by AMI_1:51
.= (IC (Comput (ProgramPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)))) + 2 by A24, A18, A14, A30, A33, T, Th51
.= (IC (Comput (ProgramPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialized ss),(Directed J)))) + 2 by A16, Th50
.= (card (ProgramPart (Directed J))) + 2 by A16, SCMFSA8A:def 5
.= (card (Directed J)) + 2 by RELAT_1:209
.= (card J) + 2 by SCMFSA8A:34 ;
then A35: CurInstr (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) = ((Initialized 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 Th63 ;
Y: (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1))) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1))) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1)) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1))) by COMPOS_1:38;
T: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) by AMI_1:123;
TX3: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1)) by AMI_1:123;
IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1)) = IC (Following (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized 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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1)) = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (((card I) + (card J)) + 3) by Y, TX3, AMI_1:54
.= (if=0 a,I,J) . (((card I) + (card J)) + 3) by A6, A22, GRFUNC_1:8
.= halt SCM+FSA by Th61 ;
then A37: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) halts_on (Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by AMI_1:146;
Y: (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) /. (IC ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) by COMPOS_1:38;
A38: CurInstr (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized 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 Th56;
A41: (if=0 a,I,J) . 2 <> halt SCM+FSA by A39, Th56;
Y: (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2)) by COMPOS_1:38;
TX2: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) by AMI_1:123;
A42: CurInstr (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . 2 by A30, Y, TX2, AMI_1:54
.= (if=0 a,I,J) . 2 by A40, Th26 ;
let k be Element of NAT ; :: thesis: ( CurInstr (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA implies (pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + (1 + 2) <= k )
TX3: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) by AMI_1:123;
assume A43: CurInstr (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = halt SCM+FSA ; :: thesis: (pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + (1 + 2) <= k
Y: (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by COMPOS_1:38;
u: Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),0 = (Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )) by AMI_1:13;
CurInstr (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized 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:48, SCMFSA_2:124;
xx: k <> 1 by A27, A28, A43, Y, TX3, 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 ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),k2) as Element of NAT ;
assume not (pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + (1 + 2) <= k ; :: thesis: contradiction
then k < ((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 1) + 2 ;
then k2 < (pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 1 by A45, XREAL_1:8;
then A46: k2 <= pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J) by NAT_1:13;
then A47: k2 <= pseudo-LifeSpan (Initialized ss),(Directed J) by A16, Th50;

A48: now

per cases ( k2 = pseudo-LifeSpan (Initialized ss),(Directed J) or k2 < pseudo-LifeSpan (Initialized ss),(Directed J) ) by A47, XXREAL_0:1;

suppose A49: k2 = pseudo-LifeSpan (Initialized ss),(Directed J) ; :: thesis: n + 2 < ((card I) + (card J)) + 3

((card I) + (card J)) + (2 + 1) = (((card J) + 2) + 1) + (card I) ;
then A50: ((card J) + 2) + 1 <= ((card I) + (card J)) + 3 by NAT_1:11;
IC (Comput (ProgramPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),k2) = card (ProgramPart (Directed J)) by A16, A49, SCMFSA8A:def 5
.= card (Directed J) by RELAT_1:209 ;
then n = card J by SCMFSA8A:34;
hence n + 2 < ((card I) + (card J)) + 3 by A50, NAT_1:13; :: thesis: verum

end;

suppose k2 < pseudo-LifeSpan (Initialized ss),(Directed J) ; :: thesis: n + 2 < ((card I) + (card J)) + 3

then n in dom (Directed J) by A16, SCMFSA8A:31;
then n < card (Directed J) by AFINSQ_1:70;
then n + 2 < (card (Directed J)) + 2 by XREAL_1:8;
then A51: n + 2 < (card J) + 2 by SCMFSA8A:34;
((card I) + (card J)) + (1 + 2) = ((card J) + 2) + ((card I) + 1) ;
then (card J) + 2 <= ((card I) + (card J)) + 3 by NAT_1:11;
hence n + 2 < ((card I) + (card J)) + 3 by A51, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then A52: n + 2 in dom (if=0 a,I,J) by Th56;
T: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) by AMI_1:123;
A53: IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized 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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by COMPOS_1:38;
TX3: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) by AMI_1:123;
CurInstr (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k) = ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by Y, TX3, AMI_1:54
.= (if=0 a,I,J) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),k)) by A53, A52, Th26 ;
hence contradiction by A43, A53, A48, Th56; :: thesis: verum

end;

then A54: LifeSpan (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2) + 1 by A36, A37, AMI_1:def 46;
Y: (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) /. (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) = (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) . (IC (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) = ((Initialized 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 Th63 ;
then InsCode (CurInstr (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) = 6 by SCMFSA_2:47;
then InsCode (CurInstr (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized 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 ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) = DataPart (Following (ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) by Th32;
T: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2) by AMI_1:123;
A56: DataPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) = DataPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),2),(pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J))) by AMI_1:51
.= DataPart (Comput (ProgramPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J))) by A24, A18, A14, A30, T, A33, Th51 ;
T: ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2)) by AMI_1:123;
thus DataPart (IExec (if=0 a,I,J),ss) = DataPart (IExec (if=0 a,I,J),(Initialized ss)) by Th17
.= DataPart ((Result (ProgramPart ((Initialized ss) +* (Initialized (if=0 a,I,J)))),((Initialized ss) +* (Initialized (if=0 a,I,J)))) +* ((Initialized ss) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))) by A5, Th35
.= DataPart (Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))))) by A37, AMI_1:122
.= DataPart (Following (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))),((pseudo-LifeSpan ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(Directed J)) + 2))) by A54, AMI_1:14
.= DataPart (Comput (ProgramPart ((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((Directed J) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialized ss),(Directed J))) by A16, A56, A55, Th50, T
.= DataPart (Result (ProgramPart ((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) by A17, A25, AMI_1:122
.= DataPart ((Result (ProgramPart ((Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA ))))),((Initialized ss) +* (Initialized (J ';' (Stop SCM+FSA ))))) +* ((Initialized ss) | NAT )) by A19, Th35
.= DataPart (IExec (J ';' (Stop SCM+FSA )),(Initialized ss)) by SCMFSA6B:def 1
.= DataPart (IExec (J ';' (Stop SCM+FSA )),ss) by Th17 ; :: thesis: verum