:: deftheorem defines iteration_terminates_for AOFA_000:def 33 :
for A being preIfWhileAlgebra
for I being Element of A
for S being non empty set
for s being Element of S
for T being Subset of S
for f being ExecutionFunction of A,S,T holds
( f iteration_terminates_for I,s iff ex r being non empty FinSequence of S st
( r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) );