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 or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s holds
DataPart (IExec ((while>0 (a,I)),s)) = DataPart ((StepWhile>0 (a,I,(Initialized s))) . (ExitsAtWhile>0 (a,I,(Initialized s))))
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st ( ProperBodyWhile>0 a,I, Initialized s or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s holds
DataPart (IExec ((while>0 (a,I)),s)) = DataPart ((StepWhile>0 (a,I,(Initialized s))) . (ExitsAtWhile>0 (a,I,(Initialized s))))
let I be Program of SCM+FSA; :: thesis: ( ( ProperBodyWhile>0 a,I, Initialized s or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s implies DataPart (IExec ((while>0 (a,I)),s)) = DataPart ((StepWhile>0 (a,I,(Initialized s))) . (ExitsAtWhile>0 (a,I,(Initialized s)))) )
set Ins = NAT ;
set WH = while>0 (a,I);
set Ids = s +* (Initialized (while>0 (a,I)));
set Is = Initialized s;
A1: s +* (Initialized (while>0 (a,I))) = (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13;
NAT misses Int-Locations \/ FinSeq-Locations by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
then A2: dom (ProgramPart s) misses Int-Locations \/ FinSeq-Locations by COMPOS_1:34;
assume A3: ( ( ProperBodyWhile>0 a,I, Initialized s or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s ) ; :: thesis: DataPart (IExec ((while>0 (a,I)),s)) = DataPart ((StepWhile>0 (a,I,(Initialized s))) . (ExitsAtWhile>0 (a,I,(Initialized s))))
then A4: ex k being Element of NAT st
( ExitsAtWhile>0 (a,I,(Initialized s)) = k & ((StepWhile>0 (a,I,(Initialized s))) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,(Initialized s))) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,(Initialized s))) . k) ) by Def6;
while>0 (a,I) is_halting_on Initialized s by A3, Th33, Th34;
then A5: ProgramPart (s +* (Initialized (while>0 (a,I)))) halts_on s +* (Initialized (while>0 (a,I))) by A1, SCMFSA7B:def 8;
thus DataPart (IExec ((while>0 (a,I)),s)) = DataPart ((Result ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (s +* (Initialized (while>0 (a,I))))),(s +* (Initialized (while>0 (a,I)))))) by A2, FUNCT_4:76, SCMFSA_2:127
.= DataPart ((StepWhile>0 (a,I,(Initialized s))) . (ExitsAtWhile>0 (a,I,(Initialized s)))) by A1, A5, A4, EXTPRO_1:23 ; :: thesis: verum