let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds IExec ((I ';' J),p,s) = (IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting Program of SCM+FSA holds IExec ((I ';' J),p,s) = (IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))
set D = Data-Locations SCM+FSA;
set A = NAT ;
let I be InitHalting keepInt0_1 Program of SCM+FSA; :: thesis: for J being InitHalting Program of SCM+FSA holds IExec ((I ';' J),p,s) = (IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))
let J be InitHalting Program of SCM+FSA; :: thesis: IExec ((I ';' J),p,s) = (IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))
set ps = s | NAT;
set s1 = s +* (Initialized I);
set p1 = p +* I;
A1: I c= p +* I by FUNCT_4:26;
set s2 = s +* (Initialized (I ';' J));
set p2 = p +* (I ';' J);
A2: I ';' J c= p +* (I ';' J) by FUNCT_4:26;
set s3 = (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J);
set p3 = (p +* I) +* J;
A3: Initialized J c= (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) by FUNCT_4:26;
A4: J c= (p +* I) +* J by FUNCT_4:26;
set m1 = LifeSpan ((p +* I),(s +* (Initialized I)));
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)));
A5: Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
A6: I ';' J c= p +* (I ';' J) by FUNCT_4:26;
s +* (Initialized (I ';' J)) = s +* ((I ';' J) +* (Initialize ((intloc 0) .--> 1))) by FUNCT_4:15
.= (s +* (I ';' J)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15 ;
then A7: Initialize ((intloc 0) .--> 1) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
A8: (s +* (Initialized I)) +* (I ';' J) = s +* ((Initialized I) +* (I ';' J)) by FUNCT_4:15
.= s +* (Initialized (I ';' J)) by SCMFSA6A:58 ;
A9: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
I c= p +* I by FUNCT_4:26;
then A10: p +* I halts_on s +* (Initialized I) by Th5, A9;
A11: Initialized J c= (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) by FUNCT_4:26;
A12: (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized J) equal_outside dom (s | NAT) by FUNCT_7:31, FUNCT_7:106;
then A13: ((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized J),(Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) equal_outside dom (s | NAT) by FUNCT_7:28;
A14: ( IExec (I,p,s) = (Result ((p +* I),(s +* (Initialized I)))) +* (s | NAT) & Initialized J c= (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) ) by FUNCT_4:26, SCMFSA6B:def 1;
A15: dom (s | NAT) = (dom s) /\ NAT by RELAT_1:90
.= (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) /\ NAT by COMPOS_1:172
.= NAT by XBOOLE_1:21 ;
A16: Initialized J c= (IExec (I,p,s)) +* (Initialized J) by FUNCT_4:26;
A17: J c= p +* J by FUNCT_4:26;
A18: ( Initialized J c= (IExec (I,p,s)) +* (Initialized J) & Initialized J c= (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) ) by FUNCT_4:26;
A19: ( J c= p +* J & J c= (p +* I) +* J ) by FUNCT_4:26;
A20: Initialized J c= (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) by FUNCT_4:26;
A21: Initialized I c= s +* (Initialized I) by FUNCT_4:26;
A22: I c= p +* I by FUNCT_4:26;
A23: (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) = (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) by A21, Th5, EXTPRO_1:23, A22;
Result ((p +* I),(s +* (Initialized I))) = Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I))))) by A21, Th5, EXTPRO_1:23, A1;
then A24: IC (Result (((p +* I) +* J),((Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J)))) = IC (Result ((p +* J),((IExec (I,p,s)) +* (Initialized J)))) by A15, A12, A14, A16, Th15, COMPOS_1:24, A17, A4;
A25: Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26, SCMFSA6A:52;
A26: I c= (p +* (I ';' J)) +* I by FUNCT_4:26;
( 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 A27: LifeSpan (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I)) = LifeSpan ((p +* I),(s +* (Initialized I))) by A21, A25, Th15, A22, A26;
then A28: Reloc (J,(card I)) c= Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1)) by A5, Th25, A6;
Reloc (J,(card I)) c= I ';' J by FUNCT_4:26;
then A29: Reloc (J,(card I)) c= p +* (I ';' J) by A2, XBOOLE_1:1;
A30: I +* (I ';' J) = I ';' J by SCMFSA6A:57;
A31: ((s +* (Initialized (I ';' J))) +* I) +* (I ';' J) = (s +* (Initialized (I ';' J))) +* (I +* (I ';' J)) by FUNCT_4:15;
A32: (s +* (Initialized (I ';' J))) +* (I ';' J) = s +* ((Initialized (I ';' J)) +* (I ';' J)) by FUNCT_4:15;
A33: (Initialized (I ';' J)) +* (I ';' J) = Initialized (I ';' J) by LATTICE2:8, SCMFSA6A:26;
(s +* (Initialized (I ';' J))) +* (I +* (Initialize ((intloc 0) .--> 1))) = ((s +* (Initialized (I ';' J))) +* I) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:15
.= ((s +* (Initialized (I ';' J))) +* (Initialize ((intloc 0) .--> 1))) +* I by Th19
.= (s +* (Initialized (I ';' J))) +* I by A7, FUNCT_4:79 ;
then I +* (Initialize ((intloc 0) .--> 1)) c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:26;
then A34: Initialized I c= (s +* (Initialized (I ';' J))) +* I by FUNCT_4:15;
A35: ((p +* (I ';' J)) +* I) +* (I ';' J) = (p +* (I ';' J)) +* (I +* (I ';' J)) by FUNCT_4:15
.= (p +* (I ';' J)) +* (I ';' J) by SCMFSA6A:57
.= p +* (I ';' J) by FUNCT_4:99
.= p +* (I +* (I ';' J)) by SCMFSA6A:57
.= (p +* I) +* (I ';' J) by FUNCT_4:15 ;
A36: Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I))))), Comput ((((p +* (I ';' J)) +* I) +* (I ';' J)),((s +* (Initialized (I ';' J))) +* (I +* (I ';' J))),(LifeSpan ((p +* I),(s +* (Initialized I))))) equal_outside NAT by A21, A10, A8, Th18, A33, A32, A30, A1, A35;
I c= (p +* (I ';' J)) +* I by FUNCT_4:26;
then (p +* (I ';' J)) +* I halts_on (s +* (Initialized (I ';' J))) +* I by Th5, A34;
then DataPart (Comput (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((p +* I),(s +* (Initialized I)))))) = DataPart (Comput ((((p +* (I ';' J)) +* I) +* (I ';' J)),((s +* (Initialized (I ';' J))) +* (I +* (I ';' J))),(LifeSpan ((p +* I),(s +* (Initialized I)))))) by A31, A25, A27, Th18, COMPOS_1:138, A26
.= DataPart (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) by COMPOS_1:138, A36 ;
then A37: DataPart ((Comput (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)) = (DataPart (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I))))))) +* (DataPart (Initialized J)) by FUNCT_4:75
.= DataPart ((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)) by FUNCT_4:75 ;
A38: ( IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1))) = DataPart ((Comput (((p +* (I ';' J)) +* I),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)) ) by A5, A27, Th25, A6;
then A39: DataPart (Comput ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) = DataPart (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) by A28, A11, A37, Th12, A4, A29;
A40: IC (Comput ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) = (IC (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I) by A38, A28, A11, A37, Th12, A4, A29;
A41: Initialized (I ';' J) c= s +* (Initialized (I ';' J)) by FUNCT_4:26;
I ';' J c= p +* (I ';' J) by FUNCT_4:26;
then A42: p +* (I ';' J) halts_on s +* (Initialized (I ';' J)) by Th5, A41;
A43: IExec ((I ';' J),p,s) = (Result ((p +* (I ';' J)),(s +* (Initialized (I ';' J))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((p +* (I ';' J)),(s +* (Initialized (I ';' J))))))) +* (s | NAT) by A42, EXTPRO_1:23
.= (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) +* (s | NAT) by A23, Th28 ;
IExec (I,p,s) = (Result ((p +* I),(s +* (Initialized I)))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (s | NAT) by A21, Th5, EXTPRO_1:23, A1 ;
then Result ((p +* J),((IExec (I,p,s)) +* (Initialized J))), Result (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))) equal_outside NAT by A15, A13, A18, Th15, A19;
then A44: (Result ((p +* J),((IExec (I,p,s)) +* (Initialized J)))) +* (s | NAT) = (Result (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)))) +* (s | NAT) by A15, FUNCT_7:108;
A45: (p +* I) +* J halts_on (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) by Th5, A3, A4;
(IExec (I,p,s)) | NAT = ((Result ((p +* I),(s +* (Initialized I)))) +* (s | NAT)) | NAT by SCMFSA6B:def 1
.= s | NAT by PBOOLE:157 ;
then A46: IExec (J,p,(IExec (I,p,s))) = (Result ((p +* J),((IExec (I,p,s)) +* (Initialized J)))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) +* (s | NAT) by A44, A45, EXTPRO_1:23 ;
A47: dom (s | NAT) misses Data-Locations SCM+FSA by A15, COMPOS_1:51;
then A48: DataPart (IExec ((I ';' J),p,s)) = DataPart (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) by A43, FUNCT_4:76
.= DataPart (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)))))) by A39, EXTPRO_1:5
.= DataPart (IExec (J,p,(IExec (I,p,s)))) by A46, A47, FUNCT_4:76 ;
A49: (Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J) = (Result ((p +* I),(s +* (Initialized I)))) +* (Initialized J) by A21, Th5, EXTPRO_1:23, A1;
A50: IC (IExec ((I ';' J),p,s)) = IC (Result ((p +* (I ';' J)),(s +* (Initialized (I ';' J))))) by SCMFSA8A:7
.= IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(LifeSpan ((p +* (I ';' J)),(s +* (Initialized (I ';' J))))))) by A5, Th5, EXTPRO_1:23, A2
.= IC (Comput ((p +* (I ';' J)),(s +* (Initialized (I ';' J))),(((LifeSpan ((p +* I),(s +* (Initialized I)))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) by A23, Th28
.= (IC (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I) by A40, EXTPRO_1:5
.= (IC (Result (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialized I)),(LifeSpan ((p +* I),(s +* (Initialized I)))))) +* (Initialized J))))) + (card I) by A20, Th5, EXTPRO_1:23, A4
.= (IC (IExec (J,p,(IExec (I,p,s))))) + (card I) by A24, A49, SCMFSA8A:7 ;
hereby :: thesis: verum
reconsider l = (IC (IExec (J,p,(IExec (I,p,s))))) + (card I) as Element of NAT ;
A51: dom (Start-At (l,SCM+FSA)) = {(IC )} by FUNCOP_1:19;
A52: now
let x be set ; :: thesis: ( x in dom (IExec ((I ';' J),p,s)) implies (IExec ((I ';' J),p,s)) . b1 = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . b1 )
assume A53: x in dom (IExec ((I ';' J),p,s)) ; :: thesis: (IExec ((I ';' J),p,s)) . b1 = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . b1
per cases ( x is Int-Location or x is FinSeq-Location or x = IC or x is Element of NAT ) by A53, SCMFSA6A:35;
suppose A54: x is Int-Location ; :: thesis: (IExec ((I ';' J),p,s)) . b1 = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . b1
then x <> IC by SCMFSA_2:81;
then A55: not x in dom (Start-At (l,SCM+FSA)) by A51, TARSKI:def 1;
(IExec ((I ';' J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x by A48, A54, SCMFSA6A:38;
hence (IExec ((I ';' J),p,s)) . x = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . x by A55, FUNCT_4:12; :: thesis: verum
end;
suppose A56: x is FinSeq-Location ; :: thesis: (IExec ((I ';' J),p,s)) . b1 = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . b1
then x <> IC by SCMFSA_2:82;
then A57: not x in dom (Start-At (l,SCM+FSA)) by A51, TARSKI:def 1;
(IExec ((I ';' J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x by A48, A56, SCMFSA6A:38;
hence (IExec ((I ';' J),p,s)) . x = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . x by A57, FUNCT_4:12; :: thesis: verum
end;
suppose A58: x = IC ; :: thesis: (IExec ((I ';' J),p,s)) . b1 = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . b1
then x in {(IC )} by TARSKI:def 1;
then A59: x in dom (Start-At (l,SCM+FSA)) by FUNCOP_1:19;
thus (IExec ((I ';' J),p,s)) . x = (Start-At (l,SCM+FSA)) . (IC ) by A50, A58, FUNCOP_1:87
.= ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . x by A58, A59, FUNCT_4:14 ; :: thesis: verum
end;
suppose A60: x is Element of NAT ; :: thesis: (IExec ((I ';' J),p,s)) . b1 = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . b1
then x <> IC by COMPOS_1:3;
then A61: not x in dom (Start-At (l,SCM+FSA)) by A51, TARSKI:def 1;
(IExec ((I ';' J),p,s)) | NAT = s | NAT by A43, PBOOLE:157
.= (IExec (J,p,(IExec (I,p,s)))) | NAT by A46, PBOOLE:157 ;
then (IExec ((I ';' J),p,s)) . x = (IExec (J,p,(IExec (I,p,s)))) . x by A60, SCMFSA6A:36;
hence (IExec ((I ';' J),p,s)) . x = ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) . x by A61, FUNCT_4:12; :: thesis: verum
end;
end;
end;
dom (IExec ((I ';' J),p,s)) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom ((IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA))) by PARTFUN1:def 4 ;
hence IExec ((I ';' J),p,s) = (IExec (J,p,(IExec (I,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (I,p,s))))) + (card I)),SCM+FSA)) by A52, FUNCT_1:9; :: thesis: verum
end;