theorem Th116: :: AOFA_000:116

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