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)),s)) = DataPart (IExec ((while>0 (a,I)),(IExec (I,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)),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 = (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)));
set m1 = LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)));
set m3 = LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(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, EXTPRO_1:def 10;
set mW = LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))));
A5:
Initialized (while>0 (a,I)) c= (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))
by FUNCT_4:26;
then A6:
ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) halts_on (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))
by A2, EXTPRO_1:def 10;
A7:
DataPart (Comput ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))),((LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I))))))))) = DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized 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 (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(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 (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = 0
by A1, A8, Th21;
A11:
DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) =
DataPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))))
by A1, A9, A8, Th21
.=
DataPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (while>0 (a,I)))
by SCMFSA8C:34
;
A12:
now let f be
FinSeq-Location ;
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . f = (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(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 ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . f =
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . f
by FUNCT_4:12
.=
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (while>0 (a,I))) . f
by A13, FUNCT_4:12
.=
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) . f
by A11, SCMFSA6A:38
;
verum end;
Wg is
keepInt0_1
;
then A14:
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) . (intloc 0) = 1
by FUNCT_4:26, SCM_HALT:def 3;
A15:
now let b be
Int-Location ;
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b1 = (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) . b1per cases
( b <> intloc 0 or b = intloc 0 )
;
suppose A16:
b <> intloc 0
;
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b1 = (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(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 ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b =
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) . b
by FUNCT_4:12
.=
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (while>0 (a,I))) . b
by A17, FUNCT_4:12
.=
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) . b
by A11, SCMFSA6A:38
;
verum end; suppose
b = intloc 0
;
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b1 = (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) . b1hence
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))) . b = (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) . b
by A14, 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 A3, XBOOLE_1:1;
then
while>0 (
a,
I)
c= Comput (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))
by AMI_1:81;
then
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) +* (while>0 (a,I)) = Comput (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))
by FUNCT_4:79;
then
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) +* (Initialized (while>0 (a,I))) = Comput (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))
by A10, A14, Th6;
then A18:
Initialized (while>0 (a,I)) c= Comput (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))
by FUNCT_4:26;
then A19:
ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) halts_on Comput (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))
by A2, EXTPRO_1:def 10;
IC (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))) = IC ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))
by A10, FUNCT_4:26, SCMFSA6B:34;
then A20:
Comput (
(ProgramPart (s +* (Initialized (while>0 (a,I))))),
(s +* (Initialized (while>0 (a,I)))),
((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)),
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))) equal_outside NAT
by A12, A15, SCMFSA10:91;
then
LifeSpan (
(ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))),
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))))
= LifeSpan (
(ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))
by A2, A5, A18, Th12;
hence DataPart (Comput ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))),((LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I))))))))) =
DataPart (Comput ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3))),(LifeSpan ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))))))
by A19, EXTPRO_1:25, NAT_1:11
.=
DataPart (Result ((ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))))
by A19, EXTPRO_1:23
.=
DataPart (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))
by A2, A5, A18, A20, Th12, SCMFSA6A:39
.=
DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))))
by A6, EXTPRO_1:23
;
verum
end;
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
then A21:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by EXTPRO_1:def 10;
A22:
Initialized (while>0 (a,I)) c= (IExec (I,s)) +* (Initialized (while>0 (a,I)))
by FUNCT_4:26;
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized (while>0 (a,I))) equal_outside dom (s | NAT)
by FUNCT_7:31, FUNCT_7:106;
then A23:
((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)) +* (Initialized (while>0 (a,I))),(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(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 ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (s | NAT)
by A21, EXTPRO_1:23
;
then
Result ((ProgramPart ((IExec (I,s)) +* (Initialized (while>0 (a,I))))),((IExec (I,s)) +* (Initialized (while>0 (a,I))))), Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))) equal_outside NAT
by A2, A5, A24, A23, A22, Th12;
then A26:
(Result ((ProgramPart ((IExec (I,s)) +* (Initialized (while>0 (a,I))))),((IExec (I,s)) +* (Initialized (while>0 (a,I)))))) +* (s | NAT) = (Result ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) +* (s | NAT)
by A24, FUNCT_7:108;
(IExec (I,s)) | NAT =
((Result ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) +* (s | NAT)) | NAT
by SCMFSA6B:def 1
.=
s | NAT
by PBOOLE:157
;
then A27: IExec ((while>0 (a,I)),(IExec (I,s))) =
(Result ((ProgramPart ((IExec (I,s)) +* (Initialized (while>0 (a,I))))),((IExec (I,s)) +* (Initialized (while>0 (a,I)))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))))) +* (s | NAT)
by A6, A26, EXTPRO_1:23
;
A28:
LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I))))) <= (((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3) + (LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))) + (LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I))))))
by NAT_1:11;
T:
ProgramPart (s +* (Initialized (while>0 (a,I)))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3)))
by AMI_1:123;
IExec ((while>0 (a,I)),s) =
(Result ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),(LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))))) +* (s | NAT)
by A4, EXTPRO_1:23
.=
(Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3) + ((LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))))))) +* (s | NAT)
by A4, A28, EXTPRO_1:25
;
then DataPart (IExec ((while>0 (a,I)),s)) =
DataPart (Comput ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))),(((LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) + 3) + ((LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))))) + (LifeSpan ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I))))))))))
by A25, FUNCT_4:76, SCMFSA_2:127
.=
DataPart (Comput ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I)))),(LifeSpan ((ProgramPart ((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))),((Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))))) +* (Initialized (while>0 (a,I))))))))
by A7, T, EXTPRO_1:5
.=
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