:: deftheorem defines complies_with_if_wrt AOFA_000:def 30 :
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_if_wrt T iff for s being Element of S
for C, I1, I2 being Element of A holds
( ( f . (s,C) in T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I1) ) & ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) ) );