let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: 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))))
set A = NAT ;
let s be State of SCM+FSA; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 SCM+FSA;
assume that
A1: s . a > 0 and
A2: while>0 (a,I) is InitHalting ; :: thesis: DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s))))
set ps = s | NAT;
set sI = s +* (Initialize ((intloc 0) .--> 1));
set PI = P +* I;
set Iwhile = Initialized (while>0 (a,I));
set sW = s +* (Initialize ((intloc 0) .--> 1));
set PW = P +* (while>0 (a,I));
set s3 = (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1));
set P3 = (P +* I) +* (while>0 (a,I));
set m1 = LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))));
set m3 = LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))));
Initialized (while>0 (a,I)) = (while>0 (a,I)) +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 4;
then Initialize ((intloc 0) .--> 1) c= Initialized (while>0 (a,I)) by FUNCT_4:26;
then ee: dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized (while>0 (a,I))) by RELAT_1:25;
A3: I c= P +* I by FUNCT_4:26;
A4: while>0 (a,I) c= (P +* I) +* (while>0 (a,I)) by FUNCT_4:26;
A5: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:26;
Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A9: P +* (while>0 (a,I)) halts_on s +* (Initialize ((intloc 0) .--> 1)) by A2, A5, SCM_HALT:def 2;
set mW = LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))));
A10: Initialize ((intloc 0) .--> 1) c= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A11: (P +* I) +* (while>0 (a,I)) halts_on (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) by A2, A4, SCM_HALT:def 2;
A12: DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))),((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1)))))))) = DataPart (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))

proof

reconsider Wg = while>0 (a,I) as InitHalting good Program of SCM+FSA by A2;
set Cm3 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3));
A13: I is_halting_onInit s,P by SCM_HALT:36;
A14: I is_closed_onInit s,P by SCM_HALT:35;
then A15: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) = 0 by A1, A13, Th21;
A16: DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A1, A14, A13, Th21
.= DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) ;

A17: now

let f be FinSeq-Location ; :: thesis: ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . f = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . f
not f in dom (Initialized (while>0 (a,I))) by SCMFSA6A:49;
then not f in dom (Initialize ((intloc 0) .--> 1)) by ee;
hence ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . f = (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . f by FUNCT_4:12
.= (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . f by A16, SCMFSA6A:38 ;
:: thesis: verum

end;

A19: Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
A20: (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . (intloc 0) = 1 by A19, A5, A2, SCM_HALT:def 3;

A21: now

let b be Int-Location ; :: thesis: ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . b₁

per cases ( b <> intloc 0 or b = intloc 0 ) ;

suppose A22: b <> intloc 0 ; :: thesis: ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . b₁

not b in dom (Initialized (while>0 (a,I))) by A22, SCMFSA6A:48;
then not b in dom (Initialize ((intloc 0) .--> 1)) by ee;
hence ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . b = (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) . b by FUNCT_4:12
.= (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . b by A16, SCMFSA6A:38 ;
:: thesis: verum

end;

suppose b = intloc 0 ; :: thesis: ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . b₁ = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . b₁

hence ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) . b = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) . b by A20, FUNCT_4:26, SCM_HALT:7; :: thesis: verum

end;

end;

end;

(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) +* (Initialize ((intloc 0) .--> 1)) = Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3)) by A15, A20, Th6;
then A24: Initialize ((intloc 0) .--> 1) c= Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3)) by FUNCT_4:26;
then A25: P +* (while>0 (a,I)) halts_on Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3)) by A2, A5, SCM_HALT:def 2;
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) = IC ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) by A15, FUNCT_4:26, SCMFSA6B:34;
then A26: NPP (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))) = NPP ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) by A17, A21, SCMFSA10:91;
then XX: NPP (Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))))) = NPP (Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) by A2, A10, A24, Th12, A5, A4;
LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3)))) = LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))) by A2, A10, A24, Th12, A5, A4, A26;
hence DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))),((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1)))))))) = DataPart (Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))),(LifeSpan ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))))))) by A25, EXTPRO_1:25, NAT_1:11
.= DataPart (Result ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3))))) by A25, EXTPRO_1:23
.= DataPart (Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) by XX, COMPOS_1:138
.= DataPart (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) by A11, EXTPRO_1:23 ;
:: thesis: verum

end;

Initialize ((intloc 0) .--> 1) c= s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
then A27: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A3, SCM_HALT:def 2;
A28: Initialize ((intloc 0) .--> 1) c= (IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:26;
NPP (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) = NPP ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)) by COMPOS_1:236;
then NPP ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) = NPP (((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)) +* (Initialize ((intloc 0) .--> 1))) by COMPOS_1:235;
then A29: NPP (((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT)) +* (Initialize ((intloc 0) .--> 1))) = NPP ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) ;
A30: dom (s | NAT) = (dom s) /\ NAT by RELAT_1:90
.= (((Data-Locations SCM+FSA) \/ {(IC )}) \/ NAT) /\ NAT by COMPOS_1:172
.= NAT by XBOOLE_1:21 ;
then A31: dom (s | NAT) misses Data-Locations SCM+FSA by COMPOS_1:51;
IExec (I,P,s) = (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT) by A27, EXTPRO_1:23 ;
then NPP (Result ((P +* (while>0 (a,I))),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))))) = NPP (Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) by A2, A10, A29, A28, Th12, A5, A4;
then A32: (Result ((P +* (while>0 (a,I))),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) = (Result (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by A30, COMPOS_1:238;
(IExec (I,P,s)) | NAT = ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)) | NAT by SCMFSA6B:def 1
.= s | NAT by PBOOLE:157 ;
then A33: IExec ((while>0 (a,I)),P,(IExec (I,P,s))) = (Result ((P +* (while>0 (a,I))),((IExec (I,P,s)) +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT) by A11, A32, EXTPRO_1:23 ;
A34: LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1)))) <= (((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3) + (LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))))) by NAT_1:11;
IExec ((while>0 (a,I)),P,s) = (Result ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (s | NAT) by A9, EXTPRO_1:23
.= (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))))))))) +* (s | NAT) by A9, A34, EXTPRO_1:25 ;
then DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 3) + ((LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) + (LifeSpan ((P +* (while>0 (a,I))),(s +* (Initialize ((intloc 0) .--> 1))))))))) by A31, FUNCT_4:76
.= DataPart (Comput (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* (while>0 (a,I))),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) by A12, EXTPRO_1:5
.= DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) by A33, A31, FUNCT_4:76 ;
hence DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) ; :: thesis: verum