:: deftheorem defines consistent PETERSON:def 18 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is consistent iff ( S is pr-complete & S is pr-ordered & S is rw-ordered & S is rw-consistent & S is rw-exclusive ) );