:: deftheorem Def32 defines ExecutionFunction AOFA_000:def 32 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for b₄ being Function of [:S, the carrier of A:],S holds
( b₄ is ExecutionFunction of A,S,T iff ( b₄ is complying_with_empty-instruction & b₄ is complying_with_catenation & b₄ complies_with_if_wrt T & b₄ complies_with_while_wrt T ) );