let s be State of SCM+FSA; :: thesis:
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis:
let J be InitHalting Program of SCM+FSA; :: thesis:
set ps = s | NAT;
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (I ';' J));
set s3 = (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J);
set m1 = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)));
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)));
A1: Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
s +* (Initialized (I ';' J)) = s +* ((I ';' J) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) by FUNCT_4:15
.= (s +* (I ';' J)) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15 ;
then A2: ((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
A3: (s +* (Initialized I)) +* (I ';' J) = s +* ((Initialized I) +* (I ';' J)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by SCMFSA6A:58 ;
A4: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by Th5, FUNCT_4:26;
A5: Initialized J c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) by FUNCT_4:26;
A6: (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized J) equal_outside dom (s | NAT) by FUNCT_7:31, FUNCT_7:106;
then A7: ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized J),(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) equal_outside dom (s | NAT) by FUNCT_7:28;
A8: ( IExec (I,s) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT) & Initialized J c= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) ) by FUNCT_4:26, SCMFSA6B:def 1;
A9: dom (s | NAT) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) /\ NAT by PARTFUN1:def 4, SCMFSA_2:8
.= NAT by XBOOLE_1:21 ;
A10: Initialized J c= (IExec (I,s)) +* (Initialized J) by FUNCT_4:26;
A11: ( Initialized J c= (IExec (I,s)) +* (Initialized J) & Initialized J c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) ) by FUNCT_4:26;
A12: Initialized J c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) by FUNCT_4:26;
A13: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then X: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by Th5;
then A14: (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) by EXTPRO_1:23;
Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))) by X, EXTPRO_1:23;
then A15: IC (Result ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J)))) = IC (Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J)))) by A9, A6, A8, A10, Th15, COMPOS_1:24;
A16: Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26, SCMFSA6A:52;
( s +* (Initialized I),s +* (Initialized (I ';' J)) equal_outside NAT & s +* (Initialized (I ';' J)),(s +* (Initialized (I ';' J))) +* I equal_outside NAT ) by FUNCT_7:132, SCMFSA6A:53;
then s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT by FUNCT_7:29;
then A17: LifeSpan ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I)) = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) by A13, A16, Th15;
then A18: ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)) by A1, Th25;
X: I +* (I ';' J) = I ';' J by SCMFSA6A:57;
X1: ((s +* (Initialized (I ';' J))) +* I) +* (I ';' J) = (s +* (Initialized (I ';' J))) +* (I +* (I ';' J)) by FUNCT_4:15;
X2: (s +* (Initialized (I ';' J))) +* (I ';' J) = s +* ((Initialized (I ';' J)) +* (I ';' J)) by FUNCT_4:15;
I ';' J c= Initialized (I ';' J) by SCMFSA6A:26;
then X3: (Initialized (I ';' J)) +* (I ';' J) = Initialized (I ';' J) by LATTICE2:8;
(s +* (Initialized (I ';' J))) +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) = ((s +* (Initialized (I ';' J))) +* I) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) by FUNCT_4:15
.= ((s +* (Initialized (I ';' J))) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) +* I by Th19
.= (s +* (Initialized (I ';' J))) +* I by A2, FUNCT_4:79 ;
then I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26;
then Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:15;
then ProgramPart ((s +* (Initialized (I ';' J))) +* I) halts_on (s +* (Initialized (I ';' J))) +* I by Th5;
then DataPart (Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) = DataPart (Comput ((ProgramPart (((s +* (Initialized (I ';' J))) +* I) +* (I ';' J))),(((s +* (Initialized (I ';' J))) +* I) +* (I ';' J)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by A16, A17, Th18, SCMFSA6A:39
.= DataPart (Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* (I +* (I ';' J)))),((s +* (Initialized (I ';' J))) +* (I +* (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by X1
.= DataPart (Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* (I ';' J))),((s +* (Initialized (I ';' J))) +* (I ';' J)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by X
.= DataPart (Comput ((ProgramPart (s +* ((Initialized (I ';' J)) +* (I ';' J)))),(s +* ((Initialized (I ';' J)) +* (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by X2
.= DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by X3
.= DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) by A13, A4, A3, Th18, SCMFSA6A:39 ;
then A19: DataPart ((Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) = (DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) by FUNCT_4:75 ;
T: ProgramPart (s +* (Initialized (I ';' J))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) by AMI_1:123;
A20: ( IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = DataPart ((Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) ) by A1, A17, Th25;
then A21: DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) = DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) by A18, A5, A19, Th12, T;
A22: IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) = (IC (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I) by A20, A18, A5, A19, Th12, T;
X: ProgramPart (s +* (Initialized (I ';' J))) halts_on s +* (Initialized (I ';' J)) by A1, Th5;
Y: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by A13, Th5;
A23: IExec ((I ';' J),s) = (Result ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))))) +* (s | NAT) by X, EXTPRO_1:23
.= (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) +* (s | NAT) by A14, Th28 ;
IExec (I,s) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT) by Y, EXTPRO_1:23 ;
then Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J))), Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))) equal_outside NAT by A9, A7, A11, Th15;
then A24: (Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J)))) +* (s | NAT) = (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))) +* (s | NAT) by A9, FUNCT_7:108;
Y: ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) by A12, Th5;
(IExec (I,s)) | NAT = ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)) | NAT by SCMFSA6B:def 1
.= s | NAT by PBOOLE:157 ;
then A25: IExec (J,(IExec (I,s))) = (Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J)))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) +* (s | NAT) by A24, Y, EXTPRO_1:23 ;
A26: dom (s | NAT) misses Int-Locations \/ FinSeq-Locations by A9, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A27: DataPart (IExec ((I ';' J),s)) = DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) by A23, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) by A21, EXTPRO_1:5
.= DataPart (IExec (J,(IExec (I,s)))) by A25, A26, FUNCT_4:76, SCMFSA_2:127 ;
X: ProgramPart (s +* (Initialized (I ';' J))) halts_on s +* (Initialized (I ';' J)) by A1, Th5;
Y: ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) by A12, Th5;
U: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by A13, Th5;
XX: (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) by U, EXTPRO_1:23;
A28: IC (IExec ((I ';' J),s)) = IC (Result ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))) by SCMFSA8A:7
.= IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))))) by X, EXTPRO_1:23
.= IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) by A14, Th28
.= (IC (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I) by A22, EXTPRO_1:5
.= (IC (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))) + (card I) by Y, EXTPRO_1:23
.= (IC (Result ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))))) + (card I) by XX
.= (IC (IExec (J,(IExec (I,s))))) + (card I) by A15, SCMFSA8A:7 ;

hereby :: thesis:

reconsider l = (IC (IExec (J,(IExec (I,s))))) + (card I) as Element of NAT ;
A29: dom (Start-At (l,SCM+FSA)) = {(IC SCM+FSA)} by FUNCOP_1:19;

A30: now

let x be set ; :: thesis:
assume A31: x in dom (IExec ((I ';' J),s)) ; :: thesis:

per cases by A31, SCMFSA6A:35;

suppose A32: x is Int-Location ; :: thesis:

then x <> IC SCM+FSA by SCMFSA_2:81;
then A33: not x in dom (Start-At (l,SCM+FSA)) by A29, TARSKI:def 1;
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x by A27, A32, SCMFSA6A:38;
hence (IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x by A33, FUNCT_4:12; :: thesis:

end;

suppose A34: x is FinSeq-Location ; :: thesis:

then x <> IC SCM+FSA by SCMFSA_2:82;
then A35: not x in dom (Start-At (l,SCM+FSA)) by A29, TARSKI:def 1;
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x by A27, A34, SCMFSA6A:38;
hence (IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x by A35, FUNCT_4:12; :: thesis:

end;

suppose A36: x = IC SCM+FSA ; :: thesis:

then x in {(IC SCM+FSA)} by TARSKI:def 1;
then A37: x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:19;
thus (IExec ((I ';' J),s)) . x = (Start-At (l,SCM+FSA)) . (IC SCM+FSA) by A28, A36, FUNCOP_1:87
.= ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x by A36, A37, FUNCT_4:14 ; :: thesis:

end;

suppose A38: x is Element of NAT ; :: thesis:

then x <> IC SCM+FSA by COMPOS_1:3;
then A39: not x in dom (Start-At (l,SCM+FSA)) by A29, TARSKI:def 1;
(IExec ((I ';' J),s)) | NAT = s | NAT by A23, PBOOLE:157
.= (IExec (J,(IExec (I,s)))) | NAT by A25, PBOOLE:157 ;
then (IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x by A38, SCMFSA6A:36;
hence (IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x by A39, FUNCT_4:12; :: thesis:

end;

end;

end;

dom (IExec ((I ';' J),s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) by PARTFUN1:def 4 ;
hence IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA)) by A30, FUNCT_1:9; :: thesis:

end;