let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction 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; for a being read-write Int-Location
for I being really-closed MacroInstruction 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; for I being really-closed MacroInstruction 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 really-closed MacroInstruction of SCM+FSA ; ( ( 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 Is = Initialized s;
set pds = p +* (while=0 (a,I));
A1:
Initialized s = Initialize (Initialized s)
by MEMSTR_0:44;
assume A2:
( ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p )
; DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
then A3:
ex k being Nat st
( ExitsAtWhile=0 (a,I,p,(Initialized s)) = k & ((StepWhile=0 (a,I,p,(Initialized s))) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,(Initialized s))) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize (Initialized s)),(LifeSpan ((p +* (while=0 (a,I))),(Initialize (Initialized s)))))) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . k) )
by Def3;
while=0 (a,I) is_halting_on Initialized s,p
by A2, Th14, Th15;
then A4:
p +* (while=0 (a,I)) halts_on Initialized s
by A1, SCMFSA7B:def 7;
thus DataPart (IExec ((while=0 (a,I)),p,s)) =
DataPart (Result ((p +* (while=0 (a,I))),(Initialized s)))
by SCMFSA6B:def 1
.=
DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
by A1, A4, A3, EXTPRO_1:23
; verum