let s be State of SCM+FSA ; :: thesis:
let J be Program of SCM+FSA ; :: thesis:
let Ig be good Program of SCM+FSA ; :: thesis:
set SAt = Start-At 0 ,SCM+FSA ;
set D = Int-Locations \/ FinSeq-Locations ;
set I = Ig;
assume that
A1: Ig is_halting_on Initialize s and
A2: J is_halting_on IExec Ig,s and
A3: Ig is_closed_on Initialize s and
A4: J is_closed_on IExec Ig,s ; :: thesis:
set Is = Initialize s;
A5: (Initialize s) . (intloc 0 ) = 1 by SCMFSA6C:3;
set s1 = s +* (Initialized Ig);
set m1 = LifeSpan (s +* (Initialized Ig));
s +* (Initialized Ig) = (Initialize s) +* (Initialized Ig) by SCMFSA8A:8;
then A6: s +* (Initialized Ig) = (Initialize s) +* (Ig +* (Start-At 0 ,SCM+FSA )) by A5, SCMFSA8C:18;
then DataPart (Initialize s) = DataPart (s +* (Initialized Ig)) by SCMFSA8A:11;
then A7: Ig is_closed_on s +* (Initialized Ig) by A3, SCMFSA8B:6;
set s3 = (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J);
A8: ProgramPart (s +* (Initialized Ig)) halts_on s +* (Initialized Ig) by A1, A6, SCMFSA7B:def 8;
then A9: (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) = (Result (s +* (Initialized Ig))) +* (Initialized J) by AMI_1:122;
set s2 = s +* (Initialized (Ig ';' J));
s +* (Initialized (Ig ';' J)) = (Initialize s) +* (Initialized (Ig ';' J)) by SCMFSA8A:8;
then A10: s +* (Initialized (Ig ';' J)) = (Initialize s) +* ((Ig ';' J) +* (Start-At 0 ,SCM+FSA )) by A5, SCMFSA8C:18;
then A11: DataPart (Initialize s) = DataPart (s +* (Initialized (Ig ';' J))) by SCMFSA8A:11;
then A12: (s +* (Initialized (Ig ';' J))) . (intloc 0 ) = 1 by A5, SCMFSA6A:38;
A13: DataPart (IExec Ig,s) = DataPart (IExec Ig,(Initialize s)) by SCMFSA8C:17
.= DataPart (IExec Ig,(s +* (Initialized (Ig ';' J)))) by A1, A3, A5, A11, SCMFSA8C:46 ;
then A14: J is_closed_on IExec Ig,(s +* (Initialized (Ig ';' J))) by A2, A4, SCMFSA8B:8;
A15: Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
Start-At 0 ,SCM+FSA c= Initialized Ig by FUNCT_4:26;
then Start-At 0 ,SCM+FSA c= (s +* (Initialized (Ig ';' J))) +* Ig by A15, XBOOLE_1:1;
then (s +* (Initialized (Ig ';' J))) +* Ig = ((s +* (Initialized (Ig ';' J))) +* Ig) +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:79
.= (s +* (Initialized (Ig ';' J))) +* (Ig +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15 ;
then A16: LifeSpan ((s +* (Initialized (Ig ';' J))) +* Ig) = LifeSpan (s +* (Initialized Ig)) by A1, A3, A6, A11, SCMFSA8C:101;
set JAt = J +* (Start-At 0 ,SCM+FSA );
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A17: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
(Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) . (intloc 0 ) = 1 by A3, A5, A6, SCMFSA8C:97;
then A18: (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) = (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (J +* (Start-At 0 ,SCM+FSA )) by SCMFSA8C:18;
set m3 = LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J));
set ps = s | NAT ;
A19: dom (s | NAT ) = (dom s) /\ NAT by RELAT_1:90
.= (((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) \/ NAT ) /\ NAT by SCMFSA6A:34
.= NAT by XBOOLE_1:21 ;
Ig ';' J is_halting_on Initialize s by A1, A2, A3, A4, Th4;
then A20: ProgramPart (s +* (Initialized (Ig ';' J))) halts_on s +* (Initialized (Ig ';' J)) by A10, SCMFSA7B:def 8;
A21: IExec (Ig ';' J),s = (Result (s +* (Initialized (Ig ';' J)))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(LifeSpan (s +* (Initialized (Ig ';' J))))) +* (s | NAT ) by A20, AMI_1:122
.= (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(((LifeSpan (s +* (Initialized Ig))) + 1) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) +* (s | NAT ) by A1, A2, A3, A4, A9, Th6 ;
A22: DataPart (IExec Ig,s) = DataPart ((Result (s +* (Initialized Ig))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized Ig))) by A17, FUNCT_4:94, SCMFSA_2:127
.= DataPart (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) by A8, AMI_1:122 ;
then J is_halting_on Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig))) by A2, A4, SCMFSA8B:8;
then A23: ProgramPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) halts_on (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) by A18, SCMFSA7B:def 8;
set IEJIs = IExec J,(IExec Ig,s);
set IAt = Ig +* (Start-At 0 ,SCM+FSA );
A24: Ig +* (Start-At 0 ,SCM+FSA ) c= s +* (Initialized Ig) by FUNCT_4:26, SCMFSA6B:8;
A25: J +* (Start-At 0 ,SCM+FSA ) c= (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
DataPart (IExec Ig,s) = DataPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by A18, A22, SCMFSA8A:11;
then A26: J is_closed_on (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J) by A4, SCMFSA8B:6;
A27: Initialized (Ig ';' J) c= s +* (Initialized (Ig ';' J)) by FUNCT_4:26;
(IExec Ig,s) . (intloc 0 ) = 1 by A1, A3, SCMFSA8C:96;
then A28: (IExec Ig,s) +* (Initialized J) = (IExec Ig,s) +* (J +* (Start-At 0 ,SCM+FSA )) by SCMFSA8C:18;
then A29: IC (Result ((Result (s +* (Initialized Ig))) +* (Initialized J))) = IC (Result ((IExec Ig,s) +* (Initialized J))) by A2, A4, A18, A22, A9, AMI_1:121, SCMFSA8C:101;
Result ((IExec Ig,s) +* (Initialized J)), Result ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) equal_outside NAT by A2, A4, A18, A22, A28, SCMFSA8C:101;
then A30: (Result ((IExec Ig,s) +* (Initialized J))) +* (s | NAT ) = (Result ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))) +* (s | NAT ) by A19, FUNCT_7:108;
(IExec Ig,s) | NAT = ((Result (s +* (Initialized Ig))) +* (s | NAT )) | NAT by SCMFSA6B:def 1
.= s | NAT by PBOOLE:157 ;
then A31: IExec J,(IExec Ig,s) = (Result ((IExec Ig,s) +* (Initialized J))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))),((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) +* (s | NAT ) by A23, A30, AMI_1:122 ;
A32: Ig is_halting_on s +* (Initialized (Ig ';' J)) by A1, A3, A11, SCMFSA8B:8;
reconsider l = (IC (IExec J,(IExec Ig,s))) + (card Ig) as Element of NAT ;
A33: (s +* (Initialized Ig)) +* (Ig ';' J) = s +* ((Initialized Ig) +* (Ig ';' J)) by FUNCT_4:15
.= s +* (Initialized (Ig ';' J)) by SCMFSA6A:58 ;
Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
then A34: Ig +* (Start-At 0 ,SCM+FSA ) c= (s +* (Initialized (Ig ';' J))) +* Ig by SCMFSA6B:8;
DataPart (s +* (Initialized (Ig ';' J))) = DataPart ((s +* (Initialized (Ig ';' J))) +* Ig) by SCMFSA8C:34;
then A35: Ig is_closed_on (s +* (Initialized (Ig ';' J))) +* Ig by A3, A11, SCMFSA8B:6;
A36: dom (Start-At l,SCM+FSA ) = {(IC SCM+FSA )} by FUNCOP_1:19;
X: Ig +* (Ig ';' J) = Ig ';' J by SCMFSA6A:57;
X1: ((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J) = (s +* (Initialized (Ig ';' J))) +* (Ig +* (Ig ';' J)) by FUNCT_4:15;
X2: (s +* (Initialized (Ig ';' J))) +* (Ig ';' J) = s +* ((Initialized (Ig ';' J)) +* (Ig ';' J)) by FUNCT_4:15;
Ig ';' J c= Initialized (Ig ';' J) by SCMFSA6A:26;
then X3: (Initialized (Ig ';' J)) +* (Ig ';' J) = Initialized (Ig ';' J) by LATTICE2:8;
Start-At 0 ,SCM+FSA c= Initialized (Ig ';' J) by SCMFSA6B:4;
then Start-At 0 ,SCM+FSA c= s +* (Initialized (Ig ';' J)) by A27, XBOOLE_1:1;
then (s +* (Initialized (Ig ';' J))) +* Ig = ((s +* (Initialized (Ig ';' J))) +* (Start-At 0 ,SCM+FSA )) +* Ig by FUNCT_4:79
.= ((s +* (Initialized (Ig ';' J))) +* Ig) +* (Start-At 0 ,SCM+FSA ) by SCMFSA6B:14
.= (s +* (Initialized (Ig ';' J))) +* (Ig +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15 ;
then ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig) halts_on (s +* (Initialized (Ig ';' J))) +* Ig by A32, SCMFSA7B:def 8;
then DataPart (Comput (ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) = DataPart (Comput (ProgramPart (((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J))),(((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J)),(LifeSpan (s +* (Initialized Ig)))) by A35, A34, A16, Th5, SCMFSA6A:39
.= DataPart (Comput (ProgramPart ((s +* (Initialized (Ig ';' J))) +* (Ig +* (Ig ';' J)))),((s +* (Initialized (Ig ';' J))) +* (Ig +* (Ig ';' J))),(LifeSpan (s +* (Initialized Ig)))) by X1
.= DataPart (Comput (ProgramPart ((s +* (Initialized (Ig ';' J))) +* (Ig ';' J))),((s +* (Initialized (Ig ';' J))) +* (Ig ';' J)),(LifeSpan (s +* (Initialized Ig)))) by X
.= DataPart (Comput (ProgramPart (s +* ((Initialized (Ig ';' J)) +* (Ig ';' J)))),(s +* ((Initialized (Ig ';' J)) +* (Ig ';' J))),(LifeSpan (s +* (Initialized Ig)))) by X2
.= DataPart (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(LifeSpan (s +* (Initialized Ig)))) by X3
.= DataPart (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) by A8, A7, A24, A33, Th5, SCMFSA6A:39 ;
then A37: DataPart ((Comput (ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) = (DataPart (Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by FUNCT_4:75 ;
A38: Ig is_closed_on s +* (Initialized (Ig ';' J)) by A3, A11, SCMFSA8B:6;
A39: J is_halting_on IExec Ig,(s +* (Initialized (Ig ';' J))) by A2, A4, A13, SCMFSA8B:8;
then A40: DataPart (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) = DataPart ((Comput (ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)) by A27, A38, A32, A16, A12, A14, Lm1;
A41: ProgramPart (Relocated J,(card Ig)) c= Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1) by A27, A38, A32, A16, A12, A14, A39, Lm1;
T: ProgramPart (s +* (Initialized (Ig ';' J))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) by AMI_1:144;
A42: IC (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)) = card Ig by A27, A38, A32, A16, A12, A14, A39, Lm1;
then A43: DataPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1))),(Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) = DataPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))),((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) by A26, A37, A40, A41, A25, SCMFSA8C:42;
A44: dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations by A19, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A45: DataPart (IExec (Ig ';' J),s) = DataPart (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(((LifeSpan (s +* (Initialized Ig))) + 1) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) by A21, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))),((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) by A43, AMI_1:51, T
.= DataPart (IExec J,(IExec Ig,s)) by A31, A44, FUNCT_4:76, SCMFSA_2:127 ;
A46: IC (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1))),(Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan (s +* (Initialized Ig))) + 1)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) = (IC (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))),((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) + (card Ig) by A26, A37, A42, A40, A41, A25, SCMFSA8C:42;
A47: IC (IExec (Ig ';' J),s) = IC (Result (s +* (Initialized (Ig ';' J)))) by SCMFSA8A:7
.= IC (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(LifeSpan (s +* (Initialized (Ig ';' J))))) by A20, AMI_1:122
.= IC (Comput (ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(((LifeSpan (s +* (Initialized Ig))) + 1) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) by A1, A2, A3, A4, A9, Th6
.= (IC (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))),((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)),(LifeSpan ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J))))) + (card Ig) by A46, AMI_1:51, T
.= (IC (Result ((Comput (ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan (s +* (Initialized Ig)))) +* (Initialized J)))) + (card Ig) by A23, AMI_1:122
.= (IC (Result ((Result (s +* (Initialized Ig))) +* (Initialized J)))) + (card Ig) by A8, AMI_1:122
.= (IC (IExec J,(IExec Ig,s))) + (card Ig) by A29, SCMFSA8A:7 ;

A48: now

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

per cases by A49, SCMFSA6A:35;

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

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

end;

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

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

end;

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

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

end;

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

then x <> IC SCM+FSA by AMI_1:48;
then A57: not x in dom (Start-At l,SCM+FSA ) by A36, TARSKI:def 1;
(IExec (Ig ';' J),s) | NAT = s | NAT by A21, PBOOLE:157
.= (IExec J,(IExec Ig,s)) | NAT by A31, PBOOLE:157 ;
then (IExec (Ig ';' J),s) . x = (IExec J,(IExec Ig,s)) . x by A56, SCMFSA6A:36;
hence (IExec (Ig ';' J),s) . x = ((IExec J,(IExec Ig,s)) +* (Start-At ((IC (IExec J,(IExec Ig,s))) + (card Ig)),SCM+FSA )) . x by A57, FUNCT_4:12; :: thesis:

end;

end;

end;

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