let s be State of SCM+FSA ; for I being InitHalting keepInt0_1 Program of SCM+FSA
for J being InitHalting 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 ;
let I be InitHalting keepInt0_1 Program of SCM+FSA ; for J being InitHalting 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 InitHalting 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;
s +* (Initialized (I ';' J)) =
s +* ((I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )))
by FUNCT_4:15
.=
(s +* (I ';' J)) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:15
;
then A2:
((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ) c= s +* (Initialized (I ';' J))
by FUNCT_4:26;
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 Th5, FUNCT_4:26;
A5:
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;
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:
( IExec I,s = (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT ) & Initialized J c= (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Initialized J) )
by FUNCT_4:26, SCMFSA6B:def 1;
A9: 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
;
A10:
Initialized J c= (IExec I,s) +* (Initialized J)
by FUNCT_4:26;
A11:
( Initialized J c= (IExec I,s) +* (Initialized J) & 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;
A12:
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;
A13:
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
then X:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by Th5;
then A14:
(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 AMI_1:122;
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 X, AMI_1:122;
then A15:
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 A9, A6, A8, A10, Th15, COMPOS_1:24;
A16:
Initialized I c= (s +* (Initialized (I ';' J))) +* I
by FUNCT_4:26, SCMFSA6A:52;
( 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 A17:
LifeSpan (ProgramPart ((s +* (Initialized (I ';' J))) +* I)),((s +* (Initialized (I ';' J))) +* I) = LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))
by A13, A16, Th15;
then A18:
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, Th25;
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;
(s +* (Initialized (I ';' J))) +* (I +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) =
((s +* (Initialized (I ';' J))) +* I) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))
by FUNCT_4:15
.=
((s +* (Initialized (I ';' J))) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) +* I
by Th19
.=
(s +* (Initialized (I ';' J))) +* I
by A2, FUNCT_4:79
;
then
I +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) c= (s +* (Initialized (I ';' J))) +* I
by FUNCT_4:26;
then
Initialized I c= (s +* (Initialized (I ';' J))) +* I
by FUNCT_4:15;
then
ProgramPart ((s +* (Initialized (I ';' J))) +* I) halts_on (s +* (Initialized (I ';' J))) +* I
by Th5;
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 A16, A17, Th18, 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 A13, A4, A3, Th18, SCMFSA6A:39
;
then A19: 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
;
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;
A20:
( 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, A17, Th25;
then A21:
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 A18, A5, A19, Th12, T;
A22:
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 A20, A18, A5, A19, Th12, T;
X:
ProgramPart (s +* (Initialized (I ';' J))) halts_on s +* (Initialized (I ';' J))
by A1, Th5;
Y:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by A13, Th5;
A23: IExec (I ';' J),s =
(Result (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))) +* (s | NAT )
by X, AMI_1:122
.=
(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 A14, Th28
;
IExec I,s =
(Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT )
by Y, AMI_1:122
;
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 A9, A7, A11, Th15;
then A24:
(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 A9, FUNCT_7:108;
Y:
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 A12, Th5;
(IExec I,s) | NAT =
((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT )) | NAT
by SCMFSA6B:def 1
.=
s | NAT
by PBOOLE:157
;
then A25: IExec J,(IExec I,s) =
(Result (ProgramPart ((IExec I,s) +* (Initialized J))),((IExec I,s) +* (Initialized J))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(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, Y, AMI_1:122
;
A26:
dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations
by A9, SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A27: 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 A23, 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 A21, AMI_1:51
.=
DataPart (IExec J,(IExec I,s))
by A25, A26, FUNCT_4:76, SCMFSA_2:127
;
X:
ProgramPart (s +* (Initialized (I ';' J))) halts_on s +* (Initialized (I ';' J))
by A1, Th5;
Y:
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 A12, Th5;
U:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by A13, Th5;
XX:
(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 U, AMI_1:122;
A28: IC (IExec (I ';' J),s) =
IC (Result (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))))
by SCMFSA8A:7
.=
IC (Comput (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J))),(LifeSpan (ProgramPart (s +* (Initialized (I ';' J)))),(s +* (Initialized (I ';' J)))))
by X, AMI_1:122
.=
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 A14, Th28
.=
(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 A22, AMI_1:51
.=
(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 Y, AMI_1:122
.=
(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 XX
.=
(IC (IExec J,(IExec I,s))) + (card I)
by A15, SCMFSA8A:7
;
hereby verum
reconsider l =
(IC (IExec J,(IExec I,s))) + (card I) as
Element of
NAT ;
A29:
dom (Start-At l,SCM+FSA ) = {(IC SCM+FSA )}
by FUNCOP_1:19;
A30:
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 A31:
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 A31, SCMFSA6A:35;
suppose A32:
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 A33:
not
x in dom (Start-At l,SCM+FSA )
by A29, TARSKI:def 1;
(IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x
by A27, A32, 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 A33, FUNCT_4:12;
verum end; suppose A34:
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 A35:
not
x in dom (Start-At l,SCM+FSA )
by A29, TARSKI:def 1;
(IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x
by A27, A34, 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 A35, FUNCT_4:12;
verum end; suppose A36:
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 A37:
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 A28, A36, FUNCOP_1:87
.=
((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)),SCM+FSA )) . x
by A36, A37, FUNCT_4:14
;
verum end; suppose A38:
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 A39:
not
x in dom (Start-At l,SCM+FSA )
by A29, TARSKI:def 1;
(IExec (I ';' J),s) | NAT =
s | NAT
by A23, PBOOLE:157
.=
(IExec J,(IExec I,s)) | NAT
by A25, PBOOLE:157
;
then
(IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x
by A38, 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 A39, 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 A30, FUNCT_1:9;
verum
end;