for A being preIfWhileAlgebra
for I being Element of A
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 holds iteration-degree (I,s,f) >= 0