let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being really-closed good InitHalting MacroInstruction 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 really-closed good InitHalting MacroInstruction 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 really-closed good InitHalting MacroInstruction 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;
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;
A9:
DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),((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
good InitHalting MacroInstruction of
SCM+FSA by A2;
set Cm3 =
Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 2));
A10:
I is_halting_onInit s,
P
by Th23;
A11:
IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0
by A1, A10, Lm7;
A12:
DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) =
DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by A1, A10, Lm7
.=
DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
;
A13:
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))) + 2))) . 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))) + 2))) . fA14:
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 A14, 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))) + 2))) . f
by A12, SCMFSA_M:2
;
verum end;
A15:
Initialize ((intloc 0) .--> 1) c= Initialized s
by SCMFSA_M:13;
A16:
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) . (intloc 0) = 1
by A15, A5, Def2;
A17:
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))) + 2))) . 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))) + 2))) . b1per cases
( b <> intloc 0 or b = intloc 0 )
;
suppose A18:
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))) + 2))) . b1A19:
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 A18, A19, 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))) + 2))) . b
by A12, SCMFSA_M:2
;
verum end; end;
Initialized (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 2))
by A11, A16, SCMFSA_M:8;
then
Initialize ((intloc 0) .--> 1) c= Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 2))
by SCMFSA_M:13;
then A20:
P +* (while>0 (a,I)) halts_on Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 2))
by A2, A5;
IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = IC (Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))
by A11, MEMSTR_0:28, SCMFSA_M:13;
then A21:
Comput (
(P +* (while>0 (a,I))),
(Initialized s),
((LifeSpan ((P +* I),(Initialized s))) + 2))
= Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
by A13, A17, SCMFSA_2:61;
then A22:
Result (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))))
= Result (
((P +* I) +* (while>0 (a,I))),
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))
by A2, A7, Lm5, A5, A4;
LifeSpan (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))))
= LifeSpan (
((P +* I) +* (while>0 (a,I))),
(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))))
by A2, A7, Lm5, A5, A4, A21;
hence DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))),((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))) + 2))),(LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)))))))
by A20, 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))) + 2)))))
by A20, EXTPRO_1:23
.=
DataPart (Result (((P +* I) +* (while>0 (a,I))),(Initialized (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))))))
by A22
.=
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 A23:
P +* I halts_on Initialized s
by A3, Def1;
IExec (I,P,s) =
Result ((P +* I),(Initialized s))
by SCMFSA6B:def 1
.=
Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))
by A23, 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, Lm5, A5, A4;
then A24:
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)))))))
;
A25: 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, A24, EXTPRO_1:23
;
A26:
LifeSpan ((P +* (while>0 (a,I))),(Initialized s)) <= (((LifeSpan ((P +* I),(Initialized s))) + 2) + (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))) + 2) + ((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, A26, 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))) + 2) + ((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 A25
;
hence
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
; verum