:: deftheorem Def36 defines absolutely-terminating AOFA_000:def 36 :
for A being preIfWhileAlgebra
for I being Element of A holds
( I is absolutely-terminating iff 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 [s,I] in TerminatingPrograms (A,S,T,f) );