:: deftheorem defines writesto PETERSON:def 11 :
for Values being Values_with_Bool
for S being Events_structure over Values
for e being Event of S
for x being Location of S
for a being Element of the carrier of Values holds
( e writesto x,a iff ( e writesto x & val e = a ) );