let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
let I be Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s )
set Ins = NAT ;
assume that
A1: s . (intloc 0) = 1 and
A2: s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
set WH = while>0 (a,I);
set Is = Initialized s;
set Ids = s +* (Initialized (while>0 (a,I)));
set pds = p +* (while>0 (a,I));
A3: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:26;
A4: ProgramPart (while>0 (a,I)) = while>0 (a,I) by RELAT_1:209;
A5: s +* (Initialized (while>0 (a,I))) = (Initialized s) +* (Initialize (while>0 (a,I))) by SCMFSA8A:13;
then A6: Initialize (while>0 (a,I)) c= s +* (Initialized (while>0 (a,I))) by FUNCT_4:26;
(Initialized s) . a = s . a by SCMFSA6C:3;
then while>0 (a,I) is_halting_on Initialized s,p by A2, SCMFSA_9:43;
then A7: p +* (while>0 (a,I)) halts_on s +* (Initialized (while>0 (a,I))) by A5, SCMFSA7B:def 8, A4;
DataPart (Initialized s) = DataPart (s +* (Initialized (while>0 (a,I)))) by SCMFSA8B:5;
then A8: (s +* (Initialized (while>0 (a,I)))) . a = (Initialized s) . a by SCMFSA6A:38
.= s . a by SCMFSA6C:3 ;
A9: dom (s | NAT) c= NAT by RELAT_1:87;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A10: dom (s | NAT) misses Int-Locations \/ FinSeq-Locations by A9, XBOOLE_1:63;
thus DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart ((Result ((p +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((p +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))))) by A10, FUNCT_4:76, SCMFSA_2:127
.= DataPart (Comput ((p +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialized (while>0 (a,I)))))))) by A7, EXTPRO_1:23
.= DataPart (s +* (Initialized (while>0 (a,I)))) by A2, A8, A6, Th35, A3
.= DataPart (Initialized s) by SCMFSA8B:5
.= DataPart s by A1, SCMFSA8C:27 ; :: thesis: verum