:: deftheorem defines complies_with_while_wrt AOFA_000:def 31 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being Function of [:S, the carrier of A:],S holds
( f complies_with_while_wrt T iff for s being Element of S
for C, I being Element of A holds
( ( f . (s,C) in T implies f . (s,(while (C,I))) = f . ((f . ((f . (s,C)),I)),(while (C,I))) ) & ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) ) );