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
s0 being
Element of
S ex
f being
ExecutionFunction of
A,
S,
T st
(
f | [:S,(ElementaryInstructions A):] = g & ( for
s being
Element of
S for
C,
I being
Element of
A st not
f iteration_terminates_for I \; C,
f . (
s,
C) holds
f . (
s,
(while (C,I)))
= s0 ) )