let s be State of SCM+FSA; 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) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
let p be 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) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
set D = Data-Locations SCM+FSA;
set A = NAT ;
let I be InitHalting keepInt0_1 Program of SCM+FSA; for J being InitHalting Program of SCM+FSA holds IExec ((I ';' J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
let J be InitHalting Program of SCM+FSA; IExec ((I ';' J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))
set ps = s | NAT;
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set p1 = p +* I;
A1:
I c= p +* I
by FUNCT_4:26;
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set p2 = p +* (I ';' J);
A2:
I ';' J c= p +* (I ';' J)
by FUNCT_4:26;
set s3 = (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1));
set p3 = (p +* I) +* J;
A3:
Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A4:
J c= (p +* I) +* J
by FUNCT_4:26;
set m1 = LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))));
set m3 = LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))));
A5:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A6:
I ';' J c= p +* (I ';' J)
by FUNCT_4:26;
A9:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
I c= p +* I
by FUNCT_4:26;
then A10:
p +* I halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th5, A9;
A11:
Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP ((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT))
by COMPOS_1:236;
then A12:
NPP ((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) = NPP (((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)) +* (Initialize ((intloc 0) .--> 1)))
by COMPOS_1:235;
then A13:
NPP (((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)) +* (Initialize ((intloc 0) .--> 1))) = NPP ((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
;
A14:
( IExec (I,p,s) = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) & Initialize ((intloc 0) .--> 1) c= (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) )
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:
Initialize ((intloc 0) .--> 1) c= (IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A17:
J c= p +* J
by FUNCT_4:26;
A18:
( Initialize ((intloc 0) .--> 1) c= (IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1)) & Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) )
by FUNCT_4:26;
A19:
( J c= p +* J & J c= (p +* I) +* J )
by FUNCT_4:26;
A20:
Initialize ((intloc 0) .--> 1) c= (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A21:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A22:
I c= p +* I
by FUNCT_4:26;
A23:
(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))
by A21, Th5, A22, EXTPRO_1:23;
Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))
by A21, Th5, A1, EXTPRO_1:23;
then
NPP (Result (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result ((p +* J),((IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1)))))
by A12, A14, A16, Th15, A17, A4;
then A24:
IC (Result (((p +* I) +* J),((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) = IC (Result ((p +* J),((IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1)))))
by COMPOS_1:230;
A25:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
A26:
I c= (p +* (I ';' J)) +* I
by FUNCT_4:26;
NPP (s +* (Initialize ((intloc 0) .--> 1))) = NPP (s +* (Initialize ((intloc 0) .--> 1)))
;
then A27:
LifeSpan (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) = LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))
by A25, Th15, A22, A26;
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;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
then A34:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
;
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:
NPP (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((((p +* (I ';' J)) +* I) +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A21, A10, Th18, A1, A35;
I c= (p +* (I ';' J)) +* I
by FUNCT_4:26;
then
(p +* (I ';' J)) +* I halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th5, A34;
then
NPP (Comput (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP (Comput ((((p +* (I ';' J)) +* I) +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A25, A27, Th18, A26;
then DataPart (Comput (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) =
DataPart (Comput ((((p +* (I ';' J)) +* I) +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by COMPOS_1:138
.=
DataPart (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A36, COMPOS_1:138
;
then A37: DataPart ((Comput (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) =
(DataPart (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) +* (DataPart (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:75
.=
DataPart ((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))
by FUNCT_4:75
;
A38:
( IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = card I & DataPart (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) = DataPart ((Comput (((p +* (I ';' J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) )
by A5, A27, Th25, A6;
then A39:
DataPart (Comput ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) = DataPart (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))
by A11, A37, Th12, A4, A29;
A40:
IC (Comput ((p +* (I ';' J)),(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) = (IC (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I)
by A38, A11, A37, Th12, A4, A29;
A41:
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1))
by FUNCT_4:26;
I ';' J c= p +* (I ';' J)
by FUNCT_4:26;
then A42:
p +* (I ';' J) halts_on s +* (Initialize ((intloc 0) .--> 1))
by Th5, A41;
A43: IExec ((I ';' J),p,s) =
(Result ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)
by A42, EXTPRO_1:23
.=
(Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) +* (s | NAT)
by A23, Th28
;
IExec (I,p,s) =
(Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)
by A21, Th5, A1, EXTPRO_1:23
;
then
NPP (Result ((p +* J),((IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))
by A13, A18, Th15, A19;
then A44:
(Result ((p +* J),((IExec (I,p,s)) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) = (Result (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by A15, COMPOS_1:238;
A45:
(p +* I) +* J halts_on (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))
by Th5, A3, A4;
(IExec (I,p,s)) | NAT =
((Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (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)) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) +* (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 +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))))
by A43, FUNCT_4:76
.=
DataPart (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))
by A39, EXTPRO_1:5
.=
DataPart (IExec (J,p,(IExec (I,p,s))))
by A46, A47, FUNCT_4:76
;
A49:
(Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) = (Result ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))
by A21, Th5, A1, EXTPRO_1:23;
A50: IC (IExec ((I ';' J),p,s)) =
IC (Result ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))))
by SCMFSA8A:7
.=
IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))))))
by A5, Th5, A2, EXTPRO_1:23
.=
IC (Comput ((p +* (I ';' J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))))
by A23, Th28
.=
(IC (Comput (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I)
by A40, EXTPRO_1:5
.=
(IC (Result (((p +* I) +* J),((Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I)
by A20, Th5, A4, EXTPRO_1:23
.=
(IC (IExec (J,p,(IExec (I,p,s))))) + (card I)
by A24, A49, SCMFSA8A:7
;
hereby 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 ;
( x in dom (IExec ((I ';' J),p,s)) implies (IExec ((I ';' J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1 )assume A53:
x in dom (IExec ((I ';' J),p,s))
;
(IExec ((I ';' J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1per 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
;
(IExec ((I ';' J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
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 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A55, FUNCT_4:12;
verum end; suppose A56:
x is
FinSeq-Location
;
(IExec ((I ';' J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
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 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A57, FUNCT_4:12;
verum end; suppose A58:
x = IC
;
(IExec ((I ';' J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
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
.=
(IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A58, A59, FUNCT_4:14
;
verum end; suppose A60:
x is
Element of
NAT
;
(IExec ((I ';' J),p,s)) . b1 = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . b1then
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, COMPOS_1:127;
hence
(IExec ((I ';' J),p,s)) . x = (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))) . x
by A61, FUNCT_4:12;
verum end; end; dom (IExec ((I ';' J),p,s)) =
the
carrier of
SCM+FSA
by PARTFUN1:def 4
.=
dom (IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I)))
by PARTFUN1:def 4
;
hence
IExec (
(I ';' J),
p,
s)
= IncIC (
(IExec (J,p,(IExec (I,p,s)))),
(card I))
by A52, FUNCT_1:9;
verum
end;