let S be State of SCM+FSA ; :: thesis: for I, J being Program of SCM+FSA st I is_halting_on Initialize S & J is_halting_on IExec I,S & I is_closed_on Initialize S & J is_closed_on IExec I,S holds
I ';' J is_halting_on Initialize S
let I, J be Program of SCM+FSA ; :: thesis: ( I is_halting_on Initialize S & J is_halting_on IExec I,S & I is_closed_on Initialize S & J is_closed_on IExec I,S implies I ';' J is_halting_on Initialize S )
set SAt = Start-At 0 ,SCM+FSA ;
assume that
A1: I is_halting_on Initialize S and
A2: J is_halting_on IExec I,S and
A3: I is_closed_on Initialize S and
A4: J is_closed_on IExec I,S ; :: thesis: I ';' J is_halting_on Initialize S
set s = (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ));
A5: DataPart (Initialize S) = DataPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) by SCMFSA8A:11;
then A6: I is_halting_on (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by A1, A3, SCMFSA8B:8;
then A7: ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))) halts_on ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
set s1 = ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ));
A8: (Initialize S) . (intloc 0 ) = 1 by SCMFSA6C:3;
then ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) . (intloc 0 ) = 1 by A5, SCMFSA6A:38;
then A9: ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )) = ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (Initialized I) by SCMFSA8C:18;
set JAt = J +* (Start-At 0 ,SCM+FSA );
set s3 = (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ));
set D = Int-Locations \/ FinSeq-Locations ;
set m3 = LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )));
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A10: dom (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
A11: DataPart (IExec I,S) = DataPart (IExec I,(Initialize S)) by SCMFSA8C:17
.= DataPart (IExec I,((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))) by A1, A3, A5, A8, SCMFSA8C:46
.= DataPart ((Result (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (Initialized I))) +* (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (Initialized I))) by A10, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) by A9, A7, AMI_1:122 ;
then J is_halting_on Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) by A2, A4, SCMFSA8B:8;
then A12: ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) halts_on (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
DataPart (IExec I,S) = DataPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) by A11, SCMFSA8A:11;
then A13: J is_closed_on (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )) by A4, SCMFSA8B:6;
dom (I ';' J) misses dom (Start-At 0 ,SCM+FSA ) by SF_MASTR:64;
then A14: I ';' J c= (I ';' J) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:33;
A15: ProgramPart (Relocated J,(card I)) c= I ';' J by FUNCT_4:26;
set m1 = LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )));
set s4 = Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1);
A16: (Directed I) +* (Start-At 0 ,SCM+FSA ) c= (I ';' J) +* (Start-At 0 ,SCM+FSA ) by PRE_CIRC:3, SCMFSA6A:55;
(I ';' J) +* (Start-At 0 ,SCM+FSA ) c= (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
then (Directed I) +* (Start-At 0 ,SCM+FSA ) c= (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by A16, XBOOLE_1:1;
then A17: (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) = ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* ((Directed I) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:79;
(I ';' J) +* (Start-At 0 ,SCM+FSA ) c= (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
then I ';' J c= (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by A14, XBOOLE_1:1;
then ProgramPart (Relocated J,(card I)) c= (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by A15, XBOOLE_1:1;
then A18: ProgramPart (Relocated J,(card I)) c= Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) by AMI_1:81;
reconsider m = ((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + (LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))) as Element of NAT ;
reconsider kk = DataPart (J +* (Start-At 0 ,SCM+FSA )) as Function ;
A19: DataPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) = (DataPart (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))))) +* kk by FUNCT_4:75;
take m ; :: according to AMI_1:def 20,SCMFSA7B:def 8 :: thesis: ( IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m) in proj1 (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))) & (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))) /. (IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m)) = halt SCM+FSA )
IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m) in NAT ;
hence IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m) in dom (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))) by AMI_1:143; :: thesis: (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))) /. (IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m)) = halt SCM+FSA
A20: J +* (Start-At 0 ,SCM+FSA ) c= (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:26;
A21: I is_closed_on (Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )) by A3, A5, SCMFSA8B:6;
then A22: IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card I by A6, A17, SCMFSA8A:36;
T: ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) = ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) by AMI_1:144;
V: Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),(((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + (LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))))) = Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),(Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))) by AMI_1:51;
DataPart (J +* (Start-At 0 ,SCM+FSA )) = {} by Th2;
then DataPart (Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) by A19, LATTICE2:8, XBOOLE_1:2;
then DataPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = DataPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))) by A21, A6, A17, SCMFSA8A:36;
then IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))))),(card I) = CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))),(Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1))),(Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))))) by A22, A20, A13, A18, SCMFSA8C:42;
then IncAddr (CurInstr (ProgramPart (Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))),((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))))),(card I) = CurInstr (ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),(((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + (LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA ))))))),(Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),(((LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))) + 1) + (LifeSpan ((Comput (ProgramPart (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA )))),(((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))) +* (I +* (Start-At 0 ,SCM+FSA ))))) +* (J +* (Start-At 0 ,SCM+FSA )))))) by V, T;
then CurInstr (ProgramPart (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m)),(Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m) = IncAddr (halt SCM+FSA ),(card I) by A12, AMI_1:def 46
.= halt SCM+FSA by SCMFSA_4:8 ;
hence (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))) /. (IC (Comput (ProgramPart ((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA )))),((Initialize S) +* ((I ';' J) +* (Start-At 0 ,SCM+FSA ))),m)) = halt SCM+FSA by AMI_1:145; :: thesis: verum