Selected Objects
| def | struct | Structure == Type Top |
| def | carrier | |S| == 1of(S) |
| def | dequiv | DecidableEquiv == T:TypeE:T  T EquivRel(T)(_1 E _2)Top |
| def | eq_dequiv | =(DE) == 1of(2of(DE)) |
| THM | eq_dequiv_equiv |  E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2) |
| def | msg_content_eq | cEQ(MS) == 1of(2of(MS)) |
| def | msg_content | content(MS) == 1of(2of(2of(MS))) |
| def | msg_sender | sender(MS) == 1of(2of(2of(2of(MS)))) |
| def | msg_id | uid(MS) == 1of(2of(2of(2of(2of(MS))))) |
| def | event_msg_str | MS(E) == 1of(2of(E)) |
| def | event_msg | msg(E) == 1of(2of(2of(E))) |
| def | event_loc | loc(E) == 1of(2of(2of(2of(E)))) |
| def | event_is_snd | is-send(E) == 1of(2of(2of(2of(2of(E))))) |
| def | event_tag | tag(E) == 1of(2of(2of(2of(2of(2of(E)))))) |
| def | compose_map | P o evt(L) == P(map(evt;L)) |
| def | event_is_deliver | Macro
is-deliver(E)(x) ==  is-send(E)(x) |
| def | str_trace | Trace(E) == |E| List |
| def | message_str | MessageStruct == M:TypeC:DecidableEquiv(M|C|)(MLabel)(M )Top |
| def | msg_eq | Infix
=(M)(m_1,m_2)
== ((content(M)(m_1)) =(cEQ(M)) (content(M)(m_2)))  sender(M)(m_1) = sender(M)(m_2)
(uid(M)(m_1)=uid(M)(m_2)) |
| def | induced_event_str | induced_event_str(E;A;f) == < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f, > |
| THM | msg_eq_equiv | M:MessageStruct. EquivRel(|M|)(_1 =(M) _2) |
| def | tag_sublist | < tr > _tg == filter( e.tag(E)(e) = tg;tr) |
| def | induced_tagged_event_str | < A,evt,tg > (E) == < A,MS(E),msg(E) o evt,loc(E) o evt,is-send(E) o evt,tg, > |
| def | event_str | EventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top |
| def | event_msg_eq | Infix
=msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2)) |
| def | tagged_event_str | TaggedEventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)(ELabel)Top |
| THM | event_msg_eq_equiv | E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) |
| def | tag_splitable | tag_splitable(E;R) == tr_1,tr_2:Trace(E). (tr_1 R tr_2)   (m:Label. < tr_1 > _m R < tr_2 > _m) |
| def | no_duplicate_send | No-dup-send(E)(tr)
== i,j: ||tr||. is-send(E)(tr[i]) is-send(E)(tr[j]) (tr[i] =msg=(E) tr[j]) i = j |
| THM | member_tag_sublist | E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x  < tr > _t)  (x tr) & tag(E)(x) = t |
| THM | tag_sublist_member_trivial | E:TaggedEventStruct, tr:|E| List, i:||tr||. (tr[i] < tr > _tag(E)(tr[i])) |