theorem Th114: :: AOFA_000:114

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 C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . (s,C) holds
[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)