:: deftheorem defines is_terminating_wrt AOFA_000:def 38 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for I being Element of A
for f being ExecutionFunction of A,S,T
for Z being set holds
( I is_terminating_wrt f,Z iff for s being Element of S st s in Z holds
[s,I] in TerminatingPrograms (A,S,T,f) );