let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
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 I = Ig;
assume that
A1: Ig is_halting_on Initialized s,p and
A2: J is_halting_on IExec (Ig,p,s),p and
A3: Ig is_closed_on Initialized s,p and
A4: J is_closed_on IExec (Ig,p,s),p ; :: thesis:
set Is = Initialized s;
set Ip = p;
A5: (Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
set s1 = s +* (Initialized Ig);
set p1 = p +* Ig;
A6: Ig c= p +* Ig by FUNCT_4:26;
set m1 = LifeSpan ((p +* Ig),(s +* (Initialized Ig)));
A7: ProgramPart J = J by RELAT_1:209;
A8: ProgramPart (Ig ';' J) = Ig ';' J by RELAT_1:209;
A9: ProgramPart Ig = Ig by RELAT_1:209;
s +* (Initialized Ig) = (Initialized s) +* (Initialized Ig) by SCMFSA8A:8;
then A10: s +* (Initialized Ig) = (Initialized s) +* (Initialize Ig) by A5, SCMFSA8C:18;
then DataPart (Initialized s) = DataPart (s +* (Initialized Ig)) by SCMFSA8A:11;
then A11: Ig is_closed_on s +* (Initialized Ig),p +* Ig by A3, SCMFSA8B:6;
set s3 = (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J);
set p3 = (p +* Ig) +* J;
A12: J c= (p +* Ig) +* J by FUNCT_4:26;
A13: p +* Ig halts_on s +* (Initialized Ig) by A1, A10, SCMFSA7B:def 8, A9;
then A14: (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) = (Result ((p +* Ig),(s +* (Initialized Ig)))) +* (Initialized J) by EXTPRO_1:23;
set s2 = s +* (Initialized (Ig ';' J));
set p2 = p +* (Ig ';' J);
A15: Ig ';' J c= p +* (Ig ';' J) by FUNCT_4:26;
s +* (Initialized (Ig ';' J)) = (Initialized s) +* (Initialized (Ig ';' J)) by SCMFSA8A:8;
then A16: s +* (Initialized (Ig ';' J)) = (Initialized s) +* (Initialize (Ig ';' J)) by A5, SCMFSA8C:18;
then A17: DataPart (Initialized s) = DataPart (s +* (Initialized (Ig ';' J))) by SCMFSA8A:11;
then A18: (s +* (Initialized (Ig ';' J))) . (intloc 0) = 1 by A5, SCMFSA6A:38;
A19: DataPart (IExec (Ig,p,s)) = DataPart (IExec (Ig,p,(Initialized s))) by SCMFSA8C:17
.= DataPart (IExec (Ig,(p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))))) by A1, A3, A5, A17, SCMFSA8C:46 ;
then A20: J is_closed_on IExec (Ig,(p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J)))),p +* (Ig ';' J) by A2, A4, SCMFSA8B:8;
A21: Initialized Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by FUNCT_4:26, SCMFSA6A:52;
Initialized Ig = Initialize (Ig +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then 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 A21, XBOOLE_1:1;
then (s +* (Initialized (Ig ';' J))) +* Ig = Initialize ((s +* (Initialized (Ig ';' J))) +* Ig) by FUNCT_4:79
.= (s +* (Initialized (Ig ';' J))) +* (Initialize Ig) by FUNCT_4:15 ;
then A22: LifeSpan (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig)) = LifeSpan ((p +* Ig),(s +* (Initialized Ig))) by A1, A3, A10, A17, SCMFSA8C:101;
set JAt = Initialize J;
(Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) . (intloc 0) = 1 by A3, A5, A10, SCMFSA8C:97;
then A23: (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) = (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialize J) by SCMFSA8C:18;
set m3 = LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)));
set ps = s | NAT;
A24: dom (s | NAT) = (dom s) /\ NAT by RELAT_1:90
.= the carrier of SCM+FSA /\ NAT by PARTFUN1:def 4
.= (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) /\ NAT by COMPOS_1:160
.= NAT by XBOOLE_1:21 ;
Ig ';' J is_halting_on Initialized s,p by A1, A2, A3, A4, Th4;
then A25: p +* (Ig ';' J) halts_on s +* (Initialized (Ig ';' J)) by A16, SCMFSA7B:def 8, A8;
A26: IExec ((Ig ';' J),p,s) = (Result ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),(LifeSpan ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))))))) +* (s | NAT) by A25, EXTPRO_1:23
.= (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),(((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1) + (LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))))))) +* (s | NAT) by A1, A2, A3, A4, A14, Th6 ;
A27: DataPart (IExec (Ig,p,s)) = DataPart ((Result ((p +* Ig),(s +* (Initialized Ig)))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((p +* Ig),(s +* (Initialized Ig)))) by COMPOS_1:82
.= DataPart (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A13, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig))))),p +* Ig by A2, A4, SCMFSA8B:8;
then A28: (p +* Ig) +* J halts_on (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) by A23, SCMFSA7B:def 8, A7;
set IEJIs = IExec (J,p,(IExec (Ig,p,s)));
set IAt = Initialize Ig;
A29: Initialize Ig c= s +* (Initialized Ig) by FUNCT_4:26, SCMFSA6B:8;
A30: Initialize J c= (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) by FUNCT_4:26, SCMFSA6B:8;
DataPart (IExec (Ig,p,s)) = DataPart ((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) by A23, A27, SCMFSA8A:11;
then A31: J is_closed_on (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J),(p +* Ig) +* J by A4, SCMFSA8B:6;
A32: Initialized (Ig ';' J) c= s +* (Initialized (Ig ';' J)) by FUNCT_4:26;
(IExec (Ig,p,s)) . (intloc 0) = 1 by A1, A3, SCMFSA8C:96;
then A33: (IExec (Ig,p,s)) +* (Initialized J) = (IExec (Ig,p,s)) +* (Initialize J) by SCMFSA8C:18;
then A34: IC (Result (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialized Ig)))) +* (Initialized J)))) = IC (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialized J)))) by A2, A4, A23, A27, A14, COMPOS_1:24, SCMFSA8C:101;
Result ((p +* J),((IExec (Ig,p,s)) +* (Initialized J))), Result (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))) equal_outside NAT by A2, A4, A23, A27, A33, SCMFSA8C:101;
then A35: (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialized J)))) +* (s | NAT) = (Result (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)))) +* (s | NAT) by A24, FUNCT_7:108;
(IExec (Ig,p,s)) | NAT = ((Result ((p +* Ig),(s +* (Initialized Ig)))) +* (s | NAT)) | NAT by SCMFSA6B:def 1
.= s | NAT by PBOOLE:157 ;
then A36: IExec (J,p,(IExec (Ig,p,s))) = (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialized J)))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)))))) +* (s | NAT) by A28, A35, EXTPRO_1:23 ;
A37: Ig is_halting_on s +* (Initialized (Ig ';' J)),p +* (Ig ';' J) by A1, A3, A17, SCMFSA8B:8;
reconsider l = (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) as Element of NAT ;
A38: (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 A39: Initialize Ig c= (s +* (Initialized (Ig ';' J))) +* Ig by SCMFSA6B:8;
DataPart (s +* (Initialized (Ig ';' J))) = DataPart ((s +* (Initialized (Ig ';' J))) +* Ig) by COMPOS_1:82;
then A40: Ig is_closed_on (s +* (Initialized (Ig ';' J))) +* Ig,(p +* (Ig ';' J)) +* Ig by A3, A17, SCMFSA8B:6;
A41: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
A42: Ig +* (Ig ';' J) = Ig ';' J by SCMFSA6A:57;
A43: ((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J) = (s +* (Initialized (Ig ';' J))) +* (Ig +* (Ig ';' J)) by FUNCT_4:15;
A44: ((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J) = (p +* (Ig ';' J)) +* (Ig +* (Ig ';' J)) by FUNCT_4:15;
A45: (s +* (Initialized (Ig ';' J))) +* (Ig ';' J) = s +* ((Initialized (Ig ';' J)) +* (Ig ';' J)) by FUNCT_4:15;
A46: (p +* (Ig ';' J)) +* (Ig ';' J) = p +* ((Ig ';' J) +* (Ig ';' J)) by FUNCT_4:15;
Ig ';' J c= Initialized (Ig ';' J) by SCMFSA6A:26;
then A47: (Initialized (Ig ';' J)) +* (Ig ';' J) = Initialized (Ig ';' J) by LATTICE2:8;
A48: Ig c= (p +* (Ig ';' J)) +* Ig by FUNCT_4:26;
A49: (p +* Ig) +* (Ig ';' J) = p +* (Ig ';' J) by A42, FUNCT_4:15;
Initialized (Ig ';' J) = Initialize ((Ig ';' J) +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then Start-At (0,SCM+FSA) c= Initialized (Ig ';' J) by FUNCT_4:26;
then Start-At (0,SCM+FSA) c= s +* (Initialized (Ig ';' J)) by A32, XBOOLE_1:1;
then (s +* (Initialized (Ig ';' J))) +* Ig = (Initialize (s +* (Initialized (Ig ';' J)))) +* Ig by FUNCT_4:79
.= Initialize ((s +* (Initialized (Ig ';' J))) +* Ig) by COMPOS_1:83
.= (s +* (Initialized (Ig ';' J))) +* (Initialize Ig) by FUNCT_4:15 ;
then (p +* (Ig ';' J)) +* Ig halts_on (s +* (Initialized (Ig ';' J))) +* Ig by A37, SCMFSA7B:def 8, A9;
then DataPart (Comput (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) = DataPart (Comput ((((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J)),(((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A40, A39, A22, Th5, COMPOS_1:138, A48
.= DataPart (Comput (((p +* (Ig ';' J)) +* (Ig +* (Ig ';' J))),((s +* (Initialized (Ig ';' J))) +* (Ig +* (Ig ';' J))),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A43, A44
.= DataPart (Comput (((p +* (Ig ';' J)) +* (Ig ';' J)),((s +* (Initialized (Ig ';' J))) +* (Ig ';' J)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A42
.= DataPart (Comput ((p +* ((Ig ';' J) +* (Ig ';' J))),(s +* ((Initialized (Ig ';' J)) +* (Ig ';' J))),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A45, A46
.= DataPart (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A47
.= DataPart (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) by A13, A11, A29, A38, Th5, COMPOS_1:138, A6, A49 ;
then A50: DataPart ((Comput (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) = (DataPart (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig))))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) by FUNCT_4:75 ;
A51: Ig is_closed_on s +* (Initialized (Ig ';' J)),p +* (Ig ';' J) by A3, A17, SCMFSA8B:6;
A52: J is_halting_on IExec (Ig,(p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J)))),p +* (Ig ';' J) by A2, A4, A19, SCMFSA8B:8;
then A53: DataPart (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1))) = DataPart ((Comput (((p +* (Ig ';' J)) +* Ig),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)) by A32, A51, A37, A22, A18, A20, Lm1, A15;
Reloc (J,(card Ig)) c= Ig ';' J by FUNCT_4:26;
then A54: Reloc (J,(card Ig)) c= p +* (Ig ';' J) by A15, XBOOLE_1:1;
A55: IC (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1))) = card Ig by A32, A51, A37, A22, A18, A20, A52, Lm1, A15;
then A56: DataPart (Comput ((p +* (Ig ';' J)),(Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1))),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)))))) = DataPart (Comput (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)))))) by A31, A50, A53, A30, SCMFSA8C:42, A12, A54;
A57: dom (s | NAT) misses Data-Locations SCM+FSA by A24, COMPOS_1:51;
then A58: DataPart (IExec ((Ig ';' J),p,s)) = DataPart (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),(((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1) + (LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))))))) by A26, FUNCT_4:76
.= DataPart (Comput (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)))))) by A56, EXTPRO_1:5
.= DataPart (IExec (J,p,(IExec (Ig,p,s)))) by A36, A57, FUNCT_4:76 ;
A59: IC (Comput ((p +* (Ig ';' J)),(Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1))),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)))))) = (IC (Comput (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))))))) + (card Ig) by A31, A50, A55, A53, A30, SCMFSA8C:42, A12, A54;
A60: (Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J) = (Result ((p +* Ig),(s +* (Initialized Ig)))) +* (Initialized J) by A13, EXTPRO_1:23;
A61: IC (IExec ((Ig ';' J),p,s)) = IC (Result ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))))) by SCMFSA8A:7
.= IC (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),(LifeSpan ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))))))) by A25, EXTPRO_1:23
.= IC (Comput ((p +* (Ig ';' J)),(s +* (Initialized (Ig ';' J))),(((LifeSpan ((p +* Ig),(s +* (Initialized Ig)))) + 1) + (LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))))))) by A1, A2, A3, A4, A14, Th6
.= (IC (Comput (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))))))) + (card Ig) by A59, EXTPRO_1:5
.= (IC (Result (((p +* Ig) +* J),((Comput ((p +* Ig),(s +* (Initialized Ig)),(LifeSpan ((p +* Ig),(s +* (Initialized Ig)))))) +* (Initialized J))))) + (card Ig) by A28, EXTPRO_1:23
.= (IC (Result (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialized Ig)))) +* (Initialized J))))) + (card Ig) by A60
.= (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) by A34, SCMFSA8A:7 ;

A62: now

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

per cases by A63, SCMFSA6A:35;

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

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

end;

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

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

end;

suppose A68: x = IC ; :: thesis:

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

end;

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

then x <> IC by COMPOS_1:3;
then A71: not x in dom (Start-At (l,SCM+FSA)) by A41, TARSKI:def 1;
(IExec ((Ig ';' J),p,s)) | NAT = s | NAT by A26, PBOOLE:157
.= (IExec (J,p,(IExec (Ig,p,s)))) | NAT by A36, PBOOLE:157 ;
then (IExec ((Ig ';' J),p,s)) . x = (IExec (J,p,(IExec (Ig,p,s)))) . x by A70, SCMFSA6A:36;
hence (IExec ((Ig ';' J),p,s)) . x = ((IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))) . x by A71, FUNCT_4:12; :: thesis:

end;

end;

end;

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