let s be State of ; for I being parahalting keeping_0 Program of
for J being parahalting Program of holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
set SA0 = Start-At (insloc 0 );
let I be parahalting keeping_0 Program of ; for J being parahalting Program of holds IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
let J be parahalting Program of ; IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
set ps = s | NAT ;
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (I ';' J));
set s3 = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J);
set m1 = LifeSpan (s +* (Initialized I));
set m3 = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J));
A1:
Initialized (I ';' J) c= s +* (Initialized (I ';' J))
by FUNCT_4:26;
I +* (Start-At (insloc 0 )) c= (s +* (Initialized (I ';' J))) +* (I +* (Start-At (insloc 0 )))
by FUNCT_4:26;
then
I +* (Start-At (insloc 0 )) c= ((s +* (Initialized (I ';' J))) +* I) +* (Start-At (insloc 0 ))
by FUNCT_4:15;
then A2:
I +* (Start-At (insloc 0 )) c= ((s +* (Initialized (I ';' J))) +* (Start-At (insloc 0 ))) +* I
by Th14;
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 (insloc 0 )) c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)
by Th8, FUNCT_4:26;
A6:
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J),((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized J) equal_outside dom (s | NAT )
by FUNCT_7:31, FUNCT_7:106;
then A7:
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized J),(Computation (s +* (Initialized I)),(LifeSpan (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 AMI_1:79, 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 (insloc 0 )) c= (s +* (Initialized (I ';' J))) +* I
by Th8;
A11:
I +* (Start-At (insloc 0 )) 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 AMI_1:120, SCMFSA6A:53;
then
s +* (Initialized I),(s +* (Initialized (I ';' J))) +* I equal_outside NAT
by FUNCT_7:29;
then A12:
LifeSpan ((s +* (Initialized (I ';' J))) +* I) = LifeSpan (s +* (Initialized I))
by A11, A10, Th29;
then A13:
ProgramPart (Relocated J,(card I)) c= Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)
by A1, Lm4;
A14:
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:
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) = (Result (s +* (Initialized I))) +* (Initialized J)
by Th19, AMI_1:122;
( Start-At (insloc 0 ) c= Initialized (I ';' J) & Initialized (I ';' J) c= s +* (Initialized (I ';' J)) )
by FUNCT_4:26;
then
Start-At (insloc 0 ) c= s +* (Initialized (I ';' J))
by XBOOLE_1:1;
then
I +* (Start-At (insloc 0 )) 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 (Computation ((s +* (Initialized (I ';' J))) +* I),(LifeSpan (s +* (Initialized I)))) =
DataPart (Computation (((s +* (Initialized (I ';' J))) +* I) +* (I ';' J)),(LifeSpan (s +* (Initialized I))))
by A10, A12, Th36, SCMFSA6A:39
.=
DataPart (Computation ((s +* (Initialized (I ';' J))) +* (I +* (I ';' J))),(LifeSpan (s +* (Initialized I))))
by FUNCT_4:15
.=
DataPart (Computation ((s +* (Initialized (I ';' J))) +* (I ';' J)),(LifeSpan (s +* (Initialized I))))
by SCMFSA6A:57
.=
DataPart (Computation (s +* ((Initialized (I ';' J)) +* (I ';' J))),(LifeSpan (s +* (Initialized I))))
by FUNCT_4:15
.=
DataPart (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized I))))
by LATTICE2:8, SCMFSA6A:26
.=
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))
by A4, A11, A3, Th36, SCMFSA6A:39
;
then A16: DataPart ((Computation ((s +* (Initialized (I ';' J))) +* I),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) =
(DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) +* (DataPart (Initialized J))
by FUNCT_4:75
.=
DataPart ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))
by FUNCT_4:75
;
A17:
( IC (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) = insloc (card I) & DataPart (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)) = DataPart ((Computation ((s +* (Initialized (I ';' J))) +* I),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) )
by A1, A12, Lm4;
then A18:
DataPart (Computation (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) = DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))
by A13, A5, A16, Th27;
A19:
IC (Computation (Computation (s +* (Initialized (I ';' J))),((LifeSpan (s +* (Initialized I))) + 1)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) = (IC (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) + (card I)
by A17, A13, A5, A16, Th27;
A20:
( J +* (Start-At (insloc 0 )) c= (Result (s +* (Initialized I))) +* (Initialized J) & J +* (Start-At (insloc 0 )) c= (IExec I,s) +* (Initialized J) )
by Th8, FUNCT_4:26;
A21:
( J +* (Start-At (insloc 0 )) c= (IExec I,s) +* (Initialized J) & J +* (Start-At (insloc 0 )) c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J) )
by Th8, FUNCT_4:26;
A22:
Initialized J c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)
by FUNCT_4:26;
then B22:
ProgramPart ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) halts_on (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)
by Th19;
Result (s +* (Initialized I)) = Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))
by A14, Th19, AMI_1:122, B14;
then A23:
IC (Result ((Result (s +* (Initialized I))) +* (Initialized J))) = IC (Result ((IExec I,s) +* (Initialized J)))
by A8, A6, A20, Th29, AMI_1:121;
A24:
(IExec I,s) | NAT = s | NAT
by CARD_3:99;
IExec I,s = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )
by A14, Th19, AMI_1:122, B14;
then
Result ((IExec I,s) +* (Initialized J)), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)) equal_outside NAT
by A8, A7, A21, Th29;
then
(Result ((IExec I,s) +* (Initialized J))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))) +* (s | NAT )
by A8, FUNCT_7:108;
then A25:
IExec J,(IExec I,s) = (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) +* (s | NAT )
by A22, A24, Th19, B22, AMI_1:122;
B1:
ProgramPart (s +* (Initialized (I ';' J))) halts_on s +* (Initialized (I ';' J))
by A1, Th19;
then IExec (I ';' J),s =
(Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized (I ';' J))))) +* (s | NAT )
by A1, Th19, AMI_1:122
.=
(Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) +* (s | NAT )
by A15, Th43
;
then A26: DataPart (IExec (I ';' J),s) =
DataPart (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))))
by A9, FUNCT_4:76, SCMFSA_2:127
.=
DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))
by A18, AMI_1:51
.=
DataPart (IExec J,(IExec I,s))
by A25, A9, FUNCT_4:76, SCMFSA_2:127
;
A27: IC (IExec (I ';' J),s) =
IC (Result (s +* (Initialized (I ';' J))))
by Th30
.=
IC (Computation (s +* (Initialized (I ';' J))),(LifeSpan (s +* (Initialized (I ';' J)))))
by A1, Th19, AMI_1:122, B1
.=
IC (Computation (s +* (Initialized (I ';' J))),(((LifeSpan (s +* (Initialized I))) + 1) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))))
by A15, Th43
.=
(IC (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J))))) + (card I)
by A19, AMI_1:51
.=
(IC (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized J)))) + (card I)
by A22, Th19, AMI_1:122, B22
.=
(IC (Result ((Result (s +* (Initialized I))) +* (Initialized J)))) + (card I)
by A14, Th19, AMI_1:122, B14
.=
(IC (IExec J,(IExec I,s))) + (card I)
by A23, Th30
;
hereby verum
reconsider l =
(IC (IExec J,(IExec I,s))) + (card I) as
Instruction-Location of
SCM+FSA ;
A28:
dom (Start-At l) = {(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)))) . 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)))) . b1per cases
( x is Int-Location or x is FinSeq-Location or x = IC SCM+FSA or x is Instruction-Location of SCM+FSA )
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)))) . b1then
x <> IC SCM+FSA
by SCMFSA_2:81;
then A32:
not
x in dom (Start-At l)
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)))) . 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)))) . b1then
x <> IC SCM+FSA
by SCMFSA_2:82;
then A34:
not
x in dom (Start-At l)
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)))) . x
by A34, FUNCT_4:12;
verum end; suppose A37:
x is
Instruction-Location of
SCM+FSA
;
(IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1then
x <> IC SCM+FSA
by AMI_1:48;
then A38:
not
x in dom (Start-At l)
by A28, TARSKI:def 1;
(IExec (I ';' J),s) | NAT =
s | NAT
by CARD_3:99
.=
(IExec J,(IExec I,s)) | NAT
by A24, CARD_3:99
;
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)))) . x
by A38, FUNCT_4:12;
verum end; end; dom (IExec (I ';' J),s) =
the
carrier of
SCM+FSA
by AMI_1:79
.=
dom ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I))))
by AMI_1:79
;
hence
IExec (I ';' J),
s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
by A29, FUNCT_1:9;
verum
end;