let s be State of SCM+FSA; for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))
set D = Int-Locations \/ FinSeq-Locations;
set A = NAT ;
set SA0 = Start-At (0,SCM+FSA);
let I be parahalting keeping_0 Program of SCM+FSA; for J being parahalting Program of SCM+FSA holds IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))
let J be parahalting Program of SCM+FSA; IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))
set ps = s | NAT;
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (I ';' J));
set s3 = (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J);
set m1 = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)));
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)));
A1:
Initialized (I ';' J) c= s +* (Initialized (I ';' J))
by FUNCT_4:26;
I +* (Start-At (0,SCM+FSA)) c= (s +* (Initialized (I ';' J))) +* (I +* (Start-At (0,SCM+FSA)))
by FUNCT_4:26;
then
Initialize I c= Initialize ((s +* (Initialized (I ';' J))) +* I)
by FUNCT_4:15;
then A2:
Initialize I c= (Initialize (s +* (Initialized (I ';' J)))) +* I
by COMPOS_1:83;
A3: (s +* (Initialized I)) +* (I ';' J) =
s +* ((Initialized I) +* (I ';' J))
by FUNCT_4:15
.=
s +* (Initialized (I ';' J))
by SCMFSA6A:58
;
A4:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by Th19, FUNCT_4:26;
A5:
J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)
by Th8, FUNCT_4:26;
A6:
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized J) equal_outside dom (s | NAT)
by FUNCT_7:31, FUNCT_7:106;
then A7:
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized J),(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) equal_outside dom (s | NAT)
by FUNCT_7:28;
A8: dom (s | NAT) =
(dom s) /\ NAT
by RELAT_1:90
.=
(((Int-Locations \/ FinSeq-Locations) \/ {(IC SCM+FSA)}) \/ NAT) /\ NAT
by PARTFUN1:def 4, SCMFSA_2:8
.=
NAT
by XBOOLE_1:21
;
then A9:
dom (s | NAT) misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
Initialized I c= (s +* (Initialized (I ';' J))) +* I
by FUNCT_4:26, SCMFSA6A:52;
then A10:
I +* (Start-At (0,SCM+FSA)) c= (s +* (Initialized (I ';' J))) +* I
by Th8;
A11:
I +* (Start-At (0,SCM+FSA)) c= s +* (Initialized I)
by Th8, 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 A12:
LifeSpan ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I)) = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))
by A11, A10, Th29;
then A13:
ProgramPart (Relocated (J,(card I))) c= Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))
by A1, Lm4;
X:
I +* (I ';' J) = I ';' J
by SCMFSA6A:57;
X1:
((s +* (Initialized (I ';' J))) +* I) +* (I ';' J) = (s +* (Initialized (I ';' J))) +* (I +* (I ';' J))
by FUNCT_4:15;
X2:
(s +* (Initialized (I ';' J))) +* (I ';' J) = s +* ((Initialized (I ';' J)) +* (I ';' J))
by FUNCT_4:15;
I ';' J c= Initialized (I ';' J)
by SCMFSA6A:26;
then X3:
(Initialized (I ';' J)) +* (I ';' J) = Initialized (I ';' J)
by LATTICE2:8;
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
then B14:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by Th19;
then A15:
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) = (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J)
by EXTPRO_1:23;
T:
ProgramPart (s +* (Initialized (I ';' J))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))
by AMI_1:123;
( Start-At (0,SCM+FSA) c= Initialized (I ';' J) & Initialized (I ';' J) c= s +* (Initialized (I ';' J)) )
by FUNCT_4:26;
then
Start-At (0,SCM+FSA) c= s +* (Initialized (I ';' J))
by XBOOLE_1:1;
then
I +* (Start-At (0,SCM+FSA)) c= (s +* (Initialized (I ';' J))) +* I
by A2, FUNCT_4:79;
then
ProgramPart ((s +* (Initialized (I ';' J))) +* I) halts_on (s +* (Initialized (I ';' J))) +* I
by Th18;
then DataPart (Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) =
DataPart (Comput ((ProgramPart (((s +* (Initialized (I ';' J))) +* I) +* (I ';' J))),(((s +* (Initialized (I ';' J))) +* I) +* (I ';' J)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by A10, A12, Th36, SCMFSA6A:39
.=
DataPart (Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* (I +* (I ';' J)))),((s +* (Initialized (I ';' J))) +* (I +* (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by X1
.=
DataPart (Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* (I ';' J))),((s +* (Initialized (I ';' J))) +* (I ';' J)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by X
.=
DataPart (Comput ((ProgramPart (s +* ((Initialized (I ';' J)) +* (I ';' J)))),(s +* ((Initialized (I ';' J)) +* (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by X2
.=
DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by X3
.=
DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by A4, A11, A3, Th36, SCMFSA6A:39
;
then A16: DataPart ((Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) =
(DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))) +* (DataPart (Initialized J))
by FUNCT_4:75
.=
DataPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))
by FUNCT_4:75
;
A17:
( IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = card I & DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))) = DataPart ((Comput ((ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) )
by A1, A12, Lm4;
then A18:
DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) = DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))
by A13, A5, A16, Th27, T;
T:
ProgramPart (s +* (Initialized (I ';' J))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1)))
by AMI_1:123;
A19:
IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) = (IC (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I)
by A17, A13, A5, A16, Th27, T;
A20:
( J +* (Start-At (0,SCM+FSA)) c= (Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J) & J +* (Start-At (0,SCM+FSA)) c= (IExec (I,s)) +* (Initialized J) )
by Th8, FUNCT_4:26;
A21:
( J +* (Start-At (0,SCM+FSA)) c= (IExec (I,s)) +* (Initialized J) & J +* (Start-At (0,SCM+FSA)) c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J) )
by Th8, FUNCT_4:26;
Initialized J c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)
by FUNCT_4:26;
then B22:
ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)) halts_on (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)
by Th19;
Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) = Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))
by B14, EXTPRO_1:23;
then A23:
IC (Result ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J)))) = IC (Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J))))
by A8, A6, A20, Th29, COMPOS_1:24;
A24:
(IExec (I,s)) | NAT = s | NAT
by PBOOLE:157;
IExec (I,s) = (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)
by B14, EXTPRO_1:23;
then
Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J))), Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))) equal_outside NAT
by A8, A7, A21, Th29;
then
(Result ((ProgramPart ((IExec (I,s)) +* (Initialized J))),((IExec (I,s)) +* (Initialized J)))) +* (s | NAT) = (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))) +* (s | NAT)
by A8, FUNCT_7:108;
then A25:
IExec (J,(IExec (I,s))) = (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))) +* (s | NAT)
by A24, B22, EXTPRO_1:23;
X:
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))) = Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))
by B14, EXTPRO_1:23;
B1:
ProgramPart (s +* (Initialized (I ';' J))) halts_on s +* (Initialized (I ';' J))
by A1, Th19;
then IExec ((I ';' J),s) =
(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))))) +* (s | NAT)
by EXTPRO_1:23
.=
(Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) +* (s | NAT)
by A15, Th43
;
then A26: DataPart (IExec ((I ';' J),s)) =
DataPart (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))))
by A9, FUNCT_4:76, SCMFSA_2:127
.=
DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))
by A18, EXTPRO_1:5
.=
DataPart (IExec (J,(IExec (I,s))))
by A25, A9, FUNCT_4:76, SCMFSA_2:127
;
A27: IC (IExec ((I ';' J),s)) =
IC (Result ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))))
by Th30
.=
IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))))))
by B1, EXTPRO_1:23
.=
IC (Comput ((ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 1) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)))))))
by A15, Th43
.=
(IC (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J)),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))))) + (card I)
by A19, EXTPRO_1:5
.=
(IC (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized J))))) + (card I)
by B22, EXTPRO_1:23
.=
(IC (Result ((ProgramPart ((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))),((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (Initialized J))))) + (card I)
by X
.=
(IC (IExec (J,(IExec (I,s))))) + (card I)
by A23, Th30
;
hereby verum
reconsider l =
(IC (IExec (J,(IExec (I,s))))) + (card I) as
Element of
NAT ;
A28:
dom (Start-At (l,SCM+FSA)) = {(IC SCM+FSA)}
by FUNCOP_1:19;
A29:
now let x be
set ;
( x in dom (IExec ((I ';' J),s)) implies (IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . b1 )assume A30:
x in dom (IExec ((I ';' J),s))
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),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 A30, SCMFSA6A:35;
suppose A31:
x is
Int-Location
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . b1then
x <> IC SCM+FSA
by SCMFSA_2:81;
then A32:
not
x in dom (Start-At (l,SCM+FSA))
by A28, TARSKI:def 1;
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A26, A31, SCMFSA6A:38;
hence
(IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x
by A32, FUNCT_4:12;
verum end; suppose A33:
x is
FinSeq-Location
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . b1then
x <> IC SCM+FSA
by SCMFSA_2:82;
then A34:
not
x in dom (Start-At (l,SCM+FSA))
by A28, TARSKI:def 1;
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A26, A33, SCMFSA6A:38;
hence
(IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x
by A34, FUNCT_4:12;
verum end; suppose A35:
x = IC SCM+FSA
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . b1then
x in {(IC SCM+FSA)}
by TARSKI:def 1;
then A36:
x in dom (Start-At (l,SCM+FSA))
by FUNCOP_1:19;
thus (IExec ((I ';' J),s)) . x =
(Start-At (l,SCM+FSA)) . (IC SCM+FSA)
by A27, A35, FUNCOP_1:87
.=
((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x
by A35, A36, FUNCT_4:14
;
verum end; suppose A37:
x is
Element of
NAT
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . b1then
x <> IC SCM+FSA
by COMPOS_1:3;
then A38:
not
x in dom (Start-At (l,SCM+FSA))
by A28, TARSKI:def 1;
(IExec ((I ';' J),s)) | NAT =
s | NAT
by PBOOLE:157
.=
(IExec (J,(IExec (I,s)))) | NAT
by A24, PBOOLE:157
;
then
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A37, SCMFSA6A:36;
hence
(IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))) . x
by A38, FUNCT_4:12;
verum end; end; dom (IExec ((I ';' J),s)) =
the
carrier of
SCM+FSA
by PARTFUN1:def 4
.=
dom ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA)))
by PARTFUN1:def 4
;
hence
IExec (
(I ';' J),
s)
= (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCM+FSA))
by A29, FUNCT_1:9;
verum
end;