let S be State of SCM+FSA; :: thesis: for I, J being Program of SCM+FSA st I is_halting_on Initialized S & J is_halting_on IExec (I,S) & I is_closed_on Initialized S & J is_closed_on IExec (I,S) holds
I ';' J is_halting_on Initialized S
let I, J be Program of SCM+FSA; :: thesis: ( I is_halting_on Initialized S & J is_halting_on IExec (I,S) & I is_closed_on Initialized S & J is_closed_on IExec (I,S) implies I ';' J is_halting_on Initialized S )
set SAt = Start-At (0,SCM+FSA);
assume that
A1: I is_halting_on Initialized S and
A2: J is_halting_on IExec (I,S) and
A3: I is_closed_on Initialized S and
A4: J is_closed_on IExec (I,S) ; :: thesis: I ';' J is_halting_on Initialized S
set s = (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)));
A5: DataPart (Initialized S) = DataPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11;
then A6: I is_halting_on (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A1, A3, SCMFSA8B:8;
then A7: ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (I +* (Start-At (0,SCM+FSA)))) halts_on ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (I +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
set s1 = ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I);
A8: (Initialized S) . (intloc 0) = 1 by SCMFSA6C:3;
then ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) . (intloc 0) = 1 by A5, SCMFSA6A:38;
then A9: ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I) = ((Initialized 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 (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)));
set D = Int-Locations \/ FinSeq-Locations;
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (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 (ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
A11: DataPart (IExec (I,S)) = DataPart (IExec (I,(Initialized S))) by SCMFSA8C:17
.= DataPart (IExec (I,((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))))) by A1, A3, A5, A8, SCMFSA8C:46
.= DataPart ((Result ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I)))) +* (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialized I)))) by A10, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) by A9, A7, EXTPRO_1:23 ;
then J is_halting_on Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))))) by A2, A4, SCMFSA8B:8;
then A12: ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) halts_on (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
DataPart (IExec (I,S)) = DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) by A11, SCMFSA8A:11;
then A13: J is_closed_on (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))) by A4, SCMFSA8B:6;
dom (I ';' J) misses dom (Start-At (0,SCM+FSA)) by COMPOS_1:140;
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 ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)));
set s4 = Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1));
T4: ProgramPart (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))) = ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) by AMI_1:123;
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= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then (Directed I) +* (Start-At (0,SCM+FSA)) c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A16, XBOOLE_1:1;
then A17: (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) = ((Initialized 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= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
then I ';' J c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A14, XBOOLE_1:1;
then ProgramPart (Relocated (J,(card I))) c= (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A15, XBOOLE_1:1;
then A18: ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1)) by AMI_1:81;
reconsider m = ((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (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 (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) = (DataPart (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))))))) +* kk by FUNCT_4:75;
take m ; :: according to EXTPRO_1:def 7,SCMFSA7B:def 8 :: thesis: ( IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m)) in proj1 (ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))) & CurInstr ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA )
IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m)) in NAT ;
hence IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m)) in dom (ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA
A20: J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))) by FUNCT_4:26;
A21: I is_closed_on (Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))) by A3, A5, SCMFSA8B:6;
then A22: IC (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))) = card I by A6, A17, SCMFSA8A:36;
V: Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))))))) = Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))))) by EXTPRO_1:5;
TX3: ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))))))) by AMI_1:123;
TX4: ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))))))) by T4, AMI_1:123;
DataPart (J +* (Start-At (0,SCM+FSA))) = {} by Th2;
then DataPart (Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) = DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) by A19, LATTICE2:8, XBOOLE_1:2;
then DataPart (Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))) = DataPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))) by A21, A6, A17, SCMFSA8A:36;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))))))))),(card I)) = CurInstr ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))))))) by A22, A20, A13, A18, TX4, TX3, T4, SCMFSA8C:42;
then IncAddr ((CurInstr ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))))))))),(card I)) = CurInstr ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),(((LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA))))),((Comput ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)),(LifeSpan ((ProgramPart (((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I))),(((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))) +* (Initialize I)))))) +* (J +* (Start-At (0,SCM+FSA)))))))))) by V;
then CurInstr ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m))) = IncAddr ((halt SCM+FSA),(card I)) by A12, EXTPRO_1:def 14
.= halt SCM+FSA by SCMFSA_4:8 ;
hence CurInstr ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA))))),((Initialized S) +* ((I ';' J) +* (Start-At (0,SCM+FSA)))),m))) = halt SCM+FSA ; :: thesis: verum