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 SCMFSA6A:44;
then A9:
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));
A10:
Initialize ((intloc 0) .--> 1) c= Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by SCMFSA6A:44;
then A11:
(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;
A12:
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));
A13:
I is_halting_onInit s,
P
by SCM_HALT:26;
A14:
I is_closed_onInit s,
P
by SCM_HALT:25;
then A15:
IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = 0
by A1, A13, Th21;
A16:
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, A14, A13, Th21
.=
DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
;
HH:
Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) = (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) +* (Initialize ((intloc 0) .--> 1))
by SCMFSA6A:def 3;
A17:
now let 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))) . fL1:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA6A:42;
(
f <> intloc 0 &
f <> IC )
by SCMFSA_2:57, SCMFSA_2:58;
then
not
f in dom (Initialize ((intloc 0) .--> 1))
by L1, 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 HH, FUNCT_4:11
.=
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . f
by A16, SCMFSA6A:7
;
verum end;
A19:
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA6A:44;
A20:
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . (intloc 0) = 1
by A19, A5, A2, SCM_HALT:def 3;
A21:
now let 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 A22:
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))) . b1L1:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by SCMFSA6A:42;
b <> IC
by SCMFSA_2:56;
then
not
b in dom (Initialize ((intloc 0) .--> 1))
by A22, L1, 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 HH, FUNCT_4:11
.=
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) . b
by A16, SCMFSA6A:7
;
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 A15, A20, Th6;
then
Initialize ((intloc 0) .--> 1) c= Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 3))
by SCMFSA6A:44;
then A25:
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 A15, SCMFSA6A:44, SCMFSA6B:10;
then A26:
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 A17, A21, SCMFSA_2:61;
then XX:
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, A10, Th12, 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, A10, Th12, A5, A4, A26;
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 A25, 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 A25, EXTPRO_1:23
.=
DataPart (Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))
by XX
.=
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 A11, EXTPRO_1:23
;
verum
end;
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA6A:44;
then A27:
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 A27, 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, A10, Th12, A5, A4;
then A32:
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)))))))
;
A33: 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 A11, A32, EXTPRO_1:23
;
A34:
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 A9, 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 A9, A34, 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 A12, EXTPRO_1:4
.=
DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
by A33
;
hence
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
; verum