set A = NAT ;
let s be State of SCM+FSA ; :: thesis: for I being good InitHalting 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 good InitHalting 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),s) = DataPart (IExec (while>0 a,I),(IExec I,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),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 ; :: thesis: 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, AMI_1:def 26;
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, AMI_1:def 26;
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 good InitHalting 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 ; :: thesis: ((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)) . f
A13: 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 ;
:: thesis: 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 A3, SCM_HALT:def 3;

A15: now

let b be Int-Location ; :: thesis: ((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₁

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

suppose A16: b <> intloc 0 ; :: thesis: ((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₁

A17: 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 ;
:: thesis: verum

end;

suppose b = intloc 0 ; :: thesis: ((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₁

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 (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; :: thesis: verum

end;

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, AMI_1:def 26;
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, AMI_1:128, 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, AMI_1:122
.= 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, AMI_1:122 ;
:: thesis: verum

end;

Initialized I c= s +* (Initialized I) by FUNCT_4:26;
then A21: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by AMI_1:def 26;
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, AMI_1:122 ;
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, AMI_1:122 ;
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, AMI_1:122
.= (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, AMI_1:128 ;
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, AMI_1:51
.= 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)) ; :: thesis: verum