let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for s being State of SCM+FSA
for I being InitHalting good Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
set A = NAT ;
let s be State of SCM+FSA; for I being InitHalting good Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
let I be InitHalting good Program of SCM+FSA; for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
let a be read-write Int-Location ; ( s . a > 0 & while>0 (a,I) is InitHalting implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) )
set D = Data-Locations SCM+FSA;
assume that
A1:
s . a > 0
and
A2:
while>0 (a,I) is InitHalting
; DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
set ps = s | NAT;
set sI = s +* (Initialized I);
set PI = P +* I;
set Iwhile = Initialized (while>0 (a,I));
set sW = s +* (Initialized (while>0 (a,I)));
set PW = P +* (while>0 (a,I));
set s3 = (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)));
set P3 = (P +* I) +* (while>0 (a,I));
set m1 = LifeSpan ((P +* I),(s +* (Initialized I)));
set m3 = LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))));
A3:
I c= P +* I
by FUNCT_4:26;
A4:
while>0 (a,I) c= (P +* I) +* (while>0 (a,I))
by FUNCT_4:26;
A5:
while>0 (a,I) c= P +* (while>0 (a,I))
by FUNCT_4:26;
A6:
ProgramPart (Initialized (while>0 (a,I))) = while>0 (a,I)
by SCMFSA6A:33;
A7:
ProgramPart (Initialized I) = I
by SCMFSA6A:33;
A8:
Initialized (while>0 (a,I)) c= s +* (Initialized (while>0 (a,I)))
by FUNCT_4:26;
then A9:
P +* (while>0 (a,I)) halts_on s +* (Initialized (while>0 (a,I)))
by A2, EXTPRO_1:def 10, A5, A6;
set mW = LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))));
A10:
Initialized (while>0 (a,I)) c= (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))
by FUNCT_4:26;
then A11:
(P +* I) +* (while>0 (a,I)) halts_on (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))
by A2, EXTPRO_1:def 10, A4, A6;
A12:
DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))),((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I))))))))) = DataPart (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))))
proof
reconsider Wg =
while>0 (
a,
I) as
InitHalting good Program of
SCM+FSA by A2;
set Cm3 =
Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3));
A13:
I is_halting_onInit s,
P
by SCM_HALT:36;
A14:
I is_closed_onInit s,
P
by SCM_HALT:35;
then A15:
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) = 0
by A1, A13, Th21;
A16:
DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) =
DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))
by A1, A14, A13, Th21
.=
DataPart ((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (while>0 (a,I)))
by COMPOS_1:82
;
A17:
now let f be
FinSeq-Location ;
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . f = (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . fA18:
not
f in dom (while>0 (a,I))
by Th13;
not
f in dom (Initialized (while>0 (a,I)))
by SCMFSA6A:49;
hence ((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . f =
(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) . f
by FUNCT_4:12
.=
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (while>0 (a,I))) . f
by A18, FUNCT_4:12
.=
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . f
by A16, SCMFSA6A:38
;
verum end;
A19:
Initialized Wg c= s +* (Initialized (while>0 (a,I)))
by FUNCT_4:26;
A20:
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . (intloc 0) = 1
by SCM_HALT:def 3, A19, A5;
A21:
now let b be
Int-Location ;
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b1 = (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . b1per cases
( b <> intloc 0 or b = intloc 0 )
;
suppose A22:
b <> intloc 0
;
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b1 = (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . b1A23:
not
b in dom (while>0 (a,I))
by Th14;
not
b in dom (Initialized (while>0 (a,I)))
by A22, SCMFSA6A:48;
hence ((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b =
(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) . b
by FUNCT_4:12
.=
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (while>0 (a,I))) . b
by A23, FUNCT_4:12
.=
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . b
by A16, SCMFSA6A:38
;
verum end; suppose
b = intloc 0
;
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b1 = (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . b1hence
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b = (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) . b
by A20, FUNCT_4:26, SCM_HALT:7;
verum end; end;
while>0 (
a,
I)
c= Initialized (while>0 (a,I))
by SCMFSA6A:26;
then
while>0 (
a,
I)
c= s +* (Initialized (while>0 (a,I)))
by A8, XBOOLE_1:1;
then
while>0 (
a,
I)
c= Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))
by AMI_1:81;
then
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) +* (while>0 (a,I)) = Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))
by FUNCT_4:79;
then
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) +* (Initialized (while>0 (a,I))) = Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))
by A15, A20, Th6;
then A24:
Initialized (while>0 (a,I)) c= Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))
by FUNCT_4:26;
then A25:
P +* (while>0 (a,I)) halts_on Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))
by A2, EXTPRO_1:def 10, A5, A6;
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))) = IC ((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))
by A15, FUNCT_4:26, SCMFSA6B:34;
then A26:
Comput (
(P +* (while>0 (a,I))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3)),
(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))) equal_outside NAT
by A17, A21, SCMFSA10:91;
then
LifeSpan (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))))
= LifeSpan (
((P +* I) +* (while>0 (a,I))),
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))
by A2, A10, A24, Th12, A5, A4;
hence DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))),((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I))))))))) =
DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3))),(LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3)))))))
by A25, EXTPRO_1:25, NAT_1:11
.=
DataPart (Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3)))))
by A25, EXTPRO_1:23
.=
DataPart (Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))
by A2, A10, A24, A26, Th12, COMPOS_1:138, A5, A4
.=
DataPart (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))))
by A11, EXTPRO_1:23
;
verum
end;
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
then A27:
P +* I halts_on s +* (Initialized I)
by EXTPRO_1:def 10, A3, A7;
A28:
Initialized (while>0 (a,I)) c= (IExec (I,P,s)) +* (Initialized (while>0 (a,I)))
by FUNCT_4:26;
(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized (while>0 (a,I))) equal_outside dom (s | NAT)
by FUNCT_7:31, FUNCT_7:106;
then A29:
((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized (while>0 (a,I))),(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))) equal_outside dom (s | NAT)
by FUNCT_7:28;
A30: 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
;
then A31:
dom (s | NAT) misses Data-Locations SCM+FSA
by COMPOS_1:51;
IExec (I,P,s) =
(Result ((P +* I),(s +* (Initialized I)))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (s | NAT)
by A27, EXTPRO_1:23
;
then
Result ((P +* (while>0 (a,I))),((IExec (I,P,s)) +* (Initialized (while>0 (a,I))))), Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))) equal_outside NAT
by A2, A10, A30, A29, A28, Th12, A5, A4;
then A32:
(Result ((P +* (while>0 (a,I))),((IExec (I,P,s)) +* (Initialized (while>0 (a,I)))))) +* (s | NAT) = (Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) +* (s | NAT)
by A30, FUNCT_7:108;
(IExec (I,P,s)) | NAT =
((Result ((P +* I),(s +* (Initialized I)))) +* (s | NAT)) | NAT
by SCMFSA6B:def 1
.=
s | NAT
by PBOOLE:157
;
then A33: IExec ((while>0 (a,I)),P,(IExec (I,P,s))) =
(Result ((P +* (while>0 (a,I))),((IExec (I,P,s)) +* (Initialized (while>0 (a,I)))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))))) +* (s | NAT)
by A11, A32, EXTPRO_1:23
;
A34:
LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I))))) <= (((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3) + (LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I))))))
by NAT_1:11;
IExec ((while>0 (a,I)),P,s) =
(Result ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))))))) +* (s | NAT)
by A9, EXTPRO_1:23
.=
(Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))))))))) +* (s | NAT)
by A9, A34, EXTPRO_1:25
;
then DataPart (IExec ((while>0 (a,I)),P,s)) =
DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(((LifeSpan ((P +* I),(s +* (Initialized I)))) + 3) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I))))))))))
by A31, FUNCT_4:76
.=
DataPart (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))))
by A12, EXTPRO_1:5
.=
DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
by A33, A31, FUNCT_4:76
;
hence
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
; verum