let P be Instruction-Sequence of SCM+FSA; 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))))
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 ;
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 sI = Initialized s;
set PI = P +* I;
set PW = P +* (while>0 (a,I));
set s3 = Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))));
set P3 = (P +* I) +* (while>0 (a,I));
set m1 = LifeSpan ((P +* I),(Initialized s));
set m3 = LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))));
A3:
I c= P +* I
by FUNCT_4:25;
A4:
while>0 (a,I) c= (P +* I) +* (while>0 (a,I))
by FUNCT_4:25;
A5:
while>0 (a,I) c= P +* (while>0 (a,I))
by FUNCT_4:25;
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA_M:13;
then A6:
P +* (while>0 (a,I)) halts_on Initialized s
by A2, A5, SCM_HALT:def 2;
set mW = LifeSpan ((P +* (while>0 (a,I))),(Initialized s));
A7:
Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by SCMFSA_M:13;
then A8:
(P +* I) +* (while>0 (a,I)) halts_on Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by A2, A4, SCM_HALT:def 2;
A9:
DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))),((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) = DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))))
proof
reconsider Wg =
while>0 (
a,
I) as
InitHalting good Program of
SCM+FSA by A2;
set Cm3 =
Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 3));
A10:
I is_halting_onInit s,
P
by SCM_HALT:26;
A11:
I is_closed_onInit s,
P
by SCM_HALT:25;
then A12:
IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = 0
by A1, A10, Th13;
A13:
DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) =
DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by A1, A11, A10, Th13
.=
DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
;
A14:
now for f being FinSeq-Location holds (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . flet f be
FinSeq-Location ;
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . fA15:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA_M:11;
(
f <> intloc 0 &
f <> IC )
by SCMFSA_2:57, SCMFSA_2:58;
then
not
f in dom (Initialize ((intloc 0) .--> 1))
by A15, TARSKI:def 2;
hence (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . f =
(Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) . f
by FUNCT_4:11
.=
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . f
by A13, SCMFSA_M:2
;
verum end;
A16:
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA_M:13;
A17:
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . (intloc 0) = 1
by A16, A5, A2, SCM_HALT:def 3;
A18:
now for b being Int-Location holds (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . blet b be
Int-Location;
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b1 = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . b1per cases
( b <> intloc 0 or b = intloc 0 )
;
suppose A19:
b <> intloc 0
;
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b1 = (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . b1A20:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA_M:11;
b <> IC
by SCMFSA_2:56;
then
not
b in dom (Initialize ((intloc 0) .--> 1))
by A19, A20, TARSKI:def 2;
hence (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) . b =
(Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) . b
by FUNCT_4:11
.=
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . b
by A13, SCMFSA_M:2
;
verum end; end;
Initialized (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 3))
by A12, A17, SCMFSA_M:8;
then
Initialize ((intloc 0) .--> 1) c= Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 3))
by SCMFSA_M:13;
then A21:
P +* (while>0 (a,I)) halts_on Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 3))
by A2, A5, SCM_HALT:def 2;
IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = IC (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))
by A12, MEMSTR_0:28, SCMFSA_M:13;
then A22:
Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 3))
= Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by A14, A18, SCMFSA_2:61;
then A23:
Result (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))))
= Result (
((P +* I) +* (while>0 (a,I))),
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))
by A2, A7, Th7, A5, A4;
LifeSpan (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))))
= LifeSpan (
((P +* I) +* (while>0 (a,I))),
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))
by A2, A7, Th7, A5, A4, A22;
hence DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))),((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))) =
DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))),(LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3)))))))
by A21, EXTPRO_1:25, NAT_1:11
.=
DataPart (Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3)))))
by A21, EXTPRO_1:23
.=
DataPart (Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))
by A23
.=
DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))))
by A8, EXTPRO_1:23
;
verum
end;
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA_M:13;
then A24:
P +* I halts_on Initialized s
by A3, SCM_HALT:def 2;
IExec (I,P,s) =
Result ((P +* I),(Initialized s))
by SCMFSA6B:def 1
.=
Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))
by A24, EXTPRO_1:23
;
then
Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))
by A2, A7, Th7, A5, A4;
then A25:
Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s)))) = Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))
;
A26: IExec ((while>0 (a,I)),P,(IExec (I,P,s))) =
Result ((P +* (while>0 (a,I))),(Initialized (IExec (I,P,s))))
by SCMFSA6B:def 1
.=
Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))))
by A8, A25, EXTPRO_1:23
;
A27:
LifeSpan ((P +* (while>0 (a,I))),(Initialized s)) <= (((LifeSpan ((P +* I),(Initialized s))) + 3) + (LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))
by NAT_1:11;
IExec ((while>0 (a,I)),P,s) =
Result ((P +* (while>0 (a,I))),(Initialized s))
by SCMFSA6B:def 1
.=
Comput ((P +* (while>0 (a,I))),(Initialized s),(LifeSpan ((P +* (while>0 (a,I))),(Initialized s))))
by A6, EXTPRO_1:23
.=
Comput ((P +* (while>0 (a,I))),(Initialized s),(((LifeSpan ((P +* I),(Initialized s))) + 3) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s))))))
by A6, A27, EXTPRO_1:25
;
then DataPart (IExec ((while>0 (a,I)),P,s)) =
DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(((LifeSpan ((P +* I),(Initialized s))) + 3) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))) + (LifeSpan ((P +* (while>0 (a,I))),(Initialized s)))))))
.=
DataPart (Comput (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))),(LifeSpan (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))))
by A9, EXTPRO_1:4
.=
DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
by A26
;
hence
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
; verum