theorem
for
S being non
empty set for
T being
Subset of
S for
A being
free ECIW-strict preIfWhileAlgebra for
g being
Function of
[:S,(ElementaryInstructions A):],
S for
F being
Function of
(Funcs (S,S)),
(Funcs (S,S)) st ( for
h being
Element of
Funcs (
S,
S) holds
(F . h) * h = F . h ) holds
ex
f being
ExecutionFunction of
A,
S,
T st
(
f | [:S,(ElementaryInstructions A):] = g & ( for
C,
I being
Element of
A for
s being
Element of
S st not
f iteration_terminates_for I \; C,
f . (
s,
C) holds
f . (
s,
(while (C,I)))
= (F . ((curry' f) . (I \; C))) . (f . (s,C)) ) )