:: deftheorem defines pr-complete PETERSON:def 13 :
for Values being Values_with_Bool
for S being Events_structure over Values holds
( S is pr-complete iff for tr being trace of S
for e being Event of S st e in tr holds
ex p being Process of S st e in p );