theorem
for
A being
preIfWhileAlgebra for
S being non
empty set for
T being
Subset of
S for
s being
Element of
S for
f being
ExecutionFunction of
A,
S,
T for
P being
set for
C,
I being
Element of
A st
C is_terminating_wrt f,
P &
I is_terminating_wrt f,
P &
P is_invariant_wrt C,
f &
P is_invariant_wrt I,
f &
f iteration_terminates_for I \; C,
f . (
s,
C) &
s in P holds
[s,(while (C,I))] in TerminatingPrograms (
A,
S,
T,
f)