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 ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
let s be State of SCM+FSA; :: thesis: for a being read-write Int-Location
for I being Program of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
let I be Program of SCM+FSA; :: thesis: ( ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p implies DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s)))) )
set Ins = NAT ;
set WH = while=0 (a,I);
set Ids = s +* (Initialized (while=0 (a,I)));
set pds = p +* (while=0 (a,I));
set Is = Initialized s;
A1: ProgramPart (while=0 (a,I)) = while=0 (a,I) by RELAT_1:209;
A2: s +* (Initialized (while=0 (a,I))) = (Initialized s) +* (Initialize (while=0 (a,I))) by SCMFSA8A:13;
A3: 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 A4: dom (s | NAT) misses Int-Locations \/ FinSeq-Locations by A3, XBOOLE_1:63;
assume A5: ( ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p ) ; :: thesis: DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
then A6: ex k being Element of NAT st
( ExitsAtWhile=0 (a,I,p,(Initialized s)) = k & ((StepWhile=0 (a,I,p,(Initialized s))) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 (a,I,p,(Initialized s))) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),((Initialized s) +* (Initialize (while=0 (a,I)))),(LifeSpan ((p +* (while=0 (a,I))),((Initialized s) +* (Initialize (while=0 (a,I)))))))) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . k) ) by Def3;
while=0 (a,I) is_halting_on Initialized s,p by A5, Th20, Th21;
then A7: p +* (while=0 (a,I)) halts_on s +* (Initialized (while=0 (a,I))) by A2, SCMFSA7B:def 8, A1;
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 A4, FUNCT_4:76, SCMFSA_2:127
.= DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s)))) by A2, A7, A6, EXTPRO_1:23 ; :: thesis: verum