Who Cites induced tagged event str?
induced_tagged_event_str	Def < A,evt,tg > (E) == < A,MS(E),msg(E) o evt,loc(E) o evt,is-send(E) o evt,tg, >
	Thm* E:EventStruct, A:Type, f:(A|E|), t:(ALabel). < A,f,t > (E) TaggedEventStruct
event_is_snd	Def is-send(E) == 1of(2of(2of(2of(2of(E)))))
	Thm* E:EventStruct. is-send(E) |E|
compose	Def (f o g)(x) == f(g(x))
	Thm* A,B,C:Type, f:(BC), g:(AB). f o g AC
event_loc	Def loc(E) == 1of(2of(2of(2of(E))))
	Thm* E:EventStruct. loc(E) |E|Label
event_msg	Def msg(E) == 1of(2of(2of(E)))
	Thm* E:EventStruct. msg(E) |E||MS(E)|
event_msg_str	Def MS(E) == 1of(2of(E))
	Thm* E:EventStruct. MS(E) MessageStruct
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

Syntax:

< A,evt,tg > (E)

has structure:

induced_tagged_event_str(E; A; evt; tg)

About: