Who Cites induced event str?
induced_event_str	Def induced_event_str(E;A;f) == < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f, >
	Thm* E:EventStruct, A:Type, f:(A|E|). induced_event_str(E;A;f) EventStruct
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:

induced_event_str(E;A;f)

has structure:

induced_event_str(E; A; f)

About: