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, Initialize s or I is parahalting ) & WithVariantWhile=0 a,I, Initialize s holds
DataPart (IExec (while=0 a,I),s) = DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s)))
let a be read-write Int-Location ; :: thesis: for I being Program of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialize s or I is parahalting ) & WithVariantWhile=0 a,I, Initialize s holds
DataPart (IExec (while=0 a,I),s) = DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s)))
let I be Program of SCM+FSA ; :: thesis: ( ( ProperBodyWhile=0 a,I, Initialize s or I is parahalting ) & WithVariantWhile=0 a,I, Initialize s implies DataPart (IExec (while=0 a,I),s) = DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s))) )
set Ins = NAT ;
set WH = while=0 a,I;
set Ids = s +* (Initialized (while=0 a,I));
set Is = Initialize s;
A1: s +* (Initialized (while=0 a,I)) = (Initialize 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 (s | NAT ) misses Int-Locations \/ FinSeq-Locations by SCMFSA8A:3;
assume A3: ( ( ProperBodyWhile=0 a,I, Initialize s or I is parahalting ) & WithVariantWhile=0 a,I, Initialize s ) ; :: thesis: DataPart (IExec (while=0 a,I),s) = DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s)))
then A4: ex k being Element of NAT st
( ExitsAtWhile=0 a,I,(Initialize s) = k & ((StepWhile=0 a,I,(Initialize s)) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,(Initialize s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput (ProgramPart ((Initialize s) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((StepWhile=0 a,I,(Initialize s)) . k) ) by Def3;
while=0 a,I is_halting_on Initialize s by A3, Th20, Th21;
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 (s +* (Initialized (while=0 a,I)))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized (while=0 a,I)))) by A2, FUNCT_4:94, SCMFSA_2:127
.= DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s))) by A1, A5, A4, AMI_1:122 ; :: thesis: verum