let s be State of SCM+FSA; for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s & J is_halting_on IExec (Ig,s) & Ig is_closed_on Initialized s & J is_closed_on IExec (Ig,s) holds
IExec ((Ig ';' J),s) = (IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))
let J be Program of SCM+FSA; for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s & J is_halting_on IExec (Ig,s) & Ig is_closed_on Initialized s & J is_closed_on IExec (Ig,s) holds
IExec ((Ig ';' J),s) = (IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))
let Ig be good Program of SCM+FSA; ( Ig is_halting_on Initialized s & J is_halting_on IExec (Ig,s) & Ig is_closed_on Initialized s & J is_closed_on IExec (Ig,s) implies IExec ((Ig ';' J),s) = (IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA)) )
set SAt = Start-At (0,SCM+FSA);
set D = Int-Locations \/ FinSeq-Locations;
set I = Ig;
assume that
A1:
Ig is_halting_on Initialized s
and
A2:
J is_halting_on IExec (Ig,s)
and
A3:
Ig is_closed_on Initialized s
and
A4:
J is_closed_on IExec (Ig,s)
; IExec ((Ig ';' J),s) = (IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))
set Is = Initialized s;
A5:
(Initialized s) . (intloc 0) = 1
by SCMFSA6C:3;
set s1 = s +* (Initialized Ig);
set m1 = LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)));
s +* (Initialized Ig) = (Initialized s) +* (Initialized Ig)
by SCMFSA8A:8;
then A6:
s +* (Initialized Ig) = (Initialized s) +* (Initialize Ig)
by A5, SCMFSA8C:18;
then
DataPart (Initialized 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 ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) = (Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J)
by EXTPRO_1:23;
set s2 = s +* (Initialized (Ig ';' J));
s +* (Initialized (Ig ';' J)) = (Initialized s) +* (Initialized (Ig ';' J))
by SCMFSA8A:8;
then A10:
s +* (Initialized (Ig ';' J)) = (Initialized s) +* (Initialize (Ig ';' J))
by A5, SCMFSA8C:18;
then A11:
DataPart (Initialized 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,(Initialized 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 ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig)) = LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))
by A1, A3, A6, A11, SCMFSA8C:101;
set JAt = Initialize J;
NAT misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A17:
dom (ProgramPart s) misses Int-Locations \/ FinSeq-Locations
by COMPOS_1:34;
(Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) . (intloc 0) = 1
by A3, A5, A6, SCMFSA8C:97;
then A18:
(Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) = (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialize J)
by SCMFSA8C:18;
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 Initialized 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 ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))))))) +* (s | NAT)
by A20, EXTPRO_1:23
.=
(Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))))))) +* (s | NAT)
by A1, A2, A3, A4, A9, Th6
;
A22: DataPart (IExec (Ig,s)) =
DataPart ((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (s | NAT))
by SCMFSA6B:def 1
.=
DataPart (Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))
by A17, FUNCT_4:76, SCMFSA_2:127
.=
DataPart (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))))
by A8, EXTPRO_1:23
;
then
J is_halting_on Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))
by A2, A4, SCMFSA8B:8;
then A23:
ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(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)) +* (Initialize J)
by SCMFSA8C:18;
then A29:
IC (Result ((ProgramPart ((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J)))) = IC (Result ((ProgramPart ((IExec (Ig,s)) +* (Initialized J))),((IExec (Ig,s)) +* (Initialized J))))
by A2, A4, A18, A22, A9, COMPOS_1:24, SCMFSA8C:101;
Result ((ProgramPart ((IExec (Ig,s)) +* (Initialized J))),((IExec (Ig,s)) +* (Initialized J))), Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))) equal_outside NAT
by A2, A4, A18, A22, A28, SCMFSA8C:101;
then A30:
(Result ((ProgramPart ((IExec (Ig,s)) +* (Initialized J))),((IExec (Ig,s)) +* (Initialized J)))) +* (s | NAT) = (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)))) +* (s | NAT)
by A19, FUNCT_7:108;
(IExec (Ig,s)) | NAT =
((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (s | NAT)) | NAT
by SCMFSA6B:def 1
.=
s | NAT
by PBOOLE:157
;
then A31: IExec (J,(IExec (Ig,s))) =
(Result ((ProgramPart ((IExec (Ig,s)) +* (Initialized J))),((IExec (Ig,s)) +* (Initialized J)))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)))))) +* (s | NAT)
by A23, A30, EXTPRO_1:23
;
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 FUNCT_4:26;
then
Start-At (0,SCM+FSA) c= s +* (Initialized (Ig ';' J))
by A27, 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))) +* (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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) =
DataPart (Comput ((ProgramPart (((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J))),(((s +* (Initialized (Ig ';' J))) +* Ig) +* (Ig ';' J)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))))
by X1
.=
DataPart (Comput ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* (Ig ';' J))),((s +* (Initialized (Ig ';' J))) +* (Ig ';' J)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))))
by X
.=
DataPart (Comput ((ProgramPart (s +* ((Initialized (Ig ';' J)) +* (Ig ';' J)))),(s +* ((Initialized (Ig ';' J)) +* (Ig ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))))
by X2
.=
DataPart (Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))))
by X3
.=
DataPart (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)) =
(DataPart (Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig))))))) +* (DataPart (Initialized J))
by FUNCT_4:75
.=
DataPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1))) = DataPart ((Comput ((ProgramPart ((s +* (Initialized (Ig ';' J))) +* Ig)),((s +* (Initialized (Ig ';' J))) +* Ig),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1)))
by AMI_1:123;
A42:
IC (Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1)))),(Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)))))) = DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))))))
by A43, T, EXTPRO_1:5
.=
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 ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1)))),(Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)))))) = (IC (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))))))) + (card Ig)
by A26, A37, A42, A40, A41, A25, SCMFSA8C:42;
XX:
(Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J) = (Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J)
by A8, EXTPRO_1:23;
A47: IC (IExec ((Ig ';' J),s)) =
IC (Result ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J)))))
by SCMFSA8A:7
.=
IC (Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J)))))))
by A20, EXTPRO_1:23
.=
IC (Comput ((ProgramPart (s +* (Initialized (Ig ';' J)))),(s +* (Initialized (Ig ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)))))))
by A1, A2, A3, A4, A9, Th6
.=
(IC (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))))))) + (card Ig)
by A46, T, EXTPRO_1:5
.=
(IC (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)),(LifeSpan ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))))) +* (Initialized J))))) + (card Ig)
by A23, EXTPRO_1:23
.=
(IC (Result ((ProgramPart ((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized Ig))),(s +* (Initialized Ig)))) +* (Initialized J))))) + (card Ig)
by XX
.=
(IC (IExec (J,(IExec (Ig,s))))) + (card Ig)
by A29, SCMFSA8A:7
;
A48:
now let x be
set ;
( x in dom (IExec ((Ig ';' J),s)) implies (IExec ((Ig ';' J),s)) . b1 = ((IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))) . b1 )assume A49:
x in dom (IExec ((Ig ';' J),s))
;
(IExec ((Ig ';' J),s)) . b1 = ((IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))) . b1per cases
( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Element of NAT )
by A49, SCMFSA6A:35;
suppose A50:
x is
Int-Location
;
(IExec ((Ig ';' J),s)) . b1 = ((IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))) . b1then
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;
verum end; suppose A52:
x is
FinSeq-Location
;
(IExec ((Ig ';' J),s)) . b1 = ((IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))) . b1then
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;
verum end; suppose A54:
x = IC SCM+FSA
;
(IExec ((Ig ';' J),s)) . b1 = ((IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))) . b1then
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
;
verum end; suppose A56:
x is
Element of
NAT
;
(IExec ((Ig ';' J),s)) . b1 = ((IExec (J,(IExec (Ig,s)))) +* (Start-At (((IC (IExec (J,(IExec (Ig,s))))) + (card Ig)),SCM+FSA))) . b1then
x <> IC SCM+FSA
by COMPOS_1:3;
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;
verum 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; verum