set A = NAT ;
let s be State of ; for I being good InitHalting Program of
for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
let I be good InitHalting Program of ; for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
let a be read-write Int-Location ; ( s . a > 0 & while>0 a,I is InitHalting implies DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s)) )
set D = Int-Locations \/ FinSeq-Locations ;
assume that
A1:
s . a > 0
and
A2:
while>0 a,I is InitHalting
; DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
set ps = s | NAT ;
set sI = s +* (Initialized I);
set Iwhile = Initialized (while>0 a,I);
set sW = s +* (Initialized (while>0 a,I));
set s3 = (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I));
set m1 = LifeSpan (s +* (Initialized I));
set m3 = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)));
A3:
Initialized (while>0 a,I) c= s +* (Initialized (while>0 a,I))
by FUNCT_4:26;
then A4:
ProgramPart (s +* (Initialized (while>0 a,I))) halts_on s +* (Initialized (while>0 a,I))
by A2, AMI_1:def 26;
set mW = LifeSpan (s +* (Initialized (while>0 a,I)));
A5:
Initialized (while>0 a,I) c= (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))
by FUNCT_4:26;
then A6:
ProgramPart ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) halts_on (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))
by A2, AMI_1:def 26;
A7:
DataPart (Computation (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)),((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I)))))) = DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))))
proof
reconsider Wg =
while>0 a,
I as
good InitHalting Program of
by A2;
set Cm3 =
Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3);
A8:
I is_halting_onInit s
by SCM_HALT:36;
A9:
I is_closed_onInit s
by SCM_HALT:35;
then A10:
IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0
by A1, A8, Th21;
A11:
DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) =
DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))
by A1, A9, A8, Th21
.=
DataPart ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (while>0 a,I))
by SCMFSA8C:34
;
A12:
now let f be
FinSeq-Location ;
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . f = (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . fA13:
not
f in dom (while>0 a,I)
by Th13;
not
f in dom (Initialized (while>0 a,I))
by SCMFSA6A:49;
hence ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . f =
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . f
by FUNCT_4:12
.=
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (while>0 a,I)) . f
by A13, FUNCT_4:12
.=
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . f
by A11, SCMFSA6A:38
;
verum end;
Wg is
keepInt0_1
;
then A14:
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . (intloc 0 ) = 1
by A3, SCM_HALT:def 3;
A15:
now let b be
Int-Location ;
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . b1 = (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . b1per cases
( b <> intloc 0 or b = intloc 0 )
;
suppose A16:
b <> intloc 0
;
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . b1 = (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . b1A17:
not
b in dom (while>0 a,I)
by Th14;
not
b in dom (Initialized (while>0 a,I))
by A16, SCMFSA6A:48;
hence ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) . b =
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) . b
by FUNCT_4:12
.=
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (while>0 a,I)) . b
by A17, FUNCT_4:12
.=
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) . b
by A11, SCMFSA6A:38
;
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 A3, XBOOLE_1:1;
then
while>0 a,
I c= Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by AMI_1:81;
then
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) +* (while>0 a,I) = Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by FUNCT_4:79;
then
(Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) +* (Initialized (while>0 a,I)) = Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by A10, A14, Th6;
then A18:
Initialized (while>0 a,I) c= Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by FUNCT_4:26;
then A19:
ProgramPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) halts_on Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3)
by A2, AMI_1:def 26;
IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = IC ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))
by A10, FUNCT_4:26, SCMFSA6B:34;
then A20:
Computation (s +* (Initialized (while>0 a,I))),
((LifeSpan (s +* (Initialized I))) + 3),
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)) equal_outside NAT
by A12, A15, SCMFSA6A:28;
then
LifeSpan (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))
by A2, A5, A18, Th12;
hence DataPart (Computation (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)),((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I)))))) =
DataPart (Computation (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)),(LifeSpan (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3))))
by A19, AMI_1:128, NAT_1:11
.=
DataPart (Result (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)))
by A19, AMI_1:122
.=
DataPart (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))))
by A2, A5, A18, A20, Th12, SCMFSA6A:39
.=
DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))))
by A6, AMI_1:122
;
verum
end;
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
then A21:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by AMI_1:def 26;
A22:
Initialized (while>0 a,I) c= (IExec I,s) +* (Initialized (while>0 a,I))
by FUNCT_4:26;
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)),((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized (while>0 a,I)) equal_outside dom (s | NAT )
by FUNCT_7:31, FUNCT_7:106;
then A23:
((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )) +* (Initialized (while>0 a,I)),(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)) equal_outside dom (s | NAT )
by FUNCT_7:28;
A24: 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
;
then A25:
dom (s | NAT ) misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
IExec I,s =
(Result (s +* (Initialized I))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (s | NAT )
by A21, AMI_1:122
;
then
Result ((IExec I,s) +* (Initialized (while>0 a,I))), Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))) equal_outside NAT
by A2, A5, A24, A23, A22, Th12;
then A26:
(Result ((IExec I,s) +* (Initialized (while>0 a,I)))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) +* (s | NAT )
by A24, FUNCT_7:108;
(IExec I,s) | NAT =
((Result (s +* (Initialized I))) +* (s | NAT )) | NAT
by SCMFSA6B:def 1
.=
s | NAT
by CARD_3:99
;
then A27: IExec (while>0 a,I),(IExec I,s) =
(Result ((IExec I,s) +* (Initialized (while>0 a,I)))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))))) +* (s | NAT )
by A6, A26, AMI_1:122
;
A28:
LifeSpan (s +* (Initialized (while>0 a,I))) <= (((LifeSpan (s +* (Initialized I))) + 3) + (LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))))) + (LifeSpan (s +* (Initialized (while>0 a,I))))
by NAT_1:11;
IExec (while>0 a,I),s =
(Result (s +* (Initialized (while>0 a,I)))) +* (s | NAT )
by SCMFSA6B:def 1
.=
(Computation (s +* (Initialized (while>0 a,I))),(LifeSpan (s +* (Initialized (while>0 a,I))))) +* (s | NAT )
by A4, AMI_1:122
.=
(Computation (s +* (Initialized (while>0 a,I))),(((LifeSpan (s +* (Initialized I))) + 3) + ((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I))))))) +* (s | NAT )
by A4, A28, AMI_1:128
;
then DataPart (IExec (while>0 a,I),s) =
DataPart (Computation (s +* (Initialized (while>0 a,I))),(((LifeSpan (s +* (Initialized I))) + 3) + ((LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))) + (LifeSpan (s +* (Initialized (while>0 a,I)))))))
by A25, FUNCT_4:76, SCMFSA_2:127
.=
DataPart (Computation ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I))),(LifeSpan ((Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) +* (Initialized (while>0 a,I)))))
by A7, AMI_1:51
.=
DataPart (IExec (while>0 a,I),(IExec I,s))
by A27, A25, FUNCT_4:76, SCMFSA_2:127
;
hence
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))
; verum