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 +* (Initialize ((intloc 0) .--> 1));
set p1 = p +* Ig;
A6: Ig c= p +* Ig by FUNCT_4:26;
set m1 = LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))));
s +* (Initialize ((intloc 0) .--> 1)) = (Initialized s) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:99;
then A10: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by A5, SCMFSA8C:18;
DataPart (Initialized s) = DataPart (s +* (Initialize ((intloc 0) .--> 1))) ;
then A11: Ig is_closed_on s +* (Initialize ((intloc 0) .--> 1)),p +* Ig by A3, SCMFSA8B:6;
set s3 = Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))));
set p3 = (p +* Ig) +* J;
A12: J c= (p +* Ig) +* J by FUNCT_4:26;
A13: p +* Ig halts_on s +* (Initialize ((intloc 0) .--> 1)) by A1, A10, SCMFSA7B:def 8;
then A14: Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) = Initialized (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) by EXTPRO_1:23;
set s2 = Initialized s;
set p2 = p +* (Ig ';' J);
A15: Ig ';' J c= p +* (Ig ';' J) by FUNCT_4:26;
Initialized s = Initialized (Initialized s) by FUNCT_4:99;
then A16: Initialized s = Initialize (Initialized s) by A5, SCMFSA8C:18;
A17: DataPart (Initialized s) = DataPart (Initialized s) ;
A18: (Initialized s) . (intloc 0) = 1 by A5;
A19: DataPart (IExec (Ig,p,s)) = DataPart (IExec (Ig,p,(Initialized s))) by SCMFSA8C:17
.= DataPart (IExec (Ig,(p +* (Ig ';' J)),(Initialized s))) by A1, A3, A5, A17, SCMFSA8C:46 ;
then A20: J is_closed_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J) by A2, A4, SCMFSA8B:8;
Initialized s = Initialize (Initialized s) by SCMFSA6A:83;
then A22: LifeSpan (((p +* (Ig ';' J)) +* Ig),(Initialized s)) = LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))) by A1, A3, A17, SCMFSA8C:101;
set JAt = Start-At (0,SCM+FSA);
(Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) = 1 by A3, A5, A10, SCMFSA8C:97;
then A23: Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) = Initialize (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by SCMFSA8C:18;
set m3 = LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))));
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 Initialized s by A16, SCMFSA7B:def 8;
A26: IExec ((Ig ';' J),p,s) = (Result ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((p +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* (Ig ';' J)),(Initialized s))))) +* (s | NAT) by A25, EXTPRO_1:23
.= (Comput ((p +* (Ig ';' J)),(Initialized s),(((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))))))))) +* (s | NAT) by A1, A2, A3, A4, A14, Th6 ;
A27: DataPart (IExec (Ig,p,s)) = DataPart ((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) by COMPOS_1:82
.= DataPart (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by A13, EXTPRO_1:23 ;
then J is_halting_on Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))),p +* Ig by A2, A4, SCMFSA8B:8;
then A28: (p +* Ig) +* J halts_on Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by A23, SCMFSA7B:def 8;
set IEJIs = IExec (J,p,(IExec (Ig,p,s)));
set IAt = Start-At (0,SCM+FSA);
A29: Start-At (0,SCM+FSA) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26, SCMFSA6B:8;
A30: Start-At (0,SCM+FSA) c= Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by FUNCT_4:26, SCMFSA6B:8;
DataPart (IExec (Ig,p,s)) = DataPart (Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))) by A23, A27, SCMFSA8A:10;
then A31: J is_closed_on Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))),(p +* Ig) +* J by A4, SCMFSA8B:6;
A32: Initialize ((intloc 0) .--> 1) c= Initialized s by FUNCT_4:26;
(IExec (Ig,p,s)) . (intloc 0) = 1 by A1, A3, SCMFSA8C:96;
then A33: (IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1)) = Initialize (IExec (Ig,p,s)) by SCMFSA8C:18;
then NPP (Result (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1))))) by A2, A4, A23, A27, A14, SCMFSA8C:101;
then A34: IC (Result (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) = IC (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1))))) by COMPOS_1:230;
NPP (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))) by A2, A4, A23, A27, A33, SCMFSA8C:101;
then A35: (Result ((p +* J),((IExec (Ig,p,s)) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) = (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))) +* (s | NAT) by A24, COMPOS_1:238;
(IExec (Ig,p,s)) | NAT = ((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (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)) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))))) +* (s | NAT) by A28, A35, EXTPRO_1:23 ;
A37: Ig is_halting_on Initialized s,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 ;
Initialized s = Initialize (s +* ((intloc 0) .--> 1)) by FUNCT_4:15;
then Start-At (0,SCM+FSA) c= Initialized s by FUNCT_4:26;
then A39: Start-At (0,SCM+FSA) c= Initialized s ;
DataPart (Initialized s) = DataPart (Initialized s) ;
then A40: Ig is_closed_on Initialized s,(p +* (Ig ';' J)) +* Ig by A3, SCMFSA8B:6;
A41: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
A42: Ig +* (Ig ';' J) = Ig ';' J by SCMFSA6A:57;
A44: ((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J) = (p +* (Ig ';' J)) +* (Ig +* (Ig ';' J)) by FUNCT_4:15;
A48: Ig c= (p +* (Ig ';' J)) +* Ig by FUNCT_4:26;
A49: (p +* Ig) +* (Ig ';' J) = p +* (Ig ';' J) by A42, FUNCT_4:15;
EO: NPP (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((p +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by A13, A11, A29, Th5, A6, A49;
Initialized s = Initialize (Initialized s) by SCMFSA6A:83;
then (p +* (Ig ';' J)) +* Ig halts_on Initialized s by A37, SCMFSA7B:def 8;
then NPP (Comput (((p +* (Ig ';' J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by A40, A39, A22, Th5, A48;
then DataPart (Comput (((p +* (Ig ';' J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput ((((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by COMPOS_1:138
.= DataPart (Comput ((((p +* (Ig ';' J)) +* Ig) +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))
.= DataPart (Comput (((p +* (Ig ';' J)) +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by A42, A44
.= DataPart (Comput ((p +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by FUNCT_4:99
.= DataPart (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) by EO, COMPOS_1:138 ;
then A50: DataPart ((Comput (((p +* (Ig ';' J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) = (DataPart (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:75
.= DataPart ((Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:75 ;
A51: Ig is_closed_on Initialized s,p +* (Ig ';' J) by A3, A17, SCMFSA8B:6;
A52: J is_halting_on IExec (Ig,(p +* (Ig ';' J)),(Initialized s)),p +* (Ig ';' J) by A2, A4, A19, SCMFSA8B:8;
then A53: DataPart (Comput ((p +* (Ig ';' J)),(Initialized s),((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart (Initialized (Comput (((p +* (Ig ';' J)) +* Ig),(Initialized s),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))) 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)),(Initialized s),((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card Ig by A32, A51, A37, A22, A18, A20, A52, Lm1, A15;
then A56: DataPart (Comput ((p +* (Ig ';' J)),(Comput ((p +* (Ig ';' J)),(Initialized s),((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))))) = DataPart (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))))) by A31, A50, A53, A30, A12, A54, SCMFSA8C:42;
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)),(Initialized s),(((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))))))))) by A26, FUNCT_4:76
.= DataPart (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))))) 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)),(Initialized s),((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))))))) = (IC (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))))))))) + (card Ig) by A31, A50, A55, A53, A30, A12, A54, SCMFSA8C:42;
A60: Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))) = (Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) by A13, EXTPRO_1:23;
A61: IC (IExec ((Ig ';' J),p,s)) = IC (Result ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1))))) by SCMFSA8A:7
.= IC (Comput ((p +* (Ig ';' J)),(Initialized s),(LifeSpan ((p +* (Ig ';' J)),(Initialized s))))) by A25, EXTPRO_1:23
.= IC (Comput ((p +* (Ig ';' J)),(Initialized s),(((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))))))))) by A1, A2, A3, A4, A14, Th6
.= (IC (Comput (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1)))))))),(LifeSpan (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))))))))) + (card Ig) by A59, EXTPRO_1:5
.= (IC (Result (((p +* Ig) +* J),(Initialized (Comput ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))))))))) + (card Ig) by A28, EXTPRO_1:23
.= (IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig) by A34, A60, 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, COMPOS_1:127;
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: